From mathcomp Require Import all_ssreflect.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

(******************************************************************************)
(*             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).
T:finType
r:rel T
n:nat
x, y:T
reflect
  (exists p : seq T,
     [/\ path r x p, last x p = y & size p = n])
  (y \in connectn n x)
Proof.
2
elim: n x y =>  [x y|n IH x y /=].
568
reflect
  (exists p : seq T,
     [/\ path r x p, last x p = y & size p = 0])
  (y \in connectn 0 x)
567
IH:forall x y : T,
reflect
  (exists p : seq T,
     [/\ path r x p, last x p = y & size p = n])
  (y \in connectn n x)
8
reflect
  (exists p : seq T,
     [/\ path r x p, last x p = y & size p = n.+1])
  (y \in \bigcup_(y in rgraph r x) connectn n y)
  rewrite inE; apply: (iffP idP) => [/eqP->|[[|a l] [] //= _ ->//]].
e
exists p : seq T,
  [/\ path r x p, last x p = x & size p = 0]
10
  by exists [::].
12
14
apply: (iffP idP) => [/bigcupP[i]|[[|i p]//= [H1 H2 H3]]].
56713
x, y, i:T
i \in rgraph r x ->
y \in connectn n i ->
exists p0 : seq T,
  [/\ path r x p0, last x p0 = y & size p0 = n.+1]
567138
H1:true
H2:x = y
H3:0 = n.+1
y \in \bigcup_(y in rgraph r x) connectn n y
5671320
p:seq T
H1:r x i && path r i p
H2:last i p = y
H3:(size p).+1 = n.+1
28
-
1d rewrite [i \in _]rgraphK => iRk /IH [p [H1 H2 H3]].
5671320
iRk:r x i
2b
H1:path r i p
2d
H3:size p = n
exists p : seq T,
  [/\ path r x p, last x p = y & size p = n.+1]
22
  by exists (i :: p); split; rewrite /= ?(iRk, H3).
24
28
29
-
39 by [].
2a
28
case/andP: H1 => H11 H12.
56713202b2d2e
H11:r x i
H12:path r i p
28
have F : i \in rgraph r x by rewrite [_ \in _]rgraphK.
56713202b2d2e4445
F:i \in rgraph r x
28 
apply: (subsetP (bigcup_sup _ F)).
49
y \in connectn n i
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).
56
t1, t2:T
( `d[t1, t2]  == 0) = (t1 == t2)
Proof.
50
have tG : #|T| > 0 by rewrite (cardD1 t1).
5653
tG:0 < #|T|
54
rewrite /gdist.
59
(find (fun n : nat => t2 \in connectn n t1)
   (iota 0 #|T|) == 0) = (t1 == t2)
case: #|_| tG => // n _.
56537
(find (fun n : nat => t2 \in connectn n t1)
   (iota 0 n.+1) == 0) = (t1 == t2)
rewrite (iota_add _ 1) /= inE [t2 == _]eq_sym.
62
((if t1 == t2
  then 0
  else
   (find (fun n : nat => t2 \in connectn n t1)
      (iota (0 + 1) n)).+1) == 0) = (t1 == t2)
by case: (t1 =P t2).
Qed.

Lemma gdist_gt0 t1 t2 : (0 < `d[t1, t2]) = (t1 != t2).
52
(0 <  `d[t1, t2] ) = (t1 != t2)
Proof.
69 by rewrite ltnNge leqn0 gdist_eq0. Qed.

Lemma gdist0 t : `d[t, t] = 0.
56
t:T
 `d[t, t]  = 0
Proof.
6e by apply/eqP; rewrite gdist_eq0. Qed.

Lemma gdist_card_le t1 t2 : `d[t1, t2] <= #|T|.
52
 `d[t1, t2]  <= #|T|
Proof.
75
rewrite -[#|T|](size_iota 0).
52
 `d[t1, t2]  <= size (iota 0 #|T|)
apply: find_size.
Qed.

Lemma gdist_path_le t1 t2 p :
  path r t1 p -> last t1 p = t2 -> `d[t1, t2] <= size p.
56532b
path r t1 p ->
last t1 p = t2 ->  `d[t1, t2]  <= size p
Proof.
7e
move=> Hp Hl.
56532b
Hp:path r t1 p
Hl:last t1 p = t2
 `d[t1, t2]  <= size p
have [tLp|pLt] := leqP #|T| (size p).
56532b8788
tLp:#|T| <= size p
89
56532b8788
pLt:size p < #|T|
89
  apply: leq_trans tLp.
86
77
8f
  by apply: gdist_card_le.
91
89
have F : t2 \in connectn (size p) t1.
91
t2 \in connectn (size p) t1
56532b878892
F:t2 \in connectn (size p) t1
89
  by apply/connectnP; exists p.
9f
89
case: leqP => // /(before_find _) // /(_ 0).
9f
(t2 \in connectn (nth 0 (iota 0 #|T|) (size p)) t1) =
false -> false
by rewrite seq.nth_iota // F.
Qed.

Lemma gdist_connect t1 t2 : connect r t1 t2 = (`d[t1,t2] < #|T|).
52
connect r t1 t2 = ( `d[t1, t2]  < #|T|)
Proof.
a9
apply/connectP/idP=> [[p /shortenP[p' Hp' Hu _ Ht]]|].
5653
p, p':seq T
Hp':path r t1 p'
Hu:uniq (t1 :: p')
Ht:t2 = last t1 p'
 `d[t1, t2]  < #|T|
52
 `d[t1, t2]  < #|T| ->
exists2 p : seq T, path r t1 p & t2 = last t1 p
  apply: leq_trans (_ : size p' < _).
b0
 `d[t1, t2]  < (size p').+1
b0
size p' < #|T|
b7
    by apply: gdist_path_le.
b0
bf
b6
  rewrite -[_.+1]/(size (t1 :: p')) cardE.
b0
size (t1 :: p') <= size (enum T)
b6
  apply: uniq_leq_size => // i.
5653b1b2b3b4
i:T
i \in t1 :: p' -> i \in enum T
b6
  by rewrite mem_enum.
52
b8
rewrite -[#|_|](size_iota 0) -has_find.
52
has (fun n : nat => t2 \in connectn n t1)
  (iota 0 #|T|) ->
exists2 p : seq T, path r t1 p & t2 = last t1 p
move => /hasP[n _ /connectnP [p [H1p H2p H3p]]].
5653
n:nat_eqType
2b
H1p:path r t1 p
H2p:last t1 p = t2
H3p:size p = n
exists2 p : seq T, path r t1 p & t2 = last t1 p
by exists p.
Qed.

Lemma gdist_nconnect t1 t2 : ~~ connect r t1 t2 -> `d[t1,t2] = #|T|.
52
~~ connect r t1 t2 ->  `d[t1, t2]  = #|T|
Proof.
de
move=> H; apply/eqP.
5653
H:~~ connect r t1 t2
 `d[t1, t2]  == #|T|
have := gdist_card_le t1 t2.
e5
 `d[t1, t2]  <= #|T| ->  `d[t1, t2]  == #|T|
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).
80
reflect
  [/\ path r t1 p, last t1 p = t2
    &  `d[t1, t2]  = size p] (gpath t1 t2 p)
Proof.
ed
apply: (iffP and3P) => [[t1Pp /eqP t1pLt2 /eqP t1t2D]|
                        [t1Pp t1pLt2 t1t2D]]; first by split.
56532b
t1Pp:path r t1 p
t1pLt2:last t1 p = t2
t1t2D: `d[t1, t2]  = size p
[/\ path r t1 p, last t1 p == t2
  &  `d[t1, t2]  == size p]
by split => //; apply/eqP.
Qed.

Lemma gpath_connect t1 t2 : connect r t1 t2 -> {p | gpath t1 t2 p}.
52
connect r t1 t2 -> {p : seq T | gpath t1 t2 p}
Proof.
fa
move=> t1Ct2.
5653
t1Ct2:connect r t1 t2
{p : seq T | gpath t1 t2 p}
case: (pickP [pred p | gpath t1 t2 (p : `d[t1, t2].-tuple T)]) => [p Hp|HC].
5653102
p:tuple_finType  `d[t1, t2]  T
Hp:[pred p | gpath t1 t2 p] p
103
5653102
HC:[pred p | gpath t1 t2 p] =1 xpred0
103
  by exists p.
10c
103
move: (t1Ct2); rewrite gdist_connect => dLT.
565310210d
dLT: `d[t1, t2]  < #|T|
103
absurd False => //.
114
False
move: (dLT); rewrite -[#|_|](size_iota 0) -has_find.
114
has (fun n : nat => t2 \in connectn n t1)
  (iota 0 #|T|) -> False
move => /(nth_find 0).
114
t2
  \in connectn
        (nth 0 (iota 0 #|T|)
           (find (fun n : nat => t2 \in connectn n t1)
              (iota 0 #|T|))) t1 -> False
rewrite -[find _ _]/`d[t1, t2].
114
t2 \in connectn (nth 0 (iota 0 #|T|)  `d[t1, t2] ) t1 ->
False
rewrite nth_iota // add0n => /connectnP[p [H1p H2p /eqP H3p]].
565310210d1152bd9da
H3p:size p ==  `d[t1, t2] 
119
have /idP[] := HC (Tuple H3p).
129
[pred p | gpath t1 t2 p] (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.
80
gpath t1 t2 p -> last t1 p = t2
Proof.
130 by case/gpathP. Qed.

Lemma gpath_dist t1 t2 p : gpath t1 t2 p -> `d[t1, t2] = size p.
80
gpath t1 t2 p ->  `d[t1, t2]  = size p
Proof.
135 by case/gpathP. Qed.

Lemma gpath_path t1 t2 p : gpath t1 t2 p -> path r t1 p.
80
gpath t1 t2 p -> path r t1 p
Proof.
13a 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.
56
A:Type
p:seq A
t, t1:A
j:nat
j <= size p -> last t1 (take j p) = nth t (t1 :: p) j
Proof.
13f
elim: p t1 j => [t1 [|] //| a l IH t1 [|j]] //= H.
56142
t, a:A
l:seq A
IH:forall (t1 : A) (j : nat),
j <= size l ->
last t1 (take j l) = nth t (t1 :: l) j
t1:A
145
H:j < (size l).+1
last a (take j l) = nth t (a :: l) j
by apply: IH.
Qed.

(* ugly proof !! *)
Lemma gpath_uniq t1 t2 p : gpath t1 t2 p ->  uniq (t1 :: p).
80
gpath t1 t2 p -> uniq (t1 :: p)
Proof.
153
move=> gH; apply/(uniqP t1) => i j iH jH.
56532b
gH:gpath t1 t2 p
i, j:nat
iH:i \in gtn (size (t1 :: p))
jH:j \in gtn (size (t1 :: p))
nth t1 (t1 :: p) i = nth t1 (t1 :: p) j -> i = j
wlog : i j iH jH / i <= j.
15a
(forall i j : nat,
 i \in gtn (size (t1 :: p)) ->
 j \in gtn (size (t1 :: p)) ->
 i <= j ->
 nth t1 (t1 :: p) i = nth t1 (t1 :: p) j -> i = j) ->
nth t1 (t1 :: p) i = nth t1 (t1 :: p) j -> i = j
15a
i <= j ->
nth t1 (t1 :: p) i = nth t1 (t1 :: p) j -> i = j
  move=> H; case: (leqP i j) => [iLj|jLi]; first by apply: H.
56532b15b15c15d15e
H:forall i j : nat,
i \in gtn (size (t1 :: p)) ->
j \in gtn (size (t1 :: p)) ->
i <= j ->
nth t1 (t1 :: p) i = nth t1 (t1 :: p) j -> i = j
jLi:j < i
15f
164
  by move=> /(@sym_equal _ _ _) /H->; rewrite // ltnW.
15a
166
rewrite leq_eqVlt => /orP[/eqP->//|iLj].
56532b15b15c15d15e
iLj:i < j
15f
case/gpathP : gH  => t1Pp t1pLt2 dt1t2E.
56532b15c15d15e174f5f6
dt1t2E: `d[t1, t2]  = size p
15f
case: j jH iLj => j // jH iLj.
56532b
i:nat
15df5f6179145
jH:j.+1 \in gtn (size (t1 :: p))
iLj:i < j.+1
nth t1 (t1 :: p) i = nth t1 (t1 :: p) j.+1 -> i = j.+1
case: i iH iLj => [_ _ t1E | ] //.
56532bf5f617914517f
t1E:nth t1 (t1 :: p) 0 = nth t1 (t1 :: p) j.+1
0 = j.+1
56532bf5f617914517f
forall n : nat,
n.+1 \in gtn (size (t1 :: p)) ->
n.+1 < j.+1 ->
nth t1 (t1 :: p) n.+1 = nth t1 (t1 :: p) j.+1 ->
n.+1 = j.+1
  pose p1 := drop j.+1 p.
56532bf5f617914517f186
p1:=drop j.+1 p:seq T
187
188
  have t1Pp1 : path r t1 p1.
18f
path r t1 p1
56532bf5f617914517f186190
t1Pp1:path r t1 p1
187
189
    move: (t1Pp); rewrite -[p](cat_take_drop j.+1) cat_path.
18f
path r t1 (take j.+1 p) &&
path r (last t1 (take j.+1 p)) (drop j.+1 p) ->
path r t1 p1
195
    rewrite /= in t1E.
56532bf5f617914517f190
t1E:t1 = nth t1 p j
19c
195
    by rewrite (last_take t1) //= -t1E => /andP[].
197
187
188
  have t1p1L : last t1 p1 = t2.
197
last t1 p1 = t2
56532bf5f617914517f186190198
t1p1L:last t1 p1 = t2
187
189
    move: (t1pLt2); rewrite -[p](cat_take_drop j.+1) last_cat.
197
last (last t1 (take j.+1 p)) (drop j.+1 p) = t2 ->
last t1 p1 = t2
1a9
    rewrite /= in t1E.
56532bf5f617914517f1901981a1
1b0
1a9
    by rewrite (last_take t1) //= -t1E.
1ab
187
188
  have [] := boolP (`d[t1, t2] <= size p1) => [|/negP[]]; last first.
1ab
 `d[t1, t2]  <= size p1
1ab
 `d[t1, t2]  <= size p1 -> 0 = j.+1
189
    by apply: gdist_path_le.
1ab
1be
188
  rewrite leqNgt => /negP[].
1ab
size p1 <  `d[t1, t2] 
188 
  rewrite size_drop dt1t2E.
1ab
size p - j.+1 < size p
188
  rewrite /= in t1E.
56532bf5f617914517f1901981ac1a1
1c9
188
  by rewrite -{2}[size p](subnK (_ : j < size p)) // addnS ltnS leq_addr.
18a
18b
move=> i iH; rewrite ltnS => iLj nE.
56532bf5f617914517f17e
iH:i.+1 \in gtn (size (t1 :: p))
174
nE:nth t1 (t1 :: p) i.+1 = nth t1 (t1 :: p) j.+1
i.+1 = j.+1
pose p1 := take i.+1 p ++ drop j.+1 p.
56532bf5f617914517f17e1d51741d6
p1:=take i.+1 p ++ drop j.+1 p:seq T
1d7
have [] := boolP (`d[t1, t2] <= size p1) => [|/negP[]].
1db
 `d[t1, t2]  <= size p1 -> i.+1 = j.+1
1db
1bb
  rewrite leqNgt => /negP[].
1db
1c5
1e1
  rewrite size_cat size_take size_drop ifT //; last first.
1db
i.+1 < size p
1db
i.+1 + (size p - j.+1) <  `d[t1, t2] 
1e2
    by rewrite -ltnS in iLj; apply: leq_trans iLj _.
1db
1ec
1e1
  rewrite dt1t2E -{2}[size p](subnK (_ : j < size _)) //.
1db
i.+1 + (size p - j.+1) < size p - j.+1 + j.+1
1e1
  by rewrite addnC ltn_add2l.
1db
1bb
apply: gdist_path_le.
1db
194
1db
1a8
  move: t1Pp; rewrite -[p](cat_take_drop i.+1).
56532bf617914517f17e1d51741d61dc
path r t1 (take i.+1 p ++ drop i.+1 p) -> path r t1 p1
1fa
  rewrite -[drop _ _](cat_take_drop (j - i)) !cat_path.
1ff
[&& path r t1 (take i.+1 p),
    path r (last t1 (take i.+1 p))
      (take (j - i) (drop i.+1 p))
  & path r
      (last (last t1 (take i.+1 p))
         (take (j - i) (drop i.+1 p)))
      (drop (j - i) (drop i.+1 p))] ->
path r t1 (take i.+1 p) &&
path r (last t1 (take i.+1 p)) (drop j.+1 p)
1fa
  case/and3P => [-> _] /=.
1ff
path r
  (last (last t1 (take i.+1 p))
     (take (j - i) (drop i.+1 p)))
  (drop (j - i) (drop i.+1 p)) ->
path r (last t1 (take i.+1 p)) (drop j.+1 p)
1fa
  rewrite !(last_take t1) /=; last first.
1ff
j - i <= size (drop i.+1 p)
1ff
i < size p
1ff
path r (nth t1 (nth t1 p i :: drop i.+1 p) (j - i))
  (drop (j - i) (drop i.+1 p)) ->
path r (nth t1 p i) (drop j.+1 p)
1fb
  -
20a rewrite size_drop -subSS.
1ff
j.+1 - i.+1 <= size p - i.+1
20d
    by apply: leq_sub2r.
1ff
20f
2101fb
  -
218 by apply: leq_trans iLj _; rewrite ltnW //.
1ff
211
1fa
  rewrite drop_drop addnS subnK; last by rewrite ltnW.
1ff
path r (nth t1 (nth t1 p i :: drop i.+1 p) (j - i))
  (drop j.+1 p) -> path r (nth t1 p i) (drop j.+1 p)
1fa
  congr path.
1ff
nth t1 (nth t1 p i :: drop i.+1 p) (j - i) =
nth t1 p i
1fa
  move: (nE) => /= ->.
1ff
nth t1 (nth t1 p j :: drop i.+1 p) (j - i) =
nth t1 p j
1fa
  rewrite -[j - i]prednK //.
1ff
nth t1 (nth t1 p j :: drop i.+1 p) (j - i).-1.+1 =
nth t1 p j
1ff
0 < j - i
1fb
  by rewrite /= nth_drop -subnS addnC subnK //.
1ff
231
1fa
  by rewrite subn_gt0.
1db
1a8
rewrite last_cat (last_take t1) // nE.
1db
last (nth t1 (t1 :: p) j.+1) (drop j.+1 p) = t2
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.
5653
p1, p2:seq T
gpath t1 t2 (p1 ++ p2) -> gpath t1 (last t1 p1) p1
Proof.
23d
move=> /gpathP[].
23f
path r t1 (p1 ++ p2) ->
last t1 (p1 ++ p2) = t2 ->
 `d[t1, t2]  = size (p1 ++ p2) ->
gpath t1 (last t1 p1) p1
rewrite cat_path last_cat => /andP[t1Pp1 t1p1LPp2] t1p1Lp2Lt2 dt1t2E.
5653240198
t1p1LPp2:path r (last t1 p1) p2
t1p1Lp2Lt2:last (last t1 p1) p2 = t2
dt1t2E: `d[t1, t2]  = size (p1 ++ p2)
gpath t1 (last t1 p1) p1
apply/gpathP; split => //.
24a
 `d[t1, last t1 p1]  = size p1 
have : `d[t1, last t1 p1] <= size p1 by rewrite gdist_path_le.
24a
 `d[t1, last t1 p1]  <= size p1 ->
 `d[t1, last t1 p1]  = size p1
rewrite leq_eqVlt => /orP[/eqP//|dLSp1].
565324019824b24c24d
dLSp1: `d[t1, last t1 p1]  < size p1
252
have /gpath_connect[p3 /gpathP[H1 H2 H3]] : 
   connect r t1 (last t1 p1) by apply/connectP; exists p1.
565324019824b24c24d25b
p3:seq T
H1:path r t1 p3
H2:last t1 p3 = last t1 p1
H3: `d[t1, last t1 p1]  = size p3
252
have : size (p3 ++ p2) < `d[t1, t2] by rewrite dt1t2E !size_cat -H3 ltn_add2r.
25f
size (p3 ++ p2) <  `d[t1, t2]  ->
 `d[t1, last t1 p1]  = size p1
rewrite ltnNge => /negP[].
25f
 `d[t1, t2]  <= size (p3 ++ p2)
apply: gdist_path_le; first by rewrite cat_path H1 // H2.
25f
last t1 (p3 ++ p2) = t2
by rewrite last_cat H2.
Qed.

Lemma gpath_catr t1 t2 p1 p2 : 
   gpath t1 t2 (p1 ++ p2) -> gpath (last t1 p1) t2 p2.
23f
gpath t1 t2 (p1 ++ p2) -> gpath (last t1 p1) t2 p2
Proof.
271
move=> /gpathP[].
23f
path r t1 (p1 ++ p2) ->
last t1 (p1 ++ p2) = t2 ->
 `d[t1, t2]  = size (p1 ++ p2) ->
gpath (last t1 p1) t2 p2
rewrite cat_path last_cat => /andP[t1Pp1 t1p1LPp2] t1p1Lp2Lt2 dt1t2E.
24a
gpath (last t1 p1) t2 p2
apply/gpathP; split => //.
24a
 `d[last t1 p1, t2]  = size p2 
have : `d[last t1 p1, t2] <= size p2 by rewrite gdist_path_le.
24a
 `d[last t1 p1, t2]  <= size p2 ->
 `d[last t1 p1, t2]  = size p2
rewrite leq_eqVlt => /orP[/eqP//|dLSp1].
565324019824b24c24d
dLSp1: `d[last t1 p1, t2]  < size p2
280
have /gpath_connect[p3 /gpathP[H1 H2 H3]] : 
   connect r (last t1 p1) t2 by apply/connectP; exists p2.
565324019824b24c24d289260
H1:path r (last t1 p1) p3
H2:last (last t1 p1) p3 = t2
H3: `d[last t1 p1, t2]  = size p3
280
have : size (p1 ++ p3) < `d[t1, t2] by rewrite dt1t2E !size_cat -H3 ltn_add2l.
28d
size (p1 ++ p3) <  `d[t1, t2]  ->
 `d[last t1 p1, t2]  = size p2
rewrite ltnNge => /negP[].
28d
 `d[t1, t2]  <= size (p1 ++ p3)
apply: gdist_path_le; first by rewrite cat_path H1 andbT.
28d
last t1 (p1 ++ p3) = t2
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].
23f
gpath t1 t2 (p1 ++ p2) ->
 `d[t1, t2]  =
 `d[t1, last t1 p1]  +  `d[last t1 p1, t2] 
Proof.
29e
move=> gH.
5653240
gH:gpath t1 t2 (p1 ++ p2)
 `d[t1, t2]  =
 `d[t1, last t1 p1]  +  `d[last t1 p1, t2] 
rewrite (gpath_dist gH).
2a5
size (p1 ++ p2) =
 `d[t1, last t1 p1]  +  `d[last t1 p1, t2] 
rewrite (gpath_dist (gpath_catl gH)) (gpath_dist (gpath_catr gH)) //.
2a5
size (p1 ++ p2) = size p1 + size p2
by rewrite size_cat.
Qed. 

Lemma gpath_consl t1 t2 t3 p :  gpath t1 t2 (t3 :: p) -> `d[t1, t3] = 1.
56
t1, t2, t3:T
2b
gpath t1 t2 (t3 :: p) ->  `d[t1, t3]  = 1
Proof.
2b1 by move=> /(@gpath_catl _ _ [::t3]) /= /gpathP[]. Qed.

Lemma gpath_consr t1 t2 t3 p : gpath t1 t2 (t3 :: p) -> gpath t3 t2 p.
2b3
gpath t1 t2 (t3 :: p) -> gpath t3 t2 p
Proof.
2b8 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.
2b3
gpath t1 t2 (t3 :: p) ->
 `d[t1, t2]  =  `d[t3, t2] .+1
Proof.
2bd
move=> gH.
562b42b
gH:gpath t1 t2 (t3 :: p)
 `d[t1, t2]  =  `d[t3, t2] .+1
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].
562b4
 `d[t1, t2]  <=  `d[t1, t3]  +  `d[t3, t2] 
Proof.
2c8
have [/gpath_connect[p pH]|/gdist_nconnect->] 
         := boolP (connect r t1 t3); last first.
2ca
 `d[t1, t2]  <= #|T| +  `d[t3, t2] 
562b42b
pH:gpath t1 t3 p
2cb
  by apply: leq_trans (gdist_card_le _ _) (leq_addr _ _).
2d3
2cb
have [/gpath_connect [p2 p2H] |/gdist_nconnect->] 
         := boolP (connect r t3 t2); last first.
2d3
 `d[t1, t2]  <=  `d[t1, t3]  + #|T|
562b42b2d4
p2:seq T
p2H:gpath t3 t2 p2
2cb
  by apply: leq_trans (gdist_card_le _ _) (leq_addl _ _).
2de
2cb
rewrite (gpath_dist pH) (gpath_dist p2H) -size_cat.
2de
 `d[t1, t2]  <= size (p ++ p2)
apply: gdist_path_le.
2de
path r t1 (p ++ p2)
2de
last t1 (p ++ p2) = t2
  rewrite cat_path (gpath_path pH).
2de
true && path r (last t1 p) p2
2ec
  by rewrite (gpath_last pH) (gpath_path p2H).
2de
2ee
by rewrite last_cat (gpath_last pH) (gpath_last p2H).
Qed.

Lemma gdist1 t1 t2 : r t1 t2 -> `d[t1, t2] = (t1 != t2).
52
r t1 t2 ->  `d[t1, t2]  = (t1 != t2)
Proof.
2f7
move=> Hr; apply/eqP.
5653
Hr:r t1 t2
 `d[t1, t2]  == (t1 != t2)
case: (t1 =P t2) => [<-|/eqP HE]; first by rewrite gdist_eq0.
56532ff
HE:t1 != t2
 `d[t1, t2]  == ~~ false
rewrite eqn_leq -{1}[nat_of_bool _]/(size [::t2]) gdist_path_le /= ?andbT //.
304
0 <  `d[t1, t2] 
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}.
52
0 <  `d[t1, t2]  < #|T| ->
{t3 : T | r t1 t3 /\  `d[t3, t2]  =  `d[t1, t2] .-1}
Proof.
30c
case/andP => dP dT.
5653
dP:0 <  `d[t1, t2] 
dT: `d[t1, t2]  < #|T|
{t3 : T | r t1 t3 /\  `d[t3, t2]  =  `d[t1, t2] .-1}
move: dT dP.
52
 `d[t1, t2]  < #|T| ->
0 <  `d[t1, t2]  ->
{t3 : T | r t1 t3 /\  `d[t3, t2]  =  `d[t1, t2] .-1}
rewrite -gdist_connect => /gpath_connect[[|t3 p] pH].
5653
pH:gpath t1 t2 [::]
0 <  `d[t1, t2]  ->
{t3 : T | r t1 t3 /\  `d[t3, t2]  =  `d[t1, t2] .-1}
562b42b
pH:gpath t1 t2 (t3 :: p)
320
  by rewrite (gpath_dist pH).
323
320
exists t3; split.
562b42b324314
r t1 t3
32b
 `d[t3, t2]  =  `d[t1, t2] .-1
  by have /andP[] := gpath_path (@gpath_catl _ _ [::t3] _ pH).
32b
32f
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].
2ca
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.
334
move=> t1Rt2 t2Rt1.
562b4
t1Rt2:r t1 t2
t2Rt1:r t2 t1
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
have : `d[t1, t3] - `d[t1, t2] <= `d[t2, t3] <= `d[t2, t1] + `d[t1, t3].
33b
 `d[t1, t3]  -  `d[t1, t2]  <=  `d[t2, t3]  <=
 `d[t2, t1]  +  `d[t1, t3] 
33b
 `d[t1, t3]  -  `d[t1, t2]  <=  `d[t2, t3]  <=
 `d[t2, t1]  +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
  by rewrite leq_subLR !gdist_triangular.
33b
345
rewrite (gdist1 t1Rt2) (gdist1 t2Rt1).
33b
 `d[t1, t3]  - (t1 != t2) <=  `d[t2, t3]  <=
(t2 != t1) +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
(do 2 case: eqP) => //= E1 E2; rewrite ?subn0.
562b433c33d
E1:t2 = t1
E2:t1 = t2
 `d[t1, t3]  <=  `d[t2, t3]  <= 0 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
562b433c33d
E1:t2 <> t1
352
 `d[t1, t3]  <=  `d[t2, t3]  <= 1 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
562b433c33d351
E2:t1 <> t2
 `d[t1, t3]  - 1 <=  `d[t2, t3]  <= 0 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
562b433c33d35735b
 `d[t1, t3]  - 1 <=  `d[t2, t3]  <= 1 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
-
34e by rewrite -eqn_leq => /eqP->; rewrite eqxx orbT.
356
358
35935d
-
362 case/andP=> E3.
562b433c33d357352
E3: `d[t1, t3]  <=  `d[t2, t3] 
 `d[t2, t3]  <= 1 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
364
  rewrite leq_eqVlt => /orP[/eqP->|].
369
[|| 1 +  `d[t1, t3]  ==  `d[t1, t3] .-1,
    1 +  `d[t1, t3]  ==  `d[t1, t3] 
  | 1 +  `d[t1, t3]  ==  `d[t1, t3] .+1]
369
 `d[t2, t3]  < 1 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
35935d
    by rewrite eqxx !orbT.
369
372
364
  rewrite ltnS => E4.
562b433c33d35735236a
E4: `d[t2, t3]  <=  `d[t1, t3] 
33e
364
  by rewrite [`d[_, _] == `d[_, _]]eqn_leq E3 E4 orbT.
35a
35c
35d
-
37c case/andP=> E3.
562b433c33d35135b
E3: `d[t1, t3]  - 1 <=  `d[t2, t3] 
 `d[t2, t3]  <= 0 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
37e
  rewrite leq_eqVlt => /orP[/eqP->|].
383
[|| 0 +  `d[t1, t3]  ==  `d[t1, t3] .-1,
    0 +  `d[t1, t3]  ==  `d[t1, t3] 
  | 0 +  `d[t1, t3]  ==  `d[t1, t3] .+1]
383
 `d[t2, t3]  < 0 +  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
35d
    by rewrite eqxx !orbT.
383
38c
37e
  case: (`d[t1, t3]) E3 => //= d.
562b433c33d35135b
d:nat
d.+1 - 1 <=  `d[t2, t3]  ->
 `d[t2, t3]  < 0 + d.+1 ->
[||  `d[t2, t3]  == d,  `d[t2, t3]  == d.+1
  |  `d[t2, t3]  == d.+2]
37e
  rewrite subSS subn0 ltnS => E3 E4.
562b433c33d35135b394
E3:d <=  `d[t2, t3] 
E4: `d[t2, t3]  <= d
[||  `d[t2, t3]  == d,  `d[t2, t3]  == d.+1
  |  `d[t2, t3]  == d.+2]
37e
  by rewrite [_ == d]eqn_leq E3 E4.
35e
35f
case/andP=> E3.
562b433c33d35735b384
36b
rewrite leq_eqVlt => /orP[/eqP->|].
3a3
36f
3a3
372
  by rewrite eqxx !orbT.
3a3
372
rewrite ltnS leq_eqVlt => /orP[/eqP->|].
3a3
[||  `d[t1, t3]  ==  `d[t1, t3] .-1,
     `d[t1, t3]  ==  `d[t1, t3] 
  |  `d[t1, t3]  ==  `d[t1, t3] .+1]
3a3
 `d[t2, t3]  <  `d[t1, t3]  ->
[||  `d[t2, t3]  ==  `d[t1, t3] .-1,
     `d[t2, t3]  ==  `d[t1, t3] 
  |  `d[t2, t3]  ==  `d[t1, t3] .+1]
  by rewrite eqxx !orbT.
3a3
3b2
case: (`d[t1, t3]) E3 => //= d.
562b433c33d35735b394
d.+1 - 1 <=  `d[t2, t3]  ->
 `d[t2, t3]  < d.+1 ->
[||  `d[t2, t3]  == d,  `d[t2, t3]  == d.+1
  |  `d[t2, t3]  == d.+2]
rewrite subSS subn0 ltnS => E3 E4.
562b433c33d35735b39439a39b
39c
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.
5
r, r1, r2:rel T
r1 =2 r2 -> connectn r1 =2 connectn r2
Proof.
3c0
move=> r1Er2.
53c3
r1Er2:r1 =2 r2
connectn r1 =2 connectn r2
elim => //= n IH y; apply: eq_big => // i.
53c33ca7
IH:forall y : T, connectn r1 n y = connectn r2 n y
y, i:T
(i \in rgraph r1 y) = (i \in rgraph r2 y)
by rewrite ![_ \in _]rgraphK r1Er2.
Qed.

Lemma eq_dist (r1 r2 : rel T) : r1 =2 r2 -> gdist r1 =2 gdist r2.
3c2
r1 =2 r2 -> gdist r1 =2 gdist r2
Proof.
3d4
move=> r1Er2 t1 t2.
53c33ca53
`d[t1, t2]_r1 = `d[t1, t2]_r2
apply: eq_find => n.
53c33ca537
(t2 \in connectn r1 n t1) = (t2 \in connectn r2 n t1)
by rewrite (eq_connectn r1Er2).
Qed.

Lemma gdist_sym t1 t2 :
 `d[t1, t2]_r  =  `d[t2, t1]_(fun z : T => r^~ z).
52
`d[t1, t2]_r = `d[t2, t1]_(fun z : T => r^~ z)
Proof.
3e3
apply: eq_find => i.
565317e
(t2 \in connectn r i t1) =
(t1 \in connectn (fun z : T => r^~ z) i t2)
apply/connectnP/connectnP => /= [] [p [H1p H2p H3p]].
565317e2bd9da
H3p:size p = i
exists p : seq T,
  [/\ path (fun z : T => r^~ z) t2 p, last t2 p = t1
    & size p = i]
565317e2b
H1p:path (fun z : T => r^~ z) t2 p
H2p:last t2 p = t1
3f0
exists p : seq T,
  [/\ path r t1 p, last t1 p = t2 & size p = i]
  exists (rev (belast t1 p)); split => //.
3ef
path (fun z : T => r^~ z) t2 (rev (belast t1 p))
3ef
last t2 (rev (belast t1 p)) = t1
3ef
size (rev (belast t1 p)) = i
3f3
  -
3f9 by rewrite -H2p rev_path.
3ef
3fe
3ff3f3
  -
403 rewrite -H2p; case: (p) => //= a p1.
565317e2bd9da3f0
a:T
p1:seq T
last (last a p1) (rev (t1 :: belast a p1)) = t1
405
    by rewrite rev_cons last_rcons.
3ef
400
3f2
  by rewrite size_rev size_belast.
3f4
3f7
exists (rev (belast t2 p)); split => //.
3f4
path r t1 (rev (belast t2 p))
3f4
last t1 (rev (belast t2 p)) = t2
3f4
size (rev (belast t2 p)) = i
-
415 by rewrite -H2p rev_path.
3f4
41a
41b
-
41f rewrite -H2p; case: (p) => //= a p1.
565317e2b3f53f63f040b40c
last (last a p1) (rev (t2 :: belast a p1)) = t2
421
  by rewrite rev_cons last_rcons.
3f4
41c
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)).
80
gpath r t1 t2 p ->
gpath (fun z : T => r^~ z) t2 t1 (rev (belast t1 p))
Proof.
42c
move=> /gpathP[H1 H2] H3.
56532b
H1:path r t1 p
H2:last t1 p = t2
H3:`d[t1, t2]_r = size p
gpath (fun z : T => r^~ z) t2 t1 (rev (belast t1 p))
apply/gpathP; split => //.
433
3fb
433
3fe
433
`d[t2, t1]_(fun z : T => r^~ z) =
size (rev (belast t1 p))
-
439 by rewrite -rev_path H2 in H1.
433
3fe
43d
-
441 case: (p) H2 => //= a p1.
56532b43443640b40c
last a p1 = t2 ->
last t2 (rev (t1 :: belast a p1)) = t1
443
  by rewrite /= rev_cons last_rcons.
433
43e
by rewrite size_rev size_belast -gdist_sym.
Qed.

Lemma gdistC t1 t2 : symmetric r -> `d[t1, t2]_r  =  `d[t2, t1]_r.
52
symmetric r -> `d[t1, t2]_r = `d[t2, t1]_r
Proof.
44e
move=> rSym; rewrite gdist_sym.
5653
rSym:symmetric r
`d[t2, t1]_(fun z : T => r^~ z) = `d[t2, t1]_r
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.
5
r, e1, e2:rel T
53
c:seq T
e1 =2 e2 -> gpath e1 t1 t2 c = gpath e2 t1 t2 c
Proof.
459
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)).
80
symmetric r ->
gpath r t1 t2 p -> gpath r t2 t1 (rev (belast t1 p))
Proof.
461
move=> hIrr /gpath_rev.
56532b
hIrr:symmetric r
gpath (fun z : T => r^~ z) t2 t1 (rev (belast t1 p)) ->
gpath r t2 t1 (rev (belast t1 p))
by rewrite (@eq_gpath _ _ _ _ _ (_ : _ =2 r)).
Qed.

End gdistProp.