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

    Exercise 7
    published 12/11/09, deadline 19/11/09, 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.

    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.
intros a b. 
unfold square.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
rewrite mult_plus_distr_l.
replace (2*a*b) with (a*b + a*b).
pattern (b*a).
rewrite mult_comm.
rewrite plus_assoc.
rewrite plus_assoc.
reflexivity.
pattern (2*a*b).
rewrite<- mult_assoc.
simpl.
rewrite plus_0_r.
reflexivity.
Qed.

(* Define a function which sums up the first n numbers. *)
Fixpoint sum (n:nat) : nat :=
  match n with
  | 0 => 0
  | S n' => n + sum n'
  end. 

(* 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).
induction n.
reflexivity.
replace (2 * sum (S n)) with (2 + 2 * n + 2 * sum n).
rewrite IHn.
ring.
simpl.
ring.
Qed.

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

(* 
To prove forall n:nat, 2*(sum n) = n * (n+1).
we use induction over n.
base case n=0: easy calculation.
step case: Assume IH : 2*(sum n) = n * (n+1).
To show that 2*(sum (n+1)) = (n+1) * (n+2)
we use that 2*(sum (n+1)) = 2*sum n + 2*n + 2
and hence using IH it remains to show
2 * (n * (n+1)) + 2*n + 2 = (n+1) * (n+2)
which follows by easy calculation.
*)

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 :=
  rep true negb.

(* Prove that you implementation agrees with the given one: *)
Goal forall n:nat, is_even n = is_even' n.
intro n.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.

(* 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: *)
Definition eqn' : nat -> nat -> bool :=
  rep (fun (n:nat) => match n with 
                      | 0 => true
                      | (S n') => false
                      end)
   (fun (eqm : nat -> bool) =>
      fun (n:nat) => match n with 
                      | 0 => false
                      | (S n') => eqm n'
                      end).
(* 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.
intro m.
induction m.
intro n.
induction n.
reflexivity.
reflexivity.
intro n.
induction n.
reflexivity.
simpl.
apply IHm.
Qed.
(* Hint: Don't do too many intros to soon. *)