(** 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.