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