Library strict_ord


Require Import List.

Require Import ZArith.

Require Import quicksort.

Require Import strict_inc_and_dec.

Require Import lex_sort.




Fixpoint order (l : list (nat*nat)) {struct l}: list (nat*nat) :=

match l with

| nil => nil

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

                      | inleft (left _) => (x,y) :: (order l')

                      | inleft (right _) => order l'

                      | inright _ => (y,x) :: (order l')

                      end

end.







Inductive is_strict_ord : list (nat*nat) -> Prop :=

  is_strict_ord_nil : is_strict_ord nil

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

                                    x < y 

                               -> is_strict_ord l

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




Lemma strict_ord_order :

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

            is_strict_ord (order l).




Proof.

induction l;intros.

simpl;constructor.




destruct a;simpl.

destruct (gt_eq_gt_dec n n0);[destruct s|];try constructor;assumption.

Qed.




Lemma only_in_order :

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

                     In (x,y) (order l)

                -> In (x,y) l \/ In (y,x) l.




Proof.

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




inversion H.




simpl in H;destruct (gt_eq_gt_dec n n0).

destruct s.

simpl in H;decompose [or] H.

intuition.

assert (In (x,y) l \/ In (y,x) l).

apply IHl;assumption.

intuition.

assert (In (x,y) l \/ In (y,x) l).

apply IHl;assumption.

intuition.

simpl in H;decompose [or]H.

inversion H0;intuition.

assert (In (x,y) l \/ In (y,x) l).

apply IHl;assumption.

intuition.

Qed.




Lemma all_in_order:

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

                 In (x,y) l 

            -> x <> y

            -> In (x,y) (order l) \/ In (y,x) (order l).




Proof.

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




inversion H.




destruct (gt_eq_gt_dec n n0).

destruct s.

simpl in H;decompose [or]H.

inversion H1;intuition.

assert (In (x,y) (order l) \/ In (y,x) (order l)).

apply IHl;assumption.

intuition.

simpl in H;decompose [or] H.

apply False_ind;inversion H1;intuition.

apply IHl;assumption.

simpl in H;decompose [or] H.

inversion H1;intuition.

assert (In (x,y) (order l) \/ In (y,x) (order l)).

apply IHl;assumption.

intuition.

Qed.




Lemma strict_in : 

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

                is_strict_ord l 

           -> In (x,y) l 

           -> x < y.




Proof.

induction l;intros;[|destruct a];inversion H0;

inversion H;[inversion H1|apply IHl];intuition.

Qed.




Lemma strict_ord_lex_aux :

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

                 Permutation l l'

            -> is_strict_ord l

            -> is_strict_ord l'.




Proof.

induction 1;intro.

constructor.

destruct x.

constructor.

inversion H0;assumption.

apply IHPermutation;inversion H0;assumption.

destruct x;destruct y.

constructor.

inversion H;inversion H4;assumption.

constructor.

inversion H;assumption.

inversion H;inversion H4;assumption.

apply (IHPermutation2 (IHPermutation1 H1)).

Qed.




Lemma strict_ord_lex :

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

                 is_strict_ord l

            -> is_strict_ord (lex_sort l).




Proof.

intro;apply strict_ord_lex_aux;apply is_perm_lex_sort.

Qed.




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

elim_dup (nat*nat) (nat_nat_eq_dec) l.




Lemma in_nat_nat_elim_dup_aux :

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

                In x (nat_nat_elim_dup (a :: l))

           -> a <> x

           -> In x (nat_nat_elim_dup l).




Proof.

unfold nat_nat_elim_dup;intros;eapply in_elim_dup_aux;eassumption.

Qed.




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

                                     In x (nat_nat_elim_dup l)

                                -> In x l.




Proof.

unfold nat_nat_elim_dup;intros;eapply in_elim_dup;eassumption.

Qed.




Lemma in_nat_nat_dup_aux :

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

            In x (nat_nat_elim_dup (x :: l)).




Proof.

unfold nat_nat_elim_dup;intros;eapply in_dup_aux;eassumption.

Qed.




Lemma in_nat_nat_dup :

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

                 In x l

            -> In x (nat_nat_elim_dup l).




Proof.

unfold nat_nat_elim_dup;intros;eapply in_dup;eassumption.

Qed.




Lemma NoDup_nat_nat_elim_dup : forall (l : list (nat*nat)),

                                             is_lex_sorted l

                                        -> NoDup (nat_nat_elim_dup l).




Proof.

unfold nat_nat_elim_dup;intros;eapply NoDup_elim_dup.

apply lex_order_antisym.

apply lex_order_trans.

assumption.

Qed.




Lemma strict_ord_nat_nat_elim_dup : 

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

                 is_strict_ord l

            -> is_strict_ord (nat_nat_elim_dup l).




Proof.

induction l;intros.




assumption.




simpl;destruct l.

assumption.

destruct (nat_nat_eq_dec a p).

apply IHl;inversion H;assumption.

destruct a;constructor.

inversion H;assumption.

apply IHl;inversion H;assumption.

Qed.




Lemma lex_sort_nat_nat_elim_dup :

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

                 is_lex_sorted l

            -> is_lex_sorted (nat_nat_elim_dup l).




Proof.

unfold is_lex_sorted;unfold nat_nat_elim_dup;intros;eapply sort_elim_dup.

apply lex_order_trans.

assumption.

Qed.