(** Introduction to Formal Reasoning (G52IFR) Tutorial 6 **) Section Tut6. (* we need to load Arith.v to use lemmas defined there *) Load Arith. (* 'induction' is a powerful version of 'destruct' *) Lemma again : forall n, 1 + n = n + 1. intro n. (* try out what happens if you do 'destruct n. reflexivity.' *) induction n. reflexivity. simpl. rewrite <- IHn. reflexivity. Qed. Lemma mult_1_bothSides : forall n, 1 * n * 1 = n. intro n. simpl. rewrite <- plus_n_O. induction n; simpl. reflexivity. rewrite IHn. reflexivity. Qed. Lemma calculating_is_easy : 1 + 2 + 3 + 4 = 10. reflexivity. Qed. Lemma calculating_is_easy_2 : forall n, 1 + 2 + 3 + n = 6 + n. intro n. reflexivity. Qed. Lemma not_so_easy_here : forall n, n + 3 + 4 = n + 7. intro n. rewrite <- plus_assoc. reflexivity. Qed. Lemma better_left_then_right : forall m n, m + 2 + n = 2 + m + n. intros m n. induction m. reflexivity. simpl. rewrite IHm. reflexivity. Qed. Lemma patt : forall m n, 3 + (m + 1 + n) = 3 + (m + (1 + n)). intros. pattern (m + (1 + n)); rewrite plus_assoc. reflexivity. Qed. (* a function that calls itself recursively *) Fixpoint sum n : nat := match n with | 0 => 0 | S k => sum k + (S k) end. (* we did not prove this in the tutorial, maybe another time *) (* Theorem gauss : forall n, 2 * sum n = n * (S n). *) End Tut6.