The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

> I was wondering if there is some sort of tutorial/FAQ for working with
> mutually-(co)inductive definitions in Coq?  I'm looking for something
> more than just the documentation of the Scheme command.  For example,
> what is the most natural way of taking an ordinary mathematical proof
> of a list of theorems by simultaneous induction, and encoding it in
> the tactic language?  Has anyone done any significant amount of
> theorem-proving using mutually-inductive definitions with more than
> (say) three branches?

My record so far is 6 mutually-inductive predicates totalling 35 cases.
(That's what happens when you work with natural semantics for
realistic programming languages.)

Here is what I learned in the process.  For the sake of example,
consider the following mutual inductive predicates:

  Require Import ZArith.
  Open Scope Z_scope.

  Inductive even: Z -> Prop :=
    | even_base: even 0
    | even_succ: forall n, odd (n - 1) -> even n

  with odd: Z -> Prop :=
    | odd_succ: forall n, even (n - 1) -> odd n.

(Yes, it's a silly example, but it fits in this e-mail.)
Just after defining the predicates, ask "Scheme" to generate its
induction principles:

Scheme even_ind_2 := Minimality for even Sort Prop
  with odd_ind_2  := Minimality for odd Sort Prop.

Do "Check even_ind_2" and stare hard at the result:

       forall P P0 : Z -> Prop,
       P 0 ->
       (forall n : Z, odd (n - 1) -> P0 (n - 1) -> P n) ->
       (forall n : Z, even (n - 1) -> P (n - 1) -> P0 n) ->
       forall z : Z, even z -> P z

P and P0 are the properties you want to prove by mutual induction:
    P n   for all n such that even n holds
    P0 n  for all n such that odd n holds

The next three lines are the steps of the inductive proof; you'll have
to prove these implications.

The last line is the conclusion.  Notice that it concludes only for n
such that even n holds.  That's because we looked at even_ind_2;
odd_ind_2 would conclude for odd n instead.

Let's use these induction principles.  Assume you want to show

      (1) forall n, even n -> n >= 0
      (2) forall n, odd n -> n >= 1

If you're only interested in property (1), and (2) is here just to get
the induction to go through, even_ind_2 will do the job:

Lemma even_pos:
  forall n, even n -> n >= 0.
Proof.
  apply (even_ind_2 (fun n => n >= 0) (fun n => n >= 1)).
  omega.
  intros. omega.
  intros. omega.
Qed.

You need to provide even_ind_2 with the two parameterized predicates P
and P0 adequate for your proof, i.e.
    P  := fun n => n >= 0
    P0 := fun n => n >= 1
You obtain them by finding the "forall" quantifications in (1),
(2) that correspond to the parameters of the inductive predicates
and turning them into "fun ... =>".

Things get more interesting if you need to use (1) AND (2) in the
remainder of your development.  You could of course re-do the proof
for (2) using odd_ind_2 instead of even_ind_2, but you're duplicating
the whole proof.

A better solution is to build and prove the real proof principle for
mutual induction that Scheme should have built in the first place:

Lemma even_odd_mutual_ind:
  forall P P0 : Z -> Prop,
  P 0 ->
  (forall n : Z, odd (n - 1) -> P0 (n - 1) -> P n) ->
  (forall n : Z, even (n - 1) -> P (n - 1) -> P0 n) ->
  (forall z : Z, even z -> P z) /\ (forall z : Z, odd z -> P0 z).

You can get the statement of this proof principle by cut-and-paste
from the output of "Check even_ind_2" and "Check odd_ind_2".

The proof of this lemma is trivial:

Proof.
  intros. split.
  apply (even_ind_2 P P0); assumption.
  apply (odd_ind_2 P P0); assumption.
Qed.

Now, you can prove (1) and (2) simultaneously, pretty much as you
would do on paper:

Lemma even_pos_odd_pos:
  (forall n, even n -> n >= 0) /\ (forall n, odd n -> n >= 1).
Proof.
  apply even_odd_mutual_ind; intros.
  omega.
  omega.
  omega.
Qed.

Note that it is no longer needed to instantiate the P and P0
parameters explicitly: Coq manages to find them from the goal.

This approach works well but has one weakness: every time
the definitions of the mutually inductive predicates change, the
statement of even_odd_mutual_ind needs to be changed accordingly.
(Its proof remains the same as long as the number of
mutually-inductive predicates doesn't change.)  For predicates with
many cases, this is a real pain because the statement of the lemma is
huge (several pages) and hard to read, let alone edit.

An alternative is to define "even_odd_mutual_ind" by giving directly
its proof term and letting Coq infer its type.

Definition even_odd_mutual_ind' (P P0: Z -> Prop) :=
  fun h1 h2 h3 => conj (even_ind_2 P P0 h1 h2 h3) (odd_ind_2 P P0 h1 h2 h3).

The inferred type is exactly that of even_odd_mutual_ind as stated above.

This looks cryptic at first, but basically you put as many "h"
parameters as there are cases in your mutually-inductive predicates.
This definition remains valid as long as the number of cases doesn't
change, but only their types.  Even if you add or remove cases, the
required edits are smaller than in the first approach.

Of course, all this footwork to define adequate induction principles
would be unnecessary if "Scheme" were extended to generate principles
of the "even_odd_mutual_ind" kind.  (Hint, hint.)

That's all I figured out so far.  Hope this could help.

- Xavier Leroy