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.