The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

This works great! Thanks Matthieu for the prompt response. Adam: I find it 
much more convenient to prove my lemma this way rather than proving the 
conjunction of P and Q for each constructor. Thanks to you too for the quick 
response. -Nik 
________________________________________
From: Matthieu Sozeau 
[Matthieu.Sozeau AT lri.fr]
Sent: Sunday, February 22, 2009 3:42 PM
To: Nikhil Swamy
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Mutual induction over a single inductive type

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