Require Import ZArith List Psatz Arith Omega. Open Scope Z_scope. (* The following is used to generate a seemingly random list of integers *) Definition myrand (n : Z) := Zmod (n * 3853) 4919. Fixpoint iter_list (n : nat) (seed : Z) := match n with 0%nat => nil | S p => seed::iter_list p (myrand seed) end. Definition my_list := Eval vm_compute in iter_list 1000 32. Fixpoint take (n :nat) (l : list Z) := match n with | 0%nat => nil | S p => match l with nil => nil | a::tl => a::take p tl end end. Compute take 20 my_list. Fixpoint insert (z : Z) (l : list Z) := match l with | nil => z::nil | a::tl => if Z.leb z a then z::l else a::insert z tl end. Fixpoint sort (l : list Z) := match l with nil => nil | a::tl => insert a (sort tl) end. Time Compute sort my_list. Section merge_aux. Variable l1 : list Z. Variable f : list Z -> list Z. Fixpoint merge_aux (a : Z) (l2 : list Z) : list Z := match l2 with | b::l' => if b a::l1 end. End merge_aux. Fixpoint merge (l1 l2 : list Z) : list Z := match l1 with | a::l1' => merge_aux l1' (merge l1') a l2 | nil => l2 end. Lemma merge_step l1 l2 : merge l1 l2 = match l1, l2 with | a::l1', b::l2' => if b l1 | nil, l2 => l2 end. destruct l1 as [|a l1']. destruct l2; reflexivity. destruct l2 as [|b l2']. reflexivity. reflexivity. Qed. Inductive binZ := NZ : binZ -> binZ -> binZ | LZ : Z -> binZ. Fixpoint insert_in_binZ (a : Z) (t : binZ) := match t with | NZ t1 t2 => NZ t2 (insert_in_binZ a t1) | LZ b => NZ (LZ a) (LZ b) end. Fixpoint list_to_binZ (a : Z) (l : list Z) := match l with | nil => LZ a | b::tl => insert_in_binZ b (list_to_binZ a tl) end. Fixpoint sort_tree (t : binZ) := match t with LZ a => a::nil | NZ t1 t2 => merge (sort_tree t1) (sort_tree t2) end. Definition merge_sort (l : list Z) := match l with nil => nil | a::l' => sort_tree (list_to_binZ a l') end. Fixpoint count (x : Z) (l : list Z) : nat := match l with | nil => 0%nat | a::l' => if Zeq_bool x a then S (count x l') else count x l' end. Lemma count_step x l : count x l = match l with | nil => 0%nat | a::l' => if Zeq_bool x a then S (count x l') else count x l' end. Proof. destruct l; reflexivity. Qed. Fixpoint countb (x : Z) (t : binZ) : nat := match t with LZ a => if Zeq_bool x a then 1%nat else 0%nat | NZ t1 t2 => (countb x t1 + countb x t2)%nat end. Lemma insert_in_binZ_count x b t : countb x (insert_in_binZ b t) = ((if Zeq_bool x b then 1%nat else 0%nat) + countb x t)%nat. Proof. induction t. simpl. rewrite IHt1. ring. simpl. reflexivity. Qed. Lemma list_to_binZ_count x a l : count x (a::l) = countb x (list_to_binZ a l). Proof. induction l as [ | b tl IHl]. simpl. reflexivity. simpl. rewrite insert_in_binZ_count. rewrite <- IHl. simpl. case (Zeq_bool x a); case (Zeq_bool x b); simpl; ring. Qed. Lemma merge_preserves_count : forall x l1 l2, count x (merge l1 l2) = (count x l1 + count x l2)%nat. Proof. assert (main: forall x n l1 l2, (length l1 + length l2)%nat = n -> count x (merge l1 l2) = (count x l1 + count x l2)%nat). induction n. intros l1 l2 len. assert (l1nil : l1 = nil). destruct l1; auto. simpl in len. discriminate. assert (l2nil : l2 = nil). rewrite plus_comm in len. destruct l2; auto; simpl in len; discriminate. rewrite l1nil, l2nil; simpl. reflexivity. intros l1 l2. destruct l1 as [ | a l1']. rewrite merge_step; destruct l2 as [ | b l2']. intros; reflexivity. simpl; intros; ring. destruct l2 as [ | b l2']. rewrite merge_step; simpl; intros; ring. simpl length; intros len. rewrite merge_step. destruct (b