# Library list_extensions.list_sort

``` Add LoadPath "basis". Set Implicit Arguments. Require Import Relations. Require Import List. Require Import more_list. Require Import Multiset. Require Import list_permut. Require Import Arith. Require Import ordered_set. Require Import Recdef. Module Type Sort. Declare Module Import DOS : ordered_set.S. Declare Module Import LPermut :   list_permut.S with Definition EDS.A := DOS.A                       with Definition EDS.eq_A := @eq DOS.A. ```

### Decomposition of the list wrt a pivot.

``` Function partition (pivot : A) (l : list A) {struct l} : (list A) * (list A) :=   match l with   | nil => (nil, nil)   | a :: l' =>         match partition pivot l' with (l1,l2) =>          if ((o_dec a pivot) : sumbool _ _) then (a :: l1, l2) else (l1, a :: l2)         end end. Parameter quicksort : list A -> list A. Function remove_list (la l : list A) {struct l} : option (list A) :=   match la with   | nil => Some l   | a :: la' =>         match l with         | nil => None         | b :: l' =>            if (eq_dec a b : sumbool _ _)            then remove_list la' l'            else              match remove_list la l' with              | None => None              | Some rmv => Some (b :: rmv)              end         end   end. ```

### Definition of a sorted list.

``` Inductive is_sorted : list A -> Prop :=   | is_sorted_nil : is_sorted nil   | is_sorted_cons1 : forall t, is_sorted (t :: nil)   | is_sorted_cons2 :       forall t1 t2 l, o t1 t2 -> is_sorted (t2 :: l) -> is_sorted (t1 :: t2 :: l). Hint Constructors is_sorted. Axiom in_remove_list :   forall l la, is_sorted la -> is_sorted l ->   match remove_list la l with   | None => forall rmv, ~ (permut (la ++ rmv) l)   | Some rmv => permut (la ++ rmv) l   end. Axiom quicksort_equation : forall l : list A,        quicksort l =        match l with        | nil => nil (A:=A)        | h :: tl =>            let (l1, l2) := partition h tl in            quicksort l1 ++ h :: quicksort l2        end. Axiom quick_permut : forall l, permut l (quicksort l). Axiom quick_permut_bis :  forall l1 l2, permut l1 l2 -> permut (quicksort l1) l2. Axiom length_quicksort : forall l, length (quicksort l) = length l. Axiom in_quick_in : forall a l, In a l <-> In a (quicksort l). Axiom sorted_tl_sorted : forall e l, is_sorted (e :: l) -> is_sorted l. Axiom quick_sorted : forall l, is_sorted (quicksort l). Axiom sort_is_unique :   forall l1 l2, is_sorted l1 -> is_sorted l2 -> permut l1 l2 -> l1 = l2. End Sort. ```

## Definition of quicksort over lists.

``` Module Make (DOS1 : ordered_set.S) <: Sort with Module DOS := DOS1. Module Import DOS := DOS1. Module EDS := decidable_set.Convert(DOS1). Module Import LPermut <:   list_permut.S with Definition EDS.A := DOS.A                       with Definition EDS.eq_A := @eq DOS.A := list_permut.Make EDS.   Add Morphism mem         with signature (@eq A) ==> permut ==> iff         as mem_morph.    Proof.     intros.    apply mem_permut_mem; trivial.   Qed.   Add Morphism (List.cons (A:=A))         with signature (@eq A) ==> permut ==> permut         as add_A_morph.   Proof.     intros e l1 l2 P; setoid_rewrite <- permut_cons; trivial.     reflexivity.   Qed. Add Morphism (length (A:=A))         with signature permut ==> (@eq nat)         as length_morph. Proof. apply permut_length. Qed. ```

### Decomposition of the list wrt a pivot.

``` Function partition (pivot : A) (l : list A) {struct l} : (list A) * (list A) :=   match l with   | nil => (nil, nil)   | a :: l' =>         match partition pivot l' with (l1,l2) =>          if ((o_dec a pivot) : sumbool _ _) then (a :: l1, l2) else (l1, a :: l2)         end end. Function quicksort (l : list A) { measure (@length A) l} : list A :=    match l with         | nil => nil         | h :: tl =>              match partition h tl with (l1, l2) =>              quicksort l1 ++ h :: quicksort l2         end     end. Proof. intros e_l e l e_l_eq_e_l; subst e_l; functional induction (partition e l)    as [ | H1 e' l' H2 IH l1 l2 rec_res e'_lt_e _ | H1 e' l' H2 IH l1 l2 rec_res H3 H4]; intros ll1 ll2 Hpart; injection Hpart; intros H H'; subst. simpl; auto with arith. apply lt_trans with (length (e :: l')); [apply (IH _ _ rec_res) | auto with arith]. simpl; apply lt_n_S; apply (IH _ _ rec_res). intros e_l e l e_l_eq_e_l; subst e_l; functional induction (partition e l)    as [ | H1 e' l' H2 IH l1 l2 rec_res e'_lt_e _ | H1 e' l' H2 IH l1 l2 rec_res H3 H4]; intros ll1 ll2 Hpart; injection Hpart; intros H H'; subst. simpl; auto with arith. simpl; apply lt_n_S; apply (IH _ _ rec_res). apply lt_trans with (length (e :: l')); [apply (IH _ _ rec_res) | auto with arith]. Defined. ```

### The result of quicksort is a permutation of the original list.

``` Lemma partition_list_permut1 :  forall e l, let (l1,l2) := partition e l in permut (l1 ++ l2) l. Proof. intros e l; functional induction (partition e l)    as [ | H1 e' l' H2 IH l1 l2 rec_res e'_lt_e _ | H1 e' l' H2 IH l1 l2 rec_res H3]. auto. simpl app; rewrite rec_res in IH; setoid_rewrite IH; auto. simpl app; rewrite rec_res in IH; apply permut_sym; setoid_rewrite <- permut_cons_inside; auto. reflexivity. Qed. Theorem quick_permut : forall l, permut l (quicksort l). Proof. intros l; functional induction (quicksort l)    as [ | l a' l' l_eq_a'_l' l1 l2 H S1 S2]; auto. setoid_rewrite <- permut_cons_inside. reflexivity. assert (P := partition_list_permut1 a' l'); rewrite H in P. setoid_rewrite <- P; setoid_rewrite <- S1; setoid_rewrite <- S2; auto. Qed. Theorem quick_permut_bis :  forall l1 l2, permut l1 l2 -> permut (quicksort l1) l2. Proof. intros l1 l2 P; apply permut_trans with l1; trivial; apply permut_sym; apply quick_permut. Qed. ```

### Definition of a sorted list.

``` Inductive is_sorted : list A -> Prop :=   | is_sorted_nil : is_sorted nil   | is_sorted_cons1 : forall t, is_sorted (t :: nil)   | is_sorted_cons2 :       forall t1 t2 l, o t1 t2 -> is_sorted (t2 :: l) -> is_sorted (t1 :: t2 :: l). Hint Constructors is_sorted. ```

### The result of quicksort is a sorted list.

``` Lemma sorted_tl_sorted :   forall e l, is_sorted (e :: l) -> is_sorted l. Proof. intros e l S; inversion S; auto. Qed. Lemma quick_sorted_aux1 :   forall l1 l2 e, is_sorted l1 -> is_sorted l2 ->   (forall a, mem a l1 -> o a e) ->   (forall a, mem a l2 -> o e a) ->   is_sorted (l1 ++ e :: l2). Proof. induction l1 as [ | e1 l1 ]; intros l2 e S1 S2 L1 L2. simpl; destruct l2 as [ | e2 l2]; intros; [apply is_sorted_cons1 | apply is_sorted_cons2 ]; trivial; apply (L2 e2); simpl; left; reflexivity. destruct l1 as [ | e1' l1] ; simpl; intros; apply is_sorted_cons2. apply L1; left; reflexivity. simpl in IHl1; apply IHl1; trivial; contradiction. inversion S1; trivial. rewrite app_comm_cons; apply IHl1; trivial. inversion S1; trivial. intros; apply L1; trivial; right; trivial. Qed. Lemma quick_sorted_aux3 :   forall l e, let (l1,_) := partition e l in forall a, mem a l1 -> o a e. Proof. intros l e; functional induction (partition e l)     as [ | l a' l' l_eq_a'_l' IH l1' l2' H a'_lt_e _ | l a' l' l_eq_a'_l' IH l1' l2' H _H _ ]. contradiction. intros a [a_eq_a' | a_in_l1']; [subst | rewrite H in IH; apply IH]; trivial. unfold EDS.eq_A, Make.EDS.eq_A in a_eq_a'; subst; trivial. intros; rewrite H in IH; apply IH; trivial. Qed. Lemma quick_sorted_aux4 :   forall l e, let (_,l2) := partition e l in forall a, mem a l2 -> o e a. Proof. intros l e; functional induction (partition e l)     as [ | l a' l' l_eq_a'_l' IH l1' l2' H a'_lt_e _ | l a' l' l_eq_a'_l' IH l1' l2' H a'_ge_e _ ]. contradiction. intros; rewrite H in IH; apply IH; trivial. intros a [a_eq_a' | a_in_l1']; [subst | rewrite H in IH; apply IH]; trivial. unfold EDS.eq_A, Make.EDS.eq_A in a_eq_a'; subst; trivial. destruct (o_total e a'); trivial; absurd (o a' e); trivial. Qed. Theorem quick_sorted : forall l, is_sorted (quicksort l). Proof. intros l; functional induction (quicksort l)    as [ | l a' l' l_eq_a'_l' l1 l2 H S1 S2]. auto. apply quick_sorted_aux1; trivial. intros a a_in_ql1; assert (H1 := quick_sorted_aux3 l' a'); rewrite H in H1; apply H1. setoid_rewrite (mem_permut_mem a (quick_permut l1)); trivial. intros a a_in_ql2; assert (H2 := quick_sorted_aux4 l' a'); rewrite H in H2; apply H2; setoid_rewrite (mem_permut_mem a (quick_permut l2)); trivial. Qed. ```

### There is a unique sorted list equivalent up to a permutation to a given list.

``` Lemma sorted_cons_min :  forall l e, is_sorted (e :: l) -> (forall e', mem e' (e :: l) -> o e e'). Proof. intros l e S e' In_e'; elim In_e'; clear In_e'; intro In_e'. unfold EDS.eq_A, Make.EDS.eq_A in In_e'; subst; trivial. generalize o_proof; intro O; inversion O as [R _ _]; apply R. generalize e S e' In_e'; clear e S e' In_e'; induction l as [ | a l ]; intros e S e' In_e'; inversion S; elim In_e'; clear In_e'; intro In_e'; unfold EDS.eq_A, Make.EDS.eq_A in In_e'; subst; trivial. generalize o_proof; intro O; inversion O as [ _ T _ ]; apply T with a; trivial; apply IHl; trivial. Qed. Theorem sort_is_unique :   forall l1 l2, is_sorted l1 -> is_sorted l2 -> permut l1 l2 -> l1 = l2. Proof. induction l1 as [ | e1 l1 ]; intros l2 S1 S2 P. inversion P; trivial. inversion P as [ | a b l k1 k2 a_eq_b P' H1 H']; subst. destruct k1 as [ | a1 k1]. rewrite (IHl1 k2); trivial. unfold EDS.eq_A, Make.EDS.eq_A in a_eq_b; subst; trivial. inversion S1; trivial. inversion S2; trivial. assert (e1_eq_a1 : e1 = a1). assert (O:= o_proof); inversion O as [ _ _ AS ]; apply AS; clear O AS. apply (sorted_cons_min S1); setoid_rewrite P; left; reflexivity. apply (sorted_cons_min S2); setoid_rewrite <- P; left; reflexivity. subst; rewrite (IHl1 (k1 ++ b :: k2)); trivial. apply sorted_tl_sorted with a1; trivial. apply sorted_tl_sorted with a1; trivial. simpl in P; setoid_rewrite <- permut_cons in P; trivial. reflexivity. Qed. ```
Some usefull properties on the result of quicksort.
``` Lemma length_quicksort : forall l, length (quicksort l) = length l. Proof. intro l; apply permut_length with EDS.eq_A; apply permut_sym; apply quick_permut. Qed. Lemma in_quick_in : forall a l, In a l <-> In a (quicksort l). Proof. intros a l; apply in_permut_in. apply quick_permut. Qed. Lemma in_quicksort_cons : forall a l, In a (quicksort (a :: l)). Proof. intros a l; setoid_rewrite <- in_quick_in; left; trivial. Qed. ```
What happens when a sorted list is removed from another one.
``` Function remove_list (la l : list A) {struct l} : option (list A) :=   match la with   | nil => Some l   | a :: la' =>         match l with         | nil => None         | b :: l' =>            if (eq_dec a b : sumbool _ _)            then remove_list la' l'            else              match remove_list la l' with              | None => None              | Some rmv => Some (b :: rmv)              end         end   end. Lemma in_remove_list :   forall l la, is_sorted la -> is_sorted l ->   match remove_list la l with   | None => forall rmv, ~ (permut (la ++ rmv) l)   | Some rmv => permut (la ++ rmv) l   end. Proof. intros l la Sa S; functional induction (remove_list la l)    as [ (* Case 1 *) | (* Case 2 *) la l a' la' H1 H2 | (* Case 3 *) la l a' la' H1 e' l' H2 H3 _ IH | (* Case 4 *) la l a' la' H1 e' l' H2 a'_diff_e' _H IH H | (* Case 5 *) la l a' la' H1 e' l' H2 a'_diff_e' _H IH rmv H]. auto. intros rmv P; assert (H := permut_length P); discriminate. destruct (remove_list la' l') as [rmv | ]. simpl; setoid_rewrite <- permut_cons. reflexivity. apply IH; apply sorted_tl_sorted with a'; trivial. intros rmv P; refine (IH _ _ rmv _); [ apply sorted_tl_sorted with a' | apply sorted_tl_sorted with a' | simpl in P; setoid_rewrite <- permut_cons in P]; trivial. reflexivity. rewrite H in IH. intros rmv P; assert (H' : mem e' ((a' :: la') ++rmv)). setoid_rewrite P; left; reflexivity. simpl in H'; destruct H' as [e'_eq_a' | H']. apply a'_diff_e'; unfold EDS.eq_A, Make.EDS.eq_A in e'_eq_a'; subst; trivial. setoid_rewrite <- mem_or_app in H'. destruct H' as [e'_in_la' | e'_in_rmv]. apply a'_diff_e'; assert (O := o_proof); inversion_clear O as [ _ _ AS]; apply AS. apply sorted_cons_min with la'; [apply Sa | right; trivial]. apply sorted_cons_min with l'; [apply S | setoid_rewrite <- P; left; reflexivity]. destruct (mem_split_set _ _ e'_in_rmv) as [e'' [l1 [l2 [e'_eq_e'' H'']]]]; simpl in e'_eq_e''; simpl in H'';subst rmv. refine (IH _ _ (l1 ++ l2) _). trivial. apply sorted_tl_sorted with e'; trivial. apply permut_sym. rewrite ass_app. setoid_rewrite (@permut_cons_inside e' e''); trivial. apply permut_sym; rewrite <- ass_app; auto. rewrite H in IH. apply permut_sym; setoid_rewrite <- permut_cons_inside. reflexivity. setoid_rewrite <- IH; subst; auto; apply sorted_tl_sorted with e'; trivial. Qed. End Make. ```