The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 23 févr. 09 à 00:32, Nikhil Swamy a écrit :

> Hi,
>
> I have a single inductively defined proposition T and
> I need to prove a lemma P over T using mutual induction with
> another lemma Q over T. What's the easiest way of doing this? Let
> me be more specific, with this contrived example:

Hi,

  You have to generate the dependent elimination principle for things
in Prop explicitely, only the non-dependent one is generated by default.
You can then use it to prove the (somewhat strenghtened) induction
principle.

<<
Inductive T : nat -> nat -> Prop :=
| T1 : forall i j k,
 T i j -> T j k -> T i k
| T2 : forall i j k,
 T k j -> T j i -> T i k.

Scheme T_dep := Induction for T Sort Prop.

Lemma T_mut_ind : forall
 (P: forall i j, T i j -> Prop)
 (Q: forall i j, T i j -> Prop),
 (* P cases *)
 (forall i j k (t1: T i j) (t2: T j k),
   (P i j t1) ->
   (P j k t2) ->
   (P i k (T1 i j k t1 t2))) ->
 (forall i j k (t1: T k j) (t2: T j i),
   (Q k j t1) ->
   (Q j i t2) ->
   (P i k (T2 i j k t1 t2))) ->
 (*Q cases *)
 (forall i j k (t1: T i j) (t2: T j k),
   (Q i j t1) ->
   (Q j k t2) ->
   (Q i k (T1 i j k t1 t2))) ->
 (forall i j k (t1: T k j) (t2: T j i),
   (P k j t1) ->
   (P j i t2) ->
   (Q i k (T2 i j k t1 t2))) ->
 (forall i j (t:T i j), P i j t /\ Q i j t).
Proof.
  intros.
  induction t using T_dep ; intuition.
Qed.
>>

-- Matthieu