(* 2008 - 02 - 18 *) (* To prove the following, we must use recursion on n. *) (* Working out the structure of the fixpoint is not too hard, but Coq will not accept it unless we give it some further type annotations. We'll do this next time. *) Lemma O_le_n : forall n, O <= n. Proof. exact ( fix F (n : nat) : 0 <= n := match n return (fun n : nat => 0 <= n) n with | O => le_n O | S n' => le_S O n' (F n') end ). Defined. (* With this proof, we can prove lots of other facts, e.g. *) Lemma O_le_500 : 0 <= 500. Proof. exact (O_le_n 500). Defined. (* We can evaluate this proof as well, it is quite large. *) (* Uncomment the next line if you would like to do that. *) (* Eval compute in O_le_500. *) (* Note that we take advantage of the C-H isomorphism here, rather conveniently. The evaluated proof is a good deal larger than the unevaluated proof. *) (* Here we prove an induction principle on natural numbers. This induction principle corresponds to the one usually used in introductory logic classes, but it is not the only induction principle and it is not always the best. However, it is the one that Coq automatically generates and names nat_ind when it process the inductive declaration of nat in the core part of the standard library. Note that the the induction principle is a higher order function--- its arguments are functions. *) Lemma nat_ind' : forall (P : nat -> Prop), P O -> (forall n : nat, P n -> P (S n)) -> forall n, P n. Proof. intros P f0 fn. exact ( fix F (n : nat) : P n := match n return P n with | O => f0 | S n' => fn n' (F n') end ). Defined. (* Note that in this proof we used the intro tactic to build the non-recursive part of the function header. Then we defined a fixpoint over n. *) (* Now, we write P, f0, and fn for forall n, n <= 0. *) Definition P := (fun n => 0 <= n) : nat -> Prop. Definition f0 := le_n 0 : P 0. (* Some people had not completed this one, but we add it anyway. *) Definition fn := (fun (n : nat) (H : P n) => le_S _ _ H) : forall n : nat, P n -> P (S n). (* With these functions we can prove forall n, 0 <= n again. *) Goal forall n, 0 <= n. exact (nat_ind' P f0 fn). Defined. (* If we evaluate we get the same function that we wrote in the beginning. *) Eval compute in Unnamed_thm.