Library nat_quicksort


Require Import List.

Require Import ZArith.

Require Import quicksort.




Definition le_dec :

               forall (a b : nat),

               {a <= b}+{~a <= b}.




Proof.

intros;destruct (le_gt_dec a b);

[left | right];intuition.

Qed.




Definition nat_quicksort (l : list nat) : list nat :=

               quicksort nat le (le_dec) l.




Definition nat_elim_dup (l : list nat) : list nat :=

               elim_dup nat eq_nat_dec l.




Lemma in_nat_elim_dup :

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

           In x (nat_elim_dup l)

           -> In x l.




Proof.

unfold nat_elim_dup;intros;eapply in_elim_dup;eassumption.

Qed.




Lemma is_sorted_rmsnd :

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

                is_sorted nat le (x :: y :: l)

           -> is_sorted nat le (x :: l).




Proof.

intros;eapply is_sorted_rmsnd;

[intuition | eassumption].

Qed.




Lemma is_sorted_in :

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

                In x (a :: l)

           -> is_sorted nat le (a :: l)

           -> a <= x.




Proof.

intros;inversion H.

intuition.

eapply is_sorted_head_min;

[intuition | eassumption | assumption].

Qed.




Lemma NoDup_nat_elim_dup :

            forall (l : list nat),

                 is_sorted nat le l

            -> NoDup (nat_elim_dup l).




Proof.

intros;unfold nat_elim_dup;eapply NoDup_elim_dup;

[apply le_antisym|apply le_trans|assumption].

Qed.




Lemma in_nat_dup :

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

                In x l

           -> In x (nat_elim_dup l).




Proof.

unfold nat_elim_dup;intros;eapply in_dup;eassumption.

Qed.




Lemma is_sorted_elim_dup_aux :

            forall (l : list nat) (a : nat),

                 is_sorted nat le l

            -> (forall (x : nat),

                  In x l

                  -> a <= x)

            -> is_sorted nat le (a :: l).




Proof.

intros;apply is_sorted_add_hd;intuition.

Qed.




Lemma is_sorted_elim_dup :

            forall (l : list nat),

                 is_sorted nat le l

            -> is_sorted nat le (nat_elim_dup l).




Proof.

unfold nat_elim_dup;intros;apply sort_elim_dup;[intuition|assumption].

Qed.




Lemma lth_nat_elim_dup :

            forall (l : list nat),

            length (nat_elim_dup l) <= length l.




Proof.

induction l;intros.

intuition.




simpl;destruct l;[ | destruct (eq_nat_dec a n);simpl];intuition.

Qed.




Lemma lth_quicksort :

            forall (l : list nat),

            length (nat_quicksort l) = length l.




Proof.

intros.

apply Permutation_length.

apply Permutation_sym.

unfold nat_quicksort;apply permutation_quicksort.

Qed.




Lemma lth_0_nil : forall (A : Type) (l : list A),

            length l = 0 -> l = nil.




Proof.

induction l;intros.




reflexivity.




simpl in H;inversion H.

Qed.




Lemma NoDup_perm :

            forall (A : Type) (l l' : list A),

            Permutation l l'

            -> NoDup l

            -> NoDup l'.




Proof.

induction 1.

intuition.

intro;constructor;inversion H0.

unfold not in *;intro;apply H3.

apply Permutation_sym in H;eapply Permutation_in;eassumption.

intuition.

constructor.

inversion H.

unfold not in *;intro;apply H2.

simpl in H4;decompose [or] H4.

rewrite H5;intuition.

inversion H3;intuition.

constructor.

inversion H.

intuition.

inversion H;inversion H3;assumption.

intro.

apply (IHPermutation2 (IHPermutation1 H1)).

Qed.