(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus and Nuo Li
    Tutorial 6 : lists **)

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?

     rev [1,2,3,4]
     rev [2,3,4]  ++  [1]
     rev [3,4]  ++ [2] ++ [1]
     rev ...

     [1,23,3,1,...,66] ++ [3] is an expensive calculation

We want to define list reversal in an efficient way **)

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

(**
Lemma frev_rev : forall (A : Set) (l : list A), frev l = rev l.
intros.
induction l.
reflexivity.
simpl.
unfold frev.
simpl.
unfold frev in IHl.

Problem: We don't know anything about frev_aux
*)


(** Sometimes, it is easier to prove a more general statement!
    Think about it: Usuall, we would expect that a special case
    is simpler than the general case. For example, it is easier
    to prove something for 0 then to prove it for all natural
    numbers. But if we have l'=nil in the following lemma,
    it is a special case and the same as frev_rev. Still, it is
    easier!
*)

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

simpl.
intro.
rewrite IHl.

clear IHl.

generalize (rev l) as rl.
intro rl.

induction rl.
simpl.
reflexivity.
simpl.
rewrite IHrl.
reflexivity.
Qed.


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


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



(** 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'. Why do we need an auxiliary function? *)

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 *)
(** This was not for the tutorial, but you can have a look at it,
    if you are interested *)
Lemma normalize_correct: 
  forall (bs : list bool), bin2nat bs = bin2nat (normalize bs).
intros.
unfold normalize.
repeat rewrite frev_rev.

pattern bs at 1.
rewrite <- revrev.

generalize (rev bs).
intro l.

induction l; simpl.
reflexivity.

destruct a; simpl.
reflexivity.

rewrite <- IHl.
clear IHl.

generalize (rev l).
clear bs.
intro bs.

induction bs; simpl.
reflexivity.
destruct a; simpl.
rewrite IHbs.
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)).


End Tutorial6.