(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch L08 (Peano arithmetic) The material in this file contains coq proofs which can be read and animated with coqide or xemacs+proofgeneral. **) Section nat. (* In Coq natural numbers are constructed from 0 : nat S : nat -> nat see http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html *) Eval compute in (S (S (S 0))). Definition pred (n : nat) : nat := match n with | 0 => 0 | S n' => n' end. Eval compute in (pred 3). Definition f_is_even : (nat -> bool) -> (nat -> bool) := fun (h : nat -> bool) => fun (n:nat) => match n with | 0 => true | S n' => negb (h n') end. Definition f_no_fix : (nat -> bool) -> (nat -> bool) := fun (h : nat -> bool) => fun (n:nat) => negb (h n). (* Fixpoint no_fix (n:nat) : nat := negb (f n). *) Fixpoint is_even (n : nat) : bool := match n with | 0 => true | S n' => negb (is_even n') end. Fixpoint double (n:nat) : nat := match n with | 0 => 0 | S n' => S (S (double n')) end. Eval compute in (double 3). Fixpoint half (n:nat) : nat := match n with | 0 => 0 | S 0 => 0 | S (S n') => S (half n') end. Eval compute in (half 9). Eval compute in (half (double 58)). Goal forall n:nat, half (double n) = n. intro n. induction n. simpl. reflexivity. simpl. rewrite IHn. reflexivity. Qed. (* Proving Peano's axioms. *) Goal forall (m n:nat), S m = S n -> m = n. intros m n smsn. replace m with (pred (S m)). rewrite smsn. unfold pred. reflexivity. reflexivity. Qed. Goal forall (m n:nat), S m = S n -> m = n. intros m n smsn. injection smsn. intros h. refine h. Qed. Goal forall (m n:nat), ~(S m = 0). intros m n sm0. discriminate sm0. Qed. Fixpoint plus (n m:nat) {struct n} : nat := match n with | 0 => m | S n' => S (plus n' m) end. Eval compute in (plus 3 4). Eval compute in (3 + 4). (* for the official definition of + see: http://coq.inria.fr/stdlib/Coq.Init.Peano.html *) Lemma plus_assoc : forall (l m n:nat), l + (m + n) = (l + m) + n. intros l m n. induction l. simpl. reflexivity. simpl. rewrite IHl. reflexivity. Qed. Lemma plus_0_n : forall n:nat, n = 0 + n. intro n. reflexivity. Qed. Lemma plus_n_O : forall n:nat, n = n + 0. intros. induction n. simpl. reflexivity. simpl. rewrite<- IHn. reflexivity. Qed. Lemma plus_n_Sm : forall n m : nat, S (m + n) = m + S n. intros. induction m. simpl. reflexivity. simpl. rewrite IHm. reflexivity. Qed. Lemma plus_comm : forall n m:nat, n + m = m + n. intros. induction n. simpl. apply plus_n_O. simpl. rewrite IHn. apply plus_n_Sm. Qed. (* using algebraic properties. *) Goal forall (i j k:nat), i + j + k = k + j + i. intros i j k. rewrite plus_comm. pattern (i + j). rewrite plus_comm. rewrite plus_assoc. reflexivity. Qed. (* Defining <= *) Definition Le (m n : nat) := exists k:nat, k+m = n. Notation "n <= m" := (Le n m). Goal 2 <= 3. unfold Le. exists 1. reflexivity. Qed. Goal ~(3 <= 2). Goal ~(3 <= 2). intro h32. unfold Le in h32. destruct h32. cut (3+x = 2). intro h32'. simpl in h32'. discriminate. rewrite plus_comm. exact H. Qed.