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
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Merge_Adjacency.
Require Import ZArith.
Require Import Edges.
Require Import MyRegisters.
Require Import Merge_Adjacency.
Require Import Interference_adjacency.
Require Import Remove_Vertex_Degree.
Module Register := Regs.
Import Edge Props RegFacts.
(* If x interferes with both (fst_ext e) and (snd_ext e), then
its degree decreases of one when e is coalesced *)
Lemma merge_degree_dec_inter : forall x e g Hin Haff,
VertexSet.In x (interference_adj (fst_ext e) g) ->
VertexSet.In x (interference_adj (snd_ext e) g) ->
interf_degree g x = S (interf_degree (merge e g Hin Haff) x).
Proof.
intros. unfold interf_degree.
rewrite (cardinal_m (merge_interf_adj_in_both _ _ _ Hin Haff H0 H)).
rewrite remove_cardinal_1. reflexivity. apply interf_adj_comm. auto.
Qed.
(* If x does not interfere with both (fst_ext e) and (snd_ext e)
then its degree is unchanged when e is coalesced *)
Lemma merge_dec_eq : forall x e g Hin Haff,
~VertexSet.In x (interference_adj (fst_ext e) g) \/
~VertexSet.In x (interference_adj (snd_ext e) g) ->
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
interf_degree g x = interf_degree (merge e g Hin Haff) x.
Proof.
intros. unfold interf_degree. destruct H.
destruct (In_dec x (interference_adj (snd_ext e) g)).
rewrite (cardinal_m (merge_interf_adj_in_snd _ _ _ Hin Haff H0 H1 i)).
rewrite add_cardinal_2. rewrite remove_cardinal_1. reflexivity.
apply interf_adj_comm. auto.
intro. elim H. apply interf_adj_comm. apply (VertexSet.remove_3 H2).
rewrite (cardinal_m (merge_interf_adj_not_in _ _ _ Hin Haff H0 H1 n)). reflexivity.
rewrite (cardinal_m (merge_interf_adj_not_in _ _ _ Hin Haff H0 H1 H)). reflexivity.
Qed.
(* The interference degree of any vertex which is not an endpoint
of e decreases when e is coalesced *)
Lemma merge_degree_dec : forall x e g Hin Haff,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
interf_degree (merge e g Hin Haff) x <= interf_degree g x.
Proof.
intros. destruct (In_dec x (interference_adj (fst_ext e) g)).
destruct (In_dec x (interference_adj (snd_ext e) g)).
rewrite (merge_degree_dec_inter x e g Hin Haff i i0). auto.
rewrite (merge_dec_eq x e g Hin Haff (or_intror _ n)); auto.
rewrite (merge_dec_eq x e g Hin Haff (or_introl _ n)); auto.
Qed.
(* If x does not interfere with the first endpoint of e then
x is of low-degree in (merge e g Hin Haff) iff it is in g *)
Lemma low_merge_low_fst : forall x e g K Hin Haff,
~VertexSet.In x (interference_adj (fst_ext e) g) ->
~Register.eq x (snd_ext e) ->
~Register.eq x (fst_ext e) ->
has_low_degree (merge e g Hin Haff) K x = has_low_degree g K x.
Proof.
intros x e g palette Hin Haff H H0 H1. unfold has_low_degree.
rewrite (merge_dec_eq x e g Hin Haff); auto.
Qed.
(* If x does not interfere with the second endpoint of e then
x is of low-degree in (merge e g Hin Haff) iff it is in g *)
Lemma low_merge_low_snd : forall x e g K Hin Haff,
~VertexSet.In x (interference_adj (snd_ext e) g) ->
~Register.eq x (snd_ext e) ->
~Register.eq x (fst_ext e) ->
has_low_degree (merge e g Hin Haff) K x = has_low_degree g K x.
Proof.
intros x e g palette Hin Haff H H0 H1. unfold has_low_degree.
rewrite (merge_dec_eq x e g Hin Haff); auto.
Qed.
(* A high-degree vertex of (merge e g Hin Haff) is of high-degree in g *)
Lemma merge_low_1 : forall g e x K Haff Hin,
has_low_degree (merge e g Hin Haff) K x = false ->
~Register.eq x (snd_ext e) ->
~Register.eq x (fst_ext e) ->
has_low_degree g K x = false.
Proof.
intros g e x K Haff Hin Hpre H0 H1. unfold has_low_degree in *.
destruct (le_lt_dec K (interf_degree (merge e g Hin Haff) x));
destruct (le_lt_dec K (interf_degree g x )); inversion Hpre.
reflexivity.
generalize (merge_degree_dec x e g Hin Haff H1 H0). intro.
apply False_ind. intuition.
Qed.
(* A low-degree vertex of g is of low-degree in (merge e g Haff Hin) *)
Lemma low_dec : forall x e g Hin Haff K,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
has_low_degree g K x = true ->
has_low_degree (merge e g Hin Haff) K x = true.
Proof.
intros.
case_eq (has_low_degree (merge e g Hin Haff) K x);[auto|intros].
rewrite (merge_low_1 g e x K Haff Hin H2 H0 H) in H1. inversion H1.
Qed.
(* A vertex high-degree vertex of g (which is not an endpoint of e)
which is of low-degree in (merge e g p q) belongs to the interference
neighborhood of the two endpoints of e in g *)
Lemma merge_dec_interf : forall x e k g p q,
has_low_degree g k x = false ->
has_low_degree (merge e g p q) k x = true ->
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
VertexSet.In x (interference_adj (fst_ext e) g) /\
VertexSet.In x (interference_adj (snd_ext e) g).
Proof.
intros.
destruct (In_dec x (interference_adj (fst_ext e) g)).
split. assumption.
destruct (In_dec x (interference_adj (snd_ext e) g)).
assumption.
rewrite (low_merge_low_snd _ _ _ _ p q n H2 H1) in H0. rewrite H0 in H. inversion H.
rewrite (low_merge_low_fst _ _ _ _ p q n H2 H1) in H0. rewrite H0 in H. inversion H.
Qed.
(* A vertex high-degree vertex of g (which is not an endpoint of e)
which is of low-degree in (merge e g p q) is of degree k in g *)
Lemma merge_dec_K : forall x e k g p q,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
has_low_degree g k x = false ->
has_low_degree (merge e g p q) k x = true ->
interf_degree g x = k.
Proof.
intros x e k g p q H0 H1 H2 H3. generalize I. intro H. unfold interf_degree.
assert (VertexSet.In x (interference_adj (fst_ext e) g) /\
VertexSet.In x (interference_adj (snd_ext e) g)).
apply (merge_dec_interf x e k g p q); auto.
destruct H4.
generalize (merge_degree_dec_inter x e g p q H4 H5). intro.
unfold has_low_degree, interf_degree in *.
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (merge e g p q)))).
inversion H3.
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x g))).
rewrite H6 in l0. rewrite (lt_le_S_eq _ _ l l0). assumption.
inversion H2.
Qed.
(* Reciprocally, a vertex of degree k interfering with
the two endpoints of g is of low-degree in (merge e g p q) *)
Lemma merge_dec_low : forall x e k g p q,
interf_degree g x = k ->
VertexSet.In x (interference_adj (fst_ext e) g) ->
VertexSet.In x (interference_adj (snd_ext e) g) ->
has_low_degree (merge e g p q) k x = true.
Proof.
unfold interf_degree. intros x e k g p q H0 H1 H2. generalize I. intro H.
assert (~Register.eq x (fst_ext e)).
intro. elim (not_in_interf_self (fst_ext e) g). rewrite H3 in H1. assumption.
assert (~Register.eq x (snd_ext e)).
intro. elim (not_in_interf_self (snd_ext e) g). rewrite H4 in H2. assumption.
generalize (merge_degree_dec_inter x e g p q H1 H2). intro.
unfold has_low_degree, interf_degree in *.
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (merge e g p q)))).
rewrite H5 in H0. rewrite <-H0 in l. elim (le_S_irrefl _ l).
reflexivity.
Qed.
(* Again, unused but meaningful theorem, summarizing evolution of degree
when an edge e is coalesced *)
Theorem merge_degree_evolution : forall x e k g p q,
~Register.eq x (fst_ext e) ->
~Register.eq x (snd_ext e) ->
((has_low_degree g k x = false /\ has_low_degree (merge e g p q) k x = true)
<->
(interf_degree g x = k /\
VertexSet.In x (interference_adj (fst_ext e) g) /\
VertexSet.In x (interference_adj (snd_ext e) g))).
Proof.
split; intros.
destruct H1.
split. apply (merge_dec_K x e k g p q); auto.
apply (merge_dec_interf x e k g p q); auto.
destruct H1. destruct H2.
split. unfold has_low_degree. rewrite H1.
destruct (le_lt_dec k k). reflexivity. elim (lt_irrefl _ l).
apply merge_dec_low; auto.
Qed.
|
