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
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Remove_Vertex_Adjacency.
Require Import ZArith.
Require Import Edges.
Require Import MyRegisters.
Require Import Interference_adjacency.
Module Register := Regs.
Import RegFacts Props.
(* The degree of any vertex different from r decreases when
r is removed from the a graph g. Hence, a low-degree vertex of g
is a low-degree vertex of (remove_vertex r g) *)
Lemma low_remove_low : forall x r g K,
has_low_degree g K x = true ->
~Register.eq x r ->
has_low_degree (remove_vertex r g) K x = true.
Proof.
intros x r g K H H0. unfold has_low_degree, interf_degree in *.
generalize (sub_remove_interf _ _ g H0);intro H1.
generalize (subset_cardinal H1);intro H2.
destruct (le_lt_dec K (VertexSet.cardinal (interference_adj x g))).
inversion H.
destruct (le_lt_dec K (VertexSet.cardinal (interference_adj x (remove_vertex r g)))).
apply False_ind;intuition.
auto.
Qed.
(* For the same reason, a high-degree vertex of (remove_vertex r g)
is a high-degree vertex of g *)
Lemma not_low_remove_not_low : forall x r g K,
has_low_degree (remove_vertex r g) K x = false ->
~Register.eq x r ->
has_low_degree g K x = false.
Proof.
intros x r g K H H0.
case_eq (has_low_degree g K x);[intros|auto].
rewrite (low_remove_low _ _ _ _ H1) in H. inversion H.
auto.
Qed.
(* The degree of any vertex x which is not an interference neighbor of
(remove_vertex r g) is the same in g and in (remove_vertex r g) *)
Lemma low_deg : forall x r g K,
~VertexSet.In x (interference_adj r g) ->
~Register.eq x r ->
has_low_degree g K x = has_low_degree (remove_vertex r g) K x.
Proof.
intros x r g K H H0. unfold has_low_degree, interf_degree.
destruct (le_lt_dec K (VertexSet.cardinal (interference_adj x g)));
destruct (le_lt_dec K (VertexSet.cardinal (interference_adj x (remove_vertex r g)))).
reflexivity.
rewrite <-(cardinal_m(interf_adj_remove _ _ _ H H0)) in l0.
apply False_ind. intuition.
elim (lt_irrefl (VertexSet.cardinal (interference_adj x g))).
apply lt_le_trans with (m := K). auto.
rewrite (cardinal_m (interf_adj_remove x r g H H0)). auto.
reflexivity.
Qed.
Lemma lt_le_S_eq : forall n x,
x < n ->
n <= S x ->
n = S x.
Proof.
induction n; intros.
intuition.
induction x; intros.
apply eq_S. intuition.
apply eq_S. apply IHn. intuition. intuition.
Qed.
Lemma le_S_irrefl : forall x,
S x <= x -> False.
Proof.
induction x; intros.
inversion H.
apply IHx. apply le_S_n. assumption.
Qed.
(* If x is a low-degree degree of (remove_vertex r g) and x is
a high-degree vertex of g then the interference degree
of x in g is exactly k *)
Lemma degree_dec_remove_K : forall x k r g,
~Register.eq x r ->
has_low_degree g k x = false ->
has_low_degree (remove_vertex r g) k x = true ->
interf_degree g x = k.
Proof.
unfold has_low_degree, interf_degree. intros.
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (remove_vertex r g)))) in H1.
inversion H1.
rewrite (cardinal_m (remove_interf_adj _ _ _ H)) in l.
unfold has_low_degree in H0.
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x g))).
destruct (In_dec r (interference_adj x g)).
generalize (remove_cardinal_1 i). intro HH. rewrite <-HH in l0.
set (card := VertexSet.cardinal (VertexSet.remove r (interference_adj x g))) in *.
rewrite <-HH. symmetry. apply lt_le_S_eq; auto.
generalize (remove_cardinal_2 n). intro HH. rewrite <-HH in l0.
elim (lt_irrefl k). intuition.
inversion H0.
Qed.
(* Any x which is of high-degree in g and of low-degree in (remove_vertex r g)
interferes with r *)
Lemma low_degree_in_interf : forall x r g K,
has_low_degree (remove_vertex r g) K x = true ->
~Register.eq x r ->
has_low_degree g K x = false ->
VertexSet.In x (interference_adj r g).
Proof.
unfold has_low_degree, interf_degree. intros x r g K H HH H0.
destruct (le_lt_dec K (VertexSet.cardinal (interference_adj x g))).
destruct (le_lt_dec K (VertexSet.cardinal (interference_adj x (remove_vertex r g)))).
inversion H.
destruct (In_dec x (interference_adj r g)).
assumption.
generalize (interf_adj_remove _ _ _ n HH);intro H2.
rewrite (cardinal_m H2) in l.
apply False_ind. intuition.
inversion H0.
Qed.
(* Reciprocally, a high-degree vertex x of g which is
exactly of degree k in g and interferes with r is
of low-degree in (remove_vertex r g) *)
Lemma degree_K_remove_dec : forall x k r g,
~Register.eq x r ->
interf_degree g x = k ->
VertexSet.In x (interference_adj r g) ->
has_low_degree (remove_vertex r g) k x = true.
Proof.
unfold has_low_degree, interf_degree. intros.
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x g))).
destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (remove_vertex r g)))).
rewrite (cardinal_m (remove_interf_adj _ _ _ H)) in l0.
generalize (remove_cardinal_1 (interf_adj_comm _ _ _ H1)).
intro HH. rewrite <-HH in l.
set (card := VertexSet.cardinal (VertexSet.remove r (interference_adj x g))) in *.
rewrite <-HH in H0. rewrite <-H0 in *. elim (le_S_irrefl _ l0).
reflexivity.
apply False_ind. intuition.
Qed.
(* Finally, an unused but meaningful theorem summarizing
conditions leading to an evolution of the interference degrees
when a vertex r is removed *)
Theorem remove_low_degree_evolution : forall x k r g,
~Register.eq x r ->
((has_low_degree g k x = false /\ has_low_degree (remove_vertex r g) k x = true)
<->
(VertexSet.In x (interference_adj r g) /\ interf_degree g x = k)).
Proof.
intros. split; intros; destruct H0.
split. eapply low_degree_in_interf; eauto. eapply degree_dec_remove_K; eauto.
cut (has_low_degree g k x = false). intro.
split. assumption.
apply degree_K_remove_dec; auto.
unfold has_low_degree. rewrite H1. destruct (le_lt_dec k k). auto. elim (lt_irrefl _ l).
Qed.
|
