(** 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 236 labelled 'g52mc2 coursework 8' 
    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.
(* insert yor proof here. *)

Goal forall sn:unit+nat,n2sn (sn2n sn) = sn.
(* insert your proof here. *)

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

Fixpoint nn2n (xy : nat * nat) : nat
(* insert your definition here. *)

Fixpoint n2nn (n : nat) : nat * nat 
(* insert your definition here. *)

(* Hint: It is allowed and indeed useful to define some auxilliary functions. *)

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

(* This part of the exercise involves reasoning about lists. 
   We are going to show that an alternative implementation of reverse (fast reverse)
   is equivalent to reverse. 
*)

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

(* 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.
(* Insert you r proof here. *)

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

End frev.