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
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Remove_Vertex_Degree.
Require Import Edges.
Require Import MyRegisters.
Require Import Interference_adjacency.
Require Import Graph_Facts.
Module Register := Regs.
Import Edge RegFacts Props.
(* The following lemmas define the interference adjacency
of the first endpoint of e after the merge of e *)
Lemma merge_interf_adj_fst_1 : forall e g H0 Haff,
VertexSet.Subset (interference_adj (fst_ext e) (merge e g H0 Haff))
(VertexSet.union (interference_adj (fst_ext e) g)
(interference_adj (snd_ext e) g)).
Proof.
unfold VertexSet.Subset. intros e g H Haff a H1.
rewrite in_interf in H1. generalize (In_merge_edge_inv _ _ _ H Haff H1); intro.
destruct H0 as [x H0]. destruct H0 as [H3 H4].
destruct x as [ex wx]. destruct ex as [x1 x2].
assert (interf_edge (x1,x2,wx)) as Hinterf.
destruct H4. unfold same_type in H2. destruct H2; destruct H2.
unfold aff_edge in H4. destruct H4. simpl in H4. congruence.
assumption.
destruct H4 as [H4 HH4].
assert (eq (a, fst_ext e, None) (redirect (snd_ext e) (fst_ext e) (x1,x2,wx))).
apply weak_eq_interf_eq. assumption. unfold interf_edge. auto.
unfold interf_edge. rewrite redirect_weight_eq. auto. clear H4.
generalize (redirect_charac (x1,x2,wx) (snd_ext e) (fst_ext e)); intros.
destruct H2. destruct H2. destruct H4. rewrite <-H2 in H0.
apply VertexSet.union_2. rewrite in_interf. rewrite H0. assumption.
destruct H2. destruct H2. rewrite <-H2 in H0. change_rewrite.
apply VertexSet.union_3. rewrite in_interf.
destruct (eq_charac _ _ H0); destruct H5; change_rewrite.
assert (eq (a, snd_ext e, None) (x1, x2, wx)).
Eq_comm_eq. apply (Register.eq_trans _ _ _ H5 H6).
generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl.
rewrite H7. assumption.
assert (eq (a,snd_ext e, None) (x1,x2,wx)).
Eq_comm_eq.
generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl.
rewrite H7. assumption.
destruct H2; change_rewrite. rewrite <-H2 in H0.
destruct (eq_charac _ _ H0); destruct H5; change_rewrite.
apply VertexSet.union_3. rewrite in_interf.
assert (eq (a, snd_ext e, None) (x1,x2,wx)).
Eq_eq.
generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl.
rewrite H7. assumption.
apply VertexSet.union_3. rewrite in_interf.
assert (eq (a, snd_ext e, None) (x1,x2,wx)).
Eq_eq.
apply (Register.eq_trans _ _ _ H5 H6).
generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl.
rewrite H7. assumption.
Qed.
Lemma merge_interf_adj_fst_2 : forall e g H0 Haff,
VertexSet.Subset (interference_adj (fst_ext e) g)
(interference_adj (fst_ext e) (merge e g H0 Haff)).
Proof.
unfold VertexSet.Subset. intros.
rewrite in_interf in H. rewrite in_interf.
destruct (redirect_charac (a, fst_ext e, None) (snd_ext e) (fst_ext e)); intros.
change_rewrite. destruct H1. destruct H2.
rewrite H1. apply In_merge_interf_edge. assumption.
unfold interf_edge. auto.
change_rewrite. destruct H1. destruct H1.
elim (interf_pref_conflict (snd_ext e) (fst_ext e) g).
split. unfold Prefere. destruct Haff. exists x.
rewrite edge_comm. rewrite <-H3. rewrite (edge_eq e) in H0. assumption.
unfold Interfere.
assert (eq (snd_ext e, fst_ext e, None) (a, fst_ext e, None)) by Eq_eq.
rewrite H3. assumption.
destruct H1. rewrite H1. apply In_merge_interf_edge. assumption.
unfold interf_edge. auto.
Qed.
Lemma merge_interf_adj_fst_3 : forall e g H0 Haff,
VertexSet.Subset (interference_adj (snd_ext e) g)
(interference_adj (fst_ext e) (merge e g H0 Haff)).
Proof.
unfold VertexSet.Subset. intros.
rewrite in_interf in H. rewrite in_interf.
destruct (redirect_charac (a, snd_ext e, None) (snd_ext e) (fst_ext e)); intros.
change_rewrite. destruct H1. destruct H2. elim H3. auto.
change_rewrite. destruct H1. destruct H1.
elim (In_graph_edge_diff_ext _ _ H). change_rewrite. auto.
destruct H1. rewrite H1. apply In_merge_interf_edge. assumption.
unfold interf_edge. auto.
Qed.
Lemma merge_interf_adj_fst : forall e g H0 Haff,
VertexSet.Equal (interference_adj (fst_ext e) (merge e g H0 Haff))
(VertexSet.union (interference_adj (fst_ext e) g)
(interference_adj (snd_ext e) g)).
Proof.
intros. split; intros.
apply (merge_interf_adj_fst_1 _ _ H0 Haff _ H).
destruct (VertexSet.union_1 H).
apply (merge_interf_adj_fst_2 _ _ H0 Haff _ H1).
apply (merge_interf_adj_fst_3 _ _ H0 Haff _ H1).
Qed.
(* The following lemmas define the equality of the interference adjacency
of any vertex which is not an endpoint of e after the merge of e *)
Lemma merge_interf_adj_1 : forall x e g Hin Haff,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
VertexSet.Subset (VertexSet.remove (snd_ext e) (interference_adj x g))
(interference_adj x (merge e g Hin Haff)).
Proof.
unfold VertexSet.Subset. intros.
rewrite in_interf. rewrite Dec.F.remove_iff in H1. destruct H1.
destruct (redirect_charac (a,x,None) (snd_ext e) (fst_ext e)); change_rewrite.
destruct H3. destruct H4. rewrite H3.
apply In_merge_interf_edge. rewrite <-in_interf. assumption.
unfold interf_edge. auto.
destruct H3. destruct H3. elim H2. auto.
destruct H3. elim H0. auto.
Qed.
Lemma merge_interf_adj_2 : forall x e g Hin Haff,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
VertexSet.Subset (interference_adj x (merge e g Hin Haff))
(VertexSet.add (fst_ext e) (interference_adj x g)).
Proof.
unfold VertexSet.Subset. intros.
destruct (Register.eq_dec a (fst_ext e)); [apply VertexSet.add_1|apply VertexSet.add_2]; intuition.
rewrite in_interf in H1. generalize (In_merge_edge_inv _ _ _ Hin Haff H1). intro.
destruct H2. destruct H2. destruct H3.
assert (eq (a,x,None) (redirect (snd_ext e) (fst_ext e) x0)).
apply weak_eq_interf_eq. assumption. unfold interf_edge. auto.
unfold interf_edge. rewrite redirect_weight_eq.
unfold same_type in H4. destruct H4; destruct H4.
unfold aff_edge in H5. destruct H5. simpl in H5. congruence.
auto. intuition.
rewrite in_interf. rewrite H5.
destruct (redirect_charac x0 (snd_ext e) (fst_ext e)).
destruct H6. destruct H7. rewrite <-H6. assumption.
destruct H6. destruct H6. rewrite <-H6 in H5.
destruct (eq_charac _ _ H5); destruct H8; change_rewrite.
elim n. auto. elim H. auto.
destruct H6. rewrite <-H6 in H5.
destruct (eq_charac _ _ H5); destruct H8; change_rewrite.
elim H. auto. elim n. auto.
Qed.
Lemma merge_interf_adj_not_in : forall x e g Hin Haff,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
~VertexSet.In x (interference_adj (snd_ext e) g) ->
VertexSet.Equal (interference_adj x (merge e g Hin Haff))
(interference_adj x g).
Proof.
intros. split; intros.
generalize (merge_interf_adj_2 x e g Hin Haff H H0 a H2). intro.
rewrite Dec.F.add_iff in H3. destruct H3.
rewrite <-H3 in H2. generalize (interf_adj_comm _ _ _ H2). intro.
rewrite merge_interf_adj_fst in H4. destruct (VertexSet.union_1 H4).
rewrite <-H3. apply interf_adj_comm. assumption.
elim H1. auto.
assumption.
apply merge_interf_adj_1; auto.
apply VertexSet.remove_2; auto.
intro. elim H1. apply interf_adj_comm. rewrite H3. assumption.
Qed.
Lemma merge_interf_adj_in_snd : forall x e g Hin Haff,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
VertexSet.In x (interference_adj (snd_ext e) g) ->
VertexSet.Equal (interference_adj x (merge e g Hin Haff))
(VertexSet.add (fst_ext e) (VertexSet.remove (snd_ext e)
(interference_adj x g))).
Proof.
intros. split; intros.
generalize (merge_interf_adj_2 _ _ _ Hin Haff H H0 _ H2). intro.
rewrite Dec.F.add_iff in H3. destruct H3.
apply VertexSet.add_1. assumption.
apply VertexSet.add_2. apply VertexSet.remove_2.
intro. rewrite <-H4 in H2. rewrite in_interf in H2.
generalize (proj1 (In_graph_edge_in_ext _ _ H2)). change_rewrite. intro.
rewrite In_merge_vertex in H5. destruct H5. elim H6. auto. assumption.
rewrite Dec.F.add_iff in H2. destruct H2.
rewrite <-H2. apply interf_adj_comm. rewrite merge_interf_adj_fst.
apply VertexSet.union_3. auto.
apply merge_interf_adj_1; auto.
Qed.
Lemma merge_interf_adj_in_both : forall x e g Hin Haff,
VertexSet.In x (interference_adj (snd_ext e) g) ->
VertexSet.In x (interference_adj (fst_ext e) g) ->
VertexSet.Equal (interference_adj x (merge e g Hin Haff))
(VertexSet.remove (snd_ext e) (interference_adj x g)).
Proof.
intros.
assert (~Register.eq x (fst_ext e)).
intro. rewrite H1 in H0. elim (not_in_interf_self _ _ H0).
assert (~Register.eq x (snd_ext e)).
intro. rewrite H2 in H. elim (not_in_interf_self _ _ H).
rewrite merge_interf_adj_in_snd; auto.
split; intros.
rewrite Dec.F.add_iff in H3. destruct H3.
apply VertexSet.remove_2. intro.
elim (In_graph_edge_diff_ext _ _ Hin). rewrite H3. auto.
rewrite <-H3. apply interf_adj_comm. assumption.
assumption.
apply VertexSet.add_2. auto.
Qed.
Lemma preference_adj_merge : forall x e g p q,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
VertexSet.Subset (preference_adj x (merge e g p q))
(VertexSet.add (fst_ext e)
(VertexSet.remove (snd_ext e) (preference_adj x g))).
Proof.
intros x e g p q H0 H1. generalize I. intro H.
unfold VertexSet.Subset; intros.
rewrite in_pref in H2. destruct H2.
generalize (In_merge_edge_inv e _ g p q H2). intro.
destruct H3. destruct H3. destruct H4 as [H4 HH4].
unfold weak_eq in H4. change_rewrite. destruct H4.
unfold redirect in H4; change_rewrite.
destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite.
destruct H4. apply VertexSet.add_1. intuition.
destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite.
destruct H4. elim H0. intuition.
destruct H4. apply VertexSet.add_2. apply VertexSet.remove_2.
intro. elim n. rewrite H6. intuition.
rewrite in_pref. unfold same_type in HH4.
destruct HH4. destruct H6.
destruct H6. exists x2.
assert (eq (a,x,Some x2) x1).
apply eq_ordered_eq. split; try split; simpl; auto.
unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl.
rewrite H8. assumption.
destruct H6. unfold interf_edge in H7. simpl in H7. congruence.
unfold redirect in H4; change_rewrite.
destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite.
destruct H4. elim H0. auto.
destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite.
destruct H4. apply VertexSet.add_1. intuition.
destruct H4. apply VertexSet.add_2. apply VertexSet.remove_2.
intro. elim n0. rewrite H6. intuition.
rewrite in_pref. unfold same_type in HH4.
destruct HH4. destruct H6.
destruct H6. exists x2.
assert (eq (a,x,Some x2) x1).
rewrite edge_comm. apply eq_ordered_eq. split; try split; simpl; auto.
unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl.
rewrite H8. assumption.
destruct H6. unfold interf_edge in H7. simpl in H7. congruence.
Qed.
Lemma preference_adj_merge_2 : forall x e g p q,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
VertexSet.Subset (VertexSet.remove (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g)))
(preference_adj x (merge e g p q)).
Proof.
unfold VertexSet.Subset; intros x e g p q H0 H1 a H2. generalize I. intro H.
assert (~Register.eq a (fst_ext e)). intro.
rewrite H3 in H2. elim (VertexSet.remove_1 (Register.eq_refl _) H2).
generalize (VertexSet.remove_3 H2). clear H2. intro H2.
assert (~Register.eq a (snd_ext e)). intro.
rewrite H4 in H2. elim (VertexSet.remove_1 (Register.eq_refl _) H2).
generalize (VertexSet.remove_3 H2). clear H2. intro.
rewrite in_pref in H2. destruct H2.
assert (exists w, In_graph_edge (a,x,Some w) (merge e g p q)).
cut (Prefere (fst_ext (redirect (snd_ext e) (fst_ext e) (a,x,Some x0)))
(snd_ext (redirect (snd_ext e) (fst_ext e) (a,x,Some x0)))
(merge e g p q)). intro.
unfold redirect in H5; change_rewrite.
destruct (OTFacts.eq_dec a (snd_ext e)); change_rewrite.
elim (H4 r).
destruct (OTFacts.eq_dec x (snd_ext e)); change_rewrite.
elim (H1 r).
unfold Prefere in H5. assumption.
apply In_merge_pref_edge. assumption.
intro. destruct (eq_charac _ _ H5); change_rewrite; destruct H6.
elim H1. auto.
elim H0. auto.
unfold aff_edge. exists x0. auto.
intro. unfold redirect in H5;change_rewrite.
destruct (OTFacts.eq_dec a (snd_ext e)); change_rewrite.
elim (H4 r).
destruct (OTFacts.eq_dec x (snd_ext e)); change_rewrite.
elim (H1 r).
unfold Interfere in H5. generalize (In_merge_edge_inv e _ g p q H5). intro H8.
generalize I. intro H7.
destruct H8. destruct H6. destruct H8.
unfold weak_eq in H8. change_rewrite. destruct H8.
unfold redirect in H8; change_rewrite.
destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite; destruct H8.
elim (H3 H8).
destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite.
elim (H0 H10).
elim (interf_pref_conflict a x g).
split.
unfold Prefere. exists x0. assumption.
unfold Interfere.
assert (eq (a,x,None) x1).
apply weak_eq_interf_eq. unfold weak_eq. change_rewrite.
left. split; auto. unfold interf_edge. auto.
unfold same_type in H9. destruct H9. destruct H9.
unfold aff_edge in H11. destruct H11. simpl in H11. congruence.
destruct H9. assumption.
rewrite H11. assumption.
unfold redirect in H8; change_rewrite.
destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite.
destruct H8. elim (H0 H10).
destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite.
destruct H8. elim (H3 H8).
elim (interf_pref_conflict a x g).
split.
unfold Prefere. exists x0. assumption.
unfold Interfere. destruct H8.
assert (eq (a,x,None) x1).
apply weak_eq_interf_eq. unfold weak_eq. change_rewrite.
right. split; auto. unfold interf_edge. auto.
unfold same_type in H9. destruct H9. destruct H9.
unfold aff_edge in H11. destruct H11. simpl in H11. congruence.
destruct H9. assumption.
rewrite H11. assumption.
rewrite in_pref. assumption.
Qed.
|
