The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Chris Dams wrote:
> 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
>   
Did you try the Scheme command:

Scheme mutual_ind_A := Induction for A Sort Prop
with mutual_ind_B := Induction for B Sort Prop.

The theorems it produces have different premise order, but they are 
equivalent to the ones you want.

Yves


Yves