(** G52IFR Tutorial 6
    Nicolai Kraus, Nuo Li
    Lists (Nuo's version)
**)


Section Tutorial6.


Load Lists.
Set Implicit Arguments.
Implicit Arguments nil [A].
Infix "::" := cons (at level 60, right associativity).
Infix "++" := app (right associativity, at level 60).


(** The list reversal from the lecture is quite inefficient. 
Can you see why?
We want to define list reversal in an efficient way **)

(** fast reverse **)

(** append the first list in reverse order to the second list called accumulation list **)

Fixpoint frev_aux (A : Set) (l acc : list A) : list A :=
  match l with
  | nil => acc
  | a :: l' => frev_aux l' (a::acc)
  end.

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


(** 'frev' is doing the same as 'rev'. We want to prove that they are the same.

We need a lemma **)

Lemma frev_aux_lem : forall(A : Set)(l l' : list A), frev_aux l l' = rev l ++ l'.
intros A l.
induction l;simpl.
reflexivity.

intro l1.
rewrite IHl.
clear IHl.

generalize (rev l).
intro l0.
induction l0;
simpl.
reflexivity.

rewrite IHl0.
reflexivity.
Qed.

Lemma frev_rev : forall (A : Set) (l : list A), frev l = rev l.
unfold frev.
intros.
rewrite frev_aux_lem.
apply app_l_nil.
Qed.

(** frev twice returns the original **)
Lemma frevfrev : forall (A : Set)(l : list A), frev (frev l) = l.
intros.
rewrite frev_rev.
rewrite frev_rev.
apply revrev.
Qed.


(** Part2 Boolean lists and natural numbers *)

(** This is a definition from the coursework
It translates a boolean list into a natural number.
A boolean list is a number in binary representation. *)

Fixpoint bin2nat (bs : list bool) : nat := 
  match bs with
    | nil => 0
    | b::bs => (if b then 1 else 0) + 2*(bin2nat bs)
  end.


(** A function that normalizes binary numbers, it delets all
    the starting 'false' 

Do we still have at least one bin for each nat? *)

(** Be careful the normalize_aux function only applied to reversed bin **)

Fixpoint normalize_aux (bs : list bool) {struct bs} : list bool :=
  match bs with
    | false :: l  =>  normalize_aux l
    | _           =>  bs
  end.

(** Now we can normalize boolean lists *)

Definition normalize (bs : list bool) : list bool :=
  frev (normalize_aux (frev bs)).


(** Normalizing a binary number does not change its value *)
Lemma normalize_correct: 
  forall (bs : list bool), bin2nat bs = bin2nat (normalize bs).
intro bs.
unfold normalize.
rewrite frev_rev.
rewrite frev_rev.

pattern bs at 1.
rewrite <- (revrev bs).

generalize (rev bs).
clear bs.
intro l.
induction l; simpl.
reflexivity.

destruct a;
simpl.
reflexivity.
rewrite <- IHl.
clear IHl.

generalize (rev l).
intro bs.

induction bs; simpl.
reflexivity.
rewrite IHbs.
reflexivity.
Qed.



Fixpoint binPredForNormalized (bs : list bool) :=
  match bs with
    | true  :: l => false :: l
    | false :: l => true :: (binPredForNormalized l)
    | nil        => nil
  end.


Definition binPred (bs : list bool) :=
  normalize (binPredForNormalized (normalize bs)).


Eval compute in (binPred (true :: nil)).

Eval compute in (binPred (true :: true :: false :: true :: nil)).


Eval compute in (binPred (false :: false :: false :: true :: nil)).

End Tutorial6.