The Coq mailing list

[Dachuan Yu <dachuan.yu AT yale.edu>]

Xavier Rival wrote:

>         Hello,
>
> > Mutual Inductive F_Weaken : F -> F -> Prop := ...
> > with G_Weaken : G -> G -> Prop := ....
>
> > To prove these two lemmas, I would need to do simultaneous inductions.
> > My question is, how to define the inductive principles and how to apply
> > them?
>
>         The solution is to use the Scheme command that allows you to
> generate mutual induction principles:
>
> Scheme ident1 := Induction for F_Weaken Sort Prop
> with ident2 := Induction for G_Weaken Sort Prop.
>
>         It generates induction principles you can apply as usual induction
> principles.
>
>         Xavier

Thanks for your help! I have tried this before. The problem was that I didn't
know when to apply (or elim using) ident1 and ident2.

Using the above scheme definition, ident1 has a type as follows:
(P:((f,f0:F)(F_Weaken f f0)->Prop);
        P0:((g,g0:G)(G_Weaken g g0)->Prop))
 ... -> ... -> (f,f0:cpenv; ff:(f_Weaken f f0))(P f f0 ff)

I don't know what I should match the above P with, since the transitivity
lemma I wanted to prove involved 3 F's and 3 F_Weaken's:

Lemma F_Weaken_trans : (f1,f2,f3:F)
 (F_Weaken f1 f2) -> (F_Weaken f2 f3) -> (F_Weaken f1 f3).

I think what's difficult for me to understand is that the P here does not
only depend on f1 and f3 and (F_Weaken f1 f3), but also f2 and (F_Weaken f1
f2) and (F_Weaken f2 f3).

Regards,

Dachuan