(* Evenness for natural numbers. *) Inductive even : nat -> Prop := | EvenO : even O | EvenB : forall n : nat, even n -> even (S (S n)) . (* The property that a proof of evenness contains the proof that 0 is even. *) Inductive containsEvenO : forall (n : nat), even n -> Prop := | CEvenO : containsEvenO O EvenO | CEvenB : forall (n : nat) (H : even n), containsEvenO n H -> containsEvenO (S (S n)) (EvenB n H) . (* Let's figure out what the maximal induction principle for even is and prove it. *) Definition even_ind' : forall (P : forall n : nat, even n -> Prop) (HO : P O EvenO) (HB : forall (n : nat) (H : even n), P n H -> P (S (S n)) (EvenB n H)), forall (n : nat) (H : even n), P n H. intros P HO HB. exact (fix F (n : nat) (H : even n) : P n H := match H in even n' return P n' H with | EvenO => HO | EvenB nb Hb => HB nb Hb (F nb Hb) end). Qed. (* We prove that every proof of evenness contains a proof that O is even using our new induction principle. *) Lemma always_contains_EvenO : forall (n : nat) (H : even n), containsEvenO n H. Proof. intros n H. apply even_ind'. apply CEvenO. intros. apply CEvenB. exact H1. Qed. (* Observe that our proof object is quite straightforward. *) Print always_contains_EvenO. (* We can also do our proof using the induction tactic but specifying the induction principle. *) Goal forall (n : nat) (H : even n), containsEvenO n H. Proof. intros n H. induction H using even_ind'. apply CEvenO. intros. apply CEvenB. exact IHeven. (* Notice that when we use the induction tactic, instead of directly applying the induction principle we get slightly more meaningful hypothesis names. *) Qed. (* We can also prove the minimal induction principle using the maximal induction principle. This is rather straightforward. *) Goal forall PMin : nat -> Prop, PMin 0 -> (forall n : nat, even n -> PMin n -> PMin (S (S n))) -> forall n : nat, even n -> PMin n. Proof. intros. (* We do this by cleverly selecting P for even_ind' such that forall (n : nat) (H : even n), P n H =~ PMin n. *) Eval compute in ((fun (n : nat) (_ : even n) => PMin n) n H1). apply (even_ind' (fun (n : nat) (_ : even n) => PMin n)); auto. (* Here we introduce auto. Basically, auto applies the modus ponens rule. *) Qed. (* You would think that the maximal induction principle was more powerful than the minimal induction principle, but it's not. We can show this by proving the maximal induction principle using the minimal induction principle, but that's a little beyond our scope at this time, so we don't do it all. *) Definition even_ind'' : forall (P : forall n : nat, even n -> Prop) (HO : P O EvenO) (HB : forall (n : nat) (H : even n), P n H -> P (S (S n)) (EvenB n H)), forall (n : nat) (H : even n), P n H. Proof. intros. (* What we have here is a function header, and hole where we need to put a proof of P n H. *) Show Proof. (* Clearly this doesn't match the minimal induction principle's type for P. But we can fix that. *) generalize H. (* What we have done here is to mutate our proof. We can inspect the new proof. *) Show Proof. (* In the proof body, we bind the result of the current subgoal to a variable and then apply that result to our hypothesis that n is even. Another way to look at is that instead of proving B, we'll prove that A -> B and then use modus ponens to prove B. *) (* We use the pattern tactic to do a beta abstraction and make P explicit. *) pattern n. (* We can check the type of the pattern and see that it has the correct type for P. *) Check (fun n0 : nat => forall H0 : even n0, P n0 H0). induction H; intros Hyp; dependent inversion Hyp; auto. Defined. (* Why didn't we just do induction on n? *) (* Note that the proof objects are _very_different. *) Eval compute in even_ind''. Print even_ind''. Print even_ind'. (* Why does Coq generate the minimal induction principle for elements in Prop? The assumption is that we want to preserve proof irrelevance; we don't want to make arguments about the structure of the proof itself. *) (* Contrarily, when defining induction principles for elements in Set, e.g., nat, it is assumed that we will want to make use of the structure in defining the result type, so the maximal induction principle is synthesized. *) (* Another interesting fact is that in general, element in Set have three structural induction principles, but elements in Prop have just one. This is not always true, sometimes elements in Prop have more than one.*) (* But we expect nat to have three, and we can print them all. *) Print nat_ind. Print nat_rec. Print nat_rect. (* The first two are defined in terms of the third. Their types differ only in the type of P. This naming convention is used universally in Coq. *) (* We could synthesize the minimal induction principle for nat by hand. Let's try this on paper and prove it. We define nat_rect' instead of nat_ind'. *) Definition nat_rect' : forall (P : Type), P -> (nat -> P -> P) -> forall n : nat, P. Proof. intros. induction n using nat_rect. apply X. apply X0. apply n. apply IHn. (* We use the maximal induction principle to prove the minimal induction principle. *) Defined. Eval compute in nat_rect'. (* We can actually build minimal or maximal structural induction principles at will using special commands. The value after the keyword Sort indicates the result type of P. *) (* Observe that you can use the templates menu to help remind yourself of the syntax for the Scheme command. *) Scheme nat_rect'' := Minimality for nat Sort Type. Print nat_rect''. Scheme even_ind''' := Induction for even Sort Prop. Print even_ind''. (* False and True break our rule that Props have only one induction principle. They are special. We'll talk about why later. *) Print False_rect. Print True_rect. (* Observe, though, that they don't violate the rule that propositions are supplied with the minimal induction principle. *)