Library mathcomp.ssreflect.fingraph
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
From mathcomp Require Import seq path fintype.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
From mathcomp Require Import seq path fintype.
This file develops the theory of finite graphs represented by an "edge"
relation over a finType T; this mainly amounts to the theory of the
transitive closure of such relations.
For g : T -> seq T, e : rel T and f : T -> T we define:
grel g == the adjacency relation y \in g x of the graph g.
rgraph e == the graph (x |-> enum (e x)) of the relation e.
dfs g n v x == the list of points traversed by a depth-first search of
the g, at depth n, starting from x, and avoiding v.
dfs_path g v x y <-> there is a path from x to y in g \ v.
connect e == the reflexive transitive closure of e (computed by dfs).
connect_sym e <-> connect e is symmetric, hence an equivalence relation.
root e x == a representative of connect e x, which is the component
of x in the transitive closure of e.
roots e == the codomain predicate of root e.
n_comp e a == the number of e-connected components of a, when a is
e-closed and connect e is symmetric.
equivalence classes of connect e if connect_sym e holds.
closed e a == the collective predicate a is e-invariant.
closure e a == the e-closure 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), i.e., "connected under f iteration".
froot f x == root (frel f) x, the 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 f-orbit of x.
order_set f n == elements of f-order n.
finv f == the inverse of f, if f is injective.
:= finv f x := iter (order x).-1 f x.
fcard f a == number of orbits of f in a, provided a is f-invariant
f is one-to-one.
fclosed f a == the collective predicate a is f-invariant.
fclosure f a == the closure of a under f iteration.
fun_adjunction == rel_adjunction (frel f).
Decidable connectivity in finite types.
Section Connect.
Variable T : finType.
Section Dfs.
Variable g : T → seq T.
Implicit Type v w a : seq T.
Fixpoint dfs n v x :=
if x \in v then v else
if n is n'.+1 then foldl (dfs n') (x :: v) (g x) else v.
Lemma subset_dfs n v a : v \subset foldl (dfs n) v a.
Inductive dfs_path v x y : Prop :=
DfsPath p of path (grel g) x p & y = last x p & [disjoint x :: p & v].
Lemma dfs_pathP n x y v :
#|T| ≤ #|v| + n → y \notin v → reflect (dfs_path v x y) (y \in dfs n v x).
Lemma dfsP x y :
reflect (exists2 p, path (grel g) x p & y = last x p) (y \in dfs #|T| [::] x).
End Dfs.
Variable e : rel T.
Definition rgraph x := enum (e x).
Lemma rgraphK : grel rgraph =2 e.
Definition connect : rel T := [rel x y | y \in dfs rgraph #|T| [::] x].
Canonical connect_app_pred x := ApplicativePred (connect x).
Lemma connectP x y :
reflect (exists2 p, path e x p & y = last x p) (connect x y).
Lemma connect_trans : transitive connect.
Lemma connect0 x : connect x x.
Lemma eq_connect0 x y : x = y → connect x y.
Lemma connect1 x y : e x y → connect x y.
Lemma path_connect x p : path e x p → subpred (mem (x :: p)) (connect x).
Lemma connect_cycle p : cycle e p → {in p &, ∀ x y, connect x y}.
Definition root x := odflt x (pick (connect x)).
Definition roots : pred T := fun x ⇒ root x == x.
Canonical roots_pred := ApplicativePred roots.
Definition n_comp_mem (m_a : mem_pred T) := #|predI roots m_a|.
Lemma connect_root x : connect x (root x).
Definition connect_sym := symmetric connect.
Hypothesis sym_e : connect_sym.
Lemma same_connect : left_transitive connect.
Lemma same_connect_r : right_transitive connect.
Lemma same_connect1 x y : e x y → connect x =1 connect y.
Lemma same_connect1r x y : e x y → connect^~ x =1 connect^~ y.
Lemma rootP x y : reflect (root x = root y) (connect x y).
Lemma root_root x : root (root x) = root x.
Lemma roots_root x : roots (root x).
Lemma root_connect x y : (root x == root y) = connect x y.
Definition closed_mem m_a := ∀ x y, e x y → in_mem x m_a = in_mem y m_a.
Definition closure_mem m_a : pred T :=
fun x ⇒ ~~ disjoint (mem (connect x)) m_a.
End Connect.
Hint Resolve connect0 : core.
Notation n_comp e a := (n_comp_mem e (mem a)).
Notation closed e a := (closed_mem e (mem a)).
Notation closure e a := (closure_mem e (mem a)).
Arguments dfsP {T g x y}.
Arguments connectP {T e x y}.
Arguments rootP [T e] _ {x y}.
Notation fconnect f := (connect (coerced_frel f)).
Notation froot f := (root (coerced_frel f)).
Notation froots f := (roots (coerced_frel f)).
Notation fcard_mem f := (n_comp_mem (coerced_frel f)).
Notation fcard f a := (fcard_mem f (mem a)).
Notation fclosed f a := (closed (coerced_frel f) a).
Notation fclosure f a := (closure (coerced_frel f) a).
Section EqConnect.
Variable T : finType.
Implicit Types (e : rel T) (a : {pred T}).
Lemma connect_sub e e' :
subrel e (connect e') → subrel (connect e) (connect e').
Lemma relU_sym e e' :
connect_sym e → connect_sym e' → connect_sym (relU e e').
Lemma eq_connect e e' : e =2 e' → connect e =2 connect e'.
Lemma eq_n_comp e e' : connect e =2 connect e' → n_comp_mem e =1 n_comp_mem e'.
Lemma eq_n_comp_r {e} a a' : a =i a' → n_comp e a = n_comp e a'.
Lemma n_compC a e : n_comp e T = n_comp e a + n_comp e [predC a].
Lemma eq_root e e' : e =2 e' → root e =1 root e'.
Lemma eq_roots e e' : e =2 e' → roots e =1 roots e'.
Lemma connect_rev e : connect [rel x y | e y x] =2 [rel x y | connect e y x].
Lemma sym_connect_sym e : symmetric e → connect_sym e.
End EqConnect.
Section Closure.
Variables (T : finType) (e : rel T).
Hypothesis sym_e : connect_sym e.
Implicit Type a : {pred T}.
Lemma same_connect_rev : connect e =2 connect [rel x y | e y x].
Lemma intro_closed a : (∀ x y, e x y → x \in a → y \in a) → closed e a.
Lemma closed_connect a :
closed e a → ∀ x y, connect e x y → (x \in a) = (y \in a).
Lemma connect_closed x : closed e (connect e x).
Lemma predC_closed a : closed e a → closed e [predC a].
Lemma closure_closed a : closed e (closure e a).
Lemma mem_closure a : {subset a ≤ closure e a}.
Lemma subset_closure a : a \subset closure e a.
Lemma n_comp_closure2 x y :
n_comp e (closure e (pred2 x y)) = (~~ connect e x y).+1.
Lemma n_comp_connect x : n_comp e (connect e x) = 1.
End Closure.
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 n x : fconnect f x (iter n f x).
Lemma fconnect1 x : fconnect f x (f x).
Lemma fconnect_finv x : fconnect f x (finv x).
Lemma orderSpred x : (order x).-1.+1 = order x.
Lemma size_orbit x : size (orbit x) = order x.
Lemma looping_order x : looping f x (order x).
Lemma fconnect_orbit x y : fconnect f x y = (y \in orbit x).
Lemma in_orbit x : x \in orbit x.
Hint Resolve in_orbit : core.
Lemma order_gt0 x : order x > 0.
Hint Resolve order_gt0 : core.
Lemma orbit_uniq x : uniq (orbit x).
Lemma findex_max x y : fconnect f x y → findex x y < order x.
Lemma findex_iter x i : i < order x → findex x (iter i f x) = i.
Lemma iter_findex x y : fconnect f x y → iter (findex x y) f x = y.
Lemma findex0 x : findex x x = 0.
Lemma findex_eq0 x y : (findex x y == 0) = (x == y).
Lemma fconnect_invariant (T' : eqType) (k : T → T') :
invariant f k =1 xpredT → ∀ x y, fconnect f x y → k x = k y.
Lemma mem_orbit x : {homo f : y / y \in orbit x}.
Lemma image_orbit x : {subset image f (orbit x) ≤ orbit x}.
Section orbit_in.
Variable S : {pred T}.
Hypothesis f_in : {homo f : x / x \in S}.
Hypothesis injf : {in S &, injective f}.
Lemma finv_in : {homo finv : x / x \in S}.
Lemma f_finv_in : {in S, cancel finv f}.
Lemma finv_f_in : {in S, cancel f finv}.
Lemma finv_inj_in : {in S &, injective finv}.
Lemma fconnect_sym_in : {in S &, ∀ x y, fconnect f x y = fconnect f y x}.
Lemma iter_order_in : {in S, ∀ x, iter (order x) f x = x}.
Lemma iter_finv_in n :
{in S, ∀ x, n ≤ order x → iter n finv x = iter (order x - n) f x}.
Lemma cycle_orbit_in : {in S, ∀ x, (fcycle f) (orbit x)}.
Lemma fpath_finv_in p x :
(x \in S) && (fpath finv x p) =
(last x p \in S) && (fpath f (last x p) (rev (belast x p))).
Lemma fpath_finv_f_in p : {in S, ∀ x,
fpath finv x p → fpath f (last x p) (rev (belast x p))}.
Lemma fpath_f_finv_in p x : last x p \in S →
fpath f (last x p) (rev (belast x p)) → fpath finv x p.
End orbit_in.
Lemma injectivePcycle x :
reflect {in orbit x &, injective f} (fcycle f (orbit x)).
Section orbit_inj.
Hypothesis injf : injective f.
Lemma f_finv : cancel finv f.
Lemma finv_f : cancel f finv.
Lemma finv_bij : bijective finv.
Lemma finv_inj : injective finv.
Lemma fconnect_sym x y : fconnect f x y = fconnect f y x.
Let symf := fconnect_sym.
Lemma iter_order x : iter (order x) f x = x.
Lemma iter_finv n x : n ≤ order x → iter n finv x = iter (order x - n) f x.
Lemma cycle_orbit x : fcycle f (orbit x).
Lemma fpath_finv 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_mem finv =1 fcard_mem f.
Definition order_set n : pred T := [pred x | order x == n].
Lemma fcard_order_set n (a : {pred T}) :
a \subset order_set n → fclosed f a → fcard f a × n = #|a|.
Lemma fclosed1 (a : {pred T}) :
fclosed f a → ∀ x, (x \in a) = (f x \in a).
Lemma same_fconnect1 x : fconnect f x =1 fconnect f (f x).
Lemma same_fconnect1_r x y : fconnect f x y = fconnect f x (f y).
Lemma fcard_gt0P (a : {pred T}) :
fclosed f a → reflect (∃ x, x \in a) (0 < fcard f a).
Lemma fcard_gt1P (A : {pred T}) :
fclosed f A →
reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y)
(1 < fcard f A).
End orbit_inj.
Hint Resolve orbit_uniq : core.
Section fcycle_p.
Variables (p : seq T) (f_p : fcycle f p).
Section mem_cycle.
Variable (Up : uniq p) (x : T) (p_x : x \in p).
Variable T : finType.
Section Dfs.
Variable g : T → seq T.
Implicit Type v w a : seq T.
Fixpoint dfs n v x :=
if x \in v then v else
if n is n'.+1 then foldl (dfs n') (x :: v) (g x) else v.
Lemma subset_dfs n v a : v \subset foldl (dfs n) v a.
Inductive dfs_path v x y : Prop :=
DfsPath p of path (grel g) x p & y = last x p & [disjoint x :: p & v].
Lemma dfs_pathP n x y v :
#|T| ≤ #|v| + n → y \notin v → reflect (dfs_path v x y) (y \in dfs n v x).
Lemma dfsP x y :
reflect (exists2 p, path (grel g) x p & y = last x p) (y \in dfs #|T| [::] x).
End Dfs.
Variable e : rel T.
Definition rgraph x := enum (e x).
Lemma rgraphK : grel rgraph =2 e.
Definition connect : rel T := [rel x y | y \in dfs rgraph #|T| [::] x].
Canonical connect_app_pred x := ApplicativePred (connect x).
Lemma connectP x y :
reflect (exists2 p, path e x p & y = last x p) (connect x y).
Lemma connect_trans : transitive connect.
Lemma connect0 x : connect x x.
Lemma eq_connect0 x y : x = y → connect x y.
Lemma connect1 x y : e x y → connect x y.
Lemma path_connect x p : path e x p → subpred (mem (x :: p)) (connect x).
Lemma connect_cycle p : cycle e p → {in p &, ∀ x y, connect x y}.
Definition root x := odflt x (pick (connect x)).
Definition roots : pred T := fun x ⇒ root x == x.
Canonical roots_pred := ApplicativePred roots.
Definition n_comp_mem (m_a : mem_pred T) := #|predI roots m_a|.
Lemma connect_root x : connect x (root x).
Definition connect_sym := symmetric connect.
Hypothesis sym_e : connect_sym.
Lemma same_connect : left_transitive connect.
Lemma same_connect_r : right_transitive connect.
Lemma same_connect1 x y : e x y → connect x =1 connect y.
Lemma same_connect1r x y : e x y → connect^~ x =1 connect^~ y.
Lemma rootP x y : reflect (root x = root y) (connect x y).
Lemma root_root x : root (root x) = root x.
Lemma roots_root x : roots (root x).
Lemma root_connect x y : (root x == root y) = connect x y.
Definition closed_mem m_a := ∀ x y, e x y → in_mem x m_a = in_mem y m_a.
Definition closure_mem m_a : pred T :=
fun x ⇒ ~~ disjoint (mem (connect x)) m_a.
End Connect.
Hint Resolve connect0 : core.
Notation n_comp e a := (n_comp_mem e (mem a)).
Notation closed e a := (closed_mem e (mem a)).
Notation closure e a := (closure_mem e (mem a)).
Arguments dfsP {T g x y}.
Arguments connectP {T e x y}.
Arguments rootP [T e] _ {x y}.
Notation fconnect f := (connect (coerced_frel f)).
Notation froot f := (root (coerced_frel f)).
Notation froots f := (roots (coerced_frel f)).
Notation fcard_mem f := (n_comp_mem (coerced_frel f)).
Notation fcard f a := (fcard_mem f (mem a)).
Notation fclosed f a := (closed (coerced_frel f) a).
Notation fclosure f a := (closure (coerced_frel f) a).
Section EqConnect.
Variable T : finType.
Implicit Types (e : rel T) (a : {pred T}).
Lemma connect_sub e e' :
subrel e (connect e') → subrel (connect e) (connect e').
Lemma relU_sym e e' :
connect_sym e → connect_sym e' → connect_sym (relU e e').
Lemma eq_connect e e' : e =2 e' → connect e =2 connect e'.
Lemma eq_n_comp e e' : connect e =2 connect e' → n_comp_mem e =1 n_comp_mem e'.
Lemma eq_n_comp_r {e} a a' : a =i a' → n_comp e a = n_comp e a'.
Lemma n_compC a e : n_comp e T = n_comp e a + n_comp e [predC a].
Lemma eq_root e e' : e =2 e' → root e =1 root e'.
Lemma eq_roots e e' : e =2 e' → roots e =1 roots e'.
Lemma connect_rev e : connect [rel x y | e y x] =2 [rel x y | connect e y x].
Lemma sym_connect_sym e : symmetric e → connect_sym e.
End EqConnect.
Section Closure.
Variables (T : finType) (e : rel T).
Hypothesis sym_e : connect_sym e.
Implicit Type a : {pred T}.
Lemma same_connect_rev : connect e =2 connect [rel x y | e y x].
Lemma intro_closed a : (∀ x y, e x y → x \in a → y \in a) → closed e a.
Lemma closed_connect a :
closed e a → ∀ x y, connect e x y → (x \in a) = (y \in a).
Lemma connect_closed x : closed e (connect e x).
Lemma predC_closed a : closed e a → closed e [predC a].
Lemma closure_closed a : closed e (closure e a).
Lemma mem_closure a : {subset a ≤ closure e a}.
Lemma subset_closure a : a \subset closure e a.
Lemma n_comp_closure2 x y :
n_comp e (closure e (pred2 x y)) = (~~ connect e x y).+1.
Lemma n_comp_connect x : n_comp e (connect e x) = 1.
End Closure.
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 n x : fconnect f x (iter n f x).
Lemma fconnect1 x : fconnect f x (f x).
Lemma fconnect_finv x : fconnect f x (finv x).
Lemma orderSpred x : (order x).-1.+1 = order x.
Lemma size_orbit x : size (orbit x) = order x.
Lemma looping_order x : looping f x (order x).
Lemma fconnect_orbit x y : fconnect f x y = (y \in orbit x).
Lemma in_orbit x : x \in orbit x.
Hint Resolve in_orbit : core.
Lemma order_gt0 x : order x > 0.
Hint Resolve order_gt0 : core.
Lemma orbit_uniq x : uniq (orbit x).
Lemma findex_max x y : fconnect f x y → findex x y < order x.
Lemma findex_iter x i : i < order x → findex x (iter i f x) = i.
Lemma iter_findex x y : fconnect f x y → iter (findex x y) f x = y.
Lemma findex0 x : findex x x = 0.
Lemma findex_eq0 x y : (findex x y == 0) = (x == y).
Lemma fconnect_invariant (T' : eqType) (k : T → T') :
invariant f k =1 xpredT → ∀ x y, fconnect f x y → k x = k y.
Lemma mem_orbit x : {homo f : y / y \in orbit x}.
Lemma image_orbit x : {subset image f (orbit x) ≤ orbit x}.
Section orbit_in.
Variable S : {pred T}.
Hypothesis f_in : {homo f : x / x \in S}.
Hypothesis injf : {in S &, injective f}.
Lemma finv_in : {homo finv : x / x \in S}.
Lemma f_finv_in : {in S, cancel finv f}.
Lemma finv_f_in : {in S, cancel f finv}.
Lemma finv_inj_in : {in S &, injective finv}.
Lemma fconnect_sym_in : {in S &, ∀ x y, fconnect f x y = fconnect f y x}.
Lemma iter_order_in : {in S, ∀ x, iter (order x) f x = x}.
Lemma iter_finv_in n :
{in S, ∀ x, n ≤ order x → iter n finv x = iter (order x - n) f x}.
Lemma cycle_orbit_in : {in S, ∀ x, (fcycle f) (orbit x)}.
Lemma fpath_finv_in p x :
(x \in S) && (fpath finv x p) =
(last x p \in S) && (fpath f (last x p) (rev (belast x p))).
Lemma fpath_finv_f_in p : {in S, ∀ x,
fpath finv x p → fpath f (last x p) (rev (belast x p))}.
Lemma fpath_f_finv_in p x : last x p \in S →
fpath f (last x p) (rev (belast x p)) → fpath finv x p.
End orbit_in.
Lemma injectivePcycle x :
reflect {in orbit x &, injective f} (fcycle f (orbit x)).
Section orbit_inj.
Hypothesis injf : injective f.
Lemma f_finv : cancel finv f.
Lemma finv_f : cancel f finv.
Lemma finv_bij : bijective finv.
Lemma finv_inj : injective finv.
Lemma fconnect_sym x y : fconnect f x y = fconnect f y x.
Let symf := fconnect_sym.
Lemma iter_order x : iter (order x) f x = x.
Lemma iter_finv n x : n ≤ order x → iter n finv x = iter (order x - n) f x.
Lemma cycle_orbit x : fcycle f (orbit x).
Lemma fpath_finv 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_mem finv =1 fcard_mem f.
Definition order_set n : pred T := [pred x | order x == n].
Lemma fcard_order_set n (a : {pred T}) :
a \subset order_set n → fclosed f a → fcard f a × n = #|a|.
Lemma fclosed1 (a : {pred T}) :
fclosed f a → ∀ x, (x \in a) = (f x \in a).
Lemma same_fconnect1 x : fconnect f x =1 fconnect f (f x).
Lemma same_fconnect1_r x y : fconnect f x y = fconnect f x (f y).
Lemma fcard_gt0P (a : {pred T}) :
fclosed f a → reflect (∃ x, x \in a) (0 < fcard f a).
Lemma fcard_gt1P (A : {pred T}) :
fclosed f A →
reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y)
(1 < fcard f A).
End orbit_inj.
Hint Resolve orbit_uniq : core.
Section fcycle_p.
Variables (p : seq T) (f_p : fcycle f p).
Section mem_cycle.
Variable (Up : uniq p) (x : T) (p_x : x \in p).
fconnect_cycle does not dependent on Up
order_le_cycle does not dependent on Up
Lemma order_le_cycle : order x ≤ size p.
Lemma order_cycle : order x = size p.
Lemma orbitE : orbit x = rot (index x p) p.
Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
End mem_cycle.
Let f_inj := inj_cycle f_p.
Let homo_f := mem_fcycle f_p.
Lemma finv_cycle : {homo finv : x / x \in p}.
Lemma f_finv_cycle : {in p, cancel finv f}.
Lemma finv_f_cycle : {in p, cancel f finv}.
Lemma finv_inj_cycle : {in p &, injective finv}.
Lemma iter_finv_cycle n :
{in p, ∀ x, n ≤ order x → iter n finv x = iter (order x - n) f x}.
Lemma cycle_orbit_cycle : {in p, ∀ x, fcycle f (orbit x)}.
Lemma fpath_finv_cycle q x : (x \in p) && (fpath finv x q) =
(last x q \in p) && fpath f (last x q) (rev (belast x q)).
Lemma fpath_finv_f_cycle q : {in p, ∀ x,
fpath finv x q → fpath f (last x q) (rev (belast x q))}.
Lemma fpath_f_finv_cycle q x : last x q \in p →
fpath f (last x q) (rev (belast x q)) → fpath finv x q.
Lemma prevE x : x \in p → prev p x = finv x.
End fcycle_p.
Section fcycle_cons.
Variables (x : T) (p : seq T) (f_p : fcycle f (x :: p)).
Lemma fcycle_rconsE : rcons (x :: p) x = traject f x (size p).+2.
Lemma fcycle_consE : x :: p = traject f x (size p).+1.
Lemma fcycle_consEflatten : ∃ k, x :: p = flatten (nseq k.+1 (orbit x)).
Lemma undup_cycle_cons : undup (x :: p) = orbit x.
End fcycle_cons.
Section fcycle_undup.
Variable (p : seq T) (f_p : fcycle f p).
Lemma fcycleEflatten : ∃ k, p = flatten (nseq k (undup p)).
Lemma fcycle_undup : fcycle f (undup p).
Let p_undup_uniq := undup_uniq p.
Let f_inj := inj_cycle f_p.
Let homo_f := mem_fcycle f_p.
Lemma in_orbit_cycle : {in p &, ∀ x, orbit x =i p}.
Lemma eq_order_cycle : {in p &, ∀ x y, order y = order x}.
Lemma iter_order_cycle : {in p &, ∀ x y, iter (order x) f y = y}.
End fcycle_undup.
Section fconnect.
Lemma fconnect_eqVf x y : fconnect f x y = (x == y) || fconnect f (f x) y.
Lemma order_cycle : order x = size p.
Lemma orbitE : orbit x = rot (index x p) p.
Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
End mem_cycle.
Let f_inj := inj_cycle f_p.
Let homo_f := mem_fcycle f_p.
Lemma finv_cycle : {homo finv : x / x \in p}.
Lemma f_finv_cycle : {in p, cancel finv f}.
Lemma finv_f_cycle : {in p, cancel f finv}.
Lemma finv_inj_cycle : {in p &, injective finv}.
Lemma iter_finv_cycle n :
{in p, ∀ x, n ≤ order x → iter n finv x = iter (order x - n) f x}.
Lemma cycle_orbit_cycle : {in p, ∀ x, fcycle f (orbit x)}.
Lemma fpath_finv_cycle q x : (x \in p) && (fpath finv x q) =
(last x q \in p) && fpath f (last x q) (rev (belast x q)).
Lemma fpath_finv_f_cycle q : {in p, ∀ x,
fpath finv x q → fpath f (last x q) (rev (belast x q))}.
Lemma fpath_f_finv_cycle q x : last x q \in p →
fpath f (last x q) (rev (belast x q)) → fpath finv x q.
Lemma prevE x : x \in p → prev p x = finv x.
End fcycle_p.
Section fcycle_cons.
Variables (x : T) (p : seq T) (f_p : fcycle f (x :: p)).
Lemma fcycle_rconsE : rcons (x :: p) x = traject f x (size p).+2.
Lemma fcycle_consE : x :: p = traject f x (size p).+1.
Lemma fcycle_consEflatten : ∃ k, x :: p = flatten (nseq k.+1 (orbit x)).
Lemma undup_cycle_cons : undup (x :: p) = orbit x.
End fcycle_cons.
Section fcycle_undup.
Variable (p : seq T) (f_p : fcycle f p).
Lemma fcycleEflatten : ∃ k, p = flatten (nseq k (undup p)).
Lemma fcycle_undup : fcycle f (undup p).
Let p_undup_uniq := undup_uniq p.
Let f_inj := inj_cycle f_p.
Let homo_f := mem_fcycle f_p.
Lemma in_orbit_cycle : {in p &, ∀ x, orbit x =i p}.
Lemma eq_order_cycle : {in p &, ∀ x y, order y = order x}.
Lemma iter_order_cycle : {in p &, ∀ x y, iter (order x) f y = y}.
End fcycle_undup.
Section fconnect.
Lemma fconnect_eqVf x y : fconnect f x y = (x == y) || fconnect f (f x) y.
Lemma orbitPcycle is of type "The Following Are Equivalent", which means
all four statements are equivalent to each other. In order to use it, one
has to apply it to the natural numbers corresponding to the line, e.g.
`orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`.
examples of this are in order_id_cycle and fconnnect_f.
One may also use lemma all_iffLR to get a one sided implication, as in
orderPcycle.
Lemma orbitPcycle {x} : [<->
(* 0 *) fcycle f (orbit x);
(* 1 *) order (f x) = order x;
(* 2 *) x \in fconnect f (f x);
(* 3 *) ∃ k, iter k.+1 f x = x;
(* 4 *) iter (order x) f x = x;
(* 5 *) {in orbit x &, injective f}].
Lemma order_id_cycle x : fcycle f (orbit x) → order (f x) = order x.
Inductive order_spec_cycle x : bool → Type :=
| OrderStepCycle of fcycle f (orbit x) & order x = order (f x) :
order_spec_cycle x true
| OrderStepNoCycle of ~~ fcycle f (orbit x) & order x = (order (f x)).+1 :
order_spec_cycle x false.
Lemma orderPcycle x : order_spec_cycle x (fcycle f (orbit x)).
Lemma fconnect_f x : fconnect f (f x) x = fcycle f (orbit x).
Lemma fconnect_findex x y :
fconnect f x y → y != x → findex x y = (findex (f x) y).+1.
End fconnect.
End Orbit.
Hint Resolve in_orbit mem_orbit order_gt0 orbit_uniq : core.
Arguments orbitPcycle {T f x}.
Section FconnectId.
Variable T : finType.
Lemma fconnect_id (x : T) : fconnect id x =1 xpred1 x.
Lemma order_id (x : T) : order id x = 1.
Lemma orbit_id (x : T) : orbit id x = [:: x].
Lemma froots_id (x : T) : froots id x.
Lemma froot_id (x : T) : froot id x = x.
Lemma fcard_id (a : {pred T}) : fcard id a = #|a|.
End FconnectId.
Section FconnectEq.
Variables (T : finType) (f f' : T → T).
Lemma finv_eq_can : cancel f f' → finv f =1 f'.
Hypothesis eq_f : f =1 f'.
Let eq_rf := eq_frel eq_f.
Lemma eq_fconnect : fconnect f =2 fconnect f'.
Lemma eq_fcard : fcard_mem f =1 fcard_mem 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'.
End FconnectEq.
Section FinvEq.
Variables (T : finType) (f : T → T).
Hypothesis injf : injective f.
Lemma finv_inv : finv (finv f) =1 f.
Lemma order_finv : order (finv f) =1 order f.
Lemma order_set_finv n : order_set (finv f) n =i order_set f n.
End FinvEq.
Section RelAdjunction.
Variables (T T' : finType) (h : T' → T) (e : rel T) (e' : rel T').
Hypotheses (sym_e : connect_sym e) (sym_e' : connect_sym e').
Record rel_adjunction_mem m_a := RelAdjunction {
rel_unit x : in_mem x m_a → {x' : T' | connect e x (h x')};
rel_functor x' y' :
in_mem (h x') m_a → connect e' x' y' = connect e (h x') (h y')
}.
Variable a : {pred T}.
Hypothesis cl_a : closed e a.
Lemma intro_adjunction (h' : ∀ x, x \in a → T') :
(∀ x a_x,
[/\ connect e x (h (h' x a_x))
& ∀ y a_y, e x y → connect e' (h' x a_x) (h' y a_y)]) →
(∀ x' a_x,
[/\ connect e' x' (h' (h x') a_x)
& ∀ 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.
Let ccl_a := closed_connect cl_a.
Lemma adjunction_closed : rel_adjunction → closed e' [preim h of a].
Lemma adjunction_n_comp :
rel_adjunction → n_comp e a = n_comp e' [preim h of a].
End RelAdjunction.
Notation rel_adjunction h e e' a := (rel_adjunction_mem h e e' (mem a)).
Notation "@ 'rel_adjunction' T T' h e e' a" :=
(@rel_adjunction_mem T T' h e e' (mem a))
(at level 10, T, T', h, e, e', a at level 8, only parsing) : type_scope.
Notation fun_adjunction h f f' a := (rel_adjunction h (frel f) (frel f') a).
Notation "@ 'fun_adjunction' T T' h f f' a" :=
(@rel_adjunction T T' h (frel f) (frel f') a)
(at level 10, T, T', h, f, f', a at level 8, only parsing) : type_scope.
Arguments intro_adjunction [T T' h e e'] _ [a].
Arguments adjunction_n_comp [T T'] h [e e'] _ _ [a].
Unset Implicit Arguments.