Library lex_sort


Require Import List.

Require Import ZArith.

Require Import quicksort.

Require Import strict_inc_and_dec.




Inductive lex_order (x : nat*nat) : (nat*nat) -> Prop :=

| lex_cons_eq : forall (y : nat*nat), 

                             fst x = fst y 

                        -> snd x <= snd y 

                        -> lex_order x y

| lex_cons_diff : forall (y : nat*nat),

                              fst x < fst y

                         -> lex_order x y.




Definition is_lex_sorted : list (nat*nat) -> Prop :=

is_sorted (nat*nat) lex_order.




Lemma lex_order_antisym :

                           forall (x y : (nat*nat)),

                           lex_order x y

                           -> lex_order y x

                           -> x = y.




Proof.

intros;destruct x;destruct y.

inversion H;inversion H0;simpl in *;intuition.

Qed.




Lemma lex_order_dec :

            forall (x y : nat*nat),{lex_order x y}+{~lex_order x y}.




Proof.

destruct x;destruct y;intros.

destruct (gt_eq_gt_dec n n1).

destruct s.

left;apply lex_cons_diff;assumption.

destruct (le_gt_dec n0 n2).

left;constructor;assumption.

right;unfold not;intro;inversion H;

simpl in *;intuition.

right;unfold not;intros;

inversion H;simpl in H0;intuition.

Qed.




Lemma lex_order_trans:

            forall (x y z : nat*nat),

            lex_order x y 

            -> lex_order y z 

            -> lex_order x z.




Proof.

induction 1;intro.

destruct (eq_nat_dec (fst x) (fst z)).

constructor;intuition.

inversion H1;intuition.

apply lex_cons_diff.

inversion H1;intuition.

apply lex_cons_diff.

inversion H0;intuition.

Qed.




Lemma lex_order_total :

            forall (x y : nat*nat),

            {lex_order x y}+{lex_order y x}.




Proof.

intros.

destruct x;destruct y.

destruct (gt_eq_gt_dec n n1).

destruct s.

left;apply lex_cons_diff;assumption.

destruct (le_gt_dec n0 n2).

left;constructor;assumption.

right;constructor;intuition.

right;apply lex_cons_diff;assumption.

Qed.




Lemma diff_proj : forall (x y : nat * nat),

      fst x <> fst y \/ snd x <> snd y -> x <> y.




Proof.

unfold not;intros;subst;intuition.

Qed.




Definition nat_nat_eq_dec (x y : nat*nat) : {x = y} + {x <> y} :=

match (eq_nat_dec (fst x) (fst y)) with

| left l =>match (eq_nat_dec (snd x) (snd y)) with

             | left l1 => left _ (injective_projections x y l l1)

             | right r1 => right _ (diff_proj x y (or_intror _ r1))

             end

| right r => right _ (diff_proj x y (or_introl _ r))

end.




Definition lex_sort (l : list (nat*nat)) : list (nat*nat) :=

               quicksort (nat*nat) lex_order lex_order_dec l.




Lemma is_lex_sorted_lex_sort :

            forall (l : list (nat*nat)), is_lex_sorted (lex_sort l).




Proof.

intros;unfold lex_sort;unfold is_lex_sorted;apply is_sorted_quicksort.

apply lex_order_trans.

apply lex_order_total.

Qed.




Lemma is_perm_lex_sort:

            forall (l : list (nat*nat)), Permutation l (lex_sort l).




Proof.

intros;unfold lex_sort;apply permutation_quicksort.

Qed.




Lemma is_lex_sorted_rmsnd : 

                forall (l : list (nat*nat)) (a b x y :nat), 

                     is_lex_sorted ((x,y) :: (a,b) :: l) 

                -> is_lex_sorted ((x,y) :: l).




Proof.

intros;unfold is_lex_sorted;eapply is_sorted_rmsnd.

intros;eapply lex_order_trans;eassumption.

eassumption.

Qed.




Lemma is_lex_sorted_tail :

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

                           is_lex_sorted (x :: l) 

                      -> is_lex_sorted l.




Proof.

intros; unfold is_lex_sorted in *;

eapply is_sorted_tail;eassumption.

Qed.




Lemma strict_sort_in : forall (l : list (nat*nat)) (a b x y : nat), 

                                      is_lex_sorted ((x,y) :: l) 

                                 -> In (a,b) l 

                                 -> x < a \/ (x = a /\ y <= b).




Proof.

induction l;intros;[|destruct a].




inversion H0.




simpl in H0;decompose [or] H0.

inversion H;inversion H1;inversion H4;subst;intuition.

apply IHl;[eapply is_lex_sorted_rmsnd | ];eassumption.

Qed.




Lemma NoDup_lex_sort_diff :

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

                 is_lex_sorted ((x,y) :: l)

            -> NoDup ((x,y) :: l)

            -> In (z,y) l

            -> x < z.




Proof.

induction l;[|destruct a];simpl;intros.

intuition.




decompose [or] H1.

inversion H;inversion H0;inversion H2;

destruct (eq_nat_dec x z);subst.

apply False_ind;intuition.

inversion H;inversion H6;intuition.

apply (IHl x y z);[eapply is_lex_sorted_rmsnd |
eapply NoDup_rmsnd |];eassumption.

Qed.




Lemma lex_sort_add_hd :

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

                 is_lex_sorted l

            -> (forall (a b : nat), 

                  In (a,b) l

                  -> x < a \/ (x = a /\ y <= b))

            -> is_lex_sorted ((x,y) :: l).




Proof.

unfold is_lex_sorted;intros;apply is_sorted_add_hd.

assumption.

destruct b;intros.

generalize (H0 n n0 H1);intro.

destruct (eq_nat_dec x n);decompose [or] H2;subst.

apply False_ind;intuition.

constructor;intuition.

apply lex_cons_diff;intuition.

constructor;intuition.

Qed.