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