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

    Exercise 8
    published 19/11/09, deadline 26/11/09, 17:00 electronic submission

    Use
    $ cw submit ex08.v
    on one of the CS servers
    then look for the coursework ??? 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

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

Section ex08.

Section omegaHotel.

(* The following exercises are related to the lecture about the omega hotel. *)

Require Import Coq.Arith.Arith.

(* We define an isomorphism between nat and unit + nat. *)

Definition sn2n (sn : unit + nat) : nat
  := match sn with
     | inl tt => 0
     | inr n => S n
     end.

Definition n2sn (n : nat) : unit + nat
  := match n with
     | O => inl nat tt
     | S n' => inr unit n'
     end.

(* SHow that this is indeed an isomorphism. *)

Goal forall n:nat, sn2n (n2sn n) = n.
intro n.
case n; reflexivity.
Qed.

Goal forall sn:unit+nat,n2sn (sn2n sn) = sn.
intros sn.
case sn.
simpl.
intro u.
case u.
simpl.
reflexivity.
intro n.
simpl.
reflexivity.
Qed.

(* Define an isomorphism between nat and nat * nat as sketched in the lecture. *)

Fixpoint sum (n : nat) : nat
  := match n with
     | O => 0
     | S n' => n + sum n'
     end.

Fixpoint nn2n' (x y : nat) {struct x} : nat
  := match x with
     | O => sum y
     | S x' => S (nn2n' x' (S y))
     end.

Definition nn2n (xy : nat * nat) : nat
  := match xy with
     | (x,y) => nn2n' x y
     end.

Fixpoint n2nn (n : nat) : nat * nat 
  := match n with
     | O => (0,0)
     | S n' => match n2nn n' with
               | (x,O) => (0,S x)
               | (x,S y) => (S x, y)
               end
     end.

(* You are not required to prove that you have actually constructed an iso
   (but welcome to do so). However, test your definition with the cases below.
*)

Eval compute in (nn2n (n2nn 0)).
Eval compute in (nn2n (n2nn 5)).
Eval compute in (nn2n (n2nn 12)).
Eval compute in (nn2n (n2nn 20)).
Eval compute in (n2nn (nn2n (0,0))).
Eval compute in (n2nn (nn2n (3,0))).
Eval compute in (n2nn (nn2n (3,3))).
Eval compute in (n2nn (nn2n (0,3))).

End omegaHotel.

Section frev.

Require Import Coq.Lists.List.

Set Implicit Arguments.

(* the reverse function as introduced in the lecture: *)

Fixpoint snoc (A:Set)(l : list A) (a:A) {struct l} : list A:=
 match l with
   | nil => cons a nil
   | b::l => b::(snoc l a)
 end.

Fixpoint rev (A:Set)(l : list A) {struct l} : list A :=
  match l with
    | nil => nil
    | a::l => snoc (rev l) a
  end.

(* here is alternative implementation, called fast reverse.
   we first implement an auxilliary function which uses the 2nd
   argument as an 'accumulator':
*)

Fixpoint fastrev (A:Set)(l acc:list A) {struct l} : list A :=
  match l with
  | nil => acc
  | a::l' => fastrev l' (a::acc)
  end.

(* frev is defined by initializing the accumulator with nil. *)

Definition frev (A:Set)(l:list A) : list A := 
  fastrev l nil.

(* a quick test: *)

Eval compute in frev (1::2::3::nil).

Lemma snoc_app_lem : forall (A:Set)(l l':list A)(a:A), (snoc l a)++l' = l++(a::l').
induction l.
  reflexivity.
  intros.
  simpl.
  rewrite IHl.
  reflexivity.
Qed.

Lemma fastrev_lem : forall (A:Set)(l l':list A),fastrev l l' = rev l ++ l'.
induction l. 
  reflexivity.
  intros.
  simpl.
  eapply trans_eq.  
    apply IHl.
    rewrite <- snoc_app_lem.
    reflexivity.
Qed.

(* Our goal is to show that rev is doing the same as frev: *)

Lemma rev_lem : forall (A:Set)(l:list A), rev l = frev l.
intros.
unfold frev.
transitivity ((rev l)++nil).
  apply app_nil_end.
  symmetry.
  apply fastrev_lem.
Qed.

(* It is useful to establish some lemmas, e.g.
   forall (A:Set)(l l':list A),fastrev l l' = rev l ++ l'.
*)

End frev.