(** Introduction to Formal Reasoning (G52IFR) Thorsten Altenkirch Exercise 5 (Lists) published 14/11/11, deadline 22/11/11, 18:00 electronic submission Use \$ cw submit ex05.v on one of the CS servers then look for the coursework 432 labelled 'g52cfr coursework 5' and enter the associated code. Multiple submissions are allowed, up to the deadline. Try to fill in the missing proofs, using only the basic tactics presented in the lectures. Do not use any additional libraries. **) Section Ex05. (** We are using all the results from the lecture. *) Load Lists. Set Implicit Arguments. Implicit Arguments nil [A]. Infix "::" := cons (at level 60, right associativity). Infix "++" := app (right associativity, at level 60). (** 1 **) Section Frev. (* The naive implementation of reverse is quite inefficient because the list is traversed many times (so indeed it has a quadratic complexity). The following (fast) implementation of reverse is better and has only linear complexity. It uses an axilliary function which accumulates the result in a 2nd parameter which is returned when the end of the list is reached. Your task is to show that the fast implementation does the same as the original one. This will require to prove some lemmas. Hint: frev_aux satisfies the following property: frev_aux l l' = rev l ++ l' *) Fixpoint frev_aux (A : Set)(l acc : list A) : list A := match l with | nil => acc | a :: l' => frev_aux l' (a::acc) end. (* frev is defined by initializing the accumulator with nil. *) Definition frev (A:Set)(l:list A) : list A := frev_aux l nil. (* a quick test: *) Eval compute in frev_aux (1::2::3::nil). (* Our goal is to show that frev is doing the same as rev: *) Lemma rev_lem : forall (A:Set)(l:list A), rev l = frev l. End Frev. (** 2 **) Section perm. (* We say that a list is a permutation of another list if one list can be obtained from the other by rearranging the elements. One way to specify this is to say is using a function which counts occurences and then a list is a permutation if the number of all elements is the same. *) Fixpoint count (n:nat)(ms:list nat) {struct ms} : nat := match ms with | nil => 0 | m::ms' => let cn := count n ms' in if eqnat n m then S cn else cn end. Definition Perm (ns ms:list nat) := forall n:nat,count n ns=count n ms. (* The first task is to show that Perm is an equivalence relation, i.e. that it is reflexive, symmetric and transitive. *) Lemma refl_perm : forall ns:list nat,Perm ns ns. Lemma trans_perm : forall ls ms ns:list nat,Perm ls ms -> Perm ms ns -> Perm ls ns. Lemma sym_perm : forall ms ns : list nat, Perm ms ns -> Perm ns ms. (* Show that rev produces a permutation of the input list. This will require a lemma about snoc. *) Theorem rev_perm : forall (ns:list nat),Perm ns (rev ns). (* Show that the sort function produces a permutation of the input list. This will require a lemma about insert and maybe more. *) Theorem sort_perm : forall ms:list nat,Perm ms (sort ms). End perm. End Ex05.