The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

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:

Given a (silly) proposition T like so:

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.

I'd like to use an induction principle that looks something like the 
following 
(note the alternation between P and Q on the T2 constructor):

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).

How can I go about generating (or explicitly proving) such a principle?

Many thanks, 
Nik