(** Introduction to Formal Reasoning (G52IFR) Nuo Li T05 **) Section T5. Load Arith. Fixpoint g (m n : nat) {struct m} : nat := match m with | 0 => n | S m' => S (g m' n) end. (* What is g? Try a few examples *) Eval compute in (g 1 2). Eval compute in (g 10 12). Lemma mult_1_bothSides : forall n, 1 * n * 1 = n. intro. simpl. rewrite <- plus_n_O. induction n. reflexivity. simpl. rewrite IHn. reflexivity. Qed. Fixpoint sum n {struct n} : nat := match n with | 0 => 0 | S k => sum k + (S k) end. Hypothesis mult_comm : forall n m, n * m = m * n. Lemma exchange : forall a b c d : nat, a + b + (c + d) = a + c + (b + d). intros. rewrite plus_assoc. pattern (a + b + c). rewrite <- plus_assoc. rewrite (plus_comm b c). rewrite plus_assoc. rewrite plus_assoc. split. Qed. Theorem gauss : forall n, 2 * sum n = n * (S n). intro. induction n. reflexivity. simpl. rewrite <- plus_n_O. rewrite exchange. replace (sum n + sum n) with (n * S n). rewrite plus_assoc. rewrite plus_comm. rewrite (plus_comm (n * S n) (S n)). replace (S n + (S n + n * S n)) with ((S (S n)) * (S n)). rewrite mult_comm. split. split. rewrite <- IHn. simpl. rewrite <- plus_n_O. split. Qed. End T5. Lemma n_Sn : forall n : nat, n <> S n. intro. induction n. intro. discriminate H. intro. apply IHn. apply peano8. assumption. Qed. Lemma t2 : forall n, n = S n -> n = n + 1. intros. destruct (n_Sn n H). Qed. Notation "m <= n" := (leq m n). Theorem le2n : forall n : nat, n <= (n + n). intros. exists n. reflexivity. Qed. End T5.