(* Tutorial 9, 5/12/12 
   Questions for the exam
   previous exam
*)

Section ex5.

Require Import Coq.Arith.Plus.

Fixpoint double  (n : nat) {struct n} : nat :=
  match n with
  | 0 => 0
  | S m => S (S (double m))
  end.

(*
It provides the following lemmas:

Lemma plus_0_l : forall n, 0 + n = n.
Lemma plus_0_r : forall n, n + 0 = n.
Lemma plus_comm : forall n m, n + m = m + n.
Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.

*)


Lemma double_lem : forall n:nat, double n = n+n.
intro n.
induction n; simpl.
reflexivity.
rewrite IHn.
pattern (n + S n).
rewrite plus_comm.
simpl.
reflexivity.
Qed.

Goal forall (i j k:nat), i*(j+k) = i*j + i*k.
intro i.
induction i; simpl.
intros.
reflexivity.
intros j k.
rewrite IHi.
simpl.
rewrite -> plus_assoc.
pattern (j + k + i * j).
rewrite <- plus_assoc.
pattern (k + i * j).
rewrite plus_comm.
rewrite plus_assoc.
rewrite plus_assoc.
reflexivity.
Qed.










End ex5.

Section ex4. (* 20 points *)

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

Open Scope type_scope.
Implicit Arguments inl [A B].
Implicit Arguments inr [A B].


Definition Four1 := bool + bool.
Definition Four2 := bool * bool.

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

Definition psi1 : Four2 -> Four1 :=
  fun f2 => match f2 with
    | (true, true)   => inl true
    | (true, false)  => inl false
    | (false, true)  => inr true
    | (false, false) => inr false
  end.

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


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

Variables A B : Set.

Definition S := A * (A + B).
Definition T := B * A + A * A.

Definition phi : S -> T :=
  fun s => match s with
    | (a , inl a') => inr (a , a')
    | (a , inr b') => inl (b', a )
  end.

Definition psi : T -> S :=
  fun t => match t with
    | inl (b , a)  => (a , inr b)
    | inr (a , a') => (a , inl a')
  end.

Lemma inv : forall s : S, psi(phi s) = s.
intro s.
destruct s as [a ab].
destruct ab as [a' | b'].
simpl.
reflexivity.
simpl.
reflexivity.
Qed.

(** prove other direction *)










End ex4.