Library coloration_renaming
Require Import List.
Require Import ZArith.
Require Import strict_inc_and_dec.
Require Import peo_search.
Require Import graph_construction.
Require Import chordal_graph_coloring.
Require Import lex_sort.
Require Import strict_ord.
Require Import nat_quicksort.
Require Import chordal_graph_optimality.
Require Import renaming.
Require Import max_color.
Fixpoint coloring_renaming (col : list (nat*nat)) (l : list nat) {struct col} : list (nat*nat) :=
match col with
| nil => nil
| (v,c) :: col' => (rename_vert_inv__aux (rename_fun l) v,c) :: coloring_renaming col' l
end.
Lemma max_color_col_rename_aux :
forall (col : list (nat*nat)) (l : list nat) (acc : nat),
max_color_aux col acc = max_color_aux (coloring_renaming col l) acc.
Proof.
induction col;intros.
reflexivity.
destruct a;simpl.
destruct (le_gt_dec n0 acc);apply IHcol.
Qed.
Lemma max_color_col_rename :
forall (col : list (nat*nat)) (l : list nat),
max_color col = max_color (coloring_renaming col l).
Proof.
unfold max_color;intros;apply max_color_col_rename_aux.
Qed.
Lemma in_coloring_renaming :
forall (col : list (nat*nat)) (l : list nat) (x cx : nat),
In (x,cx) (coloring_renaming col l)
-> (forall (y z : nat),
In (y,z) col
-> 0 < y)
-> (forall (y z : nat),
In (y,z) col
-> y <= length l)
-> NoDup l
-> In (rank l 1 x,cx) col.
Proof.
induction col;intros.
inversion H.
destruct a;simpl in *.
decompose [or] H.
inversion H3.
rewrite <-H6;rewrite in_rename_in_inv_aux.
left;intuition.
apply (H1 n n0);intuition.
assert (0 < n).
apply (H0 n n0);intuition.
intuition.
assumption.
right;apply IHcol.
assumption.
intros;apply (H0 y z);intuition.
intros;apply (H1 y z);intuition.
assumption.
Qed.
Lemma in_rename :
forall (l : list nat) (x : nat),
In x l
-> NoDup l
-> In (rank l 1 x) (rename_vert l).
Proof.
induction l;intros.
inversion H.
simpl.
destruct (eq_nat_dec a a).
destruct (eq_nat_dec x a).
intuition.
rewrite rank_S.
right.
assert (In (rank l 1 x) (intervalle_dec (length l))).
assert (In (rank l 1 x) (rev (rename_vert l))).
eapply Permutation_in.
apply Permutation_rev.
apply IHl.
simpl in H;decompose [or] H.
apply False_ind;intuition.
assumption.
inversion H0;assumption.
unfold rename_vert in H0;rewrite <-rename_interv.
assumption.
inversion H0;assumption.
assert (In (S (rank l 1 x)) (intervalle_dec (S (length l)))).
apply only_in_interv_le.
intuition.
apply le_n_S.
apply in_interv_le;assumption.
assert (S (length l) = length (a :: l)).
intuition.
rewrite H3 in H2;rewrite <-rename_interv in H2.
assert (In (S (rank l 1 x)) (rename_vert_aux (a :: l) (a :: l))).
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
rewrite rename_hd in H4.
simpl in H4;decompose [or] H4.
assert (1 <= rank l 1 x).
apply acc_le_rank_in.
simpl in H;decompose [or] H.
apply False_ind;intuition.
assumption.
apply False_ind;intuition.
assumption.
assumption.
assumption.
intuition.
Qed.
Lemma in_coloring :
forall (col : list (nat*nat)) (l : list nat) (x y : nat),
In (rank l 1 x,y) col
-> NoDup l
-> In x l
-> In (x,y) (coloring_renaming col l).
Proof.
induction col;intros.
inversion H.
destruct a;simpl.
simpl in H;decompose [or] H.
inversion H2.
rewrite in_rename_in_aux.
left;reflexivity.
assumption.
assumption.
right;apply IHcol;assumption.
Qed.
Lemma in_rank_in_inv :
forall (l : list nat) (x : nat),
In x (rename_vert_aux l l)
-> NoDup l
-> In (rename_vert_inv__aux (rename_fun l) x) l.
Proof.
induction l;intros.
inversion H.
simpl.
destruct x.
assert (0 < 0).
apply (positive_in_rename (a :: l) (a :: l));intuition.
apply False_ind;intuition.
destruct x.
intuition.
right.
rewrite (rename_fun_fst l 2 1).
apply IHl.
simpl in H.
destruct (eq_nat_dec a a).
decompose [or] H.
apply False_ind;intuition.
eapply eq_vert_aux_aux.
eassumption.
intuition.
assumption.
intuition.
inversion H0;assumption.
Qed.
Lemma in_rank_in :
forall (l : list nat) (x : nat),
In (rank l 1 x) (rename_vert_aux l l)
-> NoDup l
-> In x l.
Proof.
induction l;intros.
inversion H.
simpl in H.
destruct (eq_nat_dec a a).
destruct (eq_nat_dec x a).
subst;intuition.
decompose [or] H.
assert ({In x l}+{~In x l}).
apply In_dec;apply eq_nat_dec.
destruct H2.
intuition.
assert (rank l 2 x = S (S (S (length l)))).
rewrite rank_S.
rewrite not_in_rank.
reflexivity.
assumption.
apply False_ind;intuition.
simpl;right;apply IHl.
eapply eq_vert_aux_aux.
rewrite rank_S in H1.
eassumption.
assert ({In x l}+{~In x l}).
apply In_dec;apply eq_nat_dec.
destruct H2.
assert (1 <= rank l 1 x).
apply acc_le_rank_in;assumption.
intuition.
assert (rank l 1 x = S (S (length l))).
apply not_in_rank;assumption.
intuition.
assumption.
inversion H0;assumption.
intuition.
Qed.
Lemma NoDup_rank_diff :
forall (l : list nat) (x y : nat),
NoDup l
-> x <> y
-> In x l
-> In y l
-> rank l 1 x <> rank l 1 y.
Proof.
induction l;intros.
inversion H1.
simpl.
destruct (eq_nat_dec x a).
destruct (eq_nat_dec y a).
subst;apply False_ind;intuition.
assert (2 <= rank l 2 y).
apply acc_le_rank_in.
simpl in H2;decompose [or] H2.
subst;apply False_ind;intuition.
assumption.
intuition.
destruct (eq_nat_dec y a ).
assert (2 <= rank l 2 x).
apply acc_le_rank_in.
simpl in H1;decompose [or] H1.
subst;apply False_ind;intuition.
assumption.
intuition.
rewrite rank_S.
rewrite (rank_S l 1 y).
apply not_eq_S.
apply IHl.
inversion H;assumption.
assumption.
simpl in H1;decompose [or] H1.
subst;apply False_ind;intuition.
assumption.
simpl in H2;decompose [or] H2.
subst;apply False_ind;intuition.
assumption.
Qed.
Lemma no_fst_dup_conservation :
forall (col : list (nat*nat)) (l : list nat),
no_fst_dup col
-> NoDup l
-> (forall (y z : nat),
In (y,z) col
-> y <= length l)
-> (forall (y z : nat),
In (y,z) col
-> 0 < y)
-> no_fst_dup (coloring_renaming col l).
Proof.
induction 1;intros;simpl.
constructor.
constructor.
apply IHno_fst_dup.
assumption.
intros;apply (H2 y0 z);intuition.
intros;apply (H3 y0 z);intuition.
unfold not;intros.
assert (In (x,z) l0).
assert (rank l 1 (rename_vert_inv__aux (rename_fun l) x) = x).
apply in_rename_in_inv_aux.
apply (H2 x y);intuition.
assert (0 < x).
apply (H3 x y);intuition.
intuition.
assumption.
rewrite <-H5;apply in_coloring_renaming.
assumption.
intros;apply (H3 y0 z0);intuition.
intros;apply (H2 y0 z0);intuition.
assumption.
unfold not in H0;apply (H0 z);assumption.
Qed.
Lemma is_coloring_renaming :
forall (col : list (nat*nat)),
is_coloring my_chordal_gph col
-> is_coloring my_graph (coloring_renaming col (rev my_peo)).
Proof.
intros.
inversion H.
assert (peo my_peo my_graph).
unfold my_peo;apply peo_peo_search.
apply ax1.
assert (NoDup (rev my_peo)).
eapply NoDup_perm.
apply Permutation_rev.
eapply NoDup_perm.
inversion H6;eassumption.
apply strict_inc_NoDup;rewrite vertices_edges;apply is_strict_inc_vertices.
assert (forall (y z : nat), In (y,z) col -> 0 < y).
intros.
assert (In y (vertices my_chordal_gph)).
apply (proj2 (H0 y)).
exists z;assumption.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H10 in H9.
apply (positive_in_rename (rev my_peo) (rev my_peo)).
intuition.
rewrite eq_vert in H9;unfold rename_vert in H9;assumption.
assert (forall (y z : nat), In (y,z) col -> y <= length (rev my_peo)).
intros.
assert (In y (vertices my_chordal_gph)).
apply (proj2 (H0 y)).
exists z;assumption.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H11 in H10.
apply in_rename_vert_le_lth.
rewrite eq_vert in H10;unfold rename_vert in H10;assumption.
constructor.
split;intros.
assert (In (rank (rev my_peo) 1 x) (vertices (my_chordal_gph))).
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H11;rewrite eq_vert.
apply in_rename.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
assumption.
assumption.
assert (exists c : nat, In (rank (rev my_peo) 1 x,c) col).
apply (proj1 (H0 (rank (rev my_peo) 1 x)) H11).
inversion H12.
exists x0.
apply in_coloring.
assumption.
assumption.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
assumption.
inversion H10.
assert (In (rank (rev my_peo) 1 x,x0) col).
apply in_coloring_renaming.
assumption.
assumption.
assumption.
assumption.
assert (In x (rev my_peo)).
apply in_rank_in.
assert (vertices my_chordal_gph = rename_vert (rev my_peo)).
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H13;rewrite eq_vert;reflexivity.
unfold rename_vert in H13;rewrite <-H13.
apply (proj2 (H0 (rank (rev my_peo) 1 x))).
exists x0;assumption.
assumption.
eapply Permutation_in.
apply Permutation_sym;inversion H6;eassumption.
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
intros.
assert (In (rank (rev my_peo) 1 x,cx) col).
apply in_coloring_renaming;assumption.
assert (In (rank (rev my_peo) 1 y,cy) col).
apply in_coloring_renaming;assumption.
assert (In x (vertices my_graph) /\ In y (vertices my_graph)).
rewrite vertices_edges;apply in_vertices;assumption.
assert (In (rank (rev my_peo) 1 x,rank (rev my_peo) 1 y) new_edg).
unfold new_edg;rewrite <-my_peo_eq;apply in_rename_in_inv.
apply rank_le_lth.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
intuition.
apply rank_le_lth.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
intuition.
assert (0 < rank (rev my_peo) 1 x).
apply (H8 (rank (rev my_peo) 1 x) cx);assumption.
intuition.
assert (0 < rank (rev my_peo) 1 y).
apply (H8 (rank (rev my_peo) 1 y) cy);assumption.
intuition.
assumption.
rewrite in_rename_in_aux.
rewrite in_rename_in_aux.
assumption.
assumption.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
intuition.
assumption.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
intuition.
assert (In (rank (rev my_peo) 1 x,rank (rev my_peo) 1 y) (lto_edges new_edg)
\/ In (rank (rev my_peo) 1 y,rank (rev my_peo) 1 x) (lto_edges new_edg)).
apply correct_lto_edges_aux2.
assumption.
apply NoDup_rank_diff.
assumption.
assert (x < y).
eapply strict_in.
apply is_strict_ord_edges.
eassumption.
intuition.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
intuition.
eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
intuition.
decompose [or] H17.
eapply H1;eassumption.
assert (cx <> cy).
eapply H1;eassumption.
intuition.
intros;assert (In (rank (rev my_peo) 1 x,cx) col).
apply in_coloring_renaming;assumption.
apply (H2 (rank (rev my_peo) 1 x) cx);assumption.
apply no_fst_dup_conservation;assumption.
Qed.
Fixpoint coloring_renaming_inv (col : list (nat*nat)) (l : list nat) {struct col} : list (nat*nat) :=
match col with
| nil => nil
| (x,y) :: col' => (rank l 1 x,y) :: coloring_renaming_inv col' l
end.
Lemma max_color_renaming_inv_eq_aux :
forall (col : list (nat*nat)) (l : list nat) (acc : nat),
max_color_aux col acc = max_color_aux (coloring_renaming_inv col l) acc.
Proof.
induction col;intros;[|destruct a];simpl.
reflexivity.
destruct (le_gt_dec n0 acc);
apply IHcol.
Qed.
Lemma max_color_renaming_inv_eq :
forall (col : list (nat*nat)) (l : list nat),
max_color col = max_color (coloring_renaming_inv col l).
Proof.
intros;unfold max_color;apply max_color_renaming_inv_eq_aux.
Qed.
Lemma in_coloring_renaming_inv :
forall (col : list (nat*nat)) (l : list nat) (x y : nat),
NoDup l
-> In (x,y) col
-> In (rank l 1 x,y) (coloring_renaming_inv col l).
Proof.
induction col;intros;[|destruct a];simpl.
inversion H0.
simpl in H0;decompose [or] H0.
inversion H1;subst;left;reflexivity.
right;apply IHcol;assumption.
Qed.
Lemma in_rename_col_inv :
forall (col : list (nat*nat)) (l : list nat) (x y : nat),
NoDup l
-> In (x,y) (coloring_renaming_inv col l)
-> (forall (a b : nat),
In (a,b) col
-> In a l)
-> In (rename_vert_inv__aux (rename_fun l) x,y) col.
Proof.
induction col;intros;[|destruct a];simpl.
inversion H0.
simpl in H0;decompose [or] H0.
inversion H2;subst.
rewrite in_rename_in_aux.
left;reflexivity.
assumption.
apply (H1 n y);intuition.
right;apply IHcol.
assumption.
assumption.
intros;apply (H1 a b);intuition.
Qed.
Lemma rm_length_NoDup :
forall (l : list nat) (x k : nat),
NoDup l
-> length (remove eq_nat_dec x l) <= k
-> length l <= S k.
Proof.
induction l;intros.
intuition.
simpl in *.
destruct (eq_nat_dec x a).
assert (~In x l).
subst;inversion H;assumption.
rewrite remove_not_in in H0.
intuition.
assumption.
simpl in H0.
destruct k.
inversion H0.
apply le_S_n in H0.
apply le_n_S.
eapply IHl.
inversion H;assumption.
eassumption.
Qed.
Lemma inject_aux :
forall (col : list (nat*nat)) (l : list nat),
NoDup l
-> no_fst_dup col
-> (forall (y : nat),
In y l
-> exists z : nat, In (y,z) col)
-> length l <= length col.
Proof.
induction col;intros.
destruct l.
intuition.
assert (exists z : nat, In (n,z) nil).
apply (H1 n);intuition.
inversion H2;inversion H3.
destruct a;simpl.
assert (length (remove eq_nat_dec n l) <= length col).
apply IHcol.
apply NoDup_remove;assumption.
inversion H0;assumption.
intros.
assert (In y l).
eapply remove_in;eassumption.
assert (exists z : nat,In (y,z) ((n,n0) :: col)).
apply H1;assumption.
inversion H4;simpl in H5;decompose [or] H5.
inversion H6.
subst.
assert (~In y (remove eq_nat_dec y l)).
apply remove_In.
intuition.
exists x;assumption.
eapply rm_length_NoDup.
assumption.
eassumption.
Qed.
Lemma not_in_remove_nat_nat :
forall (l : list (nat*nat)) (x z : nat),
~In (x,z) l
-> remove nat_nat_eq_dec (x,z) l = l.
Proof.
induction l;intros.
simpl;reflexivity.
destruct a;simpl.
destruct (nat_nat_eq_dec (x,z) (n,n0)).
inversion e;subst;apply False_ind;intuition.
rewrite IHl.
reflexivity.
intuition.
Qed.
Lemma Permutation_col :
forall (col : list (nat*nat)) (x z : nat),
In (x,z) col
-> no_fst_dup col
-> Permutation col ((x,z) :: remove nat_nat_eq_dec (x,z) col).
Proof.
induction col;intros.
inversion H.
destruct a;simpl.
destruct (nat_nat_eq_dec (x,z) (n,n0)).
rewrite e;constructor.
rewrite not_in_remove_nat_nat.
apply Permutation_refl.
inversion H0;apply H5.
apply Permutation_trans with (l' := ((n,n0) :: (x,z) :: remove nat_nat_eq_dec (x,z) col)).
constructor.
apply IHcol.
simpl in H;decompose [or] H.
apply False_ind;intuition.
assumption.
inversion H0;assumption.
constructor.
Qed.
Lemma in_rm_couple :
forall (l : list (nat*nat)) (x y a b: nat),
In (x,y) (remove nat_nat_eq_dec (a,b) l)
-> In (x,y) l.
Proof.
induction l;intros.
inversion H.
destruct a;simpl in *.
destruct (nat_nat_eq_dec (a0,b) (n,n0)).
right;eapply IHl;eassumption.
simpl in H;decompose [or] H.
left;assumption.
right;eapply IHl;eassumption.
Qed.
Lemma only_in_rm_couple :
forall (l : list (nat*nat)) (a b x y : nat),
In (x,y) l
-> (x,y) <> (a,b)
-> In (x,y) (remove nat_nat_eq_dec (a,b) l).
Proof.
induction l;intros;simpl.
inversion H.
destruct a.
destruct (nat_nat_eq_dec (a0,b) (n,n0)).
apply IHl.
simpl in H;decompose [or] H.
rewrite H1 in e;apply False_ind;intuition.
assumption.
assumption.
simpl in H;decompose [or] H.
simpl;left;assumption.
simpl;right;apply IHl;assumption.
Qed.
Lemma no_fst_dup_rm :
forall (l : list (nat*nat)) (x y : nat),
no_fst_dup l
-> no_fst_dup (remove nat_nat_eq_dec (x,y) l).
Proof.
induction 1;intros;simpl.
constructor.
destruct (nat_nat_eq_dec (x,y) (x0,y0)).
assumption.
constructor.
assumption.
unfold not;intros.
unfold not in H0;apply (H0 z).
eapply in_rm_couple;eassumption.
Qed.
Lemma inject_coloring :
forall (col : list (nat*nat)) (l : list nat) (x : nat),
NoDup l
-> no_fst_dup col
-> length col = length l
-> (forall (y : nat),
In y l
-> exists z : nat, In (y,z) col)
-> (exists z : nat, In (x,z) col)
-> In x l.
Proof.
intros.
assert ({In x l}+{~In x l}).
apply In_dec;apply eq_nat_dec.
destruct H4.
assumption.
apply False_ind.
inversion H3.
assert (length l <= length (remove nat_nat_eq_dec (x,x0) col)).
apply inject_aux.
assumption.
apply no_fst_dup_rm;assumption.
intros.
assert (exists z : nat, In (y,z) col).
apply H2;assumption.
inversion H6.
exists x1.
apply only_in_rm_couple.
assumption.
unfold not;intro.
inversion H8;subst;apply False_ind;intuition.
assert (length col = length ((x,x0) :: remove nat_nat_eq_dec (x,x0) col)).
apply Permutation_length.
apply Permutation_col;assumption.
simpl in H6.
apply False_ind;intuition.
Qed.
Lemma in_rename_inv_rank :
forall (col : list (nat*nat)) (l : list nat) (x y : nat),
NoDup l
-> (forall (a b : nat),
In (a,b) col
-> In a l)
-> In x l
-> In (rank l 1 x,y) (coloring_renaming_inv col l)
-> In (x,y) col.
Proof.
induction col;intros.
inversion H2.
destruct a;simpl in *.
decompose [or] H2.
assert (n = x).
eapply rank_eq.
apply (H0 n n0);intuition.
assumption.
assumption.
inversion H3;intuition.
inversion H3;subst.
left;reflexivity.
right;eapply IHcol.
eassumption.
intros;apply (H0 a b);intuition.
assumption.
assumption.
Qed.
Lemma no_fst_dup_renaming_col_inv :
forall (col : list (nat*nat)) (l : list nat),
no_fst_dup col
-> NoDup l
-> (forall (x y : nat),
In (x,y) col
-> In x l)
-> no_fst_dup (coloring_renaming_inv col l).
Proof.
induction 1;intros;simpl.
constructor.
constructor.
apply IHno_fst_dup.
assumption.
intros;apply (H2 x0 y0);intuition.
unfold not;intros.
assert (In (x,z) l0).
eapply in_rename_inv_rank.
eassumption.
intros;apply (H2 a b);intuition.
apply (H2 x y);intuition.
assumption.
unfold not in H0;eapply H0;eassumption.
Qed.
Fixpoint remove_fst (l : list (nat*nat)) (x : nat) {struct l} :=
match l with
| nil => nil
| (a,b) :: l' => match (eq_nat_dec a x) with
| left _ => remove_fst l' x
| right _ => (a,b) :: remove_fst l' x
end
end.
Lemma in_rm_fst :
forall (l : list (nat*nat)) (x y z: nat),
In (x,y) (remove_fst l z)
-> In (x,y) l.
Proof.
induction l;intros;simpl.
inversion H.
destruct a;simpl in H.
destruct (eq_nat_dec n z).
right;eapply IHl;eassumption.
simpl in H;decompose [or] H.
left;assumption.
right;eapply IHl;eassumption.
Qed.
Lemma no_fst_dup_remove_fst :
forall (l : list (nat*nat)) (x : nat),
no_fst_dup l
-> no_fst_dup (remove_fst l x).
Proof.
induction 1;intros;simpl.
constructor.
destruct (eq_nat_dec x0 x).
assumption.
constructor.
assumption.
unfold not;intros.
assert (In (x0,z) l).
eapply in_rm_fst;eassumption.
unfold not in H0;apply (H0 z);assumption.
Qed.
Lemma in_rm_fst_diff :
forall (l : list (nat*nat)) (x y z : nat),
In (x,y) (remove_fst l z)
-> x <> z.
Proof.
induction l;intros;simpl.
inversion H.
destruct a;simpl in H.
destruct (eq_nat_dec n z).
eapply IHl;eassumption.
simpl in H;decompose [or] H.
inversion H0;subst;assumption.
eapply IHl;eassumption.
Qed.
Lemma remove_fst_not_in :
forall (l : list (nat*nat)) (x : nat),
(forall (z : nat),
~In (x,z) l)
-> remove_fst l x = l.
Proof.
induction l;intros;simpl.
reflexivity.
destruct a;simpl.
destruct (eq_nat_dec n x).
apply False_ind;unfold not in H;
subst;apply (H n0);intuition.
rewrite IHl.
reflexivity.
unfold not in *;intros.
apply (H z);intuition.
Qed.
Lemma length_no_fst_dup_remove_fst :
forall (l : list (nat*nat)) (x : nat),
no_fst_dup l
-> length l <= S (length (remove_fst l x)).
Proof.
induction l;intros;simpl.
intuition.
destruct a;simpl.
destruct (eq_nat_dec n x).
rewrite remove_fst_not_in.
intuition.
subst;inversion H;assumption.
simpl.
apply le_n_S.
apply IHl.
inversion H;assumption.
Qed.
Lemma coloring_length_aux :
forall (l : list nat) (col : list (nat*nat)),
(forall (x y : nat),
In (x,y) col
-> In x l)
-> no_fst_dup col
-> length col <= length l.
Proof.
induction l;intros.
destruct col.
intuition.
destruct p.
assert (In n nil).
apply (H n n0);intuition.
inversion H1.
simpl.
assert (length (remove_fst col a) <= length l).
apply IHl.
intros.
assert (In x (a :: l)).
apply (H x y).
eapply in_rm_fst;eassumption.
assert (x <> a).
eapply in_rm_fst_diff;eassumption.
simpl in H2;decompose [or] H2.
subst;apply False_ind;intuition.
assumption.
apply no_fst_dup_remove_fst;assumption.
assert (length col <= S (length (remove_fst col a))).
apply length_no_fst_dup_remove_fst;assumption.
intuition.
Qed.
Lemma coloring_length :
forall (col : list (nat*nat)) (g : graph),
is_coloring g col
-> length col = length (vertices g).
Proof.
intros.
inversion H.
assert (length (vertices g) <= length col).
apply inject_aux.
apply strict_inc_NoDup;rewrite vertices_edges;apply is_strict_inc_vertices.
assumption.
intros;apply (proj1 (H0 y));assumption.
assert (length col <= length (vertices g)).
apply coloring_length_aux.
intros.
apply (proj2 (H0 x)).
exists y;assumption.
assumption.
intuition.
Qed.
Lemma coloring_renaming_length :
forall (col : list (nat*nat)) (l : list nat),
length (coloring_renaming_inv col l) = length col.
Proof.
induction col;intros;simpl.
reflexivity.
destruct a;simpl.
apply eq_S;apply IHcol.
Qed.
Lemma rename_length_aux :
forall (l l' : list nat),
length (rename_vert_aux l (l' ++ l)) = length l.
Proof.
induction l;intros;simpl.
reflexivity.
apply eq_S.
assert (l'++ a :: l = (l'++ a :: nil) ++ l).
rewrite <-ass_app;intuition.
rewrite H.
apply IHl.
Qed.
Lemma rename_length :
forall (l : list nat),
length (rename_vert_aux l l) = length l.
Proof.
intros;assert (rename_vert_aux l l = rename_vert_aux l (nil ++ l)).
simpl;reflexivity.
rewrite H;apply rename_length_aux.
Qed.
Lemma is_coloring_renaming_inv :
forall (col : list (nat*nat)),
is_coloring my_graph col
-> is_coloring my_chordal_gph (coloring_renaming_inv col (rev my_peo)).
Proof.
intros;inversion H.
assert (peo my_peo my_graph).
unfold my_peo;apply peo_peo_search.
apply ax1.
assert (NoDup (rev my_peo)).
eapply NoDup_perm.
apply Permutation_rev.
eapply NoDup_perm.
inversion H6;eassumption.
apply strict_inc_NoDup;rewrite vertices_edges;apply is_strict_inc_vertices.
constructor.
assert (forall x : nat, In x (vertices my_chordal_gph)
-> exists c : nat, In (x,c) (coloring_renaming_inv col (rev my_peo))).
intros.
assert (In (rename_vert_inv__aux (rename_fun (rev my_peo)) x) (vertices my_graph)).
eapply Permutation_in.
apply Permutation_sym.
inversion H6;eassumption.
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
apply in_rank_in_inv.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H9 in H8;rewrite eq_vert in H8;
unfold rename_vert in H8;assumption.
assumption.
assert (exists c : nat, In (rename_vert_inv__aux (rename_fun (rev my_peo)) x,c) col).
apply (proj1 (H0 (rename_vert_inv__aux (rename_fun (rev my_peo)) x))).
assumption.
inversion H10;exists x0.
assert (rank (rev my_peo) 1 (rename_vert_inv__aux (rename_fun (rev my_peo)) x) = x ).
apply in_rename_in_inv_aux.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H12 in H8.
rewrite eq_vert in H8.
apply in_rename_vert_le_lth.
unfold rename_vert in H8;assumption.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H12 in H8.
rewrite eq_vert in H8.
assert (0 < x).
apply (positive_in_rename (rev my_peo) (rev my_peo)).
intuition.
unfold rename_vert in H8;assumption.
intuition.
assumption.
rewrite <-H12.
apply in_coloring_renaming_inv.
assumption.
assumption.
split.
apply H8.
apply inject_coloring.
apply strict_inc_NoDup;rewrite vertices_edges;apply is_strict_inc_vertices.
apply no_fst_dup_renaming_col_inv.
assumption.
assumption.
intros.
eapply Permutation_in.
eapply Permutation_rev.
eapply Permutation_in.
inversion H6;eassumption.
apply (proj2 (H0 x0)).
exists y;assumption.
rewrite coloring_renaming_length.
rewrite (coloring_length col my_graph).
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H9;rewrite eq_vert.
unfold rename_vert;rewrite rename_length.
apply Permutation_length.
apply Permutation_trans with (l' := my_peo).
inversion H6;assumption.
apply Permutation_rev.
assumption.
assumption.
intros.
assert (In (rename_vert_inv__aux (rename_fun (rev my_peo)) x,cx) col).
apply in_rename_col_inv.
assumption.
assumption.
intros;apply in_vert_in_rev_mypeo.
apply (proj2 (H0 a)).
exists b;assumption.
assert (In (rename_vert_inv__aux (rename_fun (rev my_peo)) y,cy) col).
apply in_rename_col_inv.
assumption.
assumption.
intros;apply in_vert_in_rev_mypeo.
apply (proj2 (H0 a)).
exists b;assumption.
assert (edges my_chordal_gph = my_chordal_gph_edg).
intuition.
rewrite H13 in H8.
unfold my_chordal_gph_edg in H8.
assert (In (x,y) new_edg \/ In (y,x) new_edg).
apply correct_lto_edges1;assumption.
decompose [or] H14.
eapply H1.
eapply in_rename_in.
eassumption.
intros;assert (In a (vertices my_graph) /\
In b (vertices my_graph)).
rewrite vertices_edges;eapply in_vertices;assumption.
decompose[and] H17;split;
apply in_vert_in_rev_mypeo;assumption.
unfold new_edg in H15;eassumption.
assumption.
assumption.
assert (cx <> cy).
eapply H1.
eapply in_rename_in.
eassumption.
intros;assert (In a (vertices my_graph) /\
In b (vertices my_graph)).
rewrite vertices_edges;eapply in_vertices;assumption.
decompose [and] H17;split;
apply in_vert_in_rev_mypeo;assumption.
unfold not in H15;eassumption.
assumption.
assumption.
apply sym_not_eq;assumption.
intros;assert (In (rename_vert_inv__aux (rename_fun (rev my_peo)) x,cx) col).
apply in_rename_col_inv.
assumption.
assumption.
intros.
apply in_vert_in_rev_mypeo.
apply (proj2 (H0 a)).
exists b;assumption.
eapply H2;eassumption.
apply no_fst_dup_renaming_col_inv.
assumption.
assumption.
intros.
apply in_vert_in_rev_mypeo.
apply (proj2 (H0 x)).
exists y;assumption.
Qed.
Lemma coloring_optimality :
forall (col : list (nat*nat)),
is_coloring my_graph col
-> max_color (coloring_renaming (graph_coloring my_chordal_gph) (rev my_peo))
<= max_color col.
Proof.
intros.
rewrite <-(max_color_col_rename (graph_coloring my_chordal_gph) (rev my_peo)).
assert (my_chordal_gph = gph my_chordal_graph).
intuition.
rewrite (max_color_renaming_inv_eq col (rev my_peo)).
rewrite H0 in *;apply graph_coloring_optimality.
apply is_coloring_renaming_inv;assumption.
Qed.
Definition chordal_graph_coloring_fun : list (nat*nat) :=
coloring_renaming (graph_coloring my_chordal_gph) (rev my_peo).
Extraction "ml_coloring" chordal_graph_coloring_fun.