(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    Exercise 7
    published 12/11/08, deadline 19/11/08, 17:00 electronic submission

    Use
    $ cw submit ex07.v
    on one of the CS servers
    then look for the coursework 235 labelled 'g52mc2 coursework 7' 
    and enter the associated code.

    Multiple submissions are allowed, up to the deadline.

    Fill in the missing proofs. You are only supposed to use the
    tactics introduced in the lectures, e.g.
    cut, exact, assumption, intro(s), apply, split, elim, left, right, case,
    exists, reflexivity, rewrite(<-), pattern, discriminate, induction, ring,
    simpl, inversion, replace.

    If you want to use another simple tactic not on the list, please
    check with your tutor.
**)

Section ex7.

Require Import Coq.Arith.Arith.

Definition square (n:nat) : nat := n*n.

(* Prove the binomial law. Use only the laws of a semiring.
** You are *not* allowed to use the ring tactic. *)
Goal forall (a b : nat),square (a+b) = square a + 2*a*b + square b.
(* insert your proof here. *)

(* Define a function which sums up the first n numbers. *)
Fixpoint sum (n:nat) : nat :=
(* insert your definition here *)

(* Test it: *)
Eval compute in (sum 0).  (* should be 0 *)
Eval compute in (sum 3).  (* should be 6=1+2+3 *)
Eval compute in (sum 10). (* should be 55=1+2+..+9+10 *)

(* Observe that sum n = n*(n+1) / 2 (why ?) 
** to avoid division we multiply both sides by 2.
** This time you *are* allowed to use ring. *)
Goal forall n:nat, 2*(sum n) = n * (n+1).
(* insert your proof here. *)

(* Turn your proof into English. Use phrases like
    "induction over n"
    "base case:" (case for 0)
    "step case:" (case for sucessor)
    "induction hypothesis" (what you have assumed for n)
    "follows by easy calculation. (if you have used ring).
*)    

(* Write your proof here:

*)

Set Implicit Arguments.

(* We use "rep" as introduced in the lecture but for any set A *)
Fixpoint rep (A : Set)
  (a : A)(f : A -> A)(n : nat) {struct n} : A :=
  match n with
  | O => a
  | S n => f (rep a f n)
  end.

(* I repeat the definition of is_even from one of the previous lectures: *)
Fixpoint is_even (n : nat) : bool :=
  match n with
  | 0 => true
  | S n' => negb (is_even n')
  end.

(* Implement an equivalent function using only rep and not fixpoint. *)
Definition is_even' : nat -> bool :=
  (* Insert your definition here. *)

(* Prove that you implementation agrees with the given one: *)
Goal forall n:nat, is_even n = is_even' n.
  (* Insert your proof here. *)

(* The following function decides wether 2 natural numbers are equal.
   I.e. it satisfies the spec:
   forall m n:nat, m=n <-> eqn m n = true.
   However, we are not going to prove this now.
*)

Fixpoint eqn (m n : nat) {struct m}: bool :=
  match (m,n) with
  | (0,0) => true
  | (S m,0) => false
  | (0,S n) => false
  | (S m,S n) => eqn m n
  end.

(* But you are supposed to reimplement the function using rep (and not fixpoint): *)
Definition eqn' : nat -> nat -> bool :=
  (* insert your definition here. *)

(* Hint: remember higher order functions. *)

(* And prove that your reimplementation is equivalent to the original program. *)
Goal forall (m n : nat), eqn m n = eqn' m n.
(* insert your proof here. *)

(* Hint: Don't do too many intros to soon. *)