Library chordal_graph_coloring
Require Import List.
Require Import ZArith.
Require Import quicksort.
Require Import lex_sort.
Require Import strict_ord.
Require Import nat_quicksort.
Require Import strict_inc_and_dec.
Require Import max_color.
Require Import graph_construction.
Fixpoint get_nghbs_aux (l : list (nat*nat)) (x : nat) (acc : list nat){struct l} : list nat:=
match l with
| nil => acc
| (a,b) :: l => match (le_lt_dec x a) with
| left _ => acc
| right _ => match (eq_nat_dec x b) with
| left _ => get_nghbs_aux l x (a :: acc)
| right _ => get_nghbs_aux l x acc
end
end
end.
Definition get_nghbs (g: graph) (x : nat) :=
get_nghbs_aux (edges g) x nil.
Lemma acc_in_nghbs :
forall (l : list (nat*nat)) (x y : nat) (acc : list nat),
In x acc
-> In x (get_nghbs_aux l y acc).
Proof.
induction l;intros.
simpl;assumption.
destruct a;simpl.
destruct (le_lt_dec y n).
assumption.
destruct (eq_nat_dec y n0);
apply IHl;intuition.
Qed.
Lemma acc_swap :
forall (l : list (nat*nat)) (acc pacc: list nat) (x : nat),
Permutation acc pacc
-> Permutation (get_nghbs_aux l x acc) (get_nghbs_aux l x pacc).
Proof.
induction l;intros;simpl.
assumption.
destruct a.
destruct (le_lt_dec x n).
assumption.
destruct (eq_nat_dec x n0);
apply IHl;[constructor | ];assumption.
Qed.
Lemma ext_acc :
forall (l : list (nat*nat)) (acc : list nat) (a x y : nat),
In x (get_nghbs_aux l y acc)
-> In x (get_nghbs_aux l y (a :: acc)).
Proof.
induction l;intros;simpl in *.
intuition.
destruct a.
destruct (le_lt_dec y n).
intuition.
destruct (eq_nat_dec y n0).
assert (In x (get_nghbs_aux l y (a0 :: n :: acc))).
apply IHl;assumption.
assert (Permutation (get_nghbs_aux l y (n :: a0 :: acc)) (get_nghbs_aux l y (a0 :: n :: acc))).
apply (acc_swap l (n::a0::acc) (a0::n::acc) y);constructor.
eapply Permutation_in;
[apply Permutation_sym | ];eassumption.
apply IHl;assumption.
Qed.
Lemma nghbs_edges_aux :
forall (l : list (nat*nat)) (x y :nat),
is_lex_sorted l
-> is_strict_ord l
-> In (x,y) l
-> In x (get_nghbs_aux l y nil).
Proof.
induction l;intros.
inversion H1.
destruct a;simpl;decompose [and] H;destruct (le_lt_dec y n).
simpl in H1;decompose [or] H1.
assert (x < y).
apply (strict_in ((n,n0) :: l) x y);
[ | rewrite H2];intuition.
apply False_ind;inversion H2;intuition.
assert (n < x \/ n = x /\ n0 <= y).
eapply strict_sort_in;eassumption.
assert (x < y).
apply (strict_in ((n,n0) :: l) x y);intuition.
apply False_ind;intuition.
destruct (eq_nat_dec y n0);simpl in H1;decompose [or] H1.
apply acc_in_nghbs;inversion H2;intuition.
apply ext_acc.
apply IHl;[apply (is_lex_sorted_tail l (n,n0)) | inversion H0 | ];
assumption.
apply False_ind;inversion H2;intuition.
apply IHl;[apply (is_lex_sorted_tail l (n,n0)) | inversion H0 | ];
assumption.
Qed.
Lemma nghbs_edges :
forall (g:graph) (x y : nat),
In (x,y) (edges g)
-> In x (get_nghbs g y).
Proof.
intros;unfold get_nghbs.
apply (nghbs_edges_aux (edges g) x y);
destruct g;assumption.
Qed.
Lemma edges_nghbs_aux :
forall (l : list (nat*nat)) (acc : list nat) (x y : nat),
is_lex_sorted l
-> is_strict_ord l
-> In y (get_nghbs_aux l x acc)
-> In (y,x) l \/ In y acc.
Proof.
induction l;intros;simpl in H1.
intuition.
destruct a.
destruct (le_lt_dec x n).
intuition.
destruct (eq_nat_dec x n0).
destruct (eq_nat_dec n y).
subst;intuition.
assert (In (y,x) l \/ In y (n :: acc)).
apply IHl.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
assumption.
intuition.
simpl in H3;decompose [or] H3.
apply False_ind;intuition.
intuition.
assert (In (y,x) l \/ In y acc).
apply IHl.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
assumption.
intuition.
Qed.
Lemma edges_nghbs :
forall (g : graph) (x y : nat),
In y (get_nghbs g x)
-> In (y,x) (edges g).
Proof.
intros;unfold get_nghbs in H.
assert (In (y,x) (edges g) \/ In y nil).
apply edges_nghbs_aux.
destruct g;decompose [and] is_lex_sorted_edges;intuition.
destruct g; decompose [and] is_lex_sorted_edges;intuition.
assumption.
intuition;inversion H1.
Qed.
Lemma not_in_x_nghbsx_aux:
forall (l : list (nat*nat)) (acc : list nat) (x :nat),
is_lex_sorted l
-> is_strict_ord l
-> ~In x acc
-> ~In x (get_nghbs_aux l x acc).
Proof.
induction l;intros;simpl.
assumption.
unfold not;destruct a;intros.
destruct (le_lt_dec x n).
intuition.
destruct (eq_nat_dec x n0).
apply (IHl (n :: acc) x).
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
unfold not;intro;simpl in H3;decompose [or] H3;intuition.
assumption.
assert (~In x (get_nghbs_aux l x acc)).
apply IHl;
[eapply is_lex_sorted_tail | inversion H0 | ];eassumption.
intuition.
Qed.
Lemma not_in_x_nghbsx:
forall (g : graph) (x : nat), ~In x (get_nghbs g x).
Proof.
intros.
destruct g.
unfold get_nghbs.
apply not_in_x_nghbsx_aux;simpl;intuition.
Qed.
Lemma not_in_greaterx_nghbsx_aux:
forall (l : list (nat*nat)) (acc : list nat) (x y :nat),
is_lex_sorted l
-> is_strict_ord l
-> ~In y acc
-> x <= y
-> ~In y (get_nghbs_aux l x acc).
Proof.
induction l;unfold not;intros.
intuition.
destruct a;simpl in H3;destruct (le_lt_dec x n).
intuition.
destruct (eq_nat_dec x n0).
assert (~In y (get_nghbs_aux l x (n::acc))).
apply IHl.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
unfold not;intros;simpl in H4;decompose [or] H4;intuition.
assumption.
intuition.
assert (~In y (get_nghbs_aux l x acc)).
apply IHl.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
intuition.
assumption.
intuition.
Qed.
Lemma not_in_greaterx_nghbsx:
forall (g : graph) (x y : nat),
x <= y
-> ~In y (get_nghbs g x).
Proof.
intros.
unfold get_nghbs.
apply (not_in_greaterx_nghbsx_aux (edges g) nil x y).
destruct g;simpl;intuition.
destruct g;simpl;intuition.
intuition.
assumption.
Qed.
Lemma NoDup_get_nghbs_aux :
forall (l : list (nat*nat)) (x : nat) (acc : list nat),
is_lex_sorted l
-> NoDup l
-> NoDup acc
-> (forall (y z : nat), In y acc -> In (y,z) l -> z > x)
-> NoDup (get_nghbs_aux l x acc).
Proof.
induction l;intros;simpl.
assumption.
destruct a.
destruct (le_lt_dec x n).
assumption.
destruct (eq_nat_dec x n0).
apply IHl.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
constructor.
unfold not;intro.
assert (n0 > x).
apply (H2 n n0);intuition.
intuition.
assumption.
intros.
simpl in H3;decompose [or] H3.
subst.
assert (y < y \/ (y = y /\ n0 <= z)).
apply (strict_sort_in l y z y n0);assumption.
decompose [or] H5.
intuition.
decompose [and] H6.
destruct (gt_eq_gt_dec z n0).
destruct s.
intuition.
subst.
inversion H0;intuition.
assumption.
apply (H2 y z);intuition.
apply IHl.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
assumption.
intros.
apply (H2 y z);intuition.
Qed.
Lemma NoDup_get_nghbs : forall (g : graph) (x : nat),
NoDup (get_nghbs g x).
Proof.
unfold get_nghbs;intros.
apply NoDup_get_nghbs_aux.
destruct g.
decompose [and] is_lex_sorted_edges.
assumption.
apply (NoDup_edges g).
constructor.
intros;inversion H.
Qed.
Lemma strict_inc_rev_nghbs__aux :
forall (l : list (nat*nat)) (x : nat) (acc : list nat),
is_strict_dec acc
-> is_lex_sorted l
-> is_strict_ord l
-> (forall (y : nat),
In (y,x) l
-> ~In y acc)
-> (forall (w y : nat),
In w acc
-> In (y,x) l
-> w < y)
-> NoDup l
-> is_strict_dec (get_nghbs_aux l x acc).
Proof.
induction l;intros.
intuition.
simpl.
destruct a.
destruct (le_lt_dec x n).
assumption.
destruct (eq_nat_dec x n0).
apply IHl;subst.
apply strict_dec;intuition.
eapply is_lex_sorted_tail;eassumption.
inversion H1;assumption.
intros.
unfold not;intro.
simpl in H6;decompose [or] H6.
subst.
inversion H4.
intuition.
unfold not in H2;apply (H2 y);intuition.
intros.
simpl in H5;decompose [or] H5.
subst.
eapply NoDup_lex_sort_diff;eassumption.
apply H3;intuition.
inversion H4;assumption.
apply IHl.
assumption.
eapply is_lex_sorted_tail;eassumption.
inversion H1;assumption.
intros.
apply H2;intuition.
intros.
apply (H3 w y);intuition.
inversion H4;assumption.
Qed.
Lemma strict_dec_nghbs :
forall (g : graph) (x : nat),
is_strict_dec (get_nghbs g x).
Proof.
unfold get_nghbs;intros.
apply strict_inc_rev_nghbs__aux.
constructor.
apply (is_lex_sorted_edges g).
apply (is_strict_ord_edges g).
unfold not;intros.
inversion H0.
intros.
inversion H.
apply (NoDup_edges g).
Qed.
Fixpoint get_used_colors2_aux (l : list (nat*nat)) (x : nat) {struct l}: (nat*(list (nat*nat))) :=
match l with
| nil => (0,nil)
| (y,z) :: l' => match (eq_nat_dec x y) with
| left _ => (z,l')
| right _ => get_used_colors2_aux l' x
end
end.
Fixpoint get_used_colors2 (l' : list nat) (l : list (nat*nat)){struct l'} : list nat :=
match l' with
| nil => nil
| x :: l'' => fst (get_used_colors2_aux l x) ::
(get_used_colors2 l'' (snd (get_used_colors2_aux l x)))
end.
Lemma in_get_used_colors2_aux1 :
forall (l : list (nat*nat)) (x y : nat),
In (x,y) l
-> no_fst_dup l
-> y = fst (get_used_colors2_aux l x).
Proof.
induction l;[|destruct a];simpl;intros.
intuition.
destruct (eq_nat_dec x n).
decompose [or] H.
inversion H1;intuition.
inversion H0.
apply False_ind;apply (H6 y);rewrite <-e;assumption.
apply IHl.
decompose [or] H.
inversion H1;apply False_ind;intuition.
assumption.
inversion H0;assumption.
Qed.
Lemma in_get_used_colors2__aux2:
forall (l : list (nat*nat)) (l' : list nat) (a x y : nat),
In (x,y) l
-> In x l'
-> is_strict_dec_fst l
-> is_strict_dec (a :: l')
-> (forall (x : nat),
In x (a :: l')
-> exists y : nat, In (x,y) l)
-> In (x,y) (snd (get_used_colors2_aux l a)).
Proof.
induction l;intros.
inversion H.
destruct a.
destruct (eq_nat_dec n a0).
subst.
simpl.
destruct (eq_nat_dec a0 a0).
simpl.
simpl in H;decompose [or] H.
assert (x < a0).
eapply strict_dec_in;eassumption.
inversion H4;apply False_ind;intuition.
assumption.
intuition.
simpl in H;decompose [or] H.
rewrite H4 in *.
assert (exists ya : nat, In (a0,ya) ((x,y) :: l)).
apply H3;intuition.
inversion H5.
assert (x < a0).
eapply strict_dec_in;eassumption.
assert (a0 < x).
simpl in H6;decompose [or] H6.
inversion H8;apply False_ind;intuition.
eapply strict_dec_fst_in;eassumption.
apply False_ind;intuition.
simpl.
destruct (eq_nat_dec a0 n).
apply False_ind;intuition.
eapply IHl.
assumption.
eassumption.
inversion H1.
constructor.
assumption.
assumption.
intros.
assert (exists y : nat, In (x0,y) ((n,n0) :: l)).
apply H3;assumption.
inversion H6.
simpl in H5;decompose [or] H5.
simpl in H7;decompose [or] H7.
inversion H9;subst;intuition.
exists x1;assumption.
assert (x0 < n).
assert (a0 <= n).
assert (exists ya : nat, In (a0,ya) ((n,n0) :: l)).
apply H3;intuition.
inversion H9.
simpl in H10;decompose [or] H10.
inversion H11;intuition.
assert (a0 < n).
eapply strict_dec_fst_in;eassumption.
intuition.
assert (x0 < a0).
eapply strict_dec_in;eassumption.
intuition.
simpl in H7;decompose [or] H7.
inversion H10;apply False_ind;intuition.
exists x1.
assumption.
Qed.
Lemma no_fst_dup_colors2_aux :
forall (l : list (nat*nat)) (x : nat),
no_fst_dup l
-> no_fst_dup (snd (get_used_colors2_aux l x)).
Proof.
induction 1.
simpl.
constructor.
simpl;destruct (eq_nat_dec x x0).
simpl;assumption.
assumption.
Qed.
Lemma strict_dec_used_colors2 :
forall (l : list (nat*nat)) (x : nat),
is_strict_dec_fst l
-> is_strict_dec_fst (snd (get_used_colors2_aux l x)).
Proof.
induction 1.
simpl.
constructor.
simpl.
destruct n.
destruct (eq_nat_dec x n);
simpl;constructor.
simpl.
destruct (eq_nat_dec x a).
simpl.
assumption.
simpl in IHis_strict_dec_fst.
destruct (eq_nat_dec x x0).
simpl.
inversion H0.
constructor.
assumption.
assumption.
Qed.
Lemma in_get_used_colors2_aux2 :
forall (l' : list nat) (l : list (nat*nat)) (a x y : nat),
(forall (x : nat),
In x (a :: l')
-> exists y : nat, In (x,y) l)
-> In x l'
-> is_strict_dec_fst l
-> is_strict_dec (a :: l')
-> In (x,y) l
-> In y (get_used_colors2 l'(snd(get_used_colors2_aux l a))).
Proof.
induction l';intros.
inversion H0.
simpl in H0;decompose [or] H0.
subst;left.
symmetry;apply in_get_used_colors2_aux1.
apply (in_get_used_colors2__aux2 l (x :: l') a0 x y);intuition.
apply no_fst_dup_colors2_aux.
apply no_fst_dup_strict_dec_fst;assumption.
simpl;right.
eapply IHl'.
intros.
assert (exists y0 : nat, In (x0,y0) l).
apply H;intuition.
inversion H6.
assert (In (x0,x1) (snd (get_used_colors2_aux l a0))).
eapply in_get_used_colors2__aux2.
assumption.
eassumption.
assumption.
assumption.
intuition.
exists x1;assumption.
eassumption.
apply strict_dec_used_colors2.
assumption.
inversion H2;assumption.
eapply in_get_used_colors2__aux2.
assumption.
eassumption.
assumption.
eapply is_strict_dec_rmsnd;eassumption.
intros.
apply H.
simpl in H5;decompose [or] H5.
subst;intuition.
intuition.
Qed.
Lemma in_get_used_colors2 :
forall (l' : list nat) (l : list (nat*nat)) (x y : nat),
no_fst_dup l
-> (forall (x : nat),
In x l'
-> exists y : nat, In (x,y) l)
-> In (x,y) l
-> is_strict_dec_fst l
-> is_strict_dec l'
-> In x l'
-> In y (get_used_colors2 l' l).
Proof.
induction l';intros;simpl.
assumption.
simpl in H4;decompose [or] H4.
left.
symmetry.
apply in_get_used_colors2_aux1.
subst;intuition.
assumption.
right;eapply in_get_used_colors2_aux2.
intuition.
eassumption.
assumption.
inversion H3.
constructor.
constructor;assumption.
assumption.
Qed.
Lemma get_used_colors2_ext_out :
forall (l' : list nat) (x y : nat) (l : list (nat*nat)),
~In x l'
-> get_used_colors2 l' l = get_used_colors2 l' ((x,y) :: l).
Proof.
induction l';intros;simpl.
reflexivity.
destruct (eq_nat_dec a x).
rewrite e in H;apply False_ind;intuition.
reflexivity.
Qed.
Fixpoint get_available_color__aux (l : list nat) (acc : nat) {struct l}: nat :=
match l with
| nil => acc
| x::l' => match gt_eq_gt_dec x acc with
| inleft (left _) => get_available_color__aux l' acc
| inleft (right _) => get_available_color__aux l' (S (acc))
| inright _ => acc
end
end.
Definition get_available_color_aux (l :list nat) :=
get_available_color__aux l 1.
Lemma acc_le_avcolor : forall (l : list nat) (acc : nat),
acc <= get_available_color__aux l acc.
Proof.
induction l;intros.
intuition.
simpl.
destruct (gt_eq_gt_dec a acc).
destruct s.
apply IHl.
assert (S (acc) <= get_available_color__aux l (S acc)).
apply IHl.
intuition.
intuition.
Qed.
Lemma acc_avcolor :
forall (l : list nat) (x acc : nat),
x < acc
-> x < get_available_color__aux l acc.
Proof.
intros.
assert (acc <= get_available_color__aux l acc).
apply acc_le_avcolor.
intuition.
Qed.
Lemma acc_avcolor_in :
forall (l : list nat) (x acc :nat),
is_strict_inc l
-> In x l
-> x <= acc
-> x < get_available_color__aux l acc.
Proof.
induction l;intros;simpl.
inversion H0.
destruct (gt_eq_gt_dec a acc).
destruct s.
simpl in H0;decompose [or] H0.
subst.
apply (acc_avcolor l x acc);assumption.
apply IHl;[eapply is_strict_inc_tail | | ];eassumption.
apply acc_avcolor;intuition.
assert (a < x ).
eapply in_strict_sort.
eassumption.
simpl in H0;destruct H0;
[apply False_ind | ];intuition.
apply False_ind;intuition.
Qed.
Lemma correct_get_available_color__aux :
forall (l : list nat) (x acc : nat),
In x l
-> is_strict_inc l
-> get_available_color__aux l acc <> x.
Proof.
induction l;intros.
inversion H.
destruct (le_gt_dec x acc).
assert (x < get_available_color__aux (a::l) acc).
apply acc_avcolor_in;assumption.
intuition.
simpl in H;decompose [or] H;simpl;subst.
destruct (gt_eq_gt_dec x acc);
[destruct s; apply False_ind | ];intuition.
destruct (gt_eq_gt_dec a acc).
destruct s;apply IHl;
[ | eapply is_strict_inc_tail | | eapply is_strict_inc_tail ];
eassumption.
intuition.
Qed.
Lemma correct_get_available_color_aux :
forall (l : list nat) (x : nat),
In x l
-> is_strict_inc l
-> get_available_color_aux l <> x.
Proof.
unfold get_available_color_aux;intros.
apply correct_get_available_color__aux;assumption.
Qed.
Definition get_available_color (g : graph) (x : nat) (l : list (nat*nat)): nat :=
get_available_color_aux(nat_elim_dup(nat_quicksort (get_used_colors2 (get_nghbs g x) l))).
Lemma get_available_color_get_used_colors_aux :
forall (g: graph) (l : list (nat*nat)) (x y z :nat),
In (x,y) (edges g)
-> is_strict_dec_fst l
-> In (x,z) l
-> (forall (n : nat),
In n (get_nghbs g y)
-> exists p : nat, In (n,p) l)
-> get_available_color_aux (nat_elim_dup(nat_quicksort(get_used_colors2 (get_nghbs g y) l))) <> z.
Proof.
intros.
assert (In x (get_nghbs g y)).
apply nghbs_edges;assumption.
assert (In z (get_used_colors2 (get_nghbs g y) l)).
apply (in_get_used_colors2 (get_nghbs g y) l x z).
apply no_fst_dup_strict_dec_fst;assumption.
assumption.
assumption.
assumption.
apply strict_dec_nghbs.
assumption.
apply correct_get_available_color_aux.
apply in_nat_dup.
assert (Permutation (get_used_colors2 (get_nghbs g y) l) (nat_quicksort (get_used_colors2 (get_nghbs g y) l))).
unfold nat_quicksort.
apply permutation_quicksort.
eapply Permutation_in.
eassumption.
assumption.
apply sort_NoDup_strict_inc.
unfold nat_quicksort;apply is_sorted_elim_dup.
unfold nat_quicksort.
apply is_sorted_quicksort.
intuition.
intuition.
intros;destruct (le_gt_dec a b);intuition.
apply NoDup_nat_elim_dup.
unfold nat_quicksort;apply is_sorted_quicksort.
intuition.
intuition.
intros;destruct (le_gt_dec a b);intuition.
Qed.
Lemma get_available_color_get_used_colors :
forall (g: graph) (l : list (nat*nat)) (x y z :nat),
In (x,y) (edges g)
-> no_fst_dup l
-> is_strict_dec_fst l
-> In (x,z) l
-> (forall (n : nat),
In n (get_nghbs g y)
-> exists p : nat, In (n,p) l)
-> get_available_color g y l <> z.
Proof.
intros;unfold get_available_color.
eapply get_available_color_get_used_colors_aux;eassumption.
Qed.
Fixpoint graph_coloring_aux (g : graph) (l : list nat) (l' : list (nat*nat)) {struct l}: list (nat*nat):=
match l with
| nil => l'
| x :: l'' => graph_coloring_aux g l'' ((x,get_available_color g x l') :: l')
end.
Definition graph_coloring (g : graph) :=
graph_coloring_aux g (vertices g) nil.
Lemma in_acc_graph_coloring:
forall (g : graph) (l : list nat) (l' : list (nat*nat)) (x y : nat),
In (x,y) l'
-> In (x,y) (graph_coloring_aux g l l').
Proof.
induction l;intros;simpl;[ | apply IHl];intuition.
Qed.
Lemma get_available_color_ext_le:
forall (g : graph) (a x y :nat) (l : list (nat*nat)),
x <= a
-> get_available_color g x l = get_available_color g x ((a,y) :: l).
Proof.
unfold get_available_color;intros.
assert (get_used_colors2 (get_nghbs g x) l = get_used_colors2 (get_nghbs g x) ((a,y) :: l)).
apply get_used_colors2_ext_out.
apply not_in_greaterx_nghbsx.
assumption.
rewrite H0;reflexivity.
Qed.
Lemma in_avcolor_get__aux:
forall (g : graph) (l : list nat) (l' : list (nat*nat)) (x y : nat),
is_strict_inc l
-> (forall (v c : nat), In v l -> ~In (v,c) l')
-> (forall (x y z : nat), In (x,y) l' -> In z l -> x <= z)
-> (forall (x y :nat), In (x,y) l' -> y = get_available_color g x l')
-> In (x,y) (graph_coloring_aux g l l')
-> y = get_available_color g x (graph_coloring_aux g l l').
Proof.
induction l;intros;simpl.
apply H2;intuition.
apply IHl.
eapply is_strict_inc_tail;eassumption.
unfold not;intros.
simpl in H5;decompose [or] H5.
assert (a < v).
eapply in_strict_sort;eassumption.
inversion H6;intuition.
generalize (H0 v c);intuition.
intros;simpl in H4;decompose [or] H4.
inversion H6.
rewrite H8 in *.
assert (x0 < z).
eapply in_strict_sort;eassumption.
intuition.
eapply H1.
eassumption.
intuition.
intros;simpl in H4;decompose [or] H4.
inversion H5.
apply get_available_color_ext_le.
intuition.
assert (get_available_color g x0 l' = get_available_color g x0 ((a,get_available_color g a l') :: l')).
apply get_available_color_ext_le.
eapply H1.
eassumption.
intuition.
rewrite <-H6.
apply H2;assumption.
assumption.
Qed.
Lemma in_avcolor_get :
forall (g : graph) (x y :nat),
In (x,y) (graph_coloring g)
-> y = get_available_color g x (graph_coloring g).
Proof.
intros;unfold graph_coloring.
apply in_avcolor_get__aux;try intros;try inversion H0;try intuition.
destruct g;simpl.
rewrite vertices_edges;apply is_strict_inc_vertices.
Qed.
Lemma no_fst_dup_graph_coloring_aux:
forall (g : graph) (l : list nat) (l' : list (nat*nat)),
is_strict_inc l
-> (forall (v c : nat), In v l -> ~In (v,c) l')
-> no_fst_dup l'
-> no_fst_dup (graph_coloring_aux g l l').
Proof.
induction l;intros;simpl.
assumption.
apply IHl.
inversion H;[constructor | assumption].
assert (~In a l).
inversion H.
intuition.
unfold not;intro.
assert (y < a).
simpl in H6;decompose [or] H6.
intuition.
assert (y < a).
eapply in_strict_sort;eassumption.
assumption.
intuition.
unfold not;intros.
simpl in H4;decompose [or] H4.
inversion H5;rewrite <-H7 in H3;intuition.
unfold not in H0.
eapply (H0 v c);[intuition | assumption].
constructor.
assumption.
intro;apply H0;intuition.
Qed.
Lemma no_fst_dup_graph_coloring :
forall (g : graph), no_fst_dup (graph_coloring g).
Proof.
unfold graph_coloring.
intro g.
assert (no_fst_dup (graph_coloring_aux g (vertices g) nil)).
apply no_fst_dup_graph_coloring_aux.
destruct g;rewrite vertices_edges;apply is_strict_inc_vertices.
intuition.
constructor.
intuition.
Qed.
Lemma is_strict_dec_fst_graph_coloring__aux :
forall (g : graph) (l : list nat) (acc : list (nat*nat)),
is_strict_inc l
-> (forall (y z a : nat),
In (y,z) acc
-> In a l
-> y < a)
-> is_strict_dec_fst acc
-> is_strict_dec_fst (graph_coloring_aux g l acc).
Proof.
induction l;intros;simpl.
assumption.
apply (IHl ((a,get_available_color g a acc) :: acc)).
eapply is_strict_inc_tail;eassumption.
intros.
assert (a < a0).
eapply in_strict_sort;eassumption.
simpl in H2;decompose [or] H2.
inversion H5;intuition.
assert (y < a).
apply (H0 y z a);intuition.
intuition.
destruct acc.
constructor.
destruct p;constructor.
apply (H0 n n0 a);intuition.
assumption.
Qed.
Lemma is_strict_dec_fst_graph_coloring_aux :
forall (g : graph) (l : list nat),
is_strict_inc l
-> is_strict_dec_fst (graph_coloring_aux g l nil).
Proof.
intros;apply is_strict_dec_fst_graph_coloring__aux.
assumption.
intros;inversion H0.
constructor.
Qed.
Lemma is_strict_dec_fst_graph_coloring :
forall (g : graph), is_strict_dec_fst (graph_coloring g).
Proof.
unfold graph_coloring;intros;apply is_strict_dec_fst_graph_coloring_aux.
rewrite vertices_edges;apply is_strict_inc_vertices.
Qed.
Lemma correct_graph_coloring2__aux1:
forall (g : graph) (l : list nat) (l' : list (nat*nat)) (x y :nat),
is_strict_inc l
-> (forall (a x y : nat), In (x,y) l' -> In a l -> x < a)
-> (forall (x y : nat), In (x,y) l' -> ~ In x l)
-> In (x,y) (graph_coloring_aux g l l')
-> ~In (x,y) l'
-> In x l.
Proof.
induction l;intros.
intuition.
destruct (eq_nat_dec a x).
rewrite e;intuition.
right.
apply (IHl ((a,get_available_color g a l') :: l') x y).
eapply is_strict_inc_tail;eassumption.
intros.
simpl in H4;decompose [or] H4.
inversion H6.
assert (a < a0).
eapply in_strict_sort;eassumption.
intuition.
eapply H0;[eassumption|intuition].
unfold not;intros.
simpl in H4;decompose [or] H4.
inversion H6.
assert (a < x0).
eapply in_strict_sort;eassumption.
intuition.
assert (~In x0 (a :: l)).
eapply H1.
eassumption.
intuition.
simpl in H2;assumption.
simpl;intuition;inversion H5;intuition.
Qed.
Lemma correct_graph_coloring2_aux1:
forall (g : graph) (x y : nat),
In (x,y) (graph_coloring g)
-> In x (vertices g).
Proof.
intros.
apply (correct_graph_coloring2__aux1 g (vertices g) nil x y).
destruct g;simpl;rewrite vertices_edges;apply is_strict_inc_vertices.
intros;inversion H0.
intros;inversion H0.
unfold graph_coloring in H.
assumption.
intuition.
Qed.
Lemma correct_graph_coloring2__aux2:
forall (g : graph) (l : list nat) (l' : list (nat*nat)) (x : nat),
is_strict_inc l
-> (forall (a x y :nat), In (x,y) l' -> In a l -> x < a)
-> (forall (x y :nat), In (x,y) l' -> ~ In x l)
-> In x l
-> exists c, In (x,c) (graph_coloring_aux g l l').
Proof.
induction l;intros;simpl.
inversion H2.
simpl in H2;decompose [or] H2.
assert (In (a,get_available_color g a l') (graph_coloring_aux g l ((a,get_available_color g a l') :: l'))).
apply in_acc_graph_coloring;intuition.
rewrite <- H3.
exists (get_available_color g a l');assumption.
apply IHl.
eapply is_strict_inc_tail;eassumption.
intros;simpl in H4;decompose [or] H4.
inversion H6.
assert (a < a0).
eapply in_strict_sort;eassumption.
intuition.
eapply H0;[eassumption|intuition].
intros;simpl in H4;decompose [or] H4.
inversion H5.
unfold not;intro.
assert (a < x0).
eapply in_strict_sort;eassumption.
intuition.
assert (~In x0 (a :: l)).
eapply H1;eassumption.
intuition.
assumption.
Qed.
Lemma correct_graph_coloring2_aux2:
forall (g : graph) (x :nat),
In x (vertices g)
-> In (x,get_available_color g x (graph_coloring g)) (graph_coloring g).
Proof.
intros;unfold graph_coloring.
assert (exists c :nat, In (x,c) (graph_coloring_aux g (vertices g) nil)).
apply correct_graph_coloring2__aux2.
destruct g;simpl;rewrite vertices_edges;apply is_strict_inc_vertices.
intros;inversion H0.
intros;inversion H0.
assumption.
assert (forall (c : nat),In (x,c) (graph_coloring g)
-> c = get_available_color g x (graph_coloring g)).
apply in_avcolor_get.
unfold graph_coloring in H1.
inversion H0.
assert (x0 = get_available_color g x (graph_coloring_aux g (vertices g) nil)).
apply H1;assumption.
rewrite <-H3;assumption.
Qed.
Lemma correct_graph_coloring1:
forall (g : graph) (x y cx cy : nat),
In (x,y) (edges g)
-> In (x,cx) (graph_coloring g)
-> In (y,cy) (graph_coloring g)
-> cy <> cx.
Proof.
intros.
assert (cy = get_available_color g y (graph_coloring g)).
apply in_avcolor_get.
assumption.
rewrite H2;eapply get_available_color_get_used_colors;
try eassumption.
apply no_fst_dup_graph_coloring.
apply is_strict_dec_fst_graph_coloring.
intros.
assert (In n (vertices g)).
assert (In (n,y) (edges g)).
apply edges_nghbs;assumption.
assert (In n (vertices g) /\ In y (vertices g)).
rewrite (vertices_edges g).
apply in_vertices;assumption.
intuition.
exists (get_available_color g n (graph_coloring g)).
apply correct_graph_coloring2_aux2;assumption.
Qed.
Lemma correct_graph_coloring2:
forall (g : graph) (x : nat),
In x (vertices g)
<->
In (x, get_available_color g x (graph_coloring g)) (graph_coloring g).
Proof.
split;intros;
[apply correct_graph_coloring2_aux2 |eapply correct_graph_coloring2_aux1];
eassumption.
Qed.
Lemma correct_graph_coloring3:
forall (g : graph) (x : nat),
1 <= get_available_color g x (graph_coloring g).
Proof.
unfold get_available_color.
intros.
unfold get_available_color_aux.
apply acc_le_avcolor.
Qed.
Inductive is_coloring : graph -> list (nat*nat) -> Prop :=
is_coloring_cons : forall (g : graph) (col : list (nat*nat)),
(forall (x : nat),
In x (vertices g)
<-> exists c, In (x,c) col )
->
(forall (x y cx cy : nat),
In (x,y) (edges g)
-> In (x,cx) col
-> In (y,cy) col
-> cy <> cx)
->
(forall (x cx : nat), In (x,cx) col -> 1 <= cx)
-> no_fst_dup col
-> is_coloring g col.
Lemma is_coloring_graph_coloring :
forall (g : graph), is_coloring g (graph_coloring g).
Proof.
intros;constructor;intros.
split;intros.
exists (get_available_color g x (graph_coloring g)).
apply (proj1 (correct_graph_coloring2 g x));assumption.
inversion H;eapply correct_graph_coloring2_aux1;eassumption.
eapply correct_graph_coloring1;eassumption.
assert (cx = get_available_color g x (graph_coloring g)).
apply in_avcolor_get;assumption.
rewrite H0;apply correct_graph_coloring3.
apply no_fst_dup_graph_coloring.
Qed.
Definition check_kcoloring (g : graph) (k : nat) : bool :=
match (le_gt_dec (max_color (graph_coloring g)) k) with
| left _ => true
| right _ => false
end.