(* G54DTP Dependently Typed Programming. Inductive predicates and relations. Venanzio Capretta, February 2011. *) Require Import Arith. (* Check the definitions and theorems in the standard library Arith. *) (* Predicate stating that a number is even. *) Inductive Even : nat -> Prop := evenO : Even O | evenSS : forall n:nat, Even n -> Even (S (S n)). Lemma even12: Even 12. Proof. apply evenSS. apply evenSS. apply evenSS. apply evenSS. apply evenSS. apply evenSS. exact evenO. Qed. (* We can avoid repeating the same tactic many times by using the tactical "repeat". *) Lemma even12' : Even 12. Proof. repeat (apply evenSS). exact evenO. Qed. Lemma twoTimesEven: forall n:nat, Even (n+n). Proof. intro n. (* Elimination of a natural number: proof by induction. *) elim n. (* Base case. *) exact evenO. (* Inductive step. *) intros n' IH. rewrite <- plus_Snm_nSm. (* The lemma plus_Snm_nSm states an equality, the arrow <- specifies that we want to rewrite it from right to left. *) simpl. apply evenSS. exact IH. Qed. (* Predicate stating that a number is odd. *) Inductive Odd: nat -> Prop := odd1 : Odd 1 | oddSS : forall n, Odd n -> Odd (S (S n)). Lemma oddSeven: forall m, Odd m -> Even (S m). Proof. intros m H. (* We do induction of the proof of (Odd m). *) elim H. (* Base case: the proof was odd1, so m=1. *) apply evenSS; apply evenO. (* Semicolon: do the tactis in succession. *) (* Inductive step: the proof was (oddSS m' Hm') for some m' and some proof Hm': Odd m'; so m=(S (S m')). *) intros m' Hm' IH. apply evenSS. exact IH. Qed. Lemma evenSodd: forall m, Even m -> Odd (S m). intros m h; elim h. exact odd1. intros m' h' IH; apply oddSS; exact IH. Qed. Lemma oddPlusOddEven: forall n, Odd n -> forall m, Odd m -> Even (n+m). Proof. intros n Hn. (* We do induction on the proof of (Odd n). *) elim Hn. (* Base case: odd1, so n=1. *) apply oddSeven. (* Inductive step: oddSS n' Hn', so n=(S (S n')). *) intros n' Hn' IH. intros m Hm; simpl. apply evenSS. apply IH. exact Hm. Qed. (* Even and odd numbers are already predefined in the standard library using a mutual inductive definition. *) Require Import Even. Print even. (* Our definitions are equivalent to those in the library. *) Lemma Even_even: forall n, Even n -> even n. Proof. intros n h; elim h. exact even_O. intros n' h' IH. apply even_S. apply odd_S. exact IH. Qed. Lemma Odd_odd: forall n, Odd n -> odd n. Proof. intros n h; elim h. apply odd_S; exact even_O. intros n' h' IH; apply odd_S; apply even_S; exact IH. Qed. (* For the implication in the other direction we must do mutual induction on even and odd. This can't be done in an ordinary proof but it can be done in a mutual fixpoint. *) Fixpoint even_Even (n:nat)(h: even n): Even n := match h in even n return Even n with even_O => evenO | even_S n' h' => oddSeven n' (odd_Odd n' h') end with odd_Odd (n:nat)(h:odd n): Odd n := match h with odd_S n' h' => evenSodd n' (even_Even n' h') end.