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
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import Merge_Move.
Require Import Edges.
Require Import MyRegisters.
Require Import Affinity_relation.
Require Import Interference_adjacency.
Require Import Delete_Preference_Edges_Adjacency.
Require Import Remove_Vertex_Move.
Import Edge Props RegFacts.
(* The frozen vertex is nonmove-related in the resulting graph *)
Lemma not_aff_related_delete_preference_edges : forall r g p,
move_related (delete_preference_edges r g p) r = false.
Proof.
intros. apply move_related_false_charac2.
intros.
rewrite In_delete_preference_edges_edge in H0. destruct H0.
intro. elim H1. split; assumption.
Qed.
(* A vertex which is move-related after a freeze is move-related before it *)
Lemma move_related_delete_move_related : forall x r g p,
move_related (delete_preference_edges r g p) x = true ->
move_related g x = true.
Proof.
intros x r g p H.
generalize (move_related_charac _ _ H);intro H0.
destruct H0 as [y H0].
destruct H0 as [H0 H1];destruct H1 as [H1 H2].
rewrite In_delete_preference_edges_edge in H1. destruct H1.
apply (move_related_charac2 _ _ _ H0 H1 H2).
Qed.
(* A vertex which is move-related in g and not in (delete_preference_edges r g H)
is a preference neighbor of r in g *)
Lemma delete_preference_edges_move_1 : forall x r g H,
~Register.eq r x ->
move_related g x = true ->
move_related (delete_preference_edges r g H) x = false ->
VertexSet.In x (preference_adj r g).
Proof.
intros. generalize (not_move_related_empty_pref _ _ H2). intro.
rewrite delete_preference_preference_adj in H3.
destruct (In_dec r (preference_adj x g)).
apply pref_adj_comm. assumption.
assert (VertexSet.Equal (preference_adj x g) VertexSet.empty).
split; intros.
rewrite <-H3. apply VertexSet.remove_2.
intro. rewrite <-H5 in H4. elim n. auto.
assumption.
elim (VertexSet.empty_1 H4).
elim (move_related_not_empty_pref _ _ H1 H4).
auto.
Qed.
(* A vertex which is move-related in g and nonmove-related in
(delete_preference_edges r g H) has a preference degree of 1 *)
Lemma delete_preference_edges_move_2 : forall x r g H,
~Register.eq r x ->
move_related g x = true ->
move_related (delete_preference_edges r g H) x = false ->
VertexSet.cardinal (preference_adj x g) = 1.
Proof.
intros. generalize (not_move_related_empty_pref _ _ H2). intro.
rewrite delete_preference_preference_adj in H3.
destruct (In_dec r (preference_adj x g)).
cut (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)). intros.
rewrite H4. apply singleton_cardinal.
split; intros.
destruct (Register.eq_dec a r).
apply VertexSet.singleton_2. intuition.
assert (VertexSet.In a VertexSet.empty).
rewrite <-H3. apply VertexSet.remove_2; auto.
elim (VertexSet.empty_1 H5).
generalize (VertexSet.singleton_1 H4). intro.
rewrite <-H5. auto.
elim (move_related_not_empty_pref _ _ H1).
rewrite <-H3.
split; intros.
rewrite Dec.F.remove_neq_iff.
assumption.
intro. rewrite <-H5 in H4. elim n. auto.
apply (VertexSet.remove_3 H4).
auto.
Qed.
(* Reciprocally, a vertex which is move-related in g,
has a preference degree of 1 and is a preference neighbor of r
is nonmove-related in (delete_preference_edges r g H) *)
Lemma delete_preference_edges_move_inv : forall x r g H,
~Register.eq r x ->
move_related g x = true ->
VertexSet.In x (preference_adj r g) ->
VertexSet.cardinal (preference_adj x g) = 1 ->
move_related (delete_preference_edges r g H) x = false.
Proof.
intros.
apply move_related_false_charac2. intros.
rewrite In_delete_preference_edges_edge in H5.
destruct H5.
intro. elim H6.
split. assumption.
cut (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)). intros.
destruct H7;[right|left].
rewrite (edge_eq e) in H5.
assert (eq (x, snd_ext e, get_weight e) (fst_ext e, snd_ext e, get_weight e)).
Eq_eq. rewrite <-H9 in H5.
destruct H4. rewrite H4 in H5.
apply VertexSet.singleton_1. rewrite <-H8.
rewrite in_pref. exists x0. rewrite edge_comm. auto.
rewrite (edge_eq e) in H5.
assert (eq (fst_ext e, x, get_weight e) (fst_ext e, snd_ext e, get_weight e)).
Eq_eq. rewrite <-H9 in H5.
destruct H4. rewrite H4 in H5.
apply VertexSet.singleton_1. rewrite <-H8.
rewrite in_pref. exists x0. rewrite edge_comm. auto.
rewrite edge_comm. assumption.
apply cardinal_1_singleton. apply pref_adj_comm. assumption. assumption.
Qed.
Lemma delete_preference_edges_move_false_false : forall x r g H,
move_related g x = false ->
move_related (delete_preference_edges r g H) x = false.
Proof.
intros.
case_eq (move_related (delete_preference_edges r g H) x); intros.
rewrite (move_related_delete_move_related _ _ _ _ H1) in H0. inversion H0.
reflexivity.
Qed.
|
