The Coq mailing list

["Vincent Siles" <vsiles AT lix.polytechnique.fr>]

Hi !
There are two ways to deal with mutually inductive theorems:

1) As Yves said, you can rebuild the induction principles with the Scheme
command to make them dependent,
but he forgot to mention that you can combine them to build a mutual
fixpoint:

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

Combined Scheme mutual_ind_AB from mutual_ind_A, mutual_ind_B.

Afther this, you can state your theorem this way:

Theorem foo: ( forall a:A, P a) /\ (forall b:B , Q b).
apply mutual_ind_AB.
....
Qed.

And the induction hypothesis should be the good ones.

2)  The second is more dangerous to use since it's build over the fix tactic:

Theorem fooA : forall a:A, P a
 with fooB : forall b: B, P b.
...
Qed.

What it does is to use the fix tactic to give you two hypothesis
  fooA : forall a:A, P a
  fooB : forall b: B, P b
in all the sub-goals, but it's up to you to only apply them on structural
subterms (beware of automation !).
You should also be carefull using inversion : you have to apply fooX
*before* rewriting in a subterm, otherwise
it won't be considered as a structural subterm.

If you want to take a look at some examples, there are some here:
https://www.lix.polytechnique.fr/~vsiles/coq/formalisation.html
in the sequent calculus section.

Cheers,
Vincent


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