Library lth_in_proof
Require Import List.
Require Import ZArith.
Require Import quicksort.
Require Import strict_inc_and_dec.
Require Import lex_sort.
Require Import strict_ord.
Require Import max_color.
Inductive no_snd_dup : list (nat*nat) -> Prop:=
no_snd_dup_nil : no_snd_dup nil
| no_snd_dup_cons :
forall (l : list (nat*nat)) (x y : nat),
no_snd_dup l
-> (forall (z : nat), ~In (z,y) l)
-> no_snd_dup ((x,y) :: l).
Inductive is_strict_inc_snd : list (nat*nat) -> Prop :=
| is_strict_inc_snd_nil : is_strict_inc_snd nil
| is_strict_inc_snd_sing : forall (n : (nat*nat)),
is_strict_inc_snd (n :: nil)
| is_strict_inc_snd_cons : forall (a b x y : nat) (l : list (nat*nat)),
b < y
-> is_strict_inc_snd ((x,y) :: l)
-> is_strict_inc_snd ((a,b) :: (x,y) :: l).
Fixpoint add_snd_sort (l : list (nat*nat)) (x y : nat) {struct l} : list (nat*nat) :=
match l with
| nil => ((x,y) :: nil)
| (a,b) :: l' => match (le_gt_dec b y) with
| left _ => (a,b) :: (add_snd_sort l' x y)
| right _ => (x,y) :: l
end
end.
Fixpoint snd_sort (l : list (nat*nat)){struct l} : list (nat*nat) :=
match l with
| nil => nil
| (a,b) :: l' => add_snd_sort (snd_sort l') a b
end.
Lemma snd_add_nil : forall (l : list (nat*nat)) (x y : nat),
add_snd_sort l x y <> nil.
Proof.
induction l;intros;simpl;[|destruct a;destruct (le_gt_dec n0 y)];intuition;inversion H.
Qed.
Lemma snd_sort_nil : forall (l : list (nat*nat)),
snd_sort l = nil
-> l = nil.
Proof.
induction l;intros;[|destruct a];simpl.
reflexivity.
simpl in H.
assert (add_snd_sort (snd_sort l) n n0 <> nil).
apply snd_add_nil.
intuition.
Qed.
Lemma perm_add_snd :
forall (l : list (nat*nat)) (x y : nat),
Permutation ((x,y) :: l) (add_snd_sort l x y).
Proof.
induction l;intros;[|destruct a];simpl.
apply Permutation_refl.
destruct (le_gt_dec n0 y).
apply Permutation_trans with (l' := ((n,n0) :: (x,y) :: l));
constructor;apply IHl.
apply Permutation_refl.
Qed.
Lemma snd_perm :
forall (l l' : list (nat*nat)) (x y : nat),
Permutation l l'
-> Permutation (add_snd_sort l x y) (add_snd_sort l' x y).
Proof.
induction 1.
apply Permutation_refl.
destruct x0;simpl.
destruct (le_gt_dec n0 y);constructor;[|constructor];assumption.
destruct x0;destruct y0;simpl.
destruct (le_gt_dec n2 y);destruct (le_gt_dec n0 y).
constructor.
apply Permutation_trans with (l' := ((x,y) :: (n1,n2) :: (n,n0) :: l));
constructor;constructor.
apply Permutation_trans with (l' := ((x,y) :: (n,n0) :: (n1,n2) :: l));
constructor;constructor.
constructor;constructor.
apply Permutation_trans with (l' := add_snd_sort l' x y);assumption.
Qed.
Lemma no_snd_dup_perm_add_snd : forall (l : list (nat*nat)),
no_snd_dup l
-> Permutation l (snd_sort l).
Proof.
induction l;intros;[|destruct a];simpl.
apply Permutation_refl.
apply Permutation_trans with (l' := add_snd_sort l n n0).
apply perm_add_snd.
apply snd_perm;apply IHl;inversion H;assumption.
Qed.
Lemma is_strict_inc_add_snd :
forall (l : list (nat*nat)) (x y : nat),
is_strict_inc_snd l
-> (forall (z : nat), ~In (z,y) l)
-> is_strict_inc_snd (add_snd_sort l x y).
Proof.
induction 1;intros.
simpl;constructor.
destruct n;simpl.
destruct (le_gt_dec n0 y).
destruct (eq_nat_dec n0 y).
subst;generalize (H n);intro;apply False_ind;intuition.
constructor;intuition;constructor.
constructor;intuition;constructor.
simpl in *.
destruct (le_gt_dec b y).
destruct (le_gt_dec y0 y).
constructor;intuition.
apply IHis_strict_inc_snd.
intro;generalize (H1 z);intuition.
assert (b <> y).
assert ((a,b) <> (a,y));generalize (H1 a);intuition.
constructor;intuition.
apply IHis_strict_inc_snd.
intro;generalize (H1 z);intuition.
constructor;[|constructor];assumption.
Qed.
Lemma no_snd_dup_strict_inc_snd :
forall (l : list (nat*nat)),
no_snd_dup l
-> is_strict_inc_snd (snd_sort l).
Proof.
induction l;intros;[|destruct a];simpl.
constructor.
apply is_strict_inc_add_snd.
apply IHl;inversion H;assumption.
inversion H.
assert (Permutation l (snd_sort l)).
apply no_snd_dup_perm_add_snd;assumption.
unfold not in *;intros;generalize (H4 z);intro.
apply H7;eapply Permutation_in;
apply Permutation_sym in H5;eassumption.
Qed.
Lemma lth_le__aux :
forall (l : list (nat*nat)) (x y : nat),
is_strict_inc_snd ((x,y) :: l)
-> exists x0 : nat, exists y0 : nat,
In (x0,y0) ((x,y) :: l) /\ length ((x,y) :: l) + y <= S y0.
Proof.
induction l;intros;[|destruct a];simpl.
exists x;exists y;intuition.
assert (exists x0 : nat,exists y0 : nat,
In (x0, y0) ((n, n0) :: l) /\ length ((n, n0) :: l) + n0 <= S y0).
apply IHl;inversion H;assumption.
inversion H0;inversion H1.
exists x0;exists x1.
decompose [and] H2.
split.
intuition.
simpl in H4;assert (S (length l + y) <= x1);
[inversion H|];intuition.
Qed.
Lemma lth_le_aux : forall (l : list (nat*nat)),
is_strict_inc_snd l
-> l <> nil
-> (forall (x y : nat),
In (x,y) l
-> 1 <= y)
-> exists x : nat, exists y : nat,
In (x,y) l /\ length l <= y.
Proof.
induction l;intros;[|destruct a].
intuition.
assert (exists x0 : nat, exists y0 : nat,
In (x0,y0) ((n,n0) :: l) /\ length ((n,n0) :: l) + n0 <= S y0).
apply lth_le__aux;assumption.
inversion H2;inversion H3.
exists x;exists x0.
split.
intuition.
assert (1 <= n0);[apply (H1 n n0)|];intuition.
Qed.
Lemma lth_le :
forall (l : list (nat*nat)),
l <> nil
-> no_snd_dup l
-> (forall (x y : nat),
In (x,y) l
-> 1 <= y)
-> exists x : nat, exists y : nat,
In (x,y) l /\ length l <= y.
Proof.
intros.
assert (Permutation l (snd_sort l)).
apply no_snd_dup_perm_add_snd;assumption.
assert (exists x : nat, exists y : nat, In (x,y) (snd_sort l) /\ length (snd_sort l) <= y).
apply lth_le_aux.
apply no_snd_dup_strict_inc_snd.
assumption.
unfold not;intro;assert (l = nil);[apply snd_sort_nil|];intuition.
intros;apply (H1 x y).
apply Permutation_in with (l := snd_sort l);
[apply Permutation_sym|];assumption.
inversion H3;inversion H4.
exists x;exists x0.
split.
apply Permutation_in with (l := snd_sort l).
apply Permutation_sym;assumption.
intuition.
assert (length l = length (snd_sort l)).
apply Permutation_length;assumption.
rewrite H6;intuition.
Qed.
Lemma NoDup_diff :
forall (l : list (nat*nat)),
(forall (a b x y : nat),
In (a,b) l
-> In (x,y) l
-> a <> x
-> b <> y)
-> NoDup l
-> no_snd_dup l.
Proof.
induction l;intros;[|destruct a].
constructor.
constructor.
apply IHl;intros.
apply (H a b x y);intuition.
inversion H0;assumption.
unfold not;intros.
destruct (eq_nat_dec z n).
inversion H0.
rewrite e in H1;intuition.
unfold not in H;apply (H n n0 z n0);intuition.
Qed.
Lemma lth_inject :
forall (l : list (nat*nat)),
(forall (a b x y : nat),
In (a,b) l
-> In (x,y) l
-> a <> x
-> b <> y)
-> NoDup l
-> l <> nil
-> (forall (x y : nat),
In (x,y) l
-> 1 <= y)
-> exists x : nat, exists y : nat,
In (x,y) l /\ length l <= y.
Proof.
intros;apply lth_le;[ | apply NoDup_diff | ];assumption.
Qed.
Fixpoint restriction (l : list (nat*nat)) (l' : list nat){struct l} : list (nat*nat) :=
match l with
| nil => nil
| (a,b) :: l'' => match (In_dec eq_nat_dec a l') with
| left _ => (a,b) ::restriction l'' l'
| right _ => restriction l'' l'
end
end.
Lemma nil_restrict : forall (l : list (nat*nat)),
restriction l nil = nil.
Proof.
induction l;intros;[|destruct a];simpl.
reflexivity.
assumption.
Qed.
Lemma in_restrict_keys_aux :
forall (l' : list (nat*nat)) (l : list nat) (a x y : nat),
In (x,y) (restriction l' (a :: l))
-> x <> a
-> In (x,y) (restriction l' l).
Proof.
induction l';simpl;intros;[|destruct a].
inversion H.
destruct (In_dec eq_nat_dec n l).
destruct (eq_nat_dec a0 n).
simpl in H;decompose [or]H.
rewrite H1;intuition.
simpl;right;apply (IHl' l a0 x y);assumption.
destruct (In_dec eq_nat_dec n l).
simpl in H;decompose [or]H.
rewrite H1;intuition.
simpl;right;apply (IHl' l a0 x y);assumption.
intuition.
simpl in H.
destruct (eq_nat_dec a0 n).
simpl in H;decompose[or]H.
inversion H1;apply False_ind;intuition.
apply (IHl' l a0 x y);assumption.
apply (IHl' l a0 x y);assumption.
Qed.
Lemma in_restrict_keys :
forall (l : list nat) (l' : list (nat*nat)) (x y : nat),
In (x,y) (restriction l' l)
-> In x l.
Proof.
induction l;intros.
assert (restriction l' nil = nil).
apply nil_restrict.
rewrite H0 in H;inversion H.
destruct (eq_nat_dec x a).
rewrite e;intuition.
simpl;right;apply (IHl l' x y).
eapply in_restrict_keys_aux;eassumption.
Qed.
Lemma in_restrict :
forall (l' : list (nat*nat)) (l : list nat) (x y : nat),
In (x,y) (restriction l' l)
-> In (x,y) l'.
Proof.
induction l';simpl;[|destruct a];intros.
assumption.
destruct (In_dec eq_nat_dec n l).
simpl in H;decompose [or] H.
rewrite H0;intuition.
simpl;right;apply (IHl' l x y);assumption.
simpl;right;apply (IHl' l x y);assumption.
Qed.
Lemma only_restrict :
forall (l' : list (nat*nat)) (l : list nat) (x y : nat),
In (x,y) l'
-> In x l
-> In (x,y) (restriction l' l).
Proof.
induction l';intros;[|destruct a;simpl].
inversion H.
destruct (In_dec eq_nat_dec n l).
simpl in H;decompose [or]H.
rewrite H1;intuition.
simpl;right;apply IHl';assumption.
apply IHl'.
simpl in H;decompose [or]H.
inversion H1;subst;intuition.
assumption.
assumption.
Qed.
Lemma NoDup_restrict :
forall (l' : list (nat*nat)) (l : list nat) ,
NoDup l'
-> NoDup (restriction l' l).
Proof.
induction l';intros;[|destruct a];simpl.
constructor.
destruct (In_dec eq_nat_dec n l).
constructor.
inversion H;unfold not in *;intro;apply H2;
eapply in_restrict;eassumption.
apply IHl';inversion H;assumption.
apply IHl';inversion H;assumption.
Qed.
Lemma lth_restrict__aux :
forall (l' : list (nat*nat)) (l : list nat) (a : nat),
length (restriction l' l) <= length (restriction l' (a :: l)).
Proof.
induction l';intros;[|destruct a];simpl.
intuition.
destruct (In_dec eq_nat_dec n l);destruct (eq_nat_dec a0 n);
simpl;[apply le_n_S | apply le_n_S | apply le_S | ];apply IHl'.
Qed.
Lemma lth_restrict_aux :
forall (l' : list (nat*nat)) (l : list nat) (a y : nat),
In (a,y) l'
-> ~ In a l
-> length (restriction l' l) < length (restriction l' (a :: l)).
Proof.
induction l';intros;[|destruct a;simpl].
inversion H.
destruct (In_dec eq_nat_dec n l);destruct (eq_nat_dec a0 n).
rewrite e in H0;intuition.
simpl;apply lt_n_S.
apply (IHl' l a0 y).
simpl in H;decompose [or]H.
inversion H1;apply False_ind;intuition.
assumption.
assumption.
assert (length (restriction l' l) <= length (restriction l' (a0 :: l))).
apply lth_restrict__aux.
simpl;intuition.
simpl in H;decompose [or]H.
inversion H1;apply False_ind;intuition.
apply (IHl' l a0 y);assumption.
Qed.
Lemma lth_restrict :
forall (l : list nat) (l' : list (nat*nat)),
(forall (x : nat), In x l -> exists y : nat, In (x,y) l')
-> NoDup l
-> no_fst_dup l'
-> length l <= length (restriction l' l).
Proof.
induction l;intros.
intuition.
assert (length (restriction l' l) < length (restriction l' (a :: l))).
assert (exists y : nat, In (a,y) l').
apply (H a);intuition.
inversion H2;apply (lth_restrict_aux l' l a x).
assumption.
inversion H0;assumption.
assert (length l <= length (restriction l' l)).
apply IHl.
intros;apply (H x);intuition.
inversion H0;assumption.
assumption.
simpl;intuition.
Qed.
Lemma max_color_lth__aux :
forall (l : list nat) (l' : list (nat*nat)),
(forall (x : nat),
In x l
-> exists y : nat, In (x,y) l')
-> (forall (a b x y : nat),
In a l
-> In x l
-> In (a,b) l'
-> In (x,y) l'
-> a <> x
-> b <> y)
-> no_fst_dup l'
-> (forall (a b x y : nat),
In (a,b) (restriction l' l)
-> In (x,y) (restriction l' l)
-> a <> x
-> b <> y).
Proof.
induction l;intros.
assert (restriction l' nil = nil).
apply nil_restrict.
rewrite H5 in H2;inversion H2.
apply (H0 a0 b x y);
[eapply in_restrict_keys | eapply in_restrict_keys |
eapply in_restrict | eapply in_restrict | ];eassumption.
Qed.
Lemma max_color_lth_aux :
forall (l : list nat) (l' : list (nat*nat)),
(forall (x : nat),
In x l
-> exists y, In (x,y) l')
-> (forall (a b x y : nat),
In a l
-> In x l
-> In (a,b) l'
-> In (x,y) l'
-> a <> x
-> b <> y)
-> NoDup l
-> no_fst_dup l'
-> l <> nil
-> (forall (x y : nat),
In (x,y) l'
-> 1 <= y)
-> exists x : nat, exists y : nat,
In (x,y) (restriction l' l) /\ length (restriction l' l) <= y.
Proof.
intros.
assert (forall (a b x y : nat), In (a,b) (restriction l' l) -> In (x,y) (restriction l' l) -> a <> x -> b <> y).
apply max_color_lth__aux;assumption.
apply lth_inject.
assumption.
apply NoDup_restrict.
apply fst_dup_dup;assumption.
destruct l.
intuition.
assert (exists y : nat, In (n,y) l').
apply H;intuition.
inversion H6.
assert (In (n,x) (restriction l' (n :: l))).
apply only_restrict;intuition.
destruct (restriction l' (n :: l)).
inversion H8.
unfold not;intro;discriminate.
intros;assert (In (x,y) l').
eapply in_restrict;eassumption.
eapply H4;eassumption.
Qed.
Lemma max_color_lth :
forall (l : list nat) (l' : list (nat*nat)),
(forall (x : nat),
In x l
-> exists y, In (x,y) l')
-> (forall (a b x y : nat),
In a l
-> In x l
-> In (a,b) l'
-> In (x,y) l'
-> a <> x
-> b <> y)
-> NoDup l
-> no_fst_dup l'
-> l <> nil
-> (forall (x y : nat),
In (x,y) l'
-> 1 <= y)
-> exists x : nat, exists y : nat,
In (x,y) l' /\ length l <= y.
Proof.
intros.
assert (exists x : nat, exists y : nat, In (x,y) (restriction l' l) /\ length (restriction l' l) <= y).
apply max_color_lth_aux;assumption.
inversion H5;inversion H6.
decompose [and] H7.
exists x;exists x0.
split.
eapply in_restrict;eassumption.
assert (length l <= length (restriction l' l)).
apply lth_restrict;assumption.
intuition.
Qed.
Lemma lth_in : forall (l : list nat) (l' : list (nat*nat)),
(forall (x : nat),
In x l
-> exists y : nat, In (x,y) l')
-> (forall (a b x y : nat),
In a l
-> In x l
-> In (a,b) l'
-> In (x,y) l'
-> a <> x
-> b <> y)
-> NoDup l
-> no_fst_dup l'
-> l <> nil
-> (forall (x y : nat),
In (x,y) l'
-> 1 <= y)
-> length l <= max_color l'.
Proof.
intros.
assert (exists x : nat, exists y : nat, In (x,y) l' /\ length l <= y).
apply max_color_lth;intuition.
inversion H5;inversion H6.
assert (x0 <= max_color l');
[apply (max_max_color l' x x0) | ];intuition.
Qed.