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].
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].