diff options
Diffstat (limited to 'backend/IRCColoring.v')
| -rwxr-xr-x | backend/IRCColoring.v | 847 |
1 files changed, 847 insertions, 0 deletions
diff --git a/backend/IRCColoring.v b/backend/IRCColoring.v new file mode 100755 index 00000000..5efeed7b --- /dev/null +++ b/backend/IRCColoring.v @@ -0,0 +1,847 @@ +Require Import Recdef. +Require Import IRC. +Require Import FSetInterface. +Require Import Edges. +Require Import Interference_adjacency. +Require Import IRC_graph. +Require Import Conservative_criteria. +Require Import InterfGraphMapImp. +Require Import Graph_Facts. +Require Import IRC_Graph_Functions. +Require Import WS. + +Import Edge RegFacts Props OTFacts. + +Module MapFacts := FMapFacts.Facts ColorMap. + +Definition proper_coloring_1 (col : Coloring) g := forall e x y, +interf_edge e -> +In_graph_edge e g -> +OptionReg.eq (col (fst_ext e)) (Some x) -> +OptionReg.eq (col (snd_ext e)) (Some y) -> +~Register.eq x y. + +Definition proper_coloring_2 (col : Coloring) g := forall x y, +OptionReg.eq (col x) (Some y) -> In_graph x g. + +Definition proper_coloring_3 (col : Coloring) palette := forall x y, +OptionReg.eq (col x) (Some y) -> VertexSet.In y palette. + +Definition proper_coloring col g palette := +proper_coloring_1 col g /\ proper_coloring_2 col g /\ proper_coloring_3 col palette. + +Lemma diff_empty_sub : forall s1 s2, +VertexSet.Empty (VertexSet.diff s1 s2) -> +VertexSet.Subset s1 s2. + +Proof. +intros s1 s2 H. +intros a H0. +destruct (In_dec a s2). +assumption. +elim (H a). +apply (VertexSet.diff_3 H0 n). +Qed. + +Lemma interf_in_forbidden : forall x y col g c, +Interfere x y g -> +OptionReg.eq (map_to_coloring col y) (Some c) -> +VertexSet.In c (forbidden_colors x col g). + +Proof. +intros x y col g c H H0. +unfold forbidden_colors. +unfold Interfere in H. rewrite <-in_interf in H. +generalize (interf_adj_comm _ _ _ H). intro H1. +generalize (VertexSet.elements_1 H1);clear H1;intro H1. +rewrite VertexSet.fold_1. +induction (VertexSet.elements (interference_adj x g)). +inversion H1. +rewrite monad_fold. +inversion H1;subst. +unfold map_to_coloring in H0. +inversion H0;subst. +rewrite (MapFacts.find_o col H3) in H2. +rewrite <-H2. +simpl;apply VertexSet.add_1. +assumption. +destruct (ColorMap.find a col);[apply VertexSet.add_2|];apply IHl;assumption. +Qed. + +Lemma available_coloring_1 : forall col x g, +proper_coloring (map_to_coloring col) (irc_g g) (pal g) -> +In_graph x (irc_g g) -> +proper_coloring (map_to_coloring (available_coloring g x col)) (irc_g g) (pal g). + +Proof. +intros col x ircg H HH. unfold available_coloring. +set (palette := pal ircg) in *. set (g := irc_g ircg) in *. +case_eq (VertexSet.choose (VertexSet.diff palette (forbidden_colors x col g))). +intros c H1. +generalize H1;intro H0. +unfold proper_coloring. +split. +unfold proper_coloring_1. +intros e x' y' H2 H3 H4 H5. +destruct (Register.eq_dec x (fst_ext e)). +unfold map_to_coloring in H4;unfold map_to_coloring in H5. +rewrite MapFacts.add_eq_o in H4. +rewrite MapFacts.add_neq_o in H5. +generalize (VertexSet.choose_1 H1);clear H1;intro H1. +generalize (VertexSet.diff_1 H1);intro H6. +generalize (VertexSet.diff_2 H1);intro H7;clear H1. +assert (Interfere x (snd_ext e) g) as Hinterf. +unfold Interfere. +assert (eq (fst_ext e, snd_ext e,None) (x, snd_ext e, None)). +Eq_eq. +rewrite (edge_eq e) in H3. +rewrite H2 in H3. +rewrite H1 in H3;assumption. +generalize (interf_in_forbidden x (snd_ext e) col g y' Hinterf H5);intro H1. +intro H8. +inversion H4;subst. +generalize (Register.eq_trans H11 H8);clear H11 H8;intro H8. +rewrite H8 in H7. +elim (H7 H1). +intro Heq. +elim (In_graph_edge_diff_ext _ _ H3). +apply (Register.eq_trans (Register.eq_sym Heq) e0). +assumption. +destruct (Register.eq_dec x (snd_ext e)). +unfold map_to_coloring in H4;unfold map_to_coloring in H5. +rewrite MapFacts.add_eq_o in H5. +rewrite MapFacts.add_neq_o in H4. +generalize (VertexSet.choose_1 H1);clear H1;intro H1. +generalize (VertexSet.diff_1 H1);intro H6. +generalize (VertexSet.diff_2 H1);intro H7;clear H1. +assert (Interfere x (fst_ext e) g) as Hinterf. +unfold Interfere. +rewrite (edge_eq e) in H3. rewrite H2 in H3. +assert (eq (fst_ext e, snd_ext e,None) (x, fst_ext e, None)) by Eq_comm_eq. +rewrite H1 in H3;assumption. +generalize (interf_in_forbidden x (fst_ext e) col g x' Hinterf H4);intro H1. +intro H8. +inversion H5;subst. +generalize (Register.eq_trans H11 (Register.eq_sym H8));clear H11 H8;intro H8. +rewrite H8 in H7. +elim (H7 H1). +intro Heq. +elim (In_graph_edge_diff_ext _ _ H3). +apply (Register.eq_trans (Register.eq_sym e0) Heq). +assumption. +unfold map_to_coloring in H4;unfold map_to_coloring in H5. +rewrite MapFacts.add_neq_o in H5. +rewrite MapFacts.add_neq_o in H4. +unfold proper_coloring in H;destruct H as [H _]. +unfold proper_coloring_1 in H. +apply (H e);assumption. +assumption. +assumption. +split. +unfold proper_coloring in *. +destruct H as [_ H];destruct H as [H _]. +unfold proper_coloring_2 in *. +intros x' y' H2. +destruct (Register.eq_dec x x'). +unfold map_to_coloring in H2. +rewrite e in HH;assumption. +apply (H x' y'). +unfold map_to_coloring in H2. +rewrite MapFacts.add_neq_o in H2. +assumption. +assumption. +unfold proper_coloring in *. +do 2 destruct H as [_ H]. +unfold proper_coloring_3 in *. +intros x' y' H2. +destruct (Register.eq_dec x x'). +unfold map_to_coloring in H2. +generalize (VertexSet.choose_1 H1);clear H1;intro H1. +generalize (VertexSet.diff_1 H1);intro H3. +rewrite MapFacts.add_eq_o in H2. +inversion H2;subst. +rewrite H6 in H3;assumption. +assumption. +apply (H x' y'). +unfold map_to_coloring in H2. +rewrite MapFacts.add_neq_o in H2. +assumption. +assumption. +auto. +Qed. + +Lemma complete_coloring_1 : forall col e g, +In_graph_edge e g -> +ColorMap.find (snd_ext e) col = None -> +OptionReg.eq +(map_to_coloring (complete_coloring e col) (snd_ext e)) +(map_to_coloring (complete_coloring e col) (fst_ext e)). + +Proof. +intros col e g HH Hin;unfold complete_coloring. +case_eq (ColorMap.find (fst_ext e) col). +intros r H. +unfold map_to_coloring. +rewrite MapFacts.add_eq_o. +rewrite MapFacts.add_neq_o. +rewrite H;apply OptionReg.eq_refl. +apply (In_graph_edge_diff_ext _ _ HH). +apply Register.eq_refl. +intro H0. +unfold map_to_coloring. +rewrite Hin;rewrite H0;apply OptionReg.eq_refl. +Qed. + +Lemma complete_coloring_2 : forall col e x, +~Register.eq (snd_ext e) x -> +OptionReg.eq +(map_to_coloring (complete_coloring e col) x) +(map_to_coloring col x). + +Proof. +intros col e x H. +unfold complete_coloring. +destruct (ColorMap.find (fst_ext e) col). +unfold map_to_coloring. +rewrite MapFacts.add_neq_o. +apply OptionReg.eq_refl. +assumption. +apply OptionReg.eq_refl. +Qed. + +Definition compat_col col := forall x y, +Register.eq x y -> OptionReg.eq (col x) (col y). + +Lemma compat_IRC : forall g palette, compat_col (IRC g palette). + +Proof. +unfold IRC. +unfold compat_col. +intros g palette x y H. +unfold map_to_coloring. +rewrite MapFacts.find_o with (y := y). +apply OptionReg.eq_refl. +assumption. +Qed. + +Lemma compat_complete : forall col e, +compat_col (map_to_coloring col) -> +compat_col (map_to_coloring (complete_coloring e col)). + +Proof. +unfold compat_col;intros col e H. +intros x y Heq;generalize (H x y Heq);clear H;intro H. +unfold complete_coloring. +destruct (ColorMap.find (fst_ext e) col). +unfold map_to_coloring. +destruct (Register.eq_dec x (snd_ext e)). +rewrite MapFacts.add_eq_o. +rewrite MapFacts.add_eq_o. +apply OptionReg.eq_refl. +apply (Register.eq_trans (Register.eq_sym e0) Heq). intuition. +rewrite MapFacts.add_neq_o. +rewrite MapFacts.add_neq_o. +assumption. +intro Helim;elim n. +apply (Register.eq_trans Heq (Register.eq_sym Helim)). +intro H0;elim n;auto. +assumption. +Qed. + +Lemma colored_complete_diff_colored : forall e col, +~Register.eq (snd_ext e) (fst_ext e) -> +OptionReg.eq (map_to_coloring (complete_coloring e col) (fst_ext e)) (map_to_coloring col (fst_ext e)). + +Proof. +intros e col H. +unfold complete_coloring. +case_eq (ColorMap.find (fst_ext e) col). +intros r H0. +unfold map_to_coloring. +rewrite MapFacts.add_neq_o. +apply OptionReg.eq_refl. +assumption. +intro H0. +apply OptionReg.eq_refl. +Qed. + +Lemma complete_coloring_coloring : forall col e g Hin Haff, +~VertexSet.In (snd_ext e) (precolored (irc_g g)) -> +proper_coloring (map_to_coloring col) (merge e (irc_g g) Hin Haff) (pal g) -> +conservative_coalescing_criteria e (irc_g g) (irc_k g) = true -> +compat_col (map_to_coloring col) -> +proper_coloring (map_to_coloring (complete_coloring e col)) (irc_g g) (pal g). + +Proof. +unfold proper_coloring;unfold proper_coloring_1; +unfold proper_coloring_2;unfold proper_coloring_3. +intros col e ircg H1 Haff Hpre H H0 Hcompat. +set (g := irc_g ircg) in *. set (palette := pal ircg) in *. +rewrite <-(Hk ircg) in *. +destruct H as [H HH];destruct HH as [HH HHH]. +split. +intros e' x' y' H2 H3 H4 H5. +apply (H (redirect (snd_ext e) (fst_ext e) e')). +unfold interf_edge;rewrite redirect_weight_eq;assumption. +apply In_merge_interf_edge. +assumption. +assumption. +(*intro Heq. +generalize (get_weight_m _ _ Heq);intro H6. +rewrite H2 in H6. +unfold aff_edge in Haff. +destruct Haff as [w Haff]. +rewrite Haff in H6. +inversion H6. +assumption.*) +destruct e' as [e' we'];destruct e' as [e'1 e'2]. +unfold redirect. +unfold interf_edge in H2;simpl in H2;subst. +change_rewrite. +destruct (OTFacts.eq_dec e'1 (snd_ext e));change_rewrite. +generalize (compat_complete col e);intro Hcompat2. +generalize (Hcompat2 Hcompat _ _ r);intro H7. +generalize (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H4) H7); +clear H7;intro H7. +assert (ColorMap.find (snd_ext e) col = None) as Hn. +case_eq (ColorMap.find (snd_ext e) col). +clear H3 H4 H5 r Hcompat2 H7. +intros r H8. +generalize (HH (snd_ext e) r);intro Helim. +unfold map_to_coloring in Helim. +rewrite H8 in Helim. +generalize (Helim (OptionReg.eq_refl _));clear Helim;intro Helim. +rewrite In_merge_vertex in Helim. destruct Helim. elim H3. auto. +auto. +generalize (complete_coloring_1 col e g H1 Hn);intro H8. +generalize (OptionReg.eq_trans _ _ _ H7 H8);intro H9. +generalize (complete_coloring_2 col e (fst_ext e) (In_graph_edge_diff_ext _ _ H1)). +intro H10. +generalize (OptionReg.eq_trans _ _ _ H9 H10);intro H11. +apply OptionReg.eq_sym;assumption. +destruct (OTFacts.eq_dec e'2 (snd_ext e));change_rewrite; +apply OptionReg.eq_trans with (y := (map_to_coloring (complete_coloring e col) e'1)); +[apply OptionReg.eq_sym;apply complete_coloring_2;intuition|assumption| +apply OptionReg.eq_sym;apply complete_coloring_2;intuition|assumption]. +destruct e' as [e' we'];destruct e' as [e'1 e'2]. +unfold redirect;change_rewrite. +unfold interf_edge in H2;simpl in H2;subst. +destruct (OTFacts.eq_dec e'1 (snd_ext e));change_rewrite. +destruct (Register.eq_dec (snd_ext e) e'2). +elim (In_graph_edge_diff_ext _ _ H3). +apply (Register.eq_trans (Register.eq_sym e0) (Register.eq_sym r)). +generalize (complete_coloring_2 col e e'2 n);intro H6. +apply OptionReg.eq_trans with (y := map_to_coloring (complete_coloring e col) e'2). +apply OptionReg.eq_sym;assumption. +assumption. +destruct (OTFacts.eq_dec e'2 (snd_ext e));change_rewrite. +generalize (compat_complete col e);intro Hcompat2. +generalize (Hcompat2 Hcompat _ _ r);intro H7. +generalize (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H5) H7); +clear H7;intro H7. +assert (ColorMap.find (snd_ext e) col = None) as Hn. +case_eq (ColorMap.find (snd_ext e) col). +clear H3 H4 H5 r Hcompat2 H7. +intros r H8. +generalize (HH (snd_ext e) r);intro Helim. +unfold map_to_coloring in Helim. +rewrite H8 in Helim. +generalize (Helim (OptionReg.eq_refl _));clear Helim;intro Helim. +rewrite In_merge_vertex in Helim. destruct Helim. elim H3. auto. +auto. +generalize (complete_coloring_1 col e g H1 Hn);intro H8. +generalize (OptionReg.eq_trans _ _ _ H7 H8);intro H9. +generalize (complete_coloring_2 col e (fst_ext e) (In_graph_edge_diff_ext _ _ H1)). +intro H10. +generalize (OptionReg.eq_trans _ _ _ H9 H10);intro H11. +apply OptionReg.eq_sym;assumption. +change (snd_ext (e'1,e'2,None)) with e'2. +assert (~Register.eq (snd_ext e) e'2) by intuition. +generalize (complete_coloring_2 col e e'2 H2);intro H6. +apply OptionReg.eq_trans with (y := map_to_coloring (complete_coloring e col) e'2). +apply OptionReg.eq_sym;assumption. +assumption. +(* second step *) +split. +intros x y H2. +destruct (Register.eq_dec x (snd_ext e)). +rewrite e0. +apply (In_graph_edge_in_ext _ _ H1). +assert (In_graph x (merge e g H1 Haff)). +apply HH with (y := y). +apply OptionReg.eq_trans with (y := map_to_coloring (complete_coloring e col) x). +apply OptionReg.eq_sym. +apply complete_coloring_2. +intuition. +assumption. +rewrite In_merge_vertex in H3. intuition. +(* third step *) +intros x y H2. +destruct (Register.eq_dec x (snd_ext e)). +assert (ColorMap.find (snd_ext e) col = None) as Hn. +case_eq (ColorMap.find (snd_ext e) col). +intros r H8. +generalize (HH (snd_ext e) r);intro Helim. +unfold map_to_coloring in Helim. +rewrite H8 in Helim. +generalize (Helim (OptionReg.eq_refl _));clear Helim;intro Helim. +rewrite In_merge_vertex in Helim. destruct Helim. elim H4. auto. +auto. +generalize (complete_coloring_1 col e g H1 Hn);intro H3. +generalize (complete_coloring_2 col e (fst_ext e) (In_graph_edge_diff_ext _ _ H1)). +intro H4. +generalize (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H4) (OptionReg.eq_sym _ _ H3)). +clear H3 H4;intro H3. +generalize (compat_complete col e Hcompat);intro Hcompat2. +generalize (Hcompat2 _ _ e0). +intro H4. +generalize (OptionReg.eq_trans _ _ _ H3 (OptionReg.eq_sym _ _ H4)). +clear H3 H4;intro H3. +apply HHH with (x:= fst_ext e). +apply (OptionReg.eq_trans _ _ _ H3 H2). +assert (~Register.eq (snd_ext e) x) by intuition. +generalize (complete_coloring_2 col e x H3). +intro H4. +apply HHH with (x:= x). +apply (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H4) H2). +Qed. + +Lemma interf_edge_in_delete_preference : forall x e g H, +interf_edge e -> +In_graph_edge e g -> +In_graph_edge e (delete_preference_edges x g H). + +Proof. +intros x e g HH H H0. +generalize (proj2 (In_graph_interf_edge_in_IE _ _) (conj H H0));intro H1. +rewrite In_delete_preference_edges_edge. +split. assumption. +intro. destruct H2. destruct H2. congruence. +Qed. + +Lemma coloring_delete_preference : forall col x g H palette, +proper_coloring col (delete_preference_edges x g H) palette -> +proper_coloring col g palette. + +Proof. +unfold proper_coloring;unfold proper_coloring_1; +unfold proper_coloring_2;unfold proper_coloring_3. +intros col x g Hdp palette H. +destruct H as [H HH];destruct HH as [HH HHH]. +split. +intros e x' y' H0 H1 H2 H3. +apply H with (e:=e). +assumption. +apply interf_edge_in_delete_preference;assumption. +assumption. +assumption. +split. +intros x' y' H0. rewrite <-(In_delete_preference_edges_vertex x' x g Hdp). +apply (HH x' y');auto. +assumption. +Qed. + +Lemma proper_remove_proper : forall col g x palette, +proper_coloring col (remove_vertex x g) palette -> +compat_col col -> +proper_coloring col g palette. + +Proof. +intros col g x palette H Hcompat. +unfold proper_coloring in *;unfold proper_coloring_1 in *; +unfold proper_coloring_2 in *;unfold proper_coloring_3 in *. +destruct H as [H HH];destruct HH as [HH HHH]. +split. +intros e x' y' H0 H1 H2 H3. +destruct (incident_dec e x). +destruct H4. +generalize (Hcompat _ _ H4);intro H5. +generalize (OptionReg.eq_trans _ _ _ H5 H2);clear H5;intro H5. +generalize (HH _ _ H5). intro. +rewrite In_remove_vertex in H6. destruct H6. elim H7. auto. +generalize (Hcompat _ _ H4);intro H5. +generalize (OptionReg.eq_trans _ _ _ H5 H3);clear H5;intro H5. +generalize (HH _ _ H5). intro. +rewrite In_remove_vertex in H6. destruct H6. elim H7. auto. +apply H with (e:=e); auto. +rewrite In_remove_edge; auto. +split. +intros x' y' H0. +generalize (HH x' y' H0);intro H1. +rewrite In_remove_vertex in H1. intuition. +assumption. +Qed. + +Section Fold_Facts. + +Variable A : Type. + +Lemma fold_left_compat_map : forall (f : ColorMap.t Register.t -> A -> ColorMap.t Register.t) l e e', +ColorMap.Equal e e' -> +(forall e1 e2 a, ColorMap.Equal e1 e2 -> ColorMap.Equal (f e1 a) (f e2 a)) -> +ColorMap.Equal (fold_left f l e) (fold_left f l e'). + +Proof. +intros f l. +induction l;simpl. +auto. +intros e e' H H0 H1. +apply (IHl (f e a) (f e' a)). +apply H0;assumption. +assumption. +Qed. + +End Fold_Facts. + +Lemma empty_coloring_simpl : forall l a, +NoDupA Register.eq (a :: l) -> +ColorMap.Equal (fold_left (fun (a0 : ColorMap.t VertexSet.elt) (e : VertexSet.elt) => + ColorMap.add e e a0) (a :: l) (ColorMap.empty Register.t)) + (ColorMap.add a a ( + fold_left (fun (a0 : ColorMap.t VertexSet.elt) (e : VertexSet.elt) => + ColorMap.add e e a0) l (ColorMap.empty Register.t))). + +Proof. +intro l;generalize (ColorMap.empty Register.t). +induction l;simpl;intros. +unfold ColorMap.Equal;auto. +assert (ColorMap.Equal (ColorMap.add a a (ColorMap.add a0 a0 t0)) + (ColorMap.add a0 a0 (ColorMap.add a a t0))). +unfold ColorMap.Equal. +intro y. +destruct (Register.eq_dec a0 a). +inversion H;subst. +elim H2. +left;auto. +destruct (Register.eq_dec y a). +destruct (Register.eq_dec y a0). +elim (n (Register.eq_trans (Register.eq_sym e0) e)). +rewrite MapFacts.add_eq_o. +rewrite MapFacts.add_neq_o. +rewrite MapFacts.add_eq_o. +reflexivity. +intuition. +intro Hneq;elim n0;auto. +intuition. +rewrite MapFacts.add_neq_o. +destruct (Register.eq_dec a0 y). +rewrite MapFacts.add_eq_o. +rewrite MapFacts.add_eq_o. +reflexivity. +assumption. +assumption. +rewrite MapFacts.add_neq_o. +rewrite MapFacts.add_neq_o. +rewrite MapFacts.add_neq_o. +reflexivity. +intro Hneq;elim n0;auto. +assumption. +assumption. +intro Hneq;elim n0;auto. +rewrite (fold_left_compat_map _ + (fun (a1 : ColorMap.t VertexSet.elt) (e : VertexSet.elt) => ColorMap.add e e a1) l _ _ H0). +simpl in IHl;apply IHl. +constructor. +inversion H;subst. +intro H5;elim H3. +right;auto. +inversion H;subst. +inversion H4;subst;assumption. +intros e1 e2 a1 H1. +unfold ColorMap.Equal;intro y. +destruct (Register.eq_dec a1 y). +rewrite MapFacts.add_eq_o. +rewrite MapFacts.add_eq_o. +reflexivity. +assumption. +assumption. +rewrite MapFacts.add_neq_o. +rewrite MapFacts.add_neq_o. +apply H1. +assumption. +assumption. +Qed. + +Lemma map_to_coloring_ext : forall c1 c2 g palette, +ColorMap.Equal c2 c1 -> +proper_coloring (map_to_coloring c1) g palette -> +proper_coloring (map_to_coloring c2) g palette. + +Proof. +unfold proper_coloring;unfold proper_coloring_1; +unfold proper_coloring_2;unfold proper_coloring_3. +intros c1 c2 g palette H H0. +destruct H0 as [H0 H1];destruct H1 as [H1 H2]. +split. +intros e x y H3 H4 H5 H6. +apply (H0 e);try assumption. +unfold ColorMap.Equal in H. +apply OptionReg.eq_trans with (y := (map_to_coloring c2 (fst_ext e))). +unfold map_to_coloring. +rewrite H. +apply OptionReg.eq_refl. +assumption. +apply OptionReg.eq_trans with (y := (map_to_coloring c2 (snd_ext e))). +unfold map_to_coloring. +rewrite H. +apply OptionReg.eq_refl. +assumption. +split. +intros x y H3. +apply (H1 x y). +apply OptionReg.eq_trans with (y := (map_to_coloring c2 x)). +unfold map_to_coloring. +rewrite H. +apply OptionReg.eq_refl. +assumption. +intros x y H3. +apply (H2 x y). +apply OptionReg.eq_trans with (y := (map_to_coloring c2 x)). +unfold map_to_coloring. +rewrite H. +apply OptionReg.eq_refl. +assumption. +Qed. + +Lemma compat_map_to_coloring : forall c1 c2 x, +ColorMap.Equal c1 c2 -> +OptionReg.eq (map_to_coloring c1 x) (map_to_coloring c2 x). + +Proof. +intros c1 c2 x H;unfold map_to_coloring; +unfold ColorMap.Equal in H. +rewrite H;apply OptionReg.eq_refl. +Qed. + +Lemma proper_coloring_empty_aux : forall g x, +OptionReg.eq (precoloring g x) (Some x) \/ +OptionReg.eq (precoloring g x) None. + +Proof. +intros g x. +unfold precoloring, precoloring_map. +rewrite VertexSet.fold_1. + +assert (NoDupA Register.eq (VertexSet.elements (precolored g))) as HNoDup by + (apply RegFacts.NoDupA_elements). +induction (VertexSet.elements (precolored g)). +simpl. +right;unfold map_to_coloring;rewrite MapFacts.empty_o. +apply OptionReg.eq_refl. +(* induction case *) +generalize (empty_coloring_simpl l a HNoDup);intro H0. +inversion HNoDup;subst. +generalize (IHl H3);clear IHl H2 H3;intro IHl. +destruct IHl. +left. +generalize (compat_map_to_coloring _ _ x H0);clear H0;intro H0. +apply (OptionReg.eq_trans _ _ _ H0). +destruct (Register.eq_dec a x). +unfold map_to_coloring. +rewrite MapFacts.add_eq_o. +constructor;assumption. +assumption. +unfold map_to_coloring. +rewrite MapFacts.add_neq_o. +apply H. +assumption. +destruct (Register.eq_dec a x). +left. +generalize (compat_map_to_coloring _ _ x H0);clear H0;intro H0. +apply (OptionReg.eq_trans _ _ _ H0). +unfold map_to_coloring. +rewrite MapFacts.add_eq_o. +constructor;assumption. +assumption. +right. +generalize (compat_map_to_coloring _ _ x H0);clear H0;intro H0. +apply (OptionReg.eq_trans _ _ _ H0). +unfold map_to_coloring. +rewrite MapFacts.add_neq_o. +apply H. +assumption. +Qed. + +Lemma in_empty_coloring_in_precolored : forall x g y, +OptionReg.eq (precoloring g x)(Some y) -> +VertexSet.In x (precolored g). + +Proof. +intros x g y H. unfold precoloring, precoloring_map in H. +rewrite VertexSet.fold_1 in H. +generalize (VertexSet.elements_2);intro H0. +generalize (H0 (precolored g));clear H0;intro H0. +assert (NoDupA Register.eq (VertexSet.elements (precolored g))) as HNoDup by + (apply RegFacts.NoDupA_elements). +induction (VertexSet.elements (precolored g)). +simpl in H. +unfold map_to_coloring in H;rewrite MapFacts.empty_o in H. +inversion H. +destruct (Register.eq_dec a x). +apply H0. +left; intuition. +apply IHl. +generalize (empty_coloring_simpl l a HNoDup);intro H1. +generalize (compat_map_to_coloring _ _ x H1);clear H1;intro H1. +unfold map_to_coloring in H1. +rewrite MapFacts.add_neq_o in H1. +apply (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H1)). +clear H1 IHl. +assumption. +assumption. +intros;apply H0;right;auto. +inversion HNoDup;auto. +Qed. + +Lemma proper_coloring_pre_inv : forall g x, +VertexSet.In x (precolored g) -> +OptionReg.eq (precoloring g x) (Some x). + +Proof. +intros g x H. unfold precoloring, precoloring_map. +rewrite VertexSet.fold_1. +generalize (VertexSet.elements_1);intro H0. +generalize (H0 (precolored g) x);clear H0;intro H0. +assert (NoDupA Register.eq (VertexSet.elements (precolored g))) as HNoDup by + (apply RegFacts.NoDupA_elements). +induction (VertexSet.elements (precolored g)). +generalize (H0 H). intro. inversion H1. +generalize (empty_coloring_simpl l a HNoDup);intro H1. simpl in *. +generalize (compat_map_to_coloring _ _ x H1). intro. +unfold map_to_coloring in H2. +destruct (Register.eq_dec x a). + rewrite MapFacts.add_eq_o in H2. +apply (OptionReg.eq_trans _ _ _ H2). +constructor. apply Register.eq_sym. auto. +apply Register.eq_sym. auto. +rewrite (MapFacts.add_neq_o) in H2. apply (OptionReg.eq_trans _ _ _ H2). +apply IHl. clear H1 H2. +intros. generalize (H0 H1). intro. +inversion H2; subst. elim n. auto. +auto. +inversion HNoDup;auto. +auto. +Qed. + +Lemma proper_coloring_empty : forall g palette, +VertexSet.Subset (precolored g) palette -> +proper_coloring (precoloring g) g palette. + +Proof. +intros g palette H. +unfold proper_coloring;unfold proper_coloring_1; +unfold proper_coloring_2;unfold proper_coloring_3. +split;[|split]. +intros e x y H0 H1 H2 H3 H4. +destruct (proper_coloring_empty_aux g (fst_ext e)); +generalize (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H2) H5); +clear H2 H5;intro H2. +destruct (proper_coloring_empty_aux g (snd_ext e)); +generalize (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H3) H5); +clear H3 H5;intro H3. +elim (In_graph_edge_diff_ext _ _ H1). +inversion H2;inversion H3;subst. +apply (Register.eq_trans (Register.eq_sym H10) (Register.eq_trans (Register.eq_sym H4) H7)). +inversion H3. +inversion H2. +intros x y H0. +assert (VertexSet.In x (precolored g)). +apply in_empty_coloring_in_precolored with (y := y). assumption. +rewrite precolored_equiv in H1. intuition. +intros x y H0. +apply H. +destruct (proper_coloring_empty_aux g x); +generalize (OptionReg.eq_trans _ _ _ (OptionReg.eq_sym _ _ H1) H0); +intro H2;inversion H2;subst. +rewrite <-H5. +apply in_empty_coloring_in_precolored with (y := x). +assumption. +Qed. + +Lemma proper_coloring_IRC_map : forall gp, +VertexSet.Subset (precolored (irc_g gp)) (pal gp) -> +proper_coloring (map_to_coloring (IRC_map gp)) (irc_g gp) (pal gp). + +Proof. +intros gp Hpre. +functional induction IRC_map gp;simpl in *. + +(* simplify *) +generalize (simplify_inv _ _ e). intro. +generalize (simplify_inv2 _ _ e). intro. destruct H0. simpl in H0. +apply available_coloring_1. +apply proper_remove_proper with (x:=r). +rewrite H0 in *. unfold simplify_irc in *. simpl in *. +apply IHt0. rewrite precolored_remove_vertex. +unfold VertexSet.Subset. intros. apply Hpre. apply (VertexSet.remove_3 H1). + +unfold compat_col. +intros. unfold map_to_coloring. +rewrite (MapFacts.find_o _ H1). apply OptionReg.eq_refl. + +apply (In_simplify_props _ _ _ _ _ _ _ _ (VertexSet.choose_1 H) (refl_equal _) (HWS_irc g)). + +(*coalesce*) +generalize (coalesce_inv _ _ e0). intro. +generalize (coalesce_inv_2 _ _ e0). intro. +destruct H0. destruct H0. simpl in *. + +assert (forall e', EdgeSet.In e' (get_movesWL (irc_wl g)) -> In_graph_edge e' (irc_g g)). +intros. generalize (In_move_props _ _ _ _ _ _ _ _ H1 (refl_equal _) (HWS_irc g)). intuition. + +apply (complete_coloring_coloring _ _ _ x x0). +apply (any_coalescible_edge_2 e1 _ _ (get_movesWL (irc_wl g)) H1 H). +rewrite H0 in *. unfold merge_irc in *. simpl in *. apply IHt0. +rewrite precolored_merge. +unfold VertexSet.Subset. intros. apply Hpre. apply (VertexSet.remove_3 H2). +apply (proj1 (any_coalescible_edge_1 _ _ _ _ H1 H)). + +unfold compat_col. +intros. unfold map_to_coloring. +rewrite (MapFacts.find_o _ H2). apply OptionReg.eq_refl. + +(* freeze *) +generalize (freeze_inv _ _ e1). intro. +generalize (freeze_inv2 _ _ e1). intro. destruct H0. destruct H0. simpl in *. +apply (coloring_delete_preference _ r (irc_g g) x0 _). +rewrite H0 in *. unfold delete_preference_edges_irc2 in *. simpl in *. apply IHt0. +unfold VertexSet.Subset. intros. apply Hpre. +rewrite precolored_delete_preference_edges in H1. assumption. + +(* spill *) +generalize (spill_inv _ _ e2). intro. +generalize (spill_inv2 _ _ e2). intro. destruct H0. simpl in *. +apply available_coloring_1. +apply proper_remove_proper with (x:=r). +rewrite H0 in *. unfold spill_irc in *. simpl in *. apply IHt0. +unfold VertexSet.Subset. intros. apply Hpre. +rewrite precolored_remove_vertex in H1. apply (VertexSet.remove_3 H1). + +unfold compat_col. +intros. unfold map_to_coloring. +rewrite (MapFacts.find_o _ H1). apply OptionReg.eq_refl. + +apply (In_spill_props _ _ _ _ _ _ _ _ (lowest_cost_in _ _ _ H) (refl_equal _) (HWS_irc g)). + +(* terminal case *) +apply proper_coloring_empty. assumption. +Qed. + +Lemma proper_coloring_IRC_aux : forall g palette, +VertexSet.Subset (precolored g) palette -> +proper_coloring (IRC g palette) g palette. + +Proof. +intros. apply proper_coloring_IRC_map. auto. +Qed. + +Lemma proper_coloring_IRC : forall g palette, +proper_coloring (precoloring g) g palette -> +proper_coloring (IRC g palette) g palette. + +Proof. +intros. apply proper_coloring_IRC_map. +intro. intro. unfold proper_coloring, proper_coloring_3 in H. +do 2 destruct H as [_ H]. unfold graph_to_IRC_graph in *. simpl in *. +apply H with (x:= a). apply proper_coloring_pre_inv. assumption. +Qed.
\ No newline at end of file |