# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220904002 14400
# Node ID 1a82839f83b7a0bcbfa2f83c5df628bae9f74e31
# Parent  4887ddb1ad23b5cbae7ed8d33e77796f26461b53
Mutual induction

diff -r 4887ddb1ad23 -r 1a82839f83b7 src/InductiveTypes.v
--- a/src/InductiveTypes.v	Mon Sep 08 15:38:34 2008 -0400
+++ b/src/InductiveTypes.v	Mon Sep 08 16:00:02 2008 -0400
@@ -451,3 +451,102 @@
 ]]
 
 Thus, even though we just saw that [T] is added as an extra argument to the constructor [Cons], there is no quantifier for [T] in the type of the inductive case like there is for each of the other arguments. *)
+
+
+(** * Mutually Inductive Types *)
+
+(** We can define inductive types that refer to each other: *)
+
+Inductive even_list : Set :=
+| ENil : even_list
+| ECons : nat -> odd_list -> even_list
+
+with odd_list : Set :=
+| OCons : nat -> even_list -> odd_list.
+
+Fixpoint elength (el : even_list) : nat :=
+  match el with
+    | ENil => O
+    | ECons _ ol => S (olength ol)
+  end
+
+with olength (ol : odd_list) : nat :=
+  match ol with
+    | OCons _ el => S (elength el)
+  end.
+
+Fixpoint eapp (el1 el2 : even_list) {struct el1} : even_list :=
+  match el1 with
+    | ENil => el2
+    | ECons n ol => ECons n (oapp ol el2)
+  end
+
+with oapp (ol : odd_list) (el : even_list) {struct ol} : odd_list :=
+  match ol with
+    | OCons n el' => OCons n (eapp el' el)
+  end.
+
+(** Everything is going roughly the same as in past examples, until we try to prove a theorem similar to those that came before. *)
+
+Theorem elength_eapp : forall el1 el2 : even_list,
+  elength (eapp el1 el2) = plus (elength el1) (elength el2).
+  induction el1; crush.
+
+  (** One goal remains: [[
+
+  n : nat
+  o : odd_list
+  el2 : even_list
+  ============================
+   S (olength (oapp o el2)) = S (plus (olength o) (elength el2))
+   ]]
+
+   We have no induction hypothesis, so we cannot prove this goal without starting another induction, which would reach a similar point, sending us into a futile infinite chain of inductions.  The problem is that Coq's generation of [T_ind] principles is incomplete.  We only get non-mutual induction principles generated by default. *)
+
+Abort.
+Check even_list_ind.
+(** [[
+
+even_list_ind
+     : forall P : even_list -> Prop,
+       P ENil ->
+       (forall (n : nat) (o : odd_list), P (ECons n o)) ->
+       forall e : even_list, P e
+]]
+
+We see that no inductive hypotheses are included anywhere in the type.  To get them, we must ask for mutual principles as we need them, using the [Scheme] command. *)
+
+Scheme even_list_mut := Induction for even_list Sort Prop
+with odd_list_mut := Induction for odd_list Sort Prop.
+
+Check even_list_mut.
+(** [[
+
+even_list_mut
+     : forall (P : even_list -> Prop) (P0 : odd_list -> Prop),
+       P ENil ->
+       (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->
+       (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) ->
+       forall e : even_list, P e
+]]
+
+This is the principle we wanted in the first place.  There is one more wrinkle left in using it: the [induction] tactic will not apply it for us automatically.  It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types. *)
+
+Theorem n_plus_O' : forall n : nat, plus n O = n.
+  apply (nat_ind (fun n => plus n O = n)); crush.
+Qed.
+
+(** From this example, we can see that [induction] is not magic.  It only does some bookkeeping for us to make it easy to apply a theorem, which we can do directly with the [apply] tactic.  We apply not just an identifier but a partial application of it, specifying the predicate we mean to prove holds for all naturals.
+
+This technique generalizes to our mutual example: *)
+
+Theorem elength_eapp : forall el1 el2 : even_list,
+  elength (eapp el1 el2) = plus (elength el1) (elength el2).
+  apply (even_list_mut
+    (fun el1 : even_list => forall el2 : even_list,
+      elength (eapp el1 el2) = plus (elength el1) (elength el2))
+    (fun ol : odd_list => forall el : even_list,
+      olength (oapp ol el) = plus (olength ol) (elength el))); crush.
+Qed.
+
+(** We simply need to specify two predicates, one for each of the mutually inductive types.  In general, it would not be a good idea to assume that a proof assistant could infer extra predicates, so this way of applying mutual induction is about as straightforward as we could hope for. *)