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
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import WS.
Require Import Edges.
Require Import MyRegisters.
Require Import Affinity_relation.
Require Import Interference_adjacency.
Module Register := Regs.
Import RegFacts Props Edge.
(* A nonmove-related vertex of g is not move-related
after the removal of a vertex *)
Lemma move_remove : forall x r g,
move_related g x = false ->
move_related (remove_vertex r g) x = false.
Proof.
intros.
apply move_related_false_charac2. intros.
apply move_related_false_charac with (g:=g); auto.
rewrite In_remove_edge in H1. intuition.
Qed.
(* Equivalently, a move-related vertex of (remove_vertex r g)
is move-related in g *)
Lemma move_remove_2 : forall x r g,
move_related (remove_vertex r g) x = true ->
move_related g x = true.
Proof.
intros x r g H.
generalize (move_related_charac _ _ H);intro H0.
destruct H0 as [y H0]. destruct H0 as [H0 H1]. destruct H1 as [H1 H2].
apply move_related_charac2 with (e:= y).
assumption.
rewrite In_remove_edge in H1. destruct H1. assumption. assumption.
Qed.
(* If x (different from r) is move-related in g and nonmove-related
in (remove_vertex r g) then x is a preference neighbor of r in g *)
Lemma move_related_not_remove_in_pref : forall x r g,
~Register.eq r x ->
move_related g x = true ->
move_related (remove_vertex r g) x = false ->
VertexSet.In x (preference_adj r g).
Proof.
intros.
generalize (move_related_charac _ _ H0). intro.
destruct H2. destruct H2. destruct H3.
destruct (incident_dec x0 r).
destruct H5. destruct H4.
elim H. rewrite H4. rewrite H5. auto.
unfold aff_edge in H2. destruct H2.
rewrite in_pref. exists x1.
assert (eq (x,r,Some x1) x0).
rewrite edge_comm. apply eq_ordered_eq.
unfold E.eq; split; simpl. split; auto.
unfold get_weight in H2. rewrite H2. apply OptionN_as_OT.eq_refl.
rewrite H6. assumption.
destruct H4.
destruct H2.
rewrite in_pref. exists x1.
assert (eq (x,r,Some x1) x0).
apply eq_ordered_eq.
unfold E.eq; split; simpl. split; auto.
unfold get_weight in H2. rewrite H2. apply OptionN_as_OT.eq_refl.
rewrite H6. assumption.
elim H. rewrite H4. rewrite H5. auto.
assert (In_graph_edge x0 (remove_vertex r g)).
rewrite In_remove_edge. split; assumption.
generalize (Aff_edge_aff _ _ H6 H2). intro.
destruct H7. destruct H4.
rewrite (compat_bool_move _ _ _ (Register.eq_sym _ _ H4)) in H7. rewrite H1 in H7. inversion H7.
rewrite (compat_bool_move _ _ _ (Register.eq_sym _ _ H4)) in H8. rewrite H1 in H8. inversion H8.
Qed.
(* The preference neighborhood of any vertex x different from r in
(remove_vertex r g) is obtained by removing r from the interference
neighborhood of x in g *)
Lemma remove_pref_adj : forall x r g,
~Register.eq x r ->
VertexSet.Equal (preference_adj x (remove_vertex r g))
(VertexSet.remove r (preference_adj x g)).
Proof.
intros.
split; intros.
apply VertexSet.remove_2. intro.
rewrite <-H1 in H0. rewrite in_pref in H0. destruct H0.
generalize (proj1 (In_graph_edge_in_ext _ _ H0)). change_rewrite. intro.
rewrite In_remove_vertex in H2. destruct H2. elim (H3 (Register.eq_refl _)).
rewrite in_pref. rewrite in_pref in H0. destruct H0. exists x0.
rewrite In_remove_edge in H0. destruct H0. assumption.
generalize (VertexSet.remove_3 H0). intro.
rewrite in_pref in H1. destruct H1.
rewrite in_pref. exists x0. rewrite In_remove_edge. split. assumption.
intro. destruct H2; change_rewrite.
elim (VertexSet.remove_1 H2 H0).
elim H. intuition.
Qed.
(* The preference degree of any vertex which is move-related
in g and nonmove-related in (remove_vertex r g) is equal to 1 *)
Lemma pref_degree_dec_remove_1 : forall x r g,
~Register.eq x r ->
move_related g x = true ->
move_related (remove_vertex r g) x = false ->
pref_degree g x = 1.
Proof.
unfold pref_degree. intros.
generalize (not_move_related_empty_pref _ _ H1). intro.
generalize (remove_pref_adj x r g H). intro.
rewrite H2 in H3.
cut (~Register.eq r x). intro.
generalize (move_related_not_remove_in_pref _ _ _ H4 H0 H1). intro.
generalize (pref_adj_comm _ _ _ H5). intro.
generalize (remove_cardinal_1 H6). intro.
rewrite <-H7. apply eq_S. rewrite <-H3.
rewrite <-Props.cardinal_Empty. apply VertexSet.empty_1.
intuition.
Qed.
Lemma cardinal_1_singleton : forall x s,
VertexSet.In x s ->
VertexSet.cardinal s = 1 ->
VertexSet.Equal s (VertexSet.singleton x).
Proof.
intros.
apply VertexSet.eq_sym.
apply remove_singleton_empty. assumption.
assert (VertexSet.cardinal (VertexSet.remove x s) = 0).
rewrite <-remove_cardinal_1 with (x:=x) in H0. auto.
assumption.
rewrite <-Props.cardinal_Empty in H1.
rewrite (empty_is_empty_1 H1). apply VertexSet.eq_refl.
Qed.
(* Reciprocally, any vertex different from r which has a preference
degree equal to 1 in g and is a preference neighbor of r in g is
nonmove-related in (remove_vertex r g) *)
Lemma pref_degree_1_remove_dec : forall x r g,
~Register.eq x r ->
pref_degree g x = 1 ->
VertexSet.In x (preference_adj r g) ->
move_related (remove_vertex r g) x = false.
Proof.
intros.
case_eq (move_related (remove_vertex r g) x); intros.
generalize (remove_pref_adj x r g H). intro.
assert (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)).
apply cardinal_1_singleton. apply pref_adj_comm. assumption. assumption.
rewrite H4 in H3.
cut (VertexSet.Equal (preference_adj x (remove_vertex r g)) VertexSet.empty). intro.
generalize (move_related_charac _ _ H2). intro.
destruct H6. destruct H6. destruct H7.
destruct H8.
assert (VertexSet.In (snd_ext x0) (preference_adj x (remove_vertex r g))).
destruct H6. rewrite in_pref. exists x1.
assert (eq (snd_ext x0, x, Some x1) x0).
rewrite edge_comm. apply eq_ordered_eq.
unfold E.eq. split; intros. simpl. split; intuition. apply Regs.eq_refl.
auto. auto. simpl. unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl.
rewrite H9. assumption.
rewrite H5 in H9. elim (VertexSet.empty_1 H9).
assert (VertexSet.In (fst_ext x0) (preference_adj x (remove_vertex r g))).
destruct H6. rewrite in_pref. exists x1.
assert (eq (fst_ext x0, x, Some x1) x0).
apply eq_ordered_eq.
unfold E.eq. split; intros. simpl. split; intuition. apply Regs.eq_refl.
auto. auto. simpl. unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl.
rewrite H9. assumption.
rewrite H5 in H9. elim (VertexSet.empty_1 H9).
rewrite H3.
split; intros.
destruct (Register.eq_dec r a).
elim (VertexSet.remove_1 e H5).
generalize (VertexSet.remove_3 H5). intro.
generalize (VertexSet.singleton_1 H6). intro.
elim (n H7).
elim (VertexSet.empty_1 H5).
reflexivity.
Qed.
(* Meaningful theorem *)
Theorem Remove_vertex_move_evolution : forall x r g,
~Register.eq x r ->
((move_related g x = true /\ move_related (remove_vertex r g) x = false)
<->
(pref_degree g x = 1 /\ VertexSet.In x (preference_adj r g))).
Proof.
split; intros.
destruct H0.
split. apply pref_degree_dec_remove_1 with (r:=r); auto.
apply move_related_not_remove_in_pref; auto.
destruct H0.
split. apply move_related_card. congruence.
apply pref_degree_1_remove_dec; auto.
Qed.
|
