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







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


Lemma frev_rev : forall (A : Set) (l : list A), frev l = rev l.


Lemma frevfrev : forall (A : Set)(l : list A), frev (frev l) = l.



(** 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 :=



(** Now we can normalize boolean lists *)

Definition normalize (bs : list bool) : list bool :=



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



Fixpoint binPredForNormalized (bs : list bool) :=


Definition binPred (bs : list bool) :=



End Tutorial6.