(** Introduction to Formal Reasoning (G52IFR) Nicolai Kraus Tutorial 5 : functions, natural numbers **) Section Tutorial5. Section Functions. (** don't worry about this *) Open Scope type_scope. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. (** some variables *) Variables A B C : Set. Variables A' B' C' : Prop. (** I want to explain how to define functions by using the Curry-Howard correspondence *) Lemma lemma : (A' -> B') /\ (A' -> C') -> (A' -> B' /\ C'). intro abac. intro a. destruct abac as [ab ac]. split. apply ab. exact a. exact (ac a). Qed. Definition function : (A -> B) * (A -> C) -> (A -> B * C) := fun abac => fun a => match abac with | (ab , ac) => ( ab(a) , ac a ) end. End Functions. (** Now, let's talk about numbers *) Section NaturalNumbers. (** We are using all the results from the lecture. *) Load Arith. (** summary Fixpoint add (m n : nat) {struct m} : nat := match m with | 0 => n | S m => S (add m n) end. Fixpoint mult (m n : nat) {struct m} : nat := match m with | 0 => 0 | S m => add n (mult m n) end. Lemma peano7 : forall n:nat, S n <> 0. Lemma peano8 : forall m n:nat, S m = S n -> m = n. Lemma peano9 : forall P : nat -> Prop, P 0 -> (forall m : nat, P m -> P (S m)) -> forall n : nat, P n. Lemma plus_O_n : forall n:nat, n = 0 + n. Lemma plus_n_O : forall n:nat, n = n + 0. Lemma plus_assoc : forall (l m n:nat),l + (m + n) = (l + m) + n. Lemma plus_n_Sm : forall n m : nat, S (m + n) = m + S n. Lemma plus_comm : forall n m:nat, n + m = m + n. **) (** Useful here and for the coursework: symmetry : turns an equation around. pattern t : focusses the next rewrite on a particular subterm. pattern t at n : focusses rewrite on the nth occurence of a subterm. *) Theorem mult_1_bothSides : forall n, 1 * n * 1 = n. intro n. simpl. rewrite <- plus_n_O. induction n; simpl. reflexivity. rewrite IHn. reflexivity. Qed. Theorem mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. intros n m p. induction n; simpl. reflexivity. rewrite IHn. rewrite plus_assoc. reflexivity. Qed. (** This is a coursework exercise. Here, we just postulate that it is true. *) Hypothesis mult_comm : forall n m, n * m = m * n. (** Gauss : 1+2+3+...+100 = 100*101/2 *) Fixpoint sum n {struct n} : nat := match n with | 0 => 0 | S k => sum k + (S k) end. Lemma opposite_of_peano8 : forall m n:nat, m = n -> S m = S n. intros. rewrite H. reflexivity. Qed. (** don't worry, the coursework is simpler. **) Theorem gauss : forall n, 2 * sum n = n * (S n). intro n. simpl. rewrite <- plus_n_O. induction n; simpl. reflexivity. rewrite plus_assoc. pattern (sum n + S n + sum n). rewrite <- plus_assoc. pattern (S n + sum n). rewrite plus_comm. rewrite plus_assoc. rewrite IHn. clear IHn. rewrite <- plus_n_Sm. rewrite <- plus_assoc. simpl. rewrite <- plus_n_Sm. apply opposite_of_peano8. apply opposite_of_peano8. rewrite plus_comm. assert (claim : n + n * S n = n * S (S n)). simpl. assert (claim2 : n = n*1). induction n; simpl. reflexivity. rewrite <- IHn; reflexivity. pattern n at 1. rewrite claim2. assert (dist : forall n m p, p * (n + m) = p * n + p * m). intros. rewrite mult_comm. rewrite (mult_comm (p)). rewrite (mult_comm p). apply mult_plus_distr_r. symmetry. assert (S (S n) = 1 + S n). reflexivity. rewrite H. apply dist. pattern (n + n * S (S n)). rewrite plus_comm. rewrite <- claim. pattern (n + n * S n + n). rewrite <- plus_assoc. pattern (n * S n + n). rewrite plus_comm. rewrite plus_assoc. reflexivity. Qed. End NaturalNumbers. End Tutorial5.