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
|
Require Import FSets.
Require Import InterfGraphMapImp.
Require Import ZArith.
Require Import Edges.
Require Import MyRegisters.
Import Edge OTFacts.
Module Import RegFacts := Facts VertexSet.
Module Import RegRegFacts := Facts EdgeSet.
(* Definition of useful morphisms *)
Add Morphism In_graph : In_graph_m.
Proof.
unfold In_graph;intros x y H g.
split;intro H0;[rewrite <-H|rewrite H];assumption.
Qed.
Add Morphism In_graph_edge : In_graph_edge_m.
Proof.
unfold In_graph_edge; intros x y H g. fold (eq x y) in H.
split;intro H0;[rewrite <-H|rewrite H];assumption.
Qed.
Add Morphism move_related : move_related_m.
Proof.
unfold move_related. intros. rewrite (compat_preference_adj _ _ _ H). reflexivity.
Qed.
Add Morphism get_weight : get_weight_m.
Proof.
intros x y H.
rewrite (weight_ordered_weight x);rewrite (weight_ordered_weight y).
unfold get_weight;unfold E.eq in H.
destruct H as [_ H];inversion H;[|rewrite H2];reflexivity.
Qed.
(* Useful rewriting lemmas *)
Lemma rewrite_fst : forall x y z,
fst_ext (x,y,z) = x.
Proof.
auto.
Qed.
Lemma rewrite_snd : forall x y z,
snd_ext (x,y,z) = y.
Proof.
auto.
Qed.
Lemma rewrite_weight : forall x y z,
get_weight (x,y,z) = z.
Proof.
auto.
Qed.
(* A rewriting tactic *)
Ltac change_rewrite :=
repeat (try rewrite rewrite_fst in *;
try rewrite rewrite_snd in *;
try rewrite rewrite_weight in *).
(* Two tactics for proving equality of edges *)
Ltac Eq_eq :=
apply eq_ordered_eq;unfold E.eq;
split;[simpl;split;auto; intuition |try apply OptionN_as_OT.eq_refl; intuition].
Ltac Eq_comm_eq := rewrite edge_comm; Eq_eq.
(* Extensionnality of redirect *)
Lemma redirect_ext : forall e e' x y,
eq e e' ->
eq (redirect x y e) (redirect x y e').
Proof.
intros e e' x y H.
destruct e as [xe we];destruct xe as [ex1 ex2];
destruct e' as [xe' we'];destruct xe' as [e'x1 e'x2];simpl in *.
generalize (get_weight_m _ _ H);simpl;intro Heq;subst.
destruct (eq_charac _ _ H);destruct H0 as [H0 H1];unfold redirect;change_rewrite.
destruct (OTFacts.eq_dec ex1 x).
destruct (OTFacts.eq_dec e'x1 x).
Eq_eq. intuition.
elim (n (Regs.eq_trans (Regs.eq_sym H0) r)).
destruct (OTFacts.eq_dec e'x1 x).
elim (n (Regs.eq_trans H0 r)).
destruct (OTFacts.eq_dec ex2 x).
destruct (OTFacts.eq_dec e'x2 x).
Eq_eq. intuition.
elim (n1 (Regs.eq_trans (Regs.eq_sym H1) r)).
destruct (OTFacts.eq_dec e'x2 x).
elim (n1 (Regs.eq_trans H1 r)).
Eq_eq.
destruct (OTFacts.eq_dec ex1 x).
destruct (OTFacts.eq_dec e'x1 x).
Eq_eq. intuition.
apply (Regs.eq_trans H1 (Regs.eq_trans r0 (Regs.eq_trans (Regs.eq_sym r) H0))).
destruct (OTFacts.eq_dec e'x2 x).
Eq_comm_eq. intuition.
elim (n0 (Regs.eq_trans (Regs.eq_sym H0) r)).
destruct (OTFacts.eq_dec e'x2 x).
elim (n (Regs.eq_trans H0 r)).
destruct (OTFacts.eq_dec ex2 x).
destruct (OTFacts.eq_dec e'x1 x).
Eq_comm_eq.
elim (n1 (Regs.eq_trans (Regs.eq_sym H1) r)).
destruct (OTFacts.eq_dec e'x1 x).
elim (n1 (Regs.eq_trans H1 r)).
Eq_comm_eq.
Qed.
(* The weight is left unchanged while applying redirect *)
Lemma redirect_weight_eq : forall e x y,
Edge.get_weight (redirect x y e) = Edge.get_weight e.
Proof.
unfold redirect;intros e x y;destruct e as [e w];destruct e as [ex1 ex2];change_rewrite.
destruct (OTFacts.eq_dec ex1 x);destruct (OTFacts.eq_dec ex2 x);reflexivity.
Qed.
(* Specification of redirect *)
Lemma redirect_charac : forall e x y,
(eq e (redirect x y e) /\ (~Regs.eq x (fst_ext e) /\ ~Regs.eq x (snd_ext e))) \/
(eq (y, snd_ext e, get_weight e) (redirect x y e) /\ Regs.eq x (fst_ext e)) \/
(eq (fst_ext e, y, get_weight e) (redirect x y e) /\ Regs.eq x (snd_ext e)).
Proof.
intros e x y.
unfold redirect. change_rewrite.
destruct (OTFacts.eq_dec (fst_ext e) x).
right. left. split. apply eq_refl. auto.
destruct (OTFacts.eq_dec (snd_ext e) x).
right. right. split. apply eq_refl. auto.
left. split. apply eq_refl. split; intuition.
Qed.
(* Weak equality implies equality for interference edges *)
Lemma weak_eq_interf_eq : forall x y,
weak_eq x y ->
interf_edge x ->
interf_edge y ->
eq x y.
Proof.
unfold weak_eq, interf_edge, get_weight. intros. destruct H; destruct H.
Eq_eq. rewrite H0. rewrite H1. apply OptionN_as_OT.eq_refl.
rewrite (edge_eq x). rewrite (edge_eq y).
Eq_comm_eq. simpl. unfold get_weight.
rewrite H0. rewrite H1. apply OptionN_as_OT.eq_refl.
Qed.
(* The second endpoint of e does not belongs to (merge e g H H0) *)
Lemma not_in_merge_snd : forall e g H H0,
~In_graph (snd_ext e) (merge e g H H0).
Proof.
intros. intro.
rewrite In_merge_vertex in H1. destruct H1.
elim (H2 (Regs.eq_refl _)).
Qed.
(* Extensionnality of the low-degree function *)
Lemma compat_bool_low : forall g K,
compat_bool Regs.eq (has_low_degree g K).
Proof.
unfold compat_bool, has_low_degree, interf_degree. intros.
rewrite (compat_interference_adj _ _ _ H). reflexivity.
Qed.
(* There cannot exist both an interference and
a preference between two vertices *)
Lemma interf_pref_conflict : forall x y g,
Prefere x y g /\ Interfere x y g -> False.
Proof.
unfold Prefere, Interfere. intros. destruct H. destruct H.
assert (eq (x,y,Some x0) (x,y,None)).
apply is_simple_graph with (g:=g); auto.
unfold weak_eq. left. change_rewrite. split; auto.
generalize (get_weight_m _ _ H1). simpl. congruence.
Qed.
|
