blob: 668063d113fb9469632c18ee57b537fcc288e9d5 (
plain)
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
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Interference_adjacency.
Require Import Edges.
Require Import MyRegisters.
Import RegFacts Props.
Module Register := Regs.
(* For any vertex x different from r, the neighborhood of x in
(remove_vertex r g) is its one in g, minus r *)
Lemma remove_interf_adj : forall x r g,
~Register.eq x r ->
VertexSet.Equal (interference_adj x (remove_vertex r g))
(VertexSet.remove r (interference_adj x g)).
Proof.
intros.
split; intros.
apply VertexSet.remove_2. intro.
rewrite <-H1 in H0. rewrite in_interf in 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_interf in H0. rewrite In_remove_edge in H0. destruct H0.
rewrite in_interf. assumption.
rewrite in_interf. rewrite In_remove_edge.
split.
rewrite <-in_interf. apply (VertexSet.remove_3 H0).
intro. destruct H1; change_rewrite.
elim (VertexSet.remove_1 H1 H0).
elim H. auto.
Qed.
(* If x is different from r and does not belong to the interference neighborhood
of r in g, then the interference neighborhood of x in (remove_vertex r g)
is equal to the interference neighborhood of x in g *)
Lemma interf_adj_remove : forall x r g,
~VertexSet.In x (interference_adj r g) ->
~Register.eq x r ->
VertexSet.Equal (interference_adj x g) (interference_adj x (remove_vertex r g)).
Proof.
intros x r g H H0.
rewrite remove_interf_adj. rewrite remove_equal. apply VertexSet.eq_refl.
intro. elim H. apply interf_adj_comm. assumption.
auto.
Qed.
(* The interference neighborhood of x in (remove_vertex r g)
is a subset of the interference neighborhood of x in g *)
Lemma sub_remove_interf : forall x r g,
~Register.eq x r ->
VertexSet.Subset (interference_adj x (remove_vertex r g))
(interference_adj x g).
Proof.
intros x r g H. rewrite remove_interf_adj.
unfold VertexSet.Subset. intros y H0.
apply (VertexSet.remove_3 H0).
assumption.
Qed.
(* If x is a neighbor of r in g, then x belongs to (remove_vertex r g) *)
Lemma in_interf_adj_in_remove : forall x r g,
VertexSet.In x (interference_adj r g) -> In_graph x (remove_vertex r g).
Proof.
intros x r g H. rewrite In_remove_vertex. split.
rewrite in_interf in H. apply (proj1 (In_graph_edge_in_ext _ _ H)).
intro H0. rewrite H0 in H. elim (not_in_interf_self _ _ H).
Qed.
|
