Library mathcomp.ssreflect.fingraph
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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 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).
+
+
+
+
+Set Implicit Arguments.
+ +
+Definition grel (T : eqType) (g : T → seq T) := [rel x y | y \in g x].
+ +
+
+
++Set Implicit Arguments.
+ +
+Definition grel (T : eqType) (g : T → seq T) := [rel x y | y \in g x].
+ +
+
+ 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 := fun 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).
+ +
+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.
+ +
+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)).
+ +
+ +
+ +
+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'.
+ +
+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 (fun 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 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 fconnect_invariant (T' : eqType) (k : T → T') :
+ invariant f k =1 xpredT → ∀ x y, fconnect f x y → k x = k y.
+ +
+Section Loop.
+ +
+Variable p : seq T.
+Hypotheses (f_p : fcycle f p) (Up : uniq p).
+Variable x : T.
+Hypothesis 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 := fun 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).
+ +
+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.
+ +
+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)).
+ +
+ +
+ +
+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'.
+ +
+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 (fun 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 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 fconnect_invariant (T' : eqType) (k : T → T') :
+ invariant f k =1 xpredT → ∀ x y, fconnect f x y → k x = k y.
+ +
+Section Loop.
+ +
+Variable p : seq T.
+Hypotheses (f_p : fcycle f p) (Up : uniq p).
+Variable x : T.
+Hypothesis p_x : x \in p.
+ +
+
+ This lemma does not depend on Up : (uniq p)
+
+
+Lemma fconnect_cycle y : fconnect f x y = (y \in p).
+ +
+Lemma order_cycle : order x = size p.
+ +
+Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
+ +
+End Loop.
+ +
+Section orbit_in.
+ +
+Variable S : pred_sort (predPredType T).
+ +
+Hypothesis f_in : {in S, ∀ x, f x \in S}.
+Hypothesis injf : {in S &, injective f}.
+ +
+Lemma iter_in : {in S, ∀ x i, iter i f x \in S}.
+ +
+Lemma finv_in : {in S, ∀ x, finv 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.
+ +
+Hypothesis injf : 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 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).
+ +
+End Orbit.
+ +
+ +
+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.
+ +
+ +
+Unset Implicit Arguments.
+
++ +
+Lemma order_cycle : order x = size p.
+ +
+Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
+ +
+End Loop.
+ +
+Section orbit_in.
+ +
+Variable S : pred_sort (predPredType T).
+ +
+Hypothesis f_in : {in S, ∀ x, f x \in S}.
+Hypothesis injf : {in S &, injective f}.
+ +
+Lemma iter_in : {in S, ∀ x i, iter i f x \in S}.
+ +
+Lemma finv_in : {in S, ∀ x, finv 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.
+ +
+Hypothesis injf : 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 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).
+ +
+End Orbit.
+ +
+ +
+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.
+ +
+ +
+Unset Implicit Arguments.
+