CODEWITHSUNDEEP
coq
Quyen
Quyen

Reputation: 1373

Adding hypotheses that are not in the current hypotheses

I have a proof and in my hypothesis I have :

...
l0 : list
         (list (ATrs.rule (Sig a)) * boolean * option (list positiveInteger) *
          option cpf.dpProof)
H: forall
         x : list (ATrs.rule (Sig a)) * bool * option (list positiveInteger) *
             option cpf.dpProof,
       In x l0 ->
       (let (p, o) := x in
        let (p0, _) := p in
        let (dps, b) := p0 in
        if b
        then
         match o with
         | Some pi => bool_of_result (dpProof n R dps pi)
         | None => false
         end
        else co_scc (dpg_unif_N 100 R D) dps) = true
 ci : list (ATrs.rule (Sig a))
 Hin : In ci l1
===========================
....

I am stuck at the technique that break the hypothesis H. If I have arguments x:list (ATrs.rule (Sig a)) * bool * option (list positiveInteger) * option cpf.dpProof and hypothesis Hx: In x l0 then I can use the tactic: ded (H x Hx) to get the part (let (p, ...) of H.

So in this case I cannot use ded (H ci Hin) because ci has different type than x in H.

I would like to know how can I add the hypothesis I want (x and Hx) ?

Thank you very much for your help.

Upvotes: 2

Views: 233

Answers (1)

Ptival
Ptival

Reputation: 9437

Well, unless your context contains more information about l0, you will never be able to deduce anything out of H, since one of its arguments has type In x l0 for some x.

If l0 is totally unconstrained in your context and in your goal, it can effectively be any arbitrary list of the proper type, so there is no way you are going to forge something of type In x l0, thus it is impossible to use H.

Maybe you have a contradiction somewhere, or another way to attack this proof.

Upvotes: 1

Related Questions