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

    Exercise 5
    published 22/10/09, deadline 29/10/09, 17:00 electronic submission

    Use
    $ cw submit ex05.v
    on one of the CS servers
    then look for the coursework ??? labelled 'g52mc2 coursework 5' 
    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(<-), discriminate, destruct, contradict

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

Axiom ext : forall (A B : Set)(f g : A -> B), (forall x:A,f x = g x) -> f = g.
Open Scope type_scope.

(* Prove that the following sets are isomorphic: *)

Definition Four1 := bool + bool.
Definition Four2 := bool * bool.
Definition Four3 := bool -> bool.

Definition phi1 : Four1 -> Four2 :=
  fun x : Four1 => match x with
                     |  inl b => (true , b)
                     |  inr c => (false , c)
                     end.


Definition psi1 : Four2 -> Four1 :=
  fun x : Four2 => match x with 
                   | (b,c) => if b then inl bool c else inr bool c
                   end.


Goal forall x : Four1, psi1 (phi1 x) = x.
intros x.
destruct x.
simpl.
reflexivity.
reflexivity.
Qed.

Goal forall x:Four2, phi1(psi1 x) = x.
intros x.
destruct x.
destruct b.
reflexivity.
reflexivity.
Qed.

Definition phi2 : Four2 -> Four3 :=
  fun x : Four2 => fun b:bool =>
    match x with 
    | (x0,x1) => if b then x0 else x1
    end.

Definition psi2 : Four3 -> Four2 :=
  fun f:Four3 => (f true, f false).

Goal forall x : Four2, psi2 (phi2 x) = x.
intros x.
destruct x.
reflexivity.
Qed.

Goal forall x:Four3, phi2(psi2 x) = x.
intro f.
apply ext.
intro x.
destruct x.
reflexivity.
reflexivity.
Qed.

(* Prove the following (surprising ?) theorem:

   Given any function f : bool -> bool, applying the function
   three times is the same as applying it once.
*)

Goal forall (f:bool -> bool) (b:bool), f( f( f( b))) = f b.
intros f b.
destruct b.
case_eq (f true).
intros ftt.
rewrite ftt.
exact ftt.
intro ftf.
case_eq (f false).
intro fft.
exact ftf.
intros fff.
exact fff.
case_eq (f false).
intro fft.
case_eq (f true).
intro ftt.
exact ftt.
intro ftf.
exact fft.
intro fff.
rewrite fff.
exact fff.
Qed.

(*
Hint: It is useful to apply the tactic case_eq. case_eq works like
case but it also introduces an equational assumption. E.g. if we want
to prove a goal "P b" and say "case b" we have to prove "P true" and
"P false". If we say instead "case_eq b" we have to prove 
"b = true -> P true" and "b = false => P false". These equations may 
come in handy during the proof.
*)