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

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

    Use
    $ cw submit ex05.v
    on one of the CS servers
    then look for the coursework 226 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,
    case_eq, exists, reflexivity, rewrite(<-), discriminate, destruct, contradict

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

(* You will need the axiom of extensionality when reasoning about functions. *)
Axiom ext : forall (A B : Set)(f g : A -> B), (forall x:A,f x = g x) -> f = g.
(* Open type_scope so that + and * are interpreted as ops on sets not numbers. *)
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 :=
  (* Insert your definition. *)

Definition psi1 : Four2 -> Four1 :=
  (* Insert your definition. *)

Goal forall x : Four1, psi1 (phi1 x) = x.
  (* Insert your proof. *)

Goal forall x:Four2, phi1 (psi1 x) = x.
  (* Insert your proof. *)

Definition phi2 : Four2 -> Four3 :=
  (* Insert your definition. *)

Definition psi2 : Four3 -> Four2 :=
  (* Insert your definition. *)

Goal forall x : Four2, psi2 (phi2 x) = x.
  (* Insert your proof. *)

Goal forall x:Four3, phi2 (psi2 x) = x.
  (* Insert your proof. *)

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

(*
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" where b is a boolean expression 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.
*)