(* N_addition.v, 30 Sep 2013 -- 31 Oct 2013 Basic arithmetic properties of the natural numbers *) Inductive N : Type := | zero : N | succ : N -> N. Definition one := succ zero. Theorem add : N -> N -> N. Proof. intro a. intro b. induction a. exact b. exact (succ IHa). Defined. Notation "a + b" := (add a b). Lemma add_succ_l (a b:N) : succ a + b = succ (a + b). Proof. simpl; reflexivity. Defined. Lemma add_succ_r (a b:N) : a + succ b = succ(a + b). Proof. induction a. simpl; reflexivity. rewrite add_succ_l. rewrite IHa. simpl. reflexivity. Defined. Lemma add_succ (a b:N) : a + succ b = succ a + b. Proof. rewrite add_succ_l. rewrite add_succ_r. reflexivity. Defined. Lemma add_zero_l (a : N) : zero + a = a. Proof. simpl. tauto. Defined. Lemma add_zero_r (a : N) : a + zero = a. Proof. induction a. simpl. reflexivity. replace (succ a + zero) with (succ (a + zero)). rewrite IHa. reflexivity. symmetry. apply add_succ_l. Defined. Lemma add_one (a:N) : a + one = succ a. Proof. induction a. simpl. reflexivity. rewrite add_succ_l. rewrite IHa. reflexivity. Defined. Lemma add_comm (a b:N) : b + a = a + b. Proof. induction a. rewrite add_zero_r. simpl. reflexivity. rewrite add_succ_l. rewrite add_succ_r. rewrite IHa. reflexivity. Defined. Lemma add_assoc (a b c:N) : (a + b) + c = a + (b + c). Proof. induction a. simpl. reflexivity. rewrite add_succ_l. rewrite add_succ_l. rewrite add_succ_l. rewrite IHa. reflexivity. Defined. Definition mult (a b:N) := N_rect (fun _ => N) zero (fun _ => (fun x => x + b)) a. Notation "a * b" := (mult a b). Lemma mult_succ_l (a b:N) : succ a * b = a * b + b. Proof. simpl. reflexivity. Defined. Lemma mult_succ_r (a b:N) : a * succ b = a + a * b. Proof. induction a. simpl. reflexivity. simpl. rewrite IHa. rewrite add_succ_r. rewrite add_assoc. reflexivity. Defined. Lemma mult_zero (a:N) : a * zero = zero. Proof. induction a. simpl. reflexivity. rewrite mult_succ_l. rewrite add_zero_r. exact IHa. Defined. Lemma mult_one_l (a:N) : one * a = a. Proof. simpl. reflexivity. Defined. Lemma mult_one_r (a:N) : a * one = a. Proof. induction a. simpl. reflexivity. simpl. rewrite IHa. rewrite add_one. reflexivity. Defined. Lemma mult_comm (a b:N) : a * b = b * a. Proof. induction a. simpl. symmetry. apply mult_zero. rewrite mult_succ_r. rewrite mult_succ_l. rewrite IHa. rewrite add_comm. reflexivity. Defined. Lemma mult_add_dist_l (a b c:N) : a * (b + c) = (a * b) + (a * c). Proof. induction a. simpl. reflexivity. simpl. rewrite IHa. rewrite add_assoc. rewrite add_assoc. rewrite (add_comm c b). rewrite <- (add_assoc (a * c) c b). rewrite (add_comm c (a * c)). rewrite (add_comm b (c + a * c)). reflexivity. Defined. Lemma mult_add_dist_r (a b c:N) : (a + b) * c = (a * c) + (b * c). Proof. rewrite mult_comm. rewrite (mult_comm a c). rewrite (mult_comm b c). rewrite (add_comm (c * b) (c * a)). rewrite (add_comm b a). apply mult_add_dist_l. Defined. Lemma mult_assoc (a b c:N) : (a * b) * c = a * (b * c). Proof. induction a. simpl. reflexivity. rewrite mult_succ_l. rewrite mult_succ_l. rewrite <- IHa. rewrite mult_add_dist_r. reflexivity. Defined.