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
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Conservative_criteria.
Require Import Edges.
Require Import MyRegisters.
Require Import Affinity_relation.
Import Edge RegFacts Props OTFacts.
(* Intersections of vertices sets of the worklists are empty *)
Lemma WS_empty_inter_1 : forall g palette WL,
WS_properties g palette WL ->
VertexSet.Empty (VertexSet.inter (get_spillWL WL) (get_freezeWL WL)).
Proof.
intros g palette WL H.
unfold VertexSet.Empty.
intros a H0.
generalize (VertexSet.inter_1 H0);intro H1.
generalize (VertexSet.inter_2 H0);intro H2.
unfold WS_properties in H.
destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5].
generalize (proj1 (H a) H1);intro H6.
destruct H6 as [H6 _].
generalize (proj1 (H3 a) H2);intro H7.
destruct H7 as [H7 _].
rewrite H6 in H7; inversion H7.
Qed.
Lemma WS_empty_inter_2 : forall g palette WL,
WS_properties g palette WL ->
VertexSet.Empty (VertexSet.inter (get_spillWL WL) (get_simplifyWL WL)).
Proof.
intros g palette WL H.
unfold VertexSet.Empty.
intros a H0.
generalize (VertexSet.inter_1 H0);intro H1.
generalize (VertexSet.inter_2 H0);intro H2.
unfold WS_properties in H.
destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5].
generalize (proj1 (H a) H1);intro H6.
destruct H6 as [H6 _].
generalize (proj1 (H4 a) H2);intro H7.
destruct H7 as [H7 _].
rewrite H6 in H7; inversion H7.
Qed.
Lemma WS_empty_inter_3 : forall g palette WL,
WS_properties g palette WL ->
VertexSet.Empty (VertexSet.inter (get_freezeWL WL) (get_simplifyWL WL)).
Proof.
intros g palette WL H.
unfold VertexSet.Empty.
intros a H0.
generalize (VertexSet.inter_1 H0);intro H1.
generalize (VertexSet.inter_2 H0);intro H2.
unfold WS_properties in H.
destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5].
generalize (proj1 (H3 a) H1);intro H6.
destruct H6 as [_ H6].
destruct H6 as [H6 _].
generalize (proj1 (H4 a) H2);intro H7.
destruct H7 as [_ H7].
destruct H7 as [H7 _].
rewrite H6 in H7; inversion H7.
Qed.
(* A tactic for simplifying proofs of belonging of a vertex to a worklist *)
Ltac WS_apply H := generalize H;intro HWS_;
match goal with
| |- (VertexSet.In ?A _) => destruct HWS_ as [HWS_ HWS__];
try (apply (proj2 (HWS_ A)));
destruct HWS__ as [HWS__ HWS___];
try (apply (proj2 (HWS__ A)));
destruct HWS___ as [HWS___ HWS____];
try (apply (proj2 (HWS___ A)));
clear HWS_ HWS__ HWS___ HWS____
| |- (EdgeSet.In ?A _) => do 3 destruct HWS_ as [_ HWS_];
apply (proj2 (HWS_ A));
clear HWS_
end.
(* Lemmas for generalizing properties of a vertex belonging to a given worklist *)
Lemma In_spill_props : forall x g WL s a b c palette,
VertexSet.In x s ->
WL = (s,a,b,c) ->
WS_properties g palette WL ->
has_low_degree g palette x = false /\ In_graph x g /\ ~VertexSet.In x (precolored g).
Proof.
intros x g WL s a b c palette H H0 H1.
unfold WS_properties in H1;rewrite H0 in H1.
destruct H1 as [H1 _].
unfold get_spillWL in H1;simpl in H1.
apply (proj1 (H1 x) H).
Qed.
Lemma In_freeze_props : forall x g WL s a b c palette,
VertexSet.In x s ->
WL = (a,s,b,c) ->
WS_properties g palette WL ->
has_low_degree g palette x = true /\ move_related g x = true /\ In_graph x g /\ ~VertexSet.In x (precolored g).
Proof.
intros x g WL s a b c palette H H0 H1.
unfold WS_properties in H1;rewrite H0 in H1.
destruct H1 as [_ H1].
destruct H1 as [H1 _].
unfold get_freezeWL in H1;simpl in H1.
generalize (proj1 (H1 x) H);intro.
intuition.
apply move_related_in_graph;intuition.
Qed.
Lemma In_simplify_props : forall x g WL s a b c palette,
VertexSet.In x s ->
WL = (a,b,s,c) ->
WS_properties g palette WL ->
has_low_degree g palette x = true /\ move_related g x = false /\ In_graph x g /\ ~VertexSet.In x (precolored g).
Proof.
intros x g WL s a b c palette H H0 H1.
unfold WS_properties in H1;rewrite H0 in H1.
do 2 destruct H1 as [_ H1].
destruct H1 as [H1 _].
unfold get_spillWL in H1;simpl in H1.
apply (proj1 (H1 x) H).
Qed.
Lemma In_move_props : forall e g WL s a b c palette,
EdgeSet.In e s ->
WL = (a,b,c,s) ->
WS_properties g palette WL ->
aff_edge e /\ In_graph_edge e g.
Proof.
intros e g WL s a b c palette H H0 H1.
unfold WS_properties in H1;rewrite H0 in H1.
do 3 destruct H1 as [_ H1].
unfold get_movesWL in H1;simpl in H1.
apply (proj1 (H1 e) H).
Qed.
Lemma WS_props_equal :
forall g palette ws ws',
VertexSet.Equal (get_simplifyWL ws) (get_simplifyWL ws') ->
VertexSet.Equal (get_freezeWL ws) (get_freezeWL ws') ->
VertexSet.Equal (get_spillWL ws) (get_spillWL ws') ->
EdgeSet.Equal (get_movesWL ws) (get_movesWL ws') ->
WS_properties g palette ws ->
WS_properties g palette ws'.
Proof.
unfold WS_properties;unfold get_spillWL;unfold get_freezeWL;
unfold get_simplifyWL;unfold get_movesWL;simpl;unfold VertexSet.Equal;
unfold EdgeSet.Equal;intros g palette ws ws' H H0 H1 H2 H3.
destruct ws as [ws d]; destruct ws as [ws c]; destruct ws as [a b].
destruct ws' as [ws' p]; destruct ws' as [ws' o]; destruct ws' as [m n]. simpl in *.
generalize (VertexSet.eq_sym H);generalize (VertexSet.eq_sym H0);
generalize (VertexSet.eq_sym H1);generalize (EdgeSet.eq_sym H2);
clear H;clear H0;clear H1;clear H2;intros H2 H1 H0 H.
destruct H3 as [Hsp H3];destruct H3 as [Hf H3];
destruct H3 as [Hsi Hm].
do 2 split.
intro H4;apply (proj1 (Hsp x) (proj1 (H1 x) H4)).
intro H4;apply (proj2 (H1 x) (proj2 (Hsp x) H4)).
split;intro H4.
apply (proj1 (Hf x) (proj1 (H0 x) H4)).
apply (proj2 (H0 x) (proj2 (Hf x) H4)).
split.
split;intro H4.
apply (proj1 (Hsi x) (proj1 (H x) H4)).
apply (proj2 (H x) (proj2 (Hsi x) H4)).
split;intro H4.
apply (proj1 (Hm e) (proj1 (H2 e) H4)).
apply (proj2 (H2 e) (proj2 (Hm e) H4)).
Qed.
(* Definition of the nonprecolored vertices of a graph *)
Definition not_precolored g := VertexSet.diff (V g) (precolored g).
(* The union of vertices worklists forms the nonprecolored vertices set of g *)
Lemma not_precolored_union_ws : forall g palette ws,
WS_properties g palette ws ->
VertexSet.Equal
(VertexSet.union (VertexSet.union (get_spillWL ws) (get_freezeWL ws)) (get_simplifyWL ws))
(not_precolored g).
Proof.
intros g palette ws HWS.
split. intro H.
unfold not_precolored. apply VertexSet.diff_3.
destruct (VertexSet.union_1 H).
destruct (VertexSet.union_1 H0).
apply (proj1(proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))).
apply (proj2(proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))).
apply (proj2(proj2 (In_simplify_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS))).
destruct (VertexSet.union_1 H).
destruct (VertexSet.union_1 H0).
apply (proj2(proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))).
apply (proj2(proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))).
apply (proj2(proj2 (In_simplify_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS))).
intro H.
unfold not_precolored in H.
generalize (VertexSet.diff_1 H). intro H0.
generalize (VertexSet.diff_2 H). clear H. intro H.
case_eq (has_low_degree g palette a); intro Hlow.
case_eq (move_related g a); intro Haff.
apply VertexSet.union_2. apply VertexSet.union_3.
WS_apply HWS. intuition.
apply VertexSet.union_3.
WS_apply HWS. intuition.
apply VertexSet.union_2. apply VertexSet.union_2.
WS_apply HWS. intuition.
Qed.
(* The moves worklists is equal to the set of affinity edges *)
Lemma moves_AE : forall g palette ws,
WS_properties g palette ws ->
EdgeSet.Equal (AE g) (get_movesWL ws).
Proof.
split; intros.
destruct ws. destruct p. destruct p.
simpl. WS_apply H. apply (proj1 (In_graph_aff_edge_in_AE _ _) H0).
generalize (In_move_props _ _ _ _ _ _ _ _ H0 (refl_equal _) H). intro H1.
apply (proj2 (In_graph_aff_edge_in_AE _ _) H1).
Qed.
|
