diff options
Diffstat (limited to 'backend/Remove_Vertex_WL.v')
| -rwxr-xr-x | backend/Remove_Vertex_WL.v | 478 |
1 files changed, 478 insertions, 0 deletions
diff --git a/backend/Remove_Vertex_WL.v b/backend/Remove_Vertex_WL.v new file mode 100755 index 00000000..2ad7c766 --- /dev/null +++ b/backend/Remove_Vertex_WL.v @@ -0,0 +1,478 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import IRC_graph. +Require Import ZArith. +Require Import Edges. +Require Import Remove_Vertex_Degree. +Require Import WS. +Require Import Remove_Vertex_Move. +Require Import Affinity_relation. +Require Import Interference_adjacency. + +Import RegFacts Props OTFacts. + +Definition eq_K x K := match eq_nat_dec x K with +|left _ => true +|right _ => false +end. + +Lemma eq_K_1 : forall x y, +y = x -> +eq_K x y = true. + +Proof. +intros. unfold eq_K. rewrite <-H. destruct (eq_nat_dec y y); intuition. +Qed. + +Lemma eq_K_2 : forall x y, +eq_K x y = true -> +x = y. + +Proof. +intros. unfold eq_K in H. destruct (eq_nat_dec x y). auto. inversion H. +Qed. + +Lemma eq_K_compat : forall K g, +compat_bool Register.eq (fun x => eq_K K (VertexSet.cardinal (interference_adj x g))). + +Proof. +unfold compat_bool. intros. rewrite (compat_interference_adj _ _ _ H). reflexivity. +Qed. + +Lemma eq_K_compat_pref : forall K g, +compat_bool Register.eq (fun x => eq_K K (VertexSet.cardinal (preference_adj x g))). + +Proof. +unfold compat_bool. intros. rewrite (compat_preference_adj _ _ _ H). reflexivity. +Qed. + +Lemma compat_move_up : forall g K, +compat_bool Register.eq +(fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g)) && has_low_degree g K x). + +Proof. +unfold compat_bool; intros. +rewrite (compat_preference_adj _ _ _ H). +destruct (eq_K 1 (VertexSet.cardinal (preference_adj y g))). simpl. +apply compat_bool_low. assumption. +simpl. reflexivity. +Qed. + +Definition remove_wl_2 r ircg K := + let g := irc_g ircg in + let wl := irc_wl ircg in + let simplify := get_simplifyWL wl in + let freeze := get_freezeWL wl in + let spillWL := get_spillWL wl in + let movesWL := get_movesWL wl in + let pre := precolored g in + let int_adj := interference_adj r g in + let not_pre_int_adj := VertexSet.diff int_adj pre in + let pre_adj := preference_adj r g in + let not_pre_pre_adj := VertexSet.diff pre_adj pre in + let newlow := VertexSet.filter (fun x => eq_K K (VertexSet.cardinal (interference_adj x g))) not_pre_int_adj in + let (free, simp) := VertexSet.partition (move_related g) newlow in + let newnmr := VertexSet.filter (fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g)) && has_low_degree g K x) not_pre_pre_adj in + let simplifyWL__ := VertexSet.union simplify simp in + let simplifyWL_ := VertexSet.union simplifyWL__ newnmr in + let simplifyWL' := VertexSet.remove r simplifyWL_ in + let freezeWL__ := VertexSet.diff freeze newnmr in + let freezeWL_ := VertexSet.union freezeWL__ free in + let freezeWL' := VertexSet.remove r freezeWL_ in + let spillWL_ := VertexSet.diff spillWL newlow in + let spillWL' := VertexSet.remove r spillWL_ in + let movesWL' := not_incident_edges r movesWL g in + (spillWL', freezeWL', simplifyWL', movesWL'). + +Lemma WS_remove_wl_2 : forall r ircg, +WS_properties (remove_vertex r (irc_g ircg)) (VertexSet.cardinal (pal ircg)) + (remove_wl_2 r ircg (VertexSet.cardinal (pal ircg))). + +Proof. +unfold remove_wl_2. intros r ircg. +generalize (HWS_irc ircg). intro HWS. rewrite <-(Hk ircg) in *. +set (g' := remove_vertex r (irc_g ircg)) in *. +set (k := VertexSet.cardinal (pal ircg)) in *. +set (g := irc_g ircg) in *. +set (wl := irc_wl ircg) in *. +set ( simplify := get_simplifyWL wl ) in *. +set ( freeze := get_freezeWL wl ) in *. +set ( spillWL := get_spillWL wl ) in *. +set ( int_adj := interference_adj r g ) in *. +set ( not_pre_int_adj := VertexSet.diff int_adj (precolored g) ) in *. +set ( pre_adj := preference_adj r g ) in *. +set ( not_pre_pre_adj := VertexSet.diff pre_adj (precolored g) ) in *. +set ( low := VertexSet.filter (fun x => eq_K k (VertexSet.cardinal (interference_adj x g))) not_pre_int_adj ) in *. +set ( simpfree := VertexSet.partition (move_related g) low ) in *. +case_eq simpfree. intros free simp Hsf. +unfold simpfree in Hsf. +set ( nmr := VertexSet.filter (fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g)) && has_low_degree g k x) not_pre_pre_adj) in *. +set ( simplifyWL__ := VertexSet.union simplify simp ) in *. +set ( simplifyWL_ := VertexSet.union simplifyWL__ nmr) in *. +set ( simplifyWL' := VertexSet.remove r simplifyWL_ ) in *. +set ( freezeWL__ := VertexSet.diff freeze nmr ) in *. +set ( freezeWL_ := VertexSet.union freezeWL__ free ) in *. +set ( freezeWL' := VertexSet.remove r freezeWL_ ) in *. +set ( spillWL_ := VertexSet.diff spillWL low ) in *. +set ( spillWL' := VertexSet.remove r spillWL_ ) in *. +set ( movesWL' := not_incident_edges r (get_movesWL wl) g) in *. + +unfold WS_properties. split. +split; intro H. +unfold get_spillWL in H. simpl in H. +(* spillWL' => *) +unfold spillWL' in H. +generalize (VertexSet.remove_3 H). intro H0. +unfold spillWL_ in H0. +generalize (VertexSet.diff_1 H0). intro H1. +generalize (VertexSet.diff_2 H0). intro H2. +split. +case_eq (has_low_degree g' k x); intros. +elim H2. apply VertexSet.filter_3. +apply eq_K_compat. +unfold not_pre_int_adj. apply VertexSet.diff_3. +apply low_degree_in_interf with (K := k). +assumption. +intro. elim (VertexSet.remove_1 (Register.eq_sym _ _ H4) H). +apply (proj1 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)). +apply (proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)). +apply eq_K_1. +apply degree_dec_remove_K with (r := r). +intro. elim (VertexSet.remove_1 (Register.eq_sym _ _ H4) H). +apply (proj1 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)). +assumption. +reflexivity. +split. +unfold g'. rewrite In_remove_vertex. split. +apply (proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)). +intro. elim (VertexSet.remove_1 (Register.eq_sym _ _ H3) H). +unfold g'. rewrite precolored_remove_vertex. +intro. elim (proj2 (proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +apply (VertexSet.remove_3 H3). + +(* spillWL' <= *) +destruct H. destruct H0. +unfold get_spillWL. simpl. +unfold spillWL'. +assert (~Register.eq r x) as Hr. +intro. rewrite <-H2 in H0. unfold g' in H0. +rewrite In_remove_vertex in H0. destruct H0. elim H3. auto. +apply VertexSet.remove_2. assumption. +unfold spillWL_. apply VertexSet.diff_3. +WS_apply HWS. +split. +apply not_low_remove_not_low with (r:=r). +assumption. +intuition. +split. +unfold g' in H0. rewrite In_remove_vertex in H0. intuition. +unfold g' in H1. rewrite precolored_remove_vertex in H1. +intro. elim H1. apply VertexSet.remove_2; auto. +intro. unfold low in H2. +generalize (VertexSet.filter_1 (eq_K_compat k g) H2). intro H3. +generalize (VertexSet.filter_2 (eq_K_compat k g) H2). clear H2. intro H2. +generalize (eq_K_2 _ _ H2). clear H2. intro H2. +assert (has_low_degree g' k x = true). +apply degree_K_remove_dec. intuition. +unfold has_low_degree, interf_degree. rewrite <-H2. +destruct (le_lt_dec k k). reflexivity. elim (lt_irrefl _ l). +auto. +unfold not_pre_int_adj in H3. generalize (VertexSet.diff_1 H3). intro. +unfold int_adj in H4. assumption. +rewrite H in H4. inversion H4. + +(* freezeWL' => *) +split. +unfold get_freezeWL. simpl. split; intros. +unfold freezeWL' in H. +assert (~Register.eq r x) as Hr. +intro. elim (VertexSet.remove_1 H0 H). +generalize (VertexSet.remove_3 H). clear H. intro. +unfold freezeWL_ in H. +destruct (VertexSet.union_1 H). +unfold freezeWL__ in H0. +generalize (VertexSet.diff_1 H0). intro. +generalize (VertexSet.diff_2 H0). clear H0. intro. +split. +apply low_remove_low. +apply (proj1 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)). +intuition. +split. +unfold nmr in H0. +case_eq (move_related g' x); intros. +reflexivity. +elim H0. apply VertexSet.filter_3. +apply compat_move_up. +unfold not_pre_pre_adj. apply VertexSet.diff_3. +unfold pre_adj. apply move_related_not_remove_in_pref. intuition. +apply (proj1 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +assumption. +apply (proj2 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +assert (VertexSet.cardinal (preference_adj x g) = 1). +apply pref_degree_dec_remove_1 with (r:=r). intuition. +apply (proj1 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). assumption. +rewrite (eq_K_1 _ _ H3). simpl. +apply (proj1 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)). +unfold g'. rewrite precolored_remove_vertex. +intro. elim (proj2 (proj2 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS)))). +apply (VertexSet.remove_3 H2). +split. +assert (VertexSet.cardinal (interference_adj x g) = k). +assert (VertexSet.In x (fst (VertexSet.partition (move_related g) low))). +rewrite Hsf. simpl. assumption. +rewrite (VertexSet.partition_1) in H1. +generalize (VertexSet.filter_1 (compat_bool_move _) H1). intro. +unfold low in H2. +generalize (VertexSet.filter_1 (eq_K_compat k g) H2). intro H3. +generalize (VertexSet.filter_2 (eq_K_compat k g) H2). clear H2. intro H2. +generalize (eq_K_2 _ _ H2). auto. apply compat_bool_move. +apply degree_K_remove_dec. +intuition. +unfold has_low_degree, interf_degree. rewrite H1. +destruct (le_lt_dec k k). reflexivity. elim (lt_irrefl _ l). auto. +assert (VertexSet.In x (fst (VertexSet.partition (move_related g) low))). +rewrite Hsf. simpl. assumption. +rewrite (VertexSet.partition_1) in H2. +generalize (VertexSet.filter_1 (compat_bool_move _) H2). intro. +unfold low in H3. +generalize (VertexSet.filter_1 (eq_K_compat k g) H3). intro H4. +generalize (VertexSet.filter_2 (eq_K_compat k g) H3). clear H3. intro H3. +unfold not_pre_int_adj in H4. apply (VertexSet.diff_1 H4). +apply compat_bool_move. +split. +case_eq (move_related g' x); intros. +reflexivity. +assert (VertexSet.In x (fst (VertexSet.partition (move_related g) low))). +rewrite Hsf. simpl. assumption. +rewrite (VertexSet.partition_1) in H2. +generalize (VertexSet.filter_1 (compat_bool_move _) H2). intro. +generalize (VertexSet.filter_2 (compat_bool_move _) H2). clear H2. intro H2. +assert (VertexSet.In x (preference_adj r g)). +apply move_related_not_remove_in_pref; assumption. +assert (VertexSet.In x (interference_adj r g)). +unfold low in H3. +generalize (VertexSet.filter_1 (eq_K_compat k g) H3). intro H5. +apply (VertexSet.diff_1 H5). +elim (interf_pref_conflict x r g). split. +rewrite in_pref in H4. destruct H4. +unfold Prefere. exists x0. assumption. +rewrite in_interf in H5. unfold Interfere. assumption. +apply compat_bool_move. +unfold g'. rewrite precolored_remove_vertex. +intro. +assert (VertexSet.In x (fst (VertexSet.partition (move_related g) low))). +rewrite Hsf. simpl. assumption. +rewrite (VertexSet.partition_1) in H2. +generalize (VertexSet.filter_1 (compat_bool_move _) H2). intro. +unfold low in H3. +generalize (VertexSet.filter_1 (eq_K_compat k g) H3). intro. +elim (VertexSet.diff_2 H4). apply (VertexSet.remove_3 H1). +apply compat_bool_move. + +(* freezeWL' <= *) +destruct H. destruct H0. +unfold freezeWL'. +assert (~Register.eq r x). +intro. generalize (move_related_in_graph _ _ H0). intro. rewrite <-H2 in H3. +unfold g' in H3. rewrite In_remove_vertex in H3. destruct H3. elim H4. auto. +apply VertexSet.remove_2. assumption. +unfold freezeWL_. +case_eq (has_low_degree g k x); intros. +apply VertexSet.union_2. unfold freezeWL__. +apply VertexSet.diff_3. +WS_apply HWS. +split. +assumption. +split. +apply move_remove_2 with (r:=r). assumption. +unfold g' in H1. rewrite precolored_remove_vertex in H1. +intro. elim H1. apply VertexSet.remove_2. assumption. assumption. +intro. unfold nmr in H4. +assert (move_related g' x = false). +apply pref_degree_1_remove_dec. +intuition. +generalize (VertexSet.filter_2 (compat_move_up g k) H4). intro. +case_eq (eq_K 1 (VertexSet.cardinal (preference_adj x g))); intros. +rewrite (eq_K_2 _ _ H6); auto. +rewrite H6 in H5. inversion H5. +generalize (VertexSet.filter_1 (compat_move_up g k) H4). intro. +apply (VertexSet.diff_1 H5). +rewrite H0 in H5. inversion H5. +apply VertexSet.union_3. +cut (VertexSet.In x (fst (VertexSet.partition (move_related g) low))). intro. +rewrite Hsf in H4. simpl in H4. assumption. +rewrite VertexSet.partition_1. +apply VertexSet.filter_3. +apply compat_bool_move. +unfold low. apply VertexSet.filter_3. +apply eq_K_compat. +apply VertexSet.diff_3. +unfold int_adj. +apply low_degree_in_interf with (K:=k). +assumption. intuition. assumption. +unfold g' in H1. rewrite precolored_remove_vertex in H1. +intro. elim H1. apply VertexSet.remove_2; auto. +apply eq_K_1. +apply degree_dec_remove_K with (r:=r). +intuition. assumption. assumption. +apply move_remove_2 with (r:=r). assumption. +apply compat_bool_move. + +(* simplifyWL' => *) +split. +unfold get_simplifyWL. simpl. +split; intros. +unfold simplifyWL' in H. +assert (~Register.eq r x) as Hr. +intro. elim (VertexSet.remove_1 H0 H). +generalize (VertexSet.remove_3 H). clear H. intro H. +unfold simplifyWL_ in H. +destruct (VertexSet.union_1 H). +unfold simplifyWL__ in H0. +destruct (VertexSet.union_1 H0). +generalize (In_simplify_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS). clear H1. intro. +destruct H1. destruct H2. destruct H3. +split. apply low_remove_low. assumption. intuition. +split. unfold g'. +apply move_remove. assumption. +split. unfold g'. rewrite In_remove_vertex. split; auto. +unfold g'. rewrite precolored_remove_vertex. intro. +elim H4. apply (VertexSet.remove_3 H5). +assert (VertexSet.In x (snd (VertexSet.partition (move_related g) low))). +rewrite Hsf. simpl. assumption. +rewrite VertexSet.partition_2 in H2. +generalize (VertexSet.filter_1 (compat_not_compat (compat_bool_move g)) H2). intro. +generalize (VertexSet.filter_2 (compat_not_compat (compat_bool_move g)) H2). clear H2. intro. +unfold low in H3. +generalize (VertexSet.filter_1 (eq_K_compat k g) H3). intro. +generalize (VertexSet.filter_2 (eq_K_compat k g) H3). clear H3. intro. +generalize (eq_K_2 _ _ H3). clear H3. intro. +split. +apply degree_K_remove_dec. intuition. +unfold has_low_degree, interf_degree. rewrite <-H3. +destruct (le_lt_dec k k). auto. elim (lt_irrefl _ l). auto. +apply (VertexSet.diff_1 H4). +split. +apply move_remove. +destruct (move_related g x). inversion H2. reflexivity. +split. +unfold g'. rewrite In_remove_vertex. split. +apply in_interf_in with (r:=r). +apply (VertexSet.diff_1 H4). intuition. +unfold g'. rewrite precolored_remove_vertex. intro. +elim (VertexSet.diff_2 H4). apply (VertexSet.remove_3 H5). +apply compat_bool_move. +(* x in nmr *) +unfold nmr in H0. +generalize (VertexSet.filter_1 (compat_move_up g k) H0). intro. +generalize (VertexSet.filter_2 (compat_move_up g k) H0). clear H0. intro. +assert (VertexSet.cardinal (preference_adj x g) = 1). +symmetry. apply eq_K_2. +case_eq (eq_K 1 (VertexSet.cardinal (preference_adj x g))); intros. +reflexivity. +rewrite H2 in H0. inversion H0. +rewrite (eq_K_1 _ _ H2) in H0. simpl in H0. +split. +apply low_remove_low. assumption. intuition. +split. +case_eq (move_related g x); intros. +apply pref_degree_1_remove_dec. intuition. assumption. +apply (VertexSet.diff_1 H1). +apply move_remove. assumption. +split. unfold g'. rewrite In_remove_vertex. split. apply in_pref_in with (r:=r). +apply (VertexSet.diff_1 H1). intuition. +unfold g'. rewrite precolored_remove_vertex. intro. +elim (VertexSet.diff_2 H1). apply (VertexSet.remove_3 H3). + +(* simplifyWL' <= *) +destruct H. destruct H0. destruct H1. +unfold simplifyWL'. +assert (~Register.eq r x) as Hr. +intro. rewrite <-H3 in H1. +unfold g' in H1. rewrite In_remove_vertex in H1. destruct H1. elim H4. auto. +apply VertexSet.remove_2. assumption. +unfold simplifyWL_. +case_eq (has_low_degree g k x); intros. +case_eq (move_related g x); intros. +apply VertexSet.union_3. +unfold nmr. apply VertexSet.filter_3. +apply compat_move_up. +apply VertexSet.diff_3. +apply move_related_not_remove_in_pref. assumption. assumption. assumption. +unfold g' in H2. rewrite precolored_remove_vertex in H2. +intro. elim H2. apply VertexSet.remove_2. intuition. assumption. +assert (eq_K 1 (VertexSet.cardinal (preference_adj x g)) = true). +apply eq_K_1. +apply pref_degree_dec_remove_1 with (r:=r). intuition . assumption. assumption. +rewrite H5. simpl. assumption. +apply VertexSet.union_2. +unfold simplifyWL__. +apply VertexSet.union_2. +WS_apply HWS. +split. +assumption. +split. +assumption. +split. +unfold g' in H1. rewrite In_remove_vertex in H1. intuition. +unfold g' in H2. rewrite precolored_remove_vertex in H2. +intro. elim H2. apply VertexSet.remove_2. intuition. assumption. +apply VertexSet.union_2. +unfold simplifyWL__. +apply VertexSet.union_3. +assert (VertexSet.In x (snd (VertexSet.partition (move_related g) low))). +rewrite VertexSet.partition_2. +apply VertexSet.filter_3. +apply compat_not_compat. apply compat_bool_move. +unfold low. +apply VertexSet.filter_3. +apply eq_K_compat. apply VertexSet.diff_3. +apply low_degree_in_interf with (K:=k). assumption. intuition. assumption. +unfold g' in H2. rewrite precolored_remove_vertex in H2. +intro. elim H2. apply VertexSet.remove_2. intuition. assumption. +apply eq_K_1. apply degree_dec_remove_K with (r:=r). intuition. assumption. assumption. +case_eq (move_related g x); intros. +assert (VertexSet.In x (interference_adj r g)). +apply low_degree_in_interf with (K:=k). assumption. intuition. assumption. +assert (VertexSet.In x (preference_adj r g)). +apply move_related_not_remove_in_pref. assumption. assumption. assumption. +elim (interf_pref_conflict x r g). +split. +unfold Prefere. rewrite in_pref in H6. assumption. +unfold Interfere. rewrite <-in_interf. assumption. +auto. +apply compat_bool_move. +rewrite Hsf in H4. simpl in H4. assumption. + +(* movesWL => *) +unfold movesWL', get_movesWL. simpl. +split; intros. +simpl in H. +rewrite not_incident_edges_1 in H. destruct H as [H HH]. +generalize (In_move_props _ _ _ _ _ _ _ _ H (refl_equal _) HWS). clear H. intro H. +destruct H. destruct H0. +split. assumption. +unfold g'. rewrite In_remove_edge. split. +apply (proj2 (proj1 (In_graph_aff_edge_in_AE _ _) H0)). +assumption. +generalize (proj1 (In_graph_interf_edge_in_IE _ _) H0). intro. +destruct H1. +inversion H. rewrite H1 in H3. inversion H3. +intros. apply (In_move_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS). +destruct H. +rewrite not_incident_edges_1. +split. +WS_apply HWS. +split. +assumption. +unfold g' in H0. rewrite In_remove_edge in H0. intuition. +intro H1. +elim (In_graph_edge_in_ext _ _ H0). +intros. +destruct H1. +rewrite <-H1 in H2. +unfold g' in H2. rewrite In_remove_vertex in H2. destruct H2. elim H4. auto. +rewrite <-H1 in H3. +unfold g' in H3. rewrite In_remove_vertex in H3. destruct H3. elim H4. auto. +intros. apply (In_move_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS). +Qed. |