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