(** 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'). Definition function : (A -> B) * (A -> C) -> (A -> B * C) := 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. Theorem mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. (** This is a coursework exercise. Here, we just postulate that it is true. *) Hypothesis mult_comm : forall n m, n * m = m * n. 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. Theorem gauss : forall n, 2 * sum n = n * (S n). End NaturalNumbers. End Tutorial5.