Library connect

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 fun_adjunction == rel_adjunction (frel f)

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)).
Notation froot f := (root (frel f)).
Notation froots f := (roots (frel f)).
Notation fcard f := (n_comp (frel f)).

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)).
Notation fclosure f := (closure (frel f)).


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.

Section RelAdjunction.

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'))) ->
  rel_adjunction.

Lemma strict_adjunction :
    injective h -> a \subset codom h -> rel_base h e e' (predC a) ->
  rel_adjunction.

Lemma adjunction_closed : rel_adjunction -> closed e' (preim h a).

Lemma adjunction_n_comp : rel_adjunction -> n_comp e a = n_comp e' (preim h a).

End RelAdjunction.

Definition fun_adjunction T T' h f f' :=
  @rel_adjunction T T' h (frel f) (frel f').

Implicit Arguments intro_adjunction [T T' h e e' a].
Implicit Arguments adjunction_n_comp [T T' e e' a].