-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathgdist.v
392 lines (346 loc) · 12.2 KB
/
gdist.v
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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
From mathcomp Require Import all_ssreflect.
(******************************************************************************)
(* Definition of a distance on graph *)
(* connectn r n x == the set of all the elements connected to x in n steps *)
(* *)
(* `d[t1, t2]_r == the distance between t1 and t2 in r *)
(* if they are not connected returns the cardinal of the *)
(* the subtype *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section gdist.
Variable T : finType.
Variable r : rel T.
Fixpoint connectn n x :=
if n is n1.+1 then \bigcup_(y in (rgraph r x)) connectn n1 y
else [set x].
Lemma connectnP n x y :
reflect
(exists p : seq T, [/\ path r x p, last x p = y & size p = n])
(y \in connectn n x).
Proof.
elim: n x y => [x y|n IH x y /=].
rewrite inE; apply: (iffP idP) => [/eqP->|[[|a l] [] //= _ ->//]].
by exists [::].
apply: (iffP idP) => [/bigcupP[i]|[[|i p]//= [H1 H2 H3]]].
- rewrite [i \in _]rgraphK => iRk /IH [p [H1 H2 H3]].
by exists (i :: p); split; rewrite /= ?(iRk, H3).
- by [].
case/andP: H1 => H11 H12.
have F : i \in rgraph r x by rewrite [_ \in _]rgraphK.
apply: (subsetP (bigcup_sup _ F)).
by apply/IH; exists p; split => //; case: H3.
Qed.
Definition gdist t1 t2 :=
find (fun n => t2 \in connectn n t1) (iota 0 #|T|).
Local Notation " `d[ t1 , t2 ] " := (gdist t1 t2)
(format " `d[ t1 , t2 ] ").
Lemma gdist_eq0 t1 t2 : (`d[t1, t2] == 0) = (t1 == t2).
Proof.
have tG : #|T| > 0 by rewrite (cardD1 t1).
rewrite /gdist.
case: #|_| tG => // n _.
rewrite (iotaD _ 1) /= inE [t2 == _]eq_sym.
by case: (t1 =P t2).
Qed.
Lemma gdist_gt0 t1 t2 : (0 < `d[t1, t2]) = (t1 != t2).
Proof. by rewrite ltnNge leqn0 gdist_eq0. Qed.
Lemma gdist0 t : `d[t, t] = 0.
Proof. by apply/eqP; rewrite gdist_eq0. Qed.
Lemma gdist_card_le t1 t2 : `d[t1, t2] <= #|T|.
Proof.
rewrite -[#|T|](size_iota 0).
apply: find_size.
Qed.
Lemma gdist_path_le t1 t2 p :
path r t1 p -> last t1 p = t2 -> `d[t1, t2] <= size p.
Proof.
move=> Hp Hl.
have [tLp|pLt] := leqP #|T| (size p).
apply: leq_trans tLp.
by apply: gdist_card_le.
have F : t2 \in connectn (size p) t1.
by apply/connectnP; exists p.
case: leqP => // /(before_find _) // /(_ 0).
by rewrite seq.nth_iota // F.
Qed.
Lemma gdist_connect t1 t2 : connect r t1 t2 = (`d[t1,t2] < #|T|).
Proof.
apply/connectP/idP=> [[p /shortenP[p' Hp' Hu _ Ht]]|].
apply: leq_trans (_ : size p' < _).
by apply: gdist_path_le.
rewrite -[_.+1]/(size (t1 :: p')) cardE.
apply: uniq_leq_size => // i.
by rewrite mem_enum.
rewrite -[#|_|](size_iota 0) -has_find.
move => /hasP[n _ /connectnP [p [H1p H2p H3p]]].
by exists p.
Qed.
Lemma gdist_nconnect t1 t2 : ~~ connect r t1 t2 -> `d[t1,t2] = #|T|.
Proof.
move=> H; apply/eqP.
have := gdist_card_le t1 t2.
by rewrite leq_eqVlt -gdist_connect (negPf H) orbF.
Qed.
(* geodesic path *)
Definition gpath t1 t2 p :=
[&& path r t1 p, last t1 p == t2 & `d[t1, t2] == size p].
Lemma gpathP t1 t2 p :
reflect ([/\ path r t1 p, last t1 p = t2 & `d[t1, t2] = size p])
(gpath t1 t2 p).
Proof.
apply: (iffP and3P) => [[t1Pp /eqP t1pLt2 /eqP t1t2D]|
[t1Pp t1pLt2 t1t2D]]; first by split.
by split => //; apply/eqP.
Qed.
Lemma gpath_connect t1 t2 : connect r t1 t2 -> {p | gpath t1 t2 p}.
Proof.
move=> t1Ct2.
case: (pickP [pred p | gpath t1 t2 (p : `d[t1, t2].-tuple T)]) => [p Hp|HC].
by exists p.
move: (t1Ct2); rewrite gdist_connect => dLT.
absurd False => //.
move: (dLT); rewrite -[#|_|](size_iota 0) -has_find.
move => /(nth_find 0).
rewrite -[find _ _]/`d[t1, t2].
rewrite nth_iota // add0n => /connectnP[p [H1p H2p /eqP H3p]].
have /idP[] := HC (Tuple H3p).
by apply/and3P; split=> //=; apply/eqP=> //; rewrite (eqP H3p).
Qed.
Lemma gpath_last t1 t2 p : gpath t1 t2 p -> last t1 p = t2.
Proof. by case/gpathP. Qed.
Lemma gpath_dist t1 t2 p : gpath t1 t2 p -> `d[t1, t2] = size p.
Proof. by case/gpathP. Qed.
Lemma gpath_path t1 t2 p : gpath t1 t2 p -> path r t1 p.
Proof. by case/gpathP. Qed.
Lemma last_take (A : Type) (p : seq A) t t1 j :
j <= size p -> last t1 (take j p) = nth t (t1 :: p) j.
Proof.
elim: p t1 j => [t1 [|] //| a l IH t1 [|j]] //= H.
by apply: IH.
Qed.
(* ugly proof !! *)
Lemma gpath_uniq t1 t2 p : gpath t1 t2 p -> uniq (t1 :: p).
Proof.
move=> gH; apply/(uniqP t1) => i j iH jH.
wlog : i j iH jH / i <= j.
move=> H; case: (leqP i j) => [iLj|jLi]; first by apply: H.
by move=> /(@sym_equal _ _ _) /H->; rewrite // ltnW.
rewrite leq_eqVlt => /orP[/eqP->//|iLj].
case/gpathP : gH => t1Pp t1pLt2 dt1t2E.
case: j jH iLj => j // jH iLj.
case: i iH iLj => [_ _ t1E | ] //.
pose p1 := drop j.+1 p.
have t1Pp1 : path r t1 p1.
move: (t1Pp); rewrite -[p](cat_take_drop j.+1) cat_path.
rewrite /= in t1E.
by rewrite (last_take t1) //= -t1E => /andP[].
have t1p1L : last t1 p1 = t2.
move: (t1pLt2); rewrite -[p](cat_take_drop j.+1) last_cat.
rewrite /= in t1E.
by rewrite (last_take t1) //= -t1E.
have [] := boolP (`d[t1, t2] <= size p1) => [|/negP[]]; last first.
by apply: gdist_path_le.
rewrite leqNgt => /negP[].
rewrite size_drop dt1t2E.
rewrite /= in t1E.
by rewrite -{2}[size p](subnK (_ : j < size p)) // addnS ltnS leq_addr.
move=> i iH; rewrite ltnS => iLj nE.
pose p1 := take i.+1 p ++ drop j.+1 p.
have [] := boolP (`d[t1, t2] <= size p1) => [|/negP[]].
rewrite leqNgt => /negP[].
rewrite size_cat size_take size_drop ifT //; last first.
by rewrite -ltnS in iLj; apply: leq_trans iLj _.
rewrite dt1t2E -{2}[size p](subnK (_ : j < size _)) //.
by rewrite addnC ltn_add2l.
apply: gdist_path_le.
move: t1Pp; rewrite -[p](cat_take_drop i.+1).
rewrite -[drop _ _](cat_take_drop (j - i)) !cat_path.
case/and3P => [-> _] /=.
rewrite !(last_take t1) /=; last first.
- rewrite size_drop -subSS.
by apply: leq_sub2r.
- by apply: leq_trans iLj _; rewrite ltnW //.
rewrite drop_drop addnS subnK; last by rewrite ltnW.
congr path.
move: (nE) => /= ->.
rewrite -[j - i]prednK //.
by rewrite /= nth_drop -subnS addnC subnK //.
by rewrite subn_gt0.
rewrite last_cat (last_take t1) // nE.
by rewrite -t1pLt2 -{3}[p](cat_take_drop j.+1) last_cat (last_take t1).
Qed.
Lemma gpath_catl t1 t2 p1 p2 :
gpath t1 t2 (p1 ++ p2) -> gpath t1 (last t1 p1) p1.
Proof.
move=> /gpathP[].
rewrite cat_path last_cat => /andP[t1Pp1 t1p1LPp2] t1p1Lp2Lt2 dt1t2E.
apply/gpathP; split => //.
have : `d[t1, last t1 p1] <= size p1 by rewrite gdist_path_le.
rewrite leq_eqVlt => /orP[/eqP//|dLSp1].
have /gpath_connect[p3 /gpathP[H1 H2 H3]] :
connect r t1 (last t1 p1) by apply/connectP; exists p1.
have : size (p3 ++ p2) < `d[t1, t2] by rewrite dt1t2E !size_cat -H3 ltn_add2r.
rewrite ltnNge => /negP[].
apply: gdist_path_le; first by rewrite cat_path H1 // H2.
by rewrite last_cat H2.
Qed.
Lemma gpath_catr t1 t2 p1 p2 :
gpath t1 t2 (p1 ++ p2) -> gpath (last t1 p1) t2 p2.
Proof.
move=> /gpathP[].
rewrite cat_path last_cat => /andP[t1Pp1 t1p1LPp2] t1p1Lp2Lt2 dt1t2E.
apply/gpathP; split => //.
have : `d[last t1 p1, t2] <= size p2 by rewrite gdist_path_le.
rewrite leq_eqVlt => /orP[/eqP//|dLSp1].
have /gpath_connect[p3 /gpathP[H1 H2 H3]] :
connect r (last t1 p1) t2 by apply/connectP; exists p2.
have : size (p1 ++ p3) < `d[t1, t2] by rewrite dt1t2E !size_cat -H3 ltn_add2l.
rewrite ltnNge => /negP[].
apply: gdist_path_le; first by rewrite cat_path H1 andbT.
by rewrite last_cat.
Qed.
Lemma gdist_cat t1 t2 p1 p2 :
gpath t1 t2 (p1 ++ p2) ->
`d[t1,t2] = `d[t1, last t1 p1] + `d[last t1 p1, t2].
Proof.
move=> gH.
rewrite (gpath_dist gH).
rewrite (gpath_dist (gpath_catl gH)) (gpath_dist (gpath_catr gH)) //.
by rewrite size_cat.
Qed.
Lemma gpath_consl t1 t2 t3 p : gpath t1 t2 (t3 :: p) -> `d[t1, t3] = 1.
Proof. by move=> /(@gpath_catl _ _ [::t3]) /= /gpathP[]. Qed.
Lemma gpath_consr t1 t2 t3 p : gpath t1 t2 (t3 :: p) -> gpath t3 t2 p.
Proof. by move=> /(@gpath_catr _ _ [::t3]). Qed.
Lemma gdist_cons t1 t2 t3 p :
gpath t1 t2 (t3 :: p) -> `d[t1,t2] = `d[t3, t2].+1.
Proof.
move=> gH.
by rewrite (@gdist_cat _ _ [::t3] p) // (gpath_consl gH).
Qed.
Lemma gdist_triangular t1 t2 t3 : `d[t1, t2] <= `d[t1, t3] + `d[t3, t2].
Proof.
have [/gpath_connect[p pH]|/gdist_nconnect->]
:= boolP (connect r t1 t3); last first.
by apply: leq_trans (gdist_card_le _ _) (leq_addr _ _).
have [/gpath_connect [p2 p2H] |/gdist_nconnect->]
:= boolP (connect r t3 t2); last first.
by apply: leq_trans (gdist_card_le _ _) (leq_addl _ _).
rewrite (gpath_dist pH) (gpath_dist p2H) -size_cat.
apply: gdist_path_le.
rewrite cat_path (gpath_path pH).
by rewrite (gpath_last pH) (gpath_path p2H).
by rewrite last_cat (gpath_last pH) (gpath_last p2H).
Qed.
Lemma gdist1 t1 t2 : r t1 t2 -> `d[t1, t2] = (t1 != t2).
Proof.
move=> Hr; apply/eqP.
case: (t1 =P t2) => [<-|/eqP HE]; first by rewrite gdist_eq0.
rewrite eqn_leq -{1}[nat_of_bool _]/(size [::t2]) gdist_path_le /= ?andbT //.
by case: gdist (gdist_eq0 t1 t2); rewrite (negPf HE) .
Qed.
Lemma gdist_succ t1 t2 :
0 < `d[t1, t2] < #|T| -> {t3 | r t1 t3 /\ `d[t3, t2] = `d[t1, t2].-1}.
Proof.
case/andP => dP dT.
move: dT dP.
rewrite -gdist_connect => /gpath_connect[[|t3 p] pH].
by rewrite (gpath_dist pH).
exists t3; split.
by have /andP[] := gpath_path (@gpath_catl _ _ [::t3] _ pH).
by rewrite (gdist_cons pH).
Qed.
Lemma gdist_neighboor t1 t2 t3 : r t1 t2 ->
r t2 t1 -> [|| `d[t2, t3] == `d[t1, t3].-1,
`d[t2, t3] == `d[t1, t3] |
`d[t2, t3] == `d[t1, t3].+1].
Proof.
move=> t1Rt2 t2Rt1.
have : `d[t1, t3] - `d[t1, t2] <= `d[t2, t3] <= `d[t2, t1] + `d[t1, t3].
by rewrite leq_subLR !gdist_triangular.
rewrite (gdist1 t1Rt2) (gdist1 t2Rt1).
(do 2 case: eqP) => //= E1 E2; rewrite ?subn0.
- by rewrite -eqn_leq => /eqP->; rewrite eqxx orbT.
- case/andP=> E3.
rewrite leq_eqVlt => /orP[/eqP->|].
by rewrite eqxx !orbT.
rewrite ltnS => E4.
by rewrite [`d[_, _] == `d[_, _]]eqn_leq E3 E4 orbT.
- case/andP=> E3.
rewrite leq_eqVlt => /orP[/eqP->|].
by rewrite eqxx !orbT.
case: (`d[t1, t3]) E3 => //= d.
rewrite subSS subn0 ltnS => E3 E4.
by rewrite [_ == d]eqn_leq E3 E4.
case/andP=> E3.
rewrite leq_eqVlt => /orP[/eqP->|].
by rewrite eqxx !orbT.
rewrite ltnS leq_eqVlt => /orP[/eqP->|].
by rewrite eqxx !orbT.
case: (`d[t1, t3]) E3 => //= d.
rewrite subSS subn0 ltnS => E3 E4.
by rewrite [_ == d]eqn_leq E3 E4.
Qed.
End gdist.
Notation " `d[ t1 , t2 ]_ r " := (gdist r t1 t2) (at level 10,
format "`d[ t1 , t2 ]_ r").
Section gdistProp.
Variable T : finType.
Variable r : rel T.
Lemma eq_connectn (r1 r2 : rel T) : r1 =2 r2 -> connectn r1 =2 connectn r2.
Proof.
move=> r1Er2.
elim => //= n IH y; apply: eq_big => // i.
by rewrite ![_ \in _]rgraphK r1Er2.
Qed.
Lemma eq_dist (r1 r2 : rel T) : r1 =2 r2 -> gdist r1 =2 gdist r2.
Proof.
move=> r1Er2 t1 t2.
apply: eq_find => n.
by rewrite (eq_connectn r1Er2).
Qed.
Lemma gdist_sym t1 t2 :
`d[t1, t2]_r = `d[t2, t1]_(fun z : T => r^~ z).
Proof.
apply: eq_find => i.
apply/connectnP/connectnP => /= [] [p [H1p H2p H3p]].
exists (rev (belast t1 p)); split => //.
- by rewrite -H2p rev_path.
- rewrite -H2p; case: (p) => //= a p1.
by rewrite rev_cons last_rcons.
by rewrite size_rev size_belast.
exists (rev (belast t2 p)); split => //.
- by rewrite -H2p rev_path.
- rewrite -H2p; case: (p) => //= a p1.
by rewrite rev_cons last_rcons.
by rewrite size_rev size_belast.
Qed.
Lemma gpath_rev t1 t2 p : gpath r t1 t2 p -> gpath (fun z : T => r^~ z) t2 t1 (rev (belast t1 p)).
Proof.
move=> /gpathP[H1 H2] H3.
apply/gpathP; split => //.
- by rewrite -rev_path H2 in H1.
- case: (p) H2 => //= a p1.
by rewrite /= rev_cons last_rcons.
by rewrite size_rev size_belast -gdist_sym.
Qed.
Lemma gdistC t1 t2 : symmetric r -> `d[t1, t2]_r = `d[t2, t1]_r.
Proof.
move=> rSym; rewrite gdist_sym.
by apply: eq_dist.
Qed.
Lemma eq_gpath (e1 e2 : rel T) t1 t2 c :
e1 =2 e2 -> gpath e1 t1 t2 c = gpath e2 t1 t2 c.
Proof.
by move=> e1Ee2; apply/gpathP/gpathP; rewrite (eq_path e1Ee2) (eq_dist e1Ee2).
Qed.
Lemma gpathC t1 t2 p :
symmetric r -> gpath r t1 t2 p -> gpath r t2 t1 (rev (belast t1 p)).
Proof.
move=> hIrr /gpath_rev.
by rewrite (@eq_gpath _ _ _ _ _ (_ : _ =2 r)).
Qed.
End gdistProp.