The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear all,

Imagine that I have a mutually recursive inductive definition like

Inductive A: Set
:= | mk_a: A
   | S: B -> A
with B: Set
:= | mk_b: B
   | T: A -> B.

And I want induction theorems for this like

Theorem mutual_ind_A:
   forall P: A -> Prop,
   forall Q: B -> Prop,
   P mk_a ->
   Q mk_b ->
   (forall b: B, Q b -> P (S b)) ->
   (forall a: A, P a -> Q (T a)) ->
   forall a: A, P a.

Theorem mutual_ind_B:
   forall P: A -> Prop,
   forall Q: B -> Prop,
   P mk_a ->
   Q mk_b ->
   (forall b: B, Q b -> P (S b)) ->
   (forall a: A, P a -> Q (T a)) ->
   forall b: B, Q b.

The only way I know to prove this involves much code duplication. It goes like

Theorem mutual_ind_A:
   forall P: A -> Prop,
   forall Q: B -> Prop,
   P mk_a ->
   Q mk_b ->
   (forall b: B, Q b -> P (S b)) ->
   (forall a: A, P a -> Q (T a)) ->
   forall a: A, P a.
Proof.
intros P Q H1 H2 IH1 IH2.
refine
   (fix f (a: A): P a := _
   with g (b: B): Q b := _
   for f).
(* first branch of the fix *)
destruct a as [|b].
assumption.
apply IH1.
apply g.
(* seconc branch of the fix *)
destruct b as [|b].
assumption.
apply IH2.
apply f.
Qed.

Theorem mutual_ind_B:
   forall P: A -> Prop,
   forall Q: B -> Prop,
   P mk_a ->
   Q mk_b ->
   (forall b: B, Q b -> P (S b)) ->
   (forall a: A, P a -> Q (T a)) ->
   forall b: B, Q b.
Proof.
intros P Q H1 H2 IH1 IH2.
refine
   (fix g (b: B): Q b := _
   with f (a: A): P a := _
   for g).
(* first branch of the fix *)
destruct b as [|a].
assumption.
apply IH2.
apply f.
(* seconc branch of the fix *)
destruct a as [|a].
assumption.
apply IH1.
apply g.
Qed.

I am aware of the Cofix ... with .... construction, but as far as I
know I cannot use tactics with that. Is there a way to avoid the code
duplication and to still use tactics?

All the best,
Chris