Mercurial > cpdt > repo
changeset 31:1a82839f83b7
Mutual induction
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 08 Sep 2008 16:00:02 -0400 |
parents | 4887ddb1ad23 |
children | 77e1a7eda0b8 |
files | src/InductiveTypes.v |
diffstat | 1 files changed, 99 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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. *)