Top

Module mathcomp.boot.fingraph

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

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition grel (T : eqType) (g : T -> seq T) := [rel x y | y \in g x].

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.

Proof.

elim: n a v => [|n IHn]; first by elim=> //= *; rewrite if_same.
elim=> //= x a IHa v; apply: subset_trans {IHa}(IHa _); case: ifP => // _.
by apply: subset_trans (IHn _ _); apply/subsetP=> y; apply: predU1r.
Qed.

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

Proof.

have dfs_id w z: z \notin w -> dfs_path w z z.
  by exists [::]; rewrite ?disjoint_has //= orbF.
elim: n => [|n IHn] /= in x y v * => le_v'_n not_vy.
  rewrite addn0 (geq_leqif (subset_leqif_card (subset_predT _))) in le_v'_n.
  by rewrite predT_subset in not_vy.
have [v_x | not_vx] := ifPn.
  by rewrite (negPf not_vy); right=> [] [p _ _]; rewrite disjoint_has /= v_x.
set v1 := x :: v; set a := g x; have sub_dfs := subsetP (subset_dfs n _ _).
have [-> | neq_yx] := eqVneq y x.
  by rewrite sub_dfs ?mem_head //; left; apply: dfs_id.
apply: (@equivP (exists2 x1, x1 \in a & dfs_path v1 x1 y)); last first.
  split=> {IHn} [[x1 a_x1 [p g_p p_y]] | [p /shortenP[]]].
    rewrite disjoint_has has_sym /= has_sym /= => /norP[_ not_pv].
    by exists (x1 :: p); rewrite /= ?a_x1 // disjoint_has negb_or not_vx.
  case=> [_ _ _ eq_yx | x1 p1 /=]; first by case/eqP: neq_yx.
  case/andP=> a_x1 g_p1 /andP[not_p1x _] /subsetP p_p1 p1y not_pv.
  exists x1 => //; exists p1 => //.
  rewrite disjoint_sym disjoint_cons not_p1x disjoint_sym.
  by move: not_pv; rewrite disjoint_cons => /andP[_ /disjointWl->].
have{neq_yx not_vy}: y \notin v1 by apply/norP.
have{le_v'_n not_vx}: #|T| <= #|v1| + n by rewrite cardU1 not_vx addSnnS.
elim: {x v}a v1 => [|x a IHa] v /= le_v'_n not_vy.
  by rewrite (negPf not_vy); right=> [] [].
set v2 := dfs n v x; have v2v: v \subset v2 := subset_dfs n v [:: x].
have [v2y | not_v2y] := boolP (y \in v2).
  by rewrite sub_dfs //; left; exists x; [apply: mem_head | apply: IHn].
apply: {IHa}(equivP (IHa _ _ not_v2y)).
  by rewrite (leq_trans le_v'_n) // leq_add2r subset_leq_card.
split=> [] [x1 a_x1 [p g_p p_y not_pv]].
  exists x1; [exact: predU1r | exists p => //].
  by rewrite disjoint_sym (disjointWl v2v) // disjoint_sym.
suffices not_p1v2: [disjoint x1 :: p & v2].
  case/predU1P: a_x1 => [def_x1 | ]; last by exists x1; last exists p.
  case/pred0Pn: not_p1v2; exists x; rewrite /= def_x1 mem_head /=.
  suffices not_vx: x \notin v by apply/IHn; last apply: dfs_id.
  by move: not_pv; rewrite disjoint_cons def_x1 => /andP[].
apply: contraR not_v2y => /pred0Pn[x2 /andP[/= p_x2 v2x2]].
case/splitPl: p_x2 p_y g_p not_pv => p0 p2 p0x2.
rewrite last_cat cat_path -cat_cons lastI cat_rcons {}p0x2 => p2y /andP[_ g_p2].
rewrite disjoint_cat disjoint_cons => /and3P[{p0}_ not_vx2 not_p2v].
have{not_vx2 v2x2} [p1 g_p1 p1_x2 not_p1v] := IHn _ _ v le_v'_n not_vx2 v2x2.
apply/IHn=> //; exists (p1 ++ p2); rewrite ?cat_path ?last_cat -?p1_x2 ?g_p1 //.
by rewrite -cat_cons disjoint_cat not_p1v.
Qed.

Lemma dfsP x y :
  reflect (exists2 p, path (grel g) x p & y = last x p) (y \in dfs #|T| [::] x).

Proof.

apply: (iffP (dfs_pathP _ _ _)); rewrite ?card0 // => [] [p]; exists p => //.
by rewrite disjoint_sym disjoint0.
Qed.

End Dfs.

Variable e : rel T.

Definition rgraph x := enum (e x).

Lemma rgraphK : grel rgraph =2 e.

Proof.

by move=> x y; rewrite /= mem_enum. Qed.

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

Proof.

apply: (equivP (dfsP _ x y)).
by split=> [] [p e_p ->]; exists p => //; rewrite (eq_path rgraphK) in e_p *.
Qed.

Lemma connect_trans : transitive connect.

Proof.

move=> x y z /connectP[p e_p ->] /connectP[q e_q ->]; apply/connectP.
by exists (p ++ q); rewrite ?cat_path ?e_p ?last_cat.
Qed.

Lemma connect0 x : connect x x.

Proof.

by apply/connectP; exists [::]. Qed.

Lemma eq_connect0 x y : x = y -> connect x y.

Proof.

by move->; apply: connect0. Qed.

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

Proof.

by move=> e_xy; apply/connectP; exists [:: y]; rewrite /= ?e_xy. Qed.

Lemma path_connect x p : path e x p -> subpred [in x :: p] (connect x).

Proof.

move=> e_p y p_y; case/splitPl: p / p_y e_p => p q <-.
by rewrite cat_path => /andP[e_p _]; apply/connectP; exists p.
Qed.

Lemma connect_cycle p : cycle e p -> {in p &, forall x y, connect x y}.

Proof.

move=> e_p x y /rot_to[i q rip]; rewrite -(mem_rot i) rip => yqx.
have /= : cycle e (x :: q) by rewrite -rip rot_cycle.
case/splitPl: yqx => r s lxr; rewrite rcons_cat cat_path => /andP[xr _].
by apply/connectP; exists r.
Qed.

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

Proof.

by rewrite /root; case: pickP; rewrite ?connect0. Qed.

Definition connect_sym := symmetric connect.

Hypothesis sym_e : connect_sym.

Lemma same_connect : left_transitive connect.

Proof.

exact: sym_left_transitive connect_trans. Qed.

Lemma same_connect_r : right_transitive connect.

Proof.

exact: sym_right_transitive connect_trans. Qed.

Lemma same_connect1 x y : e x y -> connect x =1 connect y.

Proof.

by move/connect1; apply: same_connect. Qed.

Lemma same_connect1r x y : e x y -> connect^~ x =1 connect^~ y.

Proof.

by move/connect1; apply: same_connect_r. Qed.

Lemma rootP x y : reflect (root x = root y) (connect x y).

Proof.

apply: (iffP idP) => e_xy.
  by rewrite /root -(eq_pick (same_connect e_xy)); case: pickP e_xy => // ->.
by apply: (connect_trans (connect_root x)); rewrite e_xy sym_e connect_root.
Qed.

Lemma root_root x : root (root x) = root x.

Proof.

exact/esym/rootP/connect_root. Qed.

Lemma roots_root x : roots (root x).

Proof.

exact/eqP/root_root. Qed.

Lemma root_connect x y : (root x == root y) = connect x y.

Proof.

exact: sameP eqP (rootP x y). Qed.

Definition closed_mem m_a := forall 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.
Arguments rgraphK [T].
#[global] 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)).

Prenex Implicits connect root roots.

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

Proof.

move=> e'e x _ /connectP[p e_p ->]; elim: p x e_p => //= y p IHp x /andP[exy].
by move/IHp; apply: connect_trans; apply: e'e.
Qed.

Lemma relU_sym e e' :
  connect_sym e -> connect_sym e' -> connect_sym (relU e e').

Proof.

move=> sym_e sym_e'; apply: symmetric_from_pre => x _ /connectP[p e_p ->].
elim: p x e_p => //= y p IHp x /andP[e_xy /IHp{IHp}/connect_trans]; apply.
case/orP: e_xy => /connect1; rewrite (sym_e, sym_e');
  by apply: connect_sub y x => x y e_xy; rewrite connect1 //= e_xy ?orbT.
Qed.

Lemma eq_connect e e' : e =2 e' -> connect e =2 connect e'.

Proof.

move=> eq_e x y; apply/connectP/connectP=> [] [p e_p ->];
  by exists p; rewrite // (eq_path eq_e) in e_p *.
Qed.

Arguments eq_connect [e e'].

Lemma eq_n_comp e e' : connect e =2 connect e' -> n_comp_mem e =1 n_comp_mem e'.

Proof.

move=> eq_e [a]; apply: eq_card => x /=.
by rewrite !inE /= /roots /root /= (eq_pick (eq_e x)).
Qed.

Lemma eq_n_comp_r {e} a a' : a =i a' -> n_comp e a = n_comp e a'.

Proof.

by move=> eq_a; apply: eq_card => x; rewrite inE /= eq_a. Qed.

Lemma n_compC a e : n_comp e T = n_comp e a + n_comp e [predC a].

Proof.

rewrite /n_comp_mem (eq_card (fun _ => andbT _)) -(cardID a); congr (_ + _).
by apply: eq_card => x; rewrite !inE andbC.
Qed.

Lemma eq_root e e' : e =2 e' -> root e =1 root e'.

Proof.

by move=> eq_e x; rewrite /root (eq_pick (eq_connect eq_e x)). Qed.

Lemma eq_roots e e' : e =2 e' -> roots e =1 roots e'.

Proof.

by move=> eq_e x; rewrite /roots (eq_root eq_e). Qed.

Lemma connect_rev e : connect [rel x y | e y x] =2 [rel x y | connect e y x].

Proof.

suff crev e': subrel (connect [rel x y | e' y x]) [rel x y | connect e' y x].
  by move=> x y; apply/idP/idP; apply: crev.
move=> x y /connectP[p e_p p_y]; apply/connectP.
exists (rev (belast x p)); first by rewrite p_y rev_path.
by rewrite -(last_cons x) -rev_rcons p_y -lastI rev_cons last_rcons.
Qed.

Lemma sym_connect_sym e : symmetric e -> connect_sym e.

Proof.

by move=> sym_e x y; rewrite (eq_connect sym_e) connect_rev. Qed.

End EqConnect.
Arguments eq_connect [T e e'].
Arguments connect_rev [T].

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

Proof.

by move=> x y; rewrite sym_e connect_rev. Qed.

Lemma intro_closed a : (forall x y, e x y -> x \in a -> y \in a) -> closed e a.

Proof.

move=> cl_a x y e_xy; apply/idP/idP=> [|a_y]; first exact: cl_a.
have{x e_xy} /connectP[p e_p ->]: connect e y x by rewrite sym_e connect1.
by elim: p y a_y e_p => //= y p IHp x a_x /andP[/cl_a/(_ a_x)]; apply: IHp.
Qed.

Lemma closed_connect a :
  closed e a -> forall x y, connect e x y -> (x \in a) = (y \in a).

Proof.

move=> cl_a x _ /connectP[p e_p ->].
by elim: p x e_p => //= y p IHp x /andP[/cl_a->]; apply: IHp.
Qed.

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

Proof.

by move=> y z /connect1/same_connect_r; apply. Qed.

Lemma predC_closed a : closed e a -> closed e [predC a].

Proof.

by move=> cl_a x y /cl_a /[!inE] ->. Qed.

Lemma closure_closed a : closed e (closure e a).

Proof.

apply: intro_closed => x y /connect1 e_xy; congr (~~ _).
by apply: eq_disjoint; apply: same_connect.
Qed.

Lemma mem_closure a : {subset a <= closure e a}.

Proof.

by move=> x a_x; apply/existsP; exists x; rewrite !inE connect0. Qed.

Lemma subset_closure a : a \subset closure e a.

Proof.

by apply/subsetP; apply: mem_closure. Qed.

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

Proof.

rewrite -(root_connect sym_e) -card2; apply: eq_card => z.
apply/idP/idP=> [/andP[/eqP {2}<- /pred0Pn[t /andP[/= ezt exyt]]] |].
  by case/pred2P: exyt => <-; rewrite (rootP sym_e ezt) !inE eqxx ?orbT.
by case/pred2P=> ->; rewrite !inE roots_root //; apply/existsP;
  [exists x | exists y]; rewrite !inE eqxx ?orbT sym_e connect_root.
Qed.

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

Proof.

rewrite -(card1 (root e x)); apply: eq_card => y.
apply/andP/eqP => [[/eqP r_y /rootP-> //] | ->] /=.
by rewrite inE connect_root roots_root.
Qed.

End Closure.
Arguments same_connect_rev [T e].

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

Proof.

apply/connectP.
by exists (traject f (f x) n); [apply: fpath_traject | rewrite last_traject].
Qed.

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

Proof.

exact: (fconnect_iter 1). Qed.

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

Proof.

exact: fconnect_iter. Qed.

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

Proof.

by rewrite /order (cardD1 x) [_ x _]connect0. Qed.

Lemma size_orbit x : size (orbit x) = order x.

Proof.

exact: size_traject. Qed.

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

Proof.

apply: contraFT (ltnn (order x)); rewrite -looping_uniq => /card_uniqP.
rewrite size_traject => <-; apply: subset_leq_card.
by apply/subsetP=> _ /trajectP[i _ ->]; apply: fconnect_iter.
Qed.

Lemma fconnect_orbit x y : fconnect f x y = (y \in orbit x).

Proof.

apply/idP/idP=> [/connectP[_ /fpathP[m ->] ->] | /trajectP[i _ ->]].
  by rewrite last_traject; apply/loopingP/looping_order.
exact: fconnect_iter.
Qed.

Lemma in_orbit x : x \in orbit x

Proof.

by rewrite -fconnect_orbit. Qed.

Hint Resolve in_orbit : core.

Lemma order_gt0 x : order x > 0

Proof.

by rewrite -orderSpred. Qed.

Hint Resolve order_gt0 : core.

Lemma orbit_uniq x : uniq (orbit x).

Proof.

rewrite /orbit -orderSpred looping_uniq; set n := (order x).-1.
apply: contraFN (ltnn n) => /trajectP[i lt_i_n eq_fnx_fix].
rewrite orderSpred -(size_traject f x n).
apply: (leq_trans (subset_leq_card _) (card_size _)); apply/subsetP=> z.
rewrite inE fconnect_orbit => /trajectP[j le_jn ->{z}].
rewrite -orderSpred -/n ltnS leq_eqVlt in le_jn.
by apply/trajectP; case/predU1P: le_jn => [->|]; [exists i | exists j].
Qed.

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

Proof.

by rewrite [_ y]fconnect_orbit -index_mem size_orbit. Qed.

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

Proof.

move=> lt_ix; rewrite -(nth_traject f lt_ix) /findex index_uniq ?orbit_uniq //.
by rewrite size_orbit.
Qed.

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

Proof.

rewrite [_ y]fconnect_orbit => fxy; pose i := index y (orbit x).
have lt_ix: i < order x by rewrite -size_orbit index_mem.
by rewrite -(nth_traject f lt_ix) nth_index.
Qed.

Lemma findex0 x : findex x x = 0.

Proof.

by rewrite /findex /orbit -orderSpred /= eqxx. Qed.

Lemma findex_eq0 x y : (findex x y == 0) = (x == y).

Proof.

by rewrite /findex /orbit -orderSpred /=; case: (x == y). Qed.

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

Proof.

move=> eq_k_f x y /iter_findex <-; elim: {y}(findex x y) => //= n ->.
by rewrite (eqP (eq_k_f _)).
Qed.

Lemma mem_orbit x : {homo f : y / y \in orbit x}.

Proof.

by move=> y; rewrite -!fconnect_orbit => /connect_trans->//; apply: fconnect1.
Qed.

Lemma image_orbit x : {subset image f (orbit x) <= orbit x}.

Proof.

by move=> _ /mapP[y yin ->]; apply: mem_orbit; rewrite ?mem_enum in yin.
Qed.

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

Proof.

by move=> x xS; rewrite iter_in. Qed.

Lemma f_finv_in : {in S, cancel finv f}.

Proof.

move=> x xS; move: (looping_order x) (orbit_uniq x).
rewrite /looping /orbit -orderSpred looping_uniq /= /looping; set n := _.-1.
case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr.
by move=> /injf ->; rewrite ?(iter_in _ f_in) //; case/trajectP; exists i.
Qed.

Lemma finv_f_in : {in S, cancel f finv}.

Proof.

by move=> x xS; apply/injf; rewrite ?iter_in ?f_finv_in ?f_in. Qed.

Lemma finv_inj_in : {in S &, injective finv}.

Proof.

by move=> x y xS yS q; rewrite -(f_finv_in xS) q f_finv_in. Qed.

Lemma fconnect_sym_in : {in S &, forall x y, fconnect f x y = fconnect f y x}.

Proof.

suff Sf : {in S &, forall x y, fconnect f x y -> fconnect f y x}.
  by move=> *; apply/idP/idP=> /Sf->.
move=> x _ xS _ /connectP [p f_p ->]; elim: p => //= y p IHp in x xS f_p *.
case/andP: f_p => /eqP <- /(IHp _ (f_in xS)) /connect_trans -> //.
by apply: (connect_trans (fconnect_finv _)); rewrite finv_f_in.
Qed.

Lemma iter_order_in : {in S, forall x, iter (order x) f x = x}.

Proof.

by move=> x xS; rewrite -orderSpred iterS; apply: f_finv_in. Qed.

Lemma iter_finv_in n :
  {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.

Proof.

move=> x xS; rewrite -[x in LHS]iter_order_in => // /subnKC {1}<-.
move: (_ - n) => m; rewrite iterD; elim: n => // n {2}<-.
by rewrite iterSr /= finv_f_in // -iterD iter_in.
Qed.

Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}.

Proof.

move=> x xS; rewrite /orbit -orderSpred (cycle_path x) /= last_traject.
by rewrite -/(finv x) fpath_traject f_finv_in ?eqxx.
Qed.

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

Proof.

elim: p x => //= y p IHp x; rewrite rev_cons rcons_path.
transitivity [&& y \in S, f y == x & fpath finv y p].
  apply/and3P/and3P => -[xS /eqP<- fxp]; split;
  by rewrite ?f_finv_in ?finv_f_in ?finv_in ?f_in.
rewrite andbCA {}IHp !andbA [RHS]andbC -andbA; congr [&& _, _ & _].
by case: p => //= z p; rewrite rev_cons last_rcons.
Qed.

Lemma fpath_finv_f_in p : {in S, forall x,
  fpath finv x p -> fpath f (last x p) (rev (belast x p))}.

Proof.

by move=> x xS /(conj xS)/andP; rewrite fpath_finv_in => /andP[]. Qed.

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.

Proof.

by move=> lS /(conj lS)/andP; rewrite -fpath_finv_in => /andP[]. Qed.

End orbit_in.

Lemma injectivePcycle x :
  reflect {in orbit x &, injective f} (fcycle f (orbit x)).

Proof.

apply: (iffP idP) => [/inj_cycle//|/cycle_orbit_in].
by apply; [apply: mem_orbit|apply: in_orbit].
Qed.

Section orbit_inj.

Hypothesis injf : injective f.

Lemma f_finv : cancel finv f

Proof.

exact: (in1T (f_finv_in _ (in2W _))). Qed.

Lemma finv_f : cancel f finv

Proof.

exact: (in1T (finv_f_in _ (in2W _))). Qed.

Lemma finv_bij : bijective finv.

Proof.

by exists f; [apply: f_finv|apply: finv_f]. Qed.

Lemma finv_inj : injective finv

Proof.

exact: (can_inj f_finv). Qed.

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

Proof.

exact: (in2T (fconnect_sym_in _ (in2W _))). Qed.

Let symf := fconnect_sym.

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

Proof.

exact: (in1T (iter_order_in _ (in2W _))). Qed.

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

Proof.

exact: (in1T (@iter_finv_in _ _ (in2W _) _)). Qed.

Lemma cycle_orbit x : fcycle f (orbit x).

Proof.

exact: (in1T (cycle_orbit_in _ (in2W _))). Qed.

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

Proof.

exact: (@fpath_finv_in T _ (in2W _)). Qed.

Lemma same_fconnect_finv : fconnect finv =2 fconnect f.

Proof.

move=> x y; rewrite (same_connect_rev symf); apply: {x y}eq_connect => x y /=.
by rewrite (canF_eq finv_f) eq_sym.
Qed.

Lemma fcard_finv : fcard_mem finv =1 fcard_mem f.

Proof.

exact: eq_n_comp same_fconnect_finv. Qed.

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

Proof.

move=> a_n cl_a; rewrite /n_comp_mem; set b := [predI froots f & a].
suff <-: #|preim (froot f) b| = #|b| * n.
  apply: eq_card => x; rewrite !inE (roots_root fconnect_sym).
  exact/esym/(closed_connect cl_a)/connect_root.
have{cl_a a_n} (x): b x -> froot f x = x /\ order x = n.
  by case/andP=> /eqP-> /(subsetP a_n)/eqnP->.
elim: {a b}#|b| {1 3 4}b (eqxx #|b|) => [|m IHm] b def_m f_b.
  by rewrite eq_card0 // => x; apply: (pred0P def_m).
have [x b_x | b0] := pickP b; last by rewrite (eq_card0 b0) in def_m.
have [r_x ox_n] := f_b x b_x; rewrite (cardD1 x) [x \in b]b_x eqSS in def_m.
rewrite mulSn -{1}ox_n -(IHm _ def_m) => [_ /andP[_ /f_b //]|].
rewrite -(cardID (fconnect f x)); congr (_ + _); apply: eq_card => y.
  by apply: andb_idl => /= fxy; rewrite !inE -(rootP symf fxy) r_x.
by congr (~~ _ && _); rewrite /= /in_mem /= symf -(root_connect symf) r_x.
Qed.

Lemma fclosed1 (a : {pred T}) :
  fclosed f a -> forall x, (x \in a) = (f x \in a).

Proof.

by move=> cl_a x; apply: cl_a (eqxx _). Qed.

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

Proof.

by apply: same_connect1 => /=. Qed.

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

Proof.

by apply: same_connect1r x => /=. Qed.

Lemma fcard_gt0P (a : {pred T}) :
  fclosed f a -> reflect (exists x, x \in a) (0 < fcard f a).

Proof.

move=> clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x.
exists (froot f x); rewrite inE roots_root /=; first exact: fconnect_sym.
by rewrite -(closed_connect clfA (connect_root _ x)).
Qed.

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

Proof.

move=> clAf; apply: (iffP card_gt1P) => [|[x xA [y yA not_xfy]]].
  move=> [x [y [/andP [/= rfx xA] /andP[/= rfy yA] xDy]]].
  by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy).
exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=.
by split => //; rewrite -(closed_connect clAf (connect_root _ _)).
Qed.

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

Lemma fconnect_cycle y : fconnect f x y = (y \in p).

Proof.

have [i q def_p] := rot_to p_x; rewrite -(mem_rot i p) def_p.
have{i def_p} /andP[/eqP q_x f_q]: (f (last x q) == x) && fpath f x q.
  by have:= f_p; rewrite -(rot_cycle i) def_p (cycle_path x).
apply/idP/idP=> [/connectP[_ /fpathP[j ->] ->] | ]; last exact: path_connect.
case/fpathP: f_q q_x => n ->; rewrite !last_traject -iterS => def_x.
by apply: (@loopingP _ f x n.+1); rewrite /looping def_x /= mem_head.
Qed.

Lemma order_le_cycle : order x <= size p.

Proof.

apply: leq_trans (card_size _); apply/subset_leq_card/subsetP=> y.
by rewrite !(fconnect_cycle, inE) ?eqxx.
Qed.

Lemma order_cycle : order x = size p.

Proof.

by rewrite -(card_uniqP Up); apply: (eq_card fconnect_cycle). Qed.

Lemma orbitE : orbit x = rot (index x p) p.

Proof.

set i := index _ _; rewrite /orbit order_cycle -(size_rot i) rot_index// -/i.
set q := _ ++ _; suffices /fpathP[j ->]: fpath f x q by rewrite /= size_traject.
by move: f_p; rewrite -(rot_cycle i) rot_index// (cycle_path x); case/andP.
Qed.

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

Proof.

by rewrite orbitE; exists (index x p). Qed.

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}

Proof.

exact: finv_in. Qed.

Lemma f_finv_cycle : {in p, cancel finv f}

Proof.

exact: f_finv_in. Qed.

Lemma finv_f_cycle : {in p, cancel f finv}

Proof.

exact: finv_f_in. Qed.

Lemma finv_inj_cycle : {in p &, injective finv}

Proof.

exact: finv_inj_in. Qed.

Lemma iter_finv_cycle n :
  {in p, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.

Proof.

exact: iter_finv_in. Qed.

Lemma cycle_orbit_cycle : {in p, forall x, fcycle f (orbit x)}.

Proof.

exact: cycle_orbit_in. Qed.

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

Proof.

exact: fpath_finv_in. Qed.

Lemma fpath_finv_f_cycle q : {in p, forall x,
  fpath finv x q -> fpath f (last x q) (rev (belast x q))}.

Proof.

exact: fpath_finv_f_in. Qed.

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.

Proof.

exact: fpath_f_finv_in. Qed.

Lemma prevE x : x \in p -> prev p x = finv x.

Proof.

move=> x_p; have /eqP/(congr1 finv) := prev_cycle f_p x_p.
by rewrite finv_f_cycle// mem_prev.
Qed.

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.

Proof.

by rewrite rcons_cons; have /fpathE-> := f_p; rewrite size_rcons. Qed.

Lemma fcycle_consE : x :: p = traject f x (size p).+1.

Proof.

by have := fcycle_rconsE; rewrite trajectSr => /rcons_inj[/= <-]. Qed.

Lemma fcycle_consEflatten : exists k, x :: p = flatten (nseq k.+1 (orbit x)).

Proof.

move: f_p; rewrite fcycle_consE; elim/ltn_ind: (size p) => n IHn t_cycle.
have := order_le_cycle t_cycle (mem_head _ _); rewrite size_traject.
case: ltngtP => [||<-] //; last by exists 0; rewrite /= cats0.
rewrite ltnS => n_ge _; have := t_cycle.
rewrite -(subnKC n_ge) -addnS trajectD.
rewrite (iter_order_in (mem_fcycle f_p) (inj_cycle f_p)) ?mem_head//.
set m := (_ - _) => cycle_cat.
have [||k->] := IHn m; last by exists k.+1.
  by rewrite ltn_subrL (leq_trans _ n_ge) ?order_gt0.
move: cycle_cat; rewrite -orderSpred/= rcons_cat rcons_cons -cat_rcons.
by rewrite cat_path last_rcons => /andP[].
Qed.

Lemma undup_cycle_cons : undup (x :: p) = orbit x.

Proof.

by have [n {1}->] := fcycle_consEflatten; rewrite undup_flatten_nseq ?undup_id.
Qed.

End fcycle_cons.

Section fcycle_undup.

Variable (p : seq T) (f_p : fcycle f p).

Lemma fcycleEflatten : exists k, p = flatten (nseq k (undup p)).

Proof.

case: p f_p => [//|x q] f_q; first by exists 0.
have [k {1}->] := @fcycle_consEflatten x q f_q.
by exists k.+1; rewrite undup_cycle_cons.
Qed.

Lemma fcycle_undup : fcycle f (undup p).

Proof.

case: p f_p => [//|x q] f_q; rewrite undup_cycle_cons//.
by rewrite (cycle_orbit_in (mem_fcycle f_q) (inj_cycle f_q)) ?mem_head.
Qed.

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 &, forall x, orbit x =i p}.

Proof.

by move=> x y xp yp; rewrite (orbitE fcycle_undup)// ?mem_rot ?mem_undup.
Qed.

Lemma eq_order_cycle : {in p &, forall x y, order y = order x}.

Proof.

by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup. Qed.

Lemma iter_order_cycle : {in p &, forall x y, iter (order x) f y = y}.

Proof.

by move=> x y xp yp; rewrite (eq_order_cycle yp) ?(iter_order_in homo_f f_inj).
Qed.

End fcycle_undup.

Section fconnect.

Lemma fconnect_eqVf x y : fconnect f x y = (x == y) || fconnect f (f x) y.

Proof.

apply/idP/idP => [/iter_findex <-|/predU1P [<-|] //]; last first.
  exact/connect_trans/fconnect1.
by case: findex => [|i]; rewrite ?eqxx// iterSr fconnect_iter orbT.
Qed.

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} : [<->
fcycle f (orbit x);
order (f x) = order x;
x \in fconnect f (f x);
exists k, iter k.+1 f x = x;
iter (order x) f x = x;
{in orbit x &, injective f}].

Proof.

tfae=> [xorbit_cycle|||[k fkx]|fx y z|/injectivePcycle//].
- by apply: eq_order_cycle xorbit_cycle _ _ _ _; rewrite ?mem_orbit.
- move=> /subset_cardP/(_ _)->; rewrite ?inE//; apply/subsetP=> y.
  by apply: connect_trans; apply: fconnect1.
- by exists (findex (f x) x); rewrite // iterSr iter_findex.
- apply: (@iter_order_cycle (traject f x k.+1)); rewrite /= ?mem_head//.
  by apply/fpathP; exists k.+1; rewrite trajectSr -iterSr fkx.
- rewrite -!fconnect_orbit => /iter_findex <- /iter_findex <-.
  move/(congr1 (iter (order x).-1 f)).
  by rewrite -!iterSr !orderSpred -!iterD ![order _ + _]addnC !iterD fx.
Qed.

Lemma order_id_cycle x : fcycle f (orbit x) -> order (f x) = order x.

Proof.

by move/(orbitPcycle 0 1). Qed.

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

Proof.

have [xcycle|Ncycle] := boolP (fcycle f (orbit x)); constructor => //.
  by rewrite order_id_cycle.
rewrite /order (eq_card (_ : _ =1 [predU1 x & fconnect f (f x)])).
  by move=> y; rewrite !inE fconnect_eqVf eq_sym.
by rewrite cardU1 inE (contraNN (all_iffLR orbitPcycle 2 0)).
Qed.

Lemma fconnect_f x : fconnect f (f x) x = fcycle f (orbit x).

Proof.

by apply/idP/idP => /(orbitPcycle 0 2). Qed.

Lemma fconnect_findex x y :
  fconnect f x y -> y != x -> findex x y = (findex (f x) y).+1.

Proof.

rewrite /findex fconnect_orbit /orbit -orderSpred /= inE => /orP [-> //|].
rewrite eq_sym; move=> yin /negPf->; have [_ eq_o|_ ->//] := orderPcycle x.
by rewrite -(orderSpred (f x)) trajectSr -cats1 index_cat -eq_o yin.
Qed.

End fconnect.

End Orbit.

#[global] Hint Resolve in_orbit mem_orbit order_gt0 orbit_uniq : core.
Prenex Implicits order orbit findex finv order_set.
Arguments orbitPcycle {T f x}.
Arguments same_fconnect_finv [T f].

Section FconnectId.

Variable T : finType.

Lemma fconnect_id (x : T) : fconnect id x =1 xpred1 x.

Proof.

by move=> y; rewrite (@fconnect_cycle _ _ [:: x]) //= ?inE ?eqxx. Qed.

Lemma order_id (x : T) : order id x = 1.

Proof.

by rewrite /order (eq_card (fconnect_id x)) card1. Qed.

Lemma orbit_id (x : T) : orbit id x = [:: x].

Proof.

by rewrite /orbit order_id. Qed.

Lemma froots_id (x : T) : froots id x.

Proof.

by rewrite /roots -fconnect_id connect_root. Qed.

Lemma froot_id (x : T) : froot id x = x.

Proof.

by apply/eqP; apply: froots_id. Qed.

Lemma fcard_id (a : {pred T}) : fcard id a = #|a|.

Proof.

by apply: eq_card => x; rewrite inE froots_id. Qed.

End FconnectId.

Section FconnectEq.

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

Lemma finv_eq_can : cancel f f' -> finv f =1 f'.

Proof.

move=> fK; have inj_f := can_inj fK.
by apply: bij_can_eq fK; [apply: injF_bij | apply: finv_f].
Qed.

Hypothesis eq_f : f =1 f'.
Let eq_rf := eq_frel eq_f.

Lemma eq_fconnect : fconnect f =2 fconnect f'.

Proof.

exact: eq_connect eq_rf. Qed.

Lemma eq_fcard : fcard_mem f =1 fcard_mem f'.

Proof.

exact: eq_n_comp eq_fconnect. Qed.

Lemma eq_finv : finv f =1 finv f'.

Proof.

by move=> x; rewrite /finv /order (eq_card (@eq_fconnect x)) (eq_iter eq_f).
Qed.

Lemma eq_froot : froot f =1 froot f'.

Proof.

exact: eq_root eq_rf. Qed.

Lemma eq_froots : froots f =1 froots f'.

Proof.

exact: eq_roots eq_rf. Qed.

End FconnectEq.
Arguments eq_fconnect [T f f'].

Section FinvEq.

Variables (T : finType) (f : T -> T).
Hypothesis injf : injective f.

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

Proof.

exact: (finv_eq_can (f_finv injf)). Qed.

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

Proof.

by move=> x; apply: eq_card (@same_fconnect_finv _ _ injf x). Qed.

Lemma order_set_finv n : order_set (finv f) n =i order_set f n.

Proof.

by move=> x; rewrite !inE order_finv. Qed.

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.

Local Notation rel_adjunction := (rel_adjunction_mem (mem a)).

Lemma intro_adjunction (h' : forall x, x \in a -> T') :
   (forall x a_x,
      [/\ connect e x (h (h' x a_x))
        & forall y a_y, e x y -> connect e' (h' x a_x) (h' y a_y)]) ->
   (forall x' a_x,
      [/\ connect e' x' (h' (h x') a_x)
        & forall y', e' x' y' -> connect e (h x') (h y')]) ->
  rel_adjunction.

Proof.

move=> Aee' Ae'e; split=> [y a_y | x' z' a_x].
  by exists (h' y a_y); case/Aee': (a_y).
apply/idP/idP=> [/connectP[p e'p ->{z'}] | /connectP[p e_p p_z']].
  elim: p x' a_x e'p => //= y' p IHp x' a_x.
  case: (Ae'e x' a_x) => _ Ae'x /andP[/Ae'x e_xy /IHp e_yz] {Ae'x}.
  by apply: connect_trans (e_yz _); rewrite // -(closed_connect cl_a e_xy).
case: (Ae'e x' a_x) => /connect_trans-> //.
elim: p {x'}(h x') p_z' a_x e_p => /= [|y p IHp] x p_z' a_x.
  by rewrite -p_z' in a_x *; case: (Ae'e _ a_x); rewrite sym_e'.
case/andP=> e_xy /(IHp _ p_z') e'yz; have a_y: y \in a by rewrite -(cl_a e_xy).
by apply: connect_trans (e'yz a_y); case: (Aee' _ a_x) => _ ->.
Qed.

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

Proof.

move=> /= injh h_a a_ee'; pose h' x Hx := iinv (subsetP h_a x Hx).
apply: (@intro_adjunction h') => [x a_x | x' a_x].
  rewrite f_iinv connect0; split=> // y a_y e_xy.
  by rewrite connect1 // -a_ee' !f_iinv ?negbK.
rewrite [h' _ _]iinv_f //; split=> // y' e'xy.
by rewrite connect1 // a_ee' ?negbK.
Qed.

Let ccl_a := closed_connect cl_a.

Lemma adjunction_closed : rel_adjunction -> closed e' [preim h of a].

Proof.

case=> _ Ae'e; apply: intro_closed => // x' y' /connect1 e'xy a_x.
by rewrite Ae'e // in e'xy; rewrite !inE -(ccl_a e'xy).
Qed.

Lemma adjunction_n_comp :
  rel_adjunction -> n_comp e a = n_comp e' [preim h of a].

Proof.

case=> Aee' Ae'e.
have inj_h: {in predI (roots e') [preim h of a] &, injective (root e \o h)}.
  move=> x' y' /andP[/eqP r_x' /= a_x'] /andP[/eqP r_y' _] /(rootP sym_e).
  by rewrite -Ae'e // => /(rootP sym_e'); rewrite r_x' r_y'.
rewrite /n_comp_mem -(card_in_image inj_h); apply: eq_card => x.
apply/andP/imageP=> [[/eqP rx a_x] | [x' /andP[/eqP r_x' a_x'] ->]]; last first.
  by rewrite /= -(ccl_a (connect_root _ _)) roots_root.
have [y' e_xy]:= Aee' x a_x; pose x' := root e' y'.
have ay': h y' \in a by rewrite -(ccl_a e_xy).
have e_yx: connect e (h y') (h x') by rewrite -Ae'e ?connect_root.
exists x'; first by rewrite inE /= -(ccl_a e_yx) ?roots_root.
by rewrite /= -(rootP sym_e e_yx) -(rootP sym_e e_xy).
Qed.

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.