Library quicksort


Require Import List.

Require Import Recdef.

Require Import Omega.




Chapter QuickSort.




Variable A : Type.

Variable A_eq_dec : forall a b : A, {a = b}+{~a = b}.

Variable Order : A -> A -> Prop.

Hypothesis order_antisym : forall a b : A, Order a b -> Order b a -> a = b.

Hypothesis order_trans : forall a b c : A, Order a b -> Order b c -> Order a c.

Hypothesis order_dec : forall x y : A, {Order x y}+{~Order x y}.

Hypothesis order_total : forall a b : A, {Order a b}+{Order b a}.




Lemma order_refl :

            forall (a : A), Order a a.




Proof.

intro;assert ({Order a a}+{Order a a}).

apply order_total.

destruct H;assumption.

Qed.




Lemma not_order_order : 

            forall a b : A,  ~Order a b -> Order b a.




Proof.

intros;destruct (order_total a b);[absurd(Order a b) | ];assumption.

Qed.




Fixpoint partition (p : A) (l : list A) {struct l}: (list A)*(list A) :=

match l with

| nil => (nil,nil)

| h :: t => let (less,more) := partition p t in

  match order_dec h p with

  | left _ => (h :: less, more)

  | right _ => (less, h :: more)

  end

end.




Functional Scheme partition_ind := Induction for partition Sort Prop.




Lemma partition_le : 

            forall (l : list A) (p : A) (x : A), In x (fst(partition p l)) -> (Order x p).




Proof.

  intros l p.

  functional induction partition p l;simpl;intros.

  intuition.

  decompose [or] H; [rewrite <- H0 | apply IHp0; rewrite e0];

  assumption.

  apply IHp0; rewrite e0; assumption.

Qed.




Lemma partition_gt : 

           forall (l : list A) (p : A) (x : A), In x (snd(partition p l)) -> (~Order x p).




Proof.

  intros l p.

  functional induction partition p l;simpl;intros.

  intuition.

  apply IHp0;rewrite e0;assumption.

  decompose [or] H;[rewrite <- H0 | apply IHp0; rewrite e0];

  assumption.

Qed.




Lemma partition_length_l : 

            forall (l : list A) (p : A), length (fst(partition p l)) <= length l.




Proof.

intros;functional induction partition p l;

auto;  try auto; simpl; rewrite e0 in IHp0;

  [ apply le_n_S | apply lt_le_weak; apply le_lt_n_Sm ];

  assumption.

Qed.




Lemma partition_length_r : 

            forall (l : list A) (p : A), length (snd(partition p l)) <= length l.




Proof.

intros;functional induction partition p l;

  try auto; simpl; rewrite e0 in IHp0;

  [ apply lt_le_weak; apply le_lt_n_Sm | apply le_n_S ];

  assumption.

Qed.




Lemma permutation_partition: 

            forall (l : list A) (p : A), Permutation l (fst(partition p l)++snd(partition p l)).




Proof.

intros;functional induction partition p l;

simpl; try rewrite e0 in IHp0;

first [constructor | apply Permutation_cons_app];

assumption.

Qed.




Inductive is_sorted : list A -> Prop :=

| is_sorted_nil : is_sorted nil

| is_sorted_singleton : forall x : A, is_sorted (x :: nil)

| is_sorted_cons: forall (l : list A) (x y : A),

                    (Order x y) -> is_sorted (y :: l) -> is_sorted (x :: y :: l).




Lemma is_sorted_add_hd : forall (l : list A) (a : A),

                is_sorted l -> 

                (forall b : A, 

                In b l -> (Order a b)) 

                -> is_sorted (a :: l).




Proof.

induction l;intros.

constructor.

apply is_sorted_cons;[apply H0|];intuition.

Qed.




Lemma is_sorted_tail : 

            forall (l : list A) (a : A), is_sorted (a :: l) -> is_sorted l.




Proof.

induction l; intros;

[constructor | inversion H; assumption ].

Qed.




Lemma is_sorted_head_min : 

                         forall (l : list A) (a : A), is_sorted(a :: l) 

                         -> (forall b : A, In b l -> (Order a b)).




Proof.

induction l;intros.

inversion H0.




simpl in H0;decompose [or] H0;inversion H.

subst;assumption.

eapply order_trans;[eassumption|apply IHl;intuition].

Qed.




Lemma is_sorted_cat : 

            forall (l l':list A), is_sorted l -> is_sorted l' ->

                                    (forall (x y: A), In x l -> In y l' ->

                                    (Order x y)) -> is_sorted (l ++ l').




Proof.

induction l;intros.

assumption.

simpl; apply is_sorted_add_hd.

apply IHl.

eapply is_sorted_tail; eassumption.

assumption.

intros;apply H1;intuition.




intros;assert (In b l \/ In b l').

apply in_app_or; assumption.

decompose [or] H3.

apply (is_sorted_head_min l); assumption.

apply H1; [ simpl; left; reflexivity | assumption ].

Qed.




Lemma is_sorted_rmsnd : 

            forall (l : list A) (x y : A),

            is_sorted (x :: y :: l)

            -> is_sorted (x :: l).




Proof.

intros;inversion H;inversion H4;

subst;constructor.

eapply order_trans;eassumption.

assumption.

Qed.




Lemma NoDup_rmsnd :

            forall (l : list A) (x y : A),

            NoDup (x :: y :: l)

            -> NoDup (x :: l).




Proof.

intros;constructor;inversion H;inversion H3;intuition.

Qed.




Function quicksort (l : list A) {measure length l}: list A :=

match l with

          | nil => nil

          | h::t => let (less,more) := partition h t in

                        quicksort(less) ++ h::quicksort(more)

end.




Proof.

intros; replace (more) with (snd(partition h t));

[ simpl; apply le_lt_n_Sm; apply partition_length_r
| rewrite teq0 ; reflexivity ].

intros; replace less with (fst(partition h t));

[ simpl; apply le_lt_n_Sm; apply partition_length_l
| rewrite teq0; reflexivity ].

Qed.




Theorem permutation_quicksort: 

                forall l:list A,

                Permutation l (quicksort l).




Proof.

intro;functional induction (quicksort l).

constructor.

apply Permutation_cons_app.

eapply Permutation_trans.

apply permutation_partition.

instantiate (1:=h).

rewrite e0; simpl.

apply Permutation_app; assumption.

Qed.




Lemma quicksort_in : 

                forall (l : list A) (a : A), In a (quicksort l) -> In a l.




Proof.

intros;eapply Permutation_in;

[ apply Permutation_sym; apply permutation_quicksort 
| assumption ].

Qed.




Theorem is_sorted_quicksort: forall l:list A, is_sorted(quicksort l).

Proof.

intro;functional induction quicksort l.

constructor.

apply is_sorted_cat.

assumption.

apply is_sorted_add_hd.

assumption.

intros;apply not_order_order.

apply partition_gt with (l:=t).

rewrite e0;apply quicksort_in;assumption.




intros;cut (Order x h /\ Order h y).

intro.

decompose [and] H1.

eapply order_trans; eassumption.

split.

apply (partition_le t);rewrite e0;

apply quicksort_in;assumption.




simpl in H0;decompose [or] H0.

rewrite H1;apply order_refl.

assert (In y more).

apply quicksort_in;assumption.




apply not_order_order.

apply partition_gt with (l:=t).

rewrite e0;assumption.

Qed.




Fixpoint elim_dup (l : list A) {struct l}: list A :=

match l with

  nil => nil

| x :: l' => match l' with

        | nil => l

        | y :: l'' => match (A_eq_dec x y) with

                        |left _ => elim_dup l'

                        |right _ => x :: elim_dup l'

                        end

        end

end.




Lemma in_elim_dup_aux :

           forall (l : list A) (a x : A),

                In x (elim_dup (a :: l))

           -> a <> x

           -> In x (elim_dup l).




Proof.

intros.

simpl in H;decompose[or] H;intuition.

destruct l;[|destruct (A_eq_dec a a0);[assumption|]];

simpl in H;decompose[or] H;intuition.

Qed.




Lemma in_elim_dup : forall (l : list A) (x : A),

                                     In x (elim_dup l)

                                -> In x l.




Proof.

induction l;intros;simpl.

inversion H.




destruct (A_eq_dec a x).

left;assumption.

right;apply IHl;eapply in_elim_dup_aux;eassumption.

Qed.




Lemma in_dup_aux :

            forall (l : list A) (x : A),

            In x (elim_dup (x :: l)).




Proof.

induction l;intros;simpl.

intuition.




destruct (A_eq_dec x a).

rewrite e;apply IHl.

intuition.

Qed.




Lemma in_dup :

            forall (l : list A) (x : A),

                 In x l

            -> In x (elim_dup l).




Proof.

induction l;intros.

assumption.

simpl in H;decompose [or] H.

subst;apply in_dup_aux.

simpl;destruct l.

inversion H0.

destruct (A_eq_dec a a0).

apply IHl;assumption.

simpl;right;apply IHl;assumption.

Qed.




Lemma NoDup_elim_dup : forall (l : list A),

                                             is_sorted l

                                        -> NoDup (elim_dup l).




Proof.

induction l;intros.

simpl;constructor.




simpl;destruct l.

constructor;[intuition | constructor].

destruct (A_eq_dec a a0).

apply IHl.

eapply is_sorted_tail;eassumption.

constructor.

unfold not;intro.

assert (In a (a0 :: l)).

apply in_elim_dup;assumption.

simpl in H1;decompose[or]H1.

subst;intuition.

inversion H;subst.

assert (a = a0).

apply order_antisym.

assumption.

eapply is_sorted_head_min;eassumption.

subst;intuition.

apply IHl;inversion H;assumption.

Qed.




Lemma sort_elim_dup :

            forall (l : list A),

                 is_sorted l

            -> is_sorted (elim_dup l).




Proof.

induction l;intros.

assumption.




simpl;destruct l.

assumption.




destruct (A_eq_dec a a0).

apply IHl;eapply is_sorted_tail;eassumption.




apply is_sorted_add_hd.

apply IHl;eapply is_sorted_tail;eassumption.

intros;eapply is_sorted_head_min.

eassumption.

apply in_elim_dup;assumption.

Qed.




End QuickSort.