# Library connect

(c) Copyright Microsoft Corporation and Inria. All rights reserved.

This file develops the theory of transitive closure in a finType T.
For e : rel T and f : T -> T we define:

dfs e n a x    == the list of points traversed by a depth-first search of
the graph of e, at depth n, starting from x, and
prepended to a
connect e      == the transitive closure of e (computed by dfs)
connect_sym e  <=> connect e is symmetric, hence an equivalence relation
root e x       == pick a representative of connect e x, the component of
x in the transitive closure of e
roots e        == the codomain predicate of root e
n_comp e       == number of components of connect e, i.e., the number of
equivalence classes of connect e if connect_sym e holds
closed e a     == the predicate a is e-invariant
closure e a    == closure under e of a (the image of a under connect e)
rel_adjunction h e e' a
<=> in the e-closed domain a, h is the left part of an
adjunction from e to another relation e'
fconnect f     == connect (frel f) == connected under f iteration
froot f x      == root (frel f) x == root of the orbit of x under f
froots f       == roots (frel f) == orbit representatives for f
orbit f x      == lists the f orbit of x
findex f x y   == index of y in the f-orbit of x
order f x      == size (cardinal) of the orbit of x under f
order_set f n  == elements of f-order n
finv f         == the inverse of f, if f is a permutation; specifically,
finv f x == iter (order x).-1 f x
fcard f        == number of orbits of f
fclosed f a    == closed under iteration of f
fclosure f a   == closure under f iteration


Import Prenex Implicits.

Decidable connectivity in finite types.


Section Connect.

Variables (T : finType) (e : rel T).

Fixpoint dfs (n : nat) (a : seq T) (x : T) {struct n} :=
if n is n'.+1 then
if x \in a then a else foldl (dfs n') (x :: a) (enum (e x))
else a.

Definition connect : rel T := fun x y => y \in dfs #|T| [::] x.

Lemma subset_dfs : forall n (a b : seq T), a \subset foldl (dfs n) a b.

Inductive dfs_path x y (a : seq T) : Prop :=
DfsPath p of path e x p & y = last x p & [disjoint x :: p & a].

Lemma dfsP : forall n x y (a : seq T),
#|T| <= #|a| + n -> y \notin a -> reflect (dfs_path x y a) (y \in dfs n a x).

Lemma connectP : forall x y,
reflect (exists2 p, path e x p & y = last x p) (connect x y).

Lemma connect_trans : forall x1 x2 x3,
connect x1 x2 -> connect x2 x3 -> connect x1 x3.

Lemma connect0 : forall x, connect x x.

Lemma eq_connect0 : forall x y : T, x = y -> connect x y.

Lemma connect1 : forall x y, e x y -> connect x y.

Lemma path_connect : forall x p, path e x p ->
subpred (mem (x :: p)) (connect x).

Definition root x := if pick (connect x) is Some y then y else x.

Definition roots : pred T := fun x => root x == x.

Definition n_comp a := #|predI roots a|.

Lemma connect_root : forall x, connect x (root x).

Definition connect_sym := forall x y, connect x y = connect y x.

Lemma same_connect : connect_sym -> forall x y,
connect x y -> connect x =1 connect y.

Lemma same_connect_r : connect_sym -> forall x y,
connect x y -> forall z, connect z x = connect z y.

Lemma rootP : forall x y,
connect_sym -> reflect (root x = root y) (connect x y).

Lemma root_root : connect_sym -> forall x, root (root x) = root x.

Lemma roots_root : connect_sym -> forall x, roots (root x).

Lemma root_connect :
connect_sym -> forall x y, (root x == root y) = connect x y.

End Connect.

Implicit Arguments connectP [T e x y].
Implicit Arguments rootP [T e x y].

Notation "'fconnect' f" := (connect (frel f))
(at level 10, f at level 8) : seq_scope.

Notation "'froot' f" := (root (frel f))
(at level 10, f at level 8) : seq_scope.

Notation "'froots' f" := (roots (frel f))
(at level 10, f at level 8) : seq_scope.

Notation "'fcard' f" := (n_comp (frel f))
(at level 10, f at level 8) : seq_scope.

Section EqConnect.

Variable T : finType.

Lemma connect_sub : forall e e' : rel T,
subrel e (connect e') -> subrel (connect e) (connect e').

Lemma relU_sym : forall e e' : rel T,
connect_sym e -> connect_sym e' -> connect_sym (relU e e').

Lemma eq_connect : forall e e' : rel T, e =2 e' -> connect e =2 connect e'.

Lemma eq_n_comp : forall e e' : rel T,
connect e =2 connect e' -> n_comp e =1 n_comp e'.

Lemma eq_n_comp_r : forall a a' : pred T, a =1 a' ->
forall e, n_comp e a = n_comp e a'.

Lemma n_compC : forall a e, n_comp e T = n_comp e a + n_comp e (predC a).

Lemma eq_root : forall e1 e2 : rel T, e1 =2 e2 -> root e1 =1 root e2.

Lemma eq_roots : forall e1 e2 : rel T, e1 =2 e2 -> roots e1 =1 roots e2.

End EqConnect.

Section Closure.

Variables (T : finType) (e : rel T).
Hypothesis He : connect_sym e.

Lemma same_connect_rev : connect e =2 connect (fun x y => e y x).

Definition closed (a : pred T) := forall x y, e x y -> a x = a y.

Lemma intro_closed : forall a : pred T,
(forall x y, e x y -> a x -> a y) -> closed a.

Lemma closed_connect : forall a, closed a ->
forall x y, connect e x y -> a x = a y.

Lemma connect_closed : forall x, closed (connect e x).

Lemma predC_closed : forall a, closed a -> closed (predC a).

Definition closure (a : pred T) : pred T :=
fun x => ~~ [disjoint connect e x & a].

Lemma closure_closed : forall a, closed (closure a).

Lemma subset_closure : forall a : pred T, a \subset (closure a).

Lemma n_comp_closure2 : forall x y,
n_comp e (closure (pred2 x y)) = (~~ connect e x y).+1.

Lemma n_comp_connect : forall x, n_comp e (connect e x) = 1.

End Closure.

Notation "'fclosed' f" := (closed (frel f))
(at level 10, f at level 8) : seq_scope.

Notation "'fclosure' f" := (closure (frel f))
(at level 10, f at level 8) : seq_scope.

Section Orbit.

Variables (T : finType) (f : T -> T).

Definition order x := #|fconnect f x|.

Definition orbit x := traject f x (order x).

Definition findex x y := index y (orbit x).

Definition finv x := iter (order x).-1 f x.

Lemma fconnect_iter : forall n x, fconnect f x (iter n f x).

Lemma fconnect1 : forall x, fconnect f x (f x).

Lemma fconnect_finv : forall x, fconnect f x (finv x).

Lemma orderSpred : forall x, (order x).-1.+1 = order x.

Lemma size_orbit : forall x : T, size (orbit x) = order x.

Lemma looping_order : forall x, looping f x (order x).

Lemma fconnect_orbit : forall x, fconnect f x =i orbit x.

Lemma orbit_uniq : forall x, uniq (orbit x).

Lemma findex_max : forall x y, fconnect f x y -> findex x y < order x.

Lemma findex_iter : forall x i, i < order x -> findex x (iter i f x) = i.

Lemma iter_findex : forall x y, fconnect f x y -> iter (findex x y) f x = y.

Lemma findex0 : forall x, findex x x = 0.

Lemma fconnect_invariant : forall (T' : eqType) (k : T -> T'),
invariant f k =1 xpredT -> forall x y : T, fconnect f x y -> k x = k y.

Section Loop.

Variable p : seq T.
Hypotheses (Hp : fcycle f p) (Up : uniq p).
Variable x : T.
Hypothesis Hx : x \in p.

The first lemma does not depend on Up : (uniq p)

Lemma fconnect_cycle : fconnect f x =i p.

Lemma order_cycle : order x = size p.

Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.

End Loop.

Hypothesis Hf : injective f.

Lemma f_finv : cancel finv f.

Lemma finv_f : cancel f finv.

Lemma fin_inj_bij : bijective f.

Lemma finv_bij : bijective finv.

Lemma finv_inj : injective finv.

Lemma fconnect_sym : forall x y, fconnect f x y = fconnect f y x.

Lemma iter_order : forall x, iter (order x) f x = x.

Lemma iter_finv : forall n x, n <= order x ->
iter n finv x = iter (order x - n) f x.

Lemma cycle_orbit : forall x, fcycle f (orbit x).

Lemma fpath_finv : forall x p,
fpath finv x p = fpath f (last x p) (rev (belast x p)).

Lemma same_fconnect_finv : fconnect finv =2 fconnect f.

Lemma fcard_finv : fcard finv =1 fcard f.

Definition order_set n : pred T := fun x => order x == n.

Lemma order_div_card : forall n a,
subpred a (order_set n) -> fclosed f a -> 0 < n ->
forall m, (#|a| == n * m) = (fcard f a == m).

Lemma fclosed1 : forall a, fclosed f a -> forall x, a x = a (f x).

Lemma same_fconnect1 : forall x, fconnect f x =1 fconnect f (f x).

Lemma same_fconnect1_r : forall x y, fconnect f x y = fconnect f x (f y).

End Orbit.

Section FinCancel.

Variables (T : finType) (f f' : T -> T).
Hypothesis Ef : cancel f f'.

Let Hf := can_inj Ef.

Lemma finv_eq_can : finv f =1 f'.

End FinCancel.

Section FconnectEq.

Variables (T : finType) (f f' : T -> T).
Hypothesis Eff' : f =1 f'.

Lemma eq_pred1 : frel f =2 frel f'.

Lemma eq_fpath : fpath f =2 fpath f'.

Lemma eq_fconnect : fconnect f =2 fconnect f'.

Lemma eq_fcard : fcard f =1 fcard f'.

Lemma eq_finv : finv f =1 finv f'.

Lemma eq_froot : froot f =1 froot f'.

Lemma eq_froots : froots f =1 froots f'.

Hypothesis Hf : injective f.

Lemma finv_inv : finv (finv f) =1 f.

Lemma order_finv : order (finv f) =1 order f.

Lemma order_set_finv : order_set (finv f) =2 order_set f.

End FconnectEq.

Variables (T T' : finType) (h : T' -> T) (e : rel T) (e' : rel T').
Hypotheses (He : connect_sym e) (He' : connect_sym e').

Variable a : pred T.
Hypothesis Ha : closed e a.

Record rel_adjunction : Type := RelAdjunction {
rel_unit : forall x, a x -> {x' : T' | connect e x (h x')};
rel_functor : forall x' y',
a (h x') -> connect e' x' y' = connect e (h x') (h y')
}.

Lemma intro_adjunction : forall h' : (forall x, a x -> T'),
(forall x Hx, connect e x (h (h' x Hx))
/\ (forall y Hy, e x y -> connect e' (h' x Hx) (h' y Hy))) ->
(forall x' Hx, connect e' x' (h' (h x') Hx)
/\ (forall y', e' x' y' -> connect e (h x') (h y'))) ->

injective h -> a \subset codom h -> rel_base h e e' (predC a) ->