blob: a235374b12cdbe0e1aa5fc1dfbea698a7a584547 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Merge_WL.
Require Import Edges.
Require Import Remove_Vertex_WL.
Require Import IRC_graph.
Require Import Delete_Preference_Edges_Degree.
Require Import WS.
Require Import Delete_Preference_Edges_Move.
Require Import Graph_Facts.
Require Import Interference_adjacency.
Require Import Affinity_relation.
Import RegFacts Props.
Definition delete_preferences_wl2 v ircg k :=
let wl := irc_wl ircg in
let g := irc_g ircg in
let simplify := get_simplifyWL wl in
let freeze := get_freezeWL wl in
let spill := get_spillWL wl in
let moves := get_movesWL wl in
let adj_fst := VertexSet.diff (preference_adj v g) (precolored g) in
let new_simp := VertexSet.filter (fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g)) && has_low_degree g k x) adj_fst in
let simplifyWL' := VertexSet.add v (VertexSet.union simplify new_simp) in
let freezeWL' := VertexSet.remove v (VertexSet.diff freeze new_simp) in
let movesWL' := not_incident_edges v moves g in
(spill, freezeWL', simplifyWL', movesWL').
Lemma WS_delete_preferences_wl2 : forall r ircg (Hin : In_graph r (irc_g ircg)),
VertexSet.In r (get_freezeWL (irc_wl ircg)) ->
WS_properties (delete_preference_edges r (irc_g ircg) Hin)
(VertexSet.cardinal (pal ircg))
(delete_preferences_wl2 r ircg (VertexSet.cardinal (pal ircg))).
Proof.
intros r ircg Hin HH.
unfold WS_properties. unfold delete_preferences_wl2.
generalize (HWS_irc ircg). intro HWS.
set (wl := irc_wl ircg) in *.
set (g := irc_g ircg) in *.
set (simplify := get_simplifyWL wl) in *.
set (freeze := get_freezeWL wl) in *.
set (spill := get_spillWL wl) in *.
set (adj_fst := VertexSet.diff (preference_adj r g) (precolored g)) in *.
set (new_simp := VertexSet.filter (fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g))) adj_fst) in *.
set (simplifyWL_ := VertexSet.union simplify new_simp) in *.
set (simplifyWL' := VertexSet.add r simplifyWL_) in *.
set (freezeWL' := VertexSet.diff freeze new_simp) in *.
set (movesWL' := not_incident_edges r (get_movesWL wl) g) in *.
rewrite <-(Hk ircg) in HWS. set (K := VertexSet.cardinal (pal ircg)) in *.
unfold get_spillWL, get_simplifyWL, get_freezeWL, get_movesWL. simpl.
split. intro x.
rewrite <-delete_preference_edges_low.
rewrite precolored_delete_preference_edges.
rewrite In_delete_preference_edges_vertex.
split; intros.
apply (In_spill_props _ _ _ _ _ _ _ _ H (refl_equal _) HWS).
WS_apply HWS. assumption.
(* freeze *)
split. intro x.
rewrite precolored_delete_preference_edges.
rewrite <-delete_preference_edges_low.
split; intros.
unfold freezeWL' in H.
assert (~Register.eq r x) as Hneq.
intro. elim (VertexSet.remove_1 H0 H).
generalize (VertexSet.remove_3 H). clear H. intro H.
generalize (VertexSet.diff_1 H). generalize (VertexSet.diff_2 H). clear H. intros.
generalize (In_freeze_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS). intro.
destruct H1. destruct H2. destruct H3.
split.
assumption.
split.
destruct (Register.eq_dec r x). elim (Hneq e).
case_eq (move_related (delete_preference_edges r g Hin) x); intros.
reflexivity.
elim H. unfold new_simp.
apply VertexSet.filter_3.
apply compat_move_up.
apply VertexSet.diff_3.
apply delete_preference_edges_move_1 with (H := Hin); auto.
assumption.
rewrite andb_true_iff. split.
apply eq_K_1.
apply delete_preference_edges_move_2 with (H := Hin); auto.
assumption.
assumption.
destruct H. destruct H0.
apply VertexSet.remove_2. intro.
rewrite (compat_bool_move _ _ _ (Register.eq_sym _ _ H2)) in H0.
rewrite (not_aff_related_delete_preference_edges r g Hin) in H0. inversion H0.
unfold freezeWL'. apply VertexSet.diff_3.
WS_apply HWS. split.
assumption.
split.
apply (move_related_delete_move_related _ _ _ _ H0).
assumption.
intro. assert (move_related (delete_preference_edges r g Hin) x = false).
apply delete_preference_edges_move_inv.
intro.
rewrite (compat_bool_move _ _ _ (Register.eq_sym _ _ H3)) in H0.
rewrite (not_aff_related_delete_preference_edges r g Hin) in H0. inversion H0.
apply (move_related_delete_move_related _ _ _ _ H0).
unfold new_simp in H2.
apply (VertexSet.diff_1 (VertexSet.filter_1 (compat_move_up _ _) H2)).
symmetry. apply eq_K_2. generalize (VertexSet.filter_2 (compat_move_up _ _) H2). intro.
rewrite andb_true_iff in H3. destruct H3. assumption.
rewrite H0 in H3. inversion H3.
(* simplify *)
split. intro x.
rewrite <-delete_preference_edges_low.
rewrite precolored_delete_preference_edges.
rewrite In_delete_preference_edges_vertex.
split; intros.
unfold simplifyWL' in H.
destruct (proj1 (Dec.F.add_iff _ _ _) H).
generalize (In_freeze_props _ _ _ _ _ _ _ _ HH (refl_equal _) HWS). intro.
destruct H1. destruct H2. destruct H3.
split. rewrite <-(compat_bool_low _ _ _ _ H0). assumption.
split. rewrite <-(compat_bool_move _ _ _ H0). apply not_aff_related_delete_preference_edges.
split. rewrite <-H0. assumption.
rewrite <-H0. assumption.
unfold simplifyWL_ in H0.
destruct (VertexSet.union_1 H0).
generalize (In_simplify_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS). intro.
destruct H2. destruct H3. destruct H4.
split.
assumption.
split.
apply delete_preference_edges_move_false_false. assumption.
split; assumption.
unfold new_simp in H1.
generalize (VertexSet.filter_1 (compat_move_up _ _) H1). intro.
generalize (VertexSet.filter_2 (compat_move_up _ _) H1). clear H1. intro.
rewrite andb_true_iff in H1. destruct H1.
split. assumption.
split. apply delete_preference_edges_move_inv.
intro. elim (not_in_pref_self r g).
rewrite <-H4 in H2. apply (VertexSet.diff_1 H2).
apply move_related_card.
unfold pref_degree. rewrite <-(eq_K_2 _ _ H1). auto.
apply (VertexSet.diff_1 H2).
symmetry. apply (eq_K_2 _ _ H1).
split.
apply (in_pref_in _ _ _ (VertexSet.diff_1 H2)).
apply (VertexSet.diff_2 H2).
destruct H. destruct H0. destruct H1.
destruct (Register.eq_dec r x).
apply VertexSet.add_1. auto.
apply VertexSet.add_2.
case_eq (In_dec x adj_fst); intros.
case_eq (eq_K 1 (VertexSet.cardinal (preference_adj x g))); intros.
apply VertexSet.union_3. apply VertexSet.filter_3.
apply compat_move_up.
assumption.
rewrite H4. rewrite H. auto.
apply VertexSet.union_2. WS_apply HWS.
split. assumption.
split.
case_eq (move_related g x); intros.
generalize (delete_preference_edges_move_2 _ _ _ Hin n H5 H0). intro.
rewrite (eq_K_1 _ _ H6) in H4. inversion H4.
reflexivity.
split; assumption.
apply VertexSet.union_2.
WS_apply HWS.
split. assumption.
split. case_eq (move_related g x); intros.
generalize (delete_preference_edges_move_1 _ _ _ Hin n H4 H0). intro.
elim n0. apply VertexSet.diff_3; assumption.
reflexivity.
split; assumption.
unfold movesWL'. intro. rewrite not_incident_edges_1.
rewrite In_delete_preference_edges_edge.
split; intros.
destruct H.
generalize (In_move_props _ _ _ _ _ _ _ _ H (refl_equal _) HWS). intro.
destruct H1.
split. assumption.
split. assumption.
intro. elim H0. destruct H3. assumption.
destruct H. destruct H0.
split. WS_apply HWS. split; assumption.
intro. elim H1. split; assumption.
intros. apply (In_move_props _ _ _ _ _ _ _ _ H (refl_equal _) HWS).
Qed.
Lemma WS_freeze : forall r ircg (Hin : In_graph r (irc_g ircg)),
VertexSet.In r (get_freezeWL (irc_wl ircg)) ->
WS_properties (delete_preference_edges r (irc_g ircg) Hin)
(irc_k ircg)
(delete_preferences_wl2 r ircg (irc_k ircg)).
Proof.
intros. rewrite <-(Hk ircg). apply WS_delete_preferences_wl2. auto.
Qed.
|
