Section Naturals. Inductive Nat : Set := zero : Nat | succ : Nat -> Nat. End Naturals. Section Negation. Inductive False : Set := . Definition not : Set -> Set := fun A : Set => A -> False. Lemma ex2 : forall A : Set, forall B : Set, A -> (not A) -> B. Proof. intros A B a na. unfold not in na. destruct (na a). Qed. Print ex2. Lemma ex2_more_coqish : forall A : Set, forall B : Set, A -> (not A) -> B. Proof. intros A B a na. destruct na. assumption. Qed. Print ex2_more_coqish. End Negation. Section MoreNaturals. Definition one : Nat := succ zero. Definition two : Nat := succ one. Definition three : Nat := succ two. Definition four : Nat := succ three. Fixpoint primrec (nz : Nat) (ns : Nat -> Nat) (n : Nat) {struct n} : Nat := match n with zero => nz | succ m => ns (primrec nz ns m) end. Definition plus : Nat -> Nat -> Nat := fun n : Nat => primrec n succ. Eval compute in (plus two three). Definition times : Nat -> Nat -> Nat := fun n : Nat => primrec zero (plus n). Eval compute in (times three two). Check Nat_rec. End MoreNaturals. Section LeibnizEquality. Inductive eq (A : Set) (x : A) : A -> Set := refl_equal : eq A x x. Theorem equality_symmetric : forall A : Set, forall x y : A, eq A x y -> eq A y x. Proof. intros A x y H. destruct H. apply refl_equal. Qed. Theorem equality_transitive : forall A : Set, forall x y z : A, eq A x y -> eq A y z -> eq A x z. Proof. intros A x y z Hxy Hyz. destruct Hxy. assumption. Qed. End LeibnizEquality. Section EqualityOnNaturals. Lemma eq_succ : forall n : Nat, forall m : Nat, eq Nat n m -> eq Nat (succ n) (succ m). Proof. intros n m H. destruct H. apply refl_equal. Qed. Definition pred : Nat -> Nat := fun n : Nat => match n with zero => zero | succ m => m end. Definition eq_succ_inv : forall n : Nat, forall m : Nat, eq Nat (succ n) (succ m) -> eq Nat n m := fun n m : Nat => fun H : eq Nat (succ n) (succ m) => match H in (eq _ _ m') return (eq Nat n (pred m')) with | refl_equal => refl_equal Nat n end. Theorem plus_zero_right : forall n : Nat, eq Nat (plus n zero) n . Proof. intro n. compute. apply refl_equal. Qed. Theorem plus_zero_left : forall n : Nat, eq Nat (plus zero n) n . Proof. intro n. induction n. compute. apply refl_equal. unfold plus. compute; fold primrec. apply eq_succ. apply IHn. Qed. Lemma plus_succ_right : forall n m : Nat, eq Nat (plus m (succ n)) (succ (plus m n)). Proof. intros n m. compute; fold primrec. apply eq_succ. apply refl_equal. Qed. Lemma plus_succ_left : forall n m : Nat, eq Nat (plus (succ m) n) (succ (plus m n)). Proof. intro n. induction n. intro m. compute. apply refl_equal. intro m. compute; fold primrec. fold (plus (succ m) n) (plus m n). apply eq_succ. apply IHn. Qed. Theorem plus_commutative : forall n m : Nat, eq Nat (plus n m) (plus m n). Proof. intro n. induction n. intro m. apply equality_transitive with (y := m). apply plus_zero_left. apply equality_symmetric. apply plus_zero_right. intro m. apply equality_transitive with (y := succ (plus n m)). apply plus_succ_left. apply equality_transitive with (y := succ (plus m n)). apply eq_succ. apply IHn. apply equality_symmetric. apply plus_succ_right. Qed. Print plus_commutative. End EqualityOnNaturals.