The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

A "low-level" proof can also be obtained using "Lemma ... with ...".

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

Section T_mut_ind.

Variables
  (P: forall i j, T i j -> Prop)
  (Q: forall i j, T i j -> Prop).

Hypotheses
  (* P cases *)
  (HP1 : 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)))
  (HP2 : 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 *)
  (HQ1 : 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)))
  (HQ2 : 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))).

Lemma T_mut_ind_fst : forall i j (t:T i j), P i j t
with  T_mut_ind_snd : forall i j (t:T i j), Q i j t.
Proof.
  intros; case t; intros; [apply HP1|apply HP2]; auto.
  intros; case t; intros; [apply HQ1|apply HQ2]; auto.
Qed.

End T_mut_ind.
--------------------

Hugo Herbelin