Library MathComp.fingraph

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path fintype.


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

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

Section Connect.

Variable T : finType.

Section Dfs.

Variable g : Tseq 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/subsetPy; exact: 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| + ny \notin vreflect (dfs_path v x y) (y \in dfs n v x).
Proof.
have dfs_id w z: z \notin wdfs_path w z z.
  by [::]; 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; exact: 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 (x1 :: p); rewrite /= ?a_x1 // disjoint_has negb_or not_vx.
  case⇒ [_ _ _ eq_yx | x1 p1 /=]; first by case/eqP: neq_yx.
  case/andPa_x1 g_p1 /andP[not_p1x _] /subsetP p_p1 p1y not_pv.
   x1 ⇒ //; p1 ⇒ //.
  rewrite disjoint_sym disjoint_cons not_p1x disjoint_sym.
  by move: not_pv; rewrite disjoint_cons ⇒ /andP[_ /disjoint_trans->].
have{neq_yx not_vy}: y \notin v1 by exact/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; x; [exact: mem_head | exact: 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]].
   x1; [exact: predU1r | p ⇒ //].
  by rewrite disjoint_sym (disjoint_trans v2v) // disjoint_sym.
suffices not_p1v2: [disjoint x1 :: p & v2].
  case/predU1P: a_x1 ⇒ [def_x1 | ]; last by x1; last p.
  case/pred0Pn: not_p1v2; x; rewrite /= def_x1 mem_head /=.
  suffices not_vx: x \notin v by apply/IHn; last exact: 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_pvp0 p2 p0x2.
rewrite last_cat cat_path -cat_cons lastI cat_rcons {}p0x2p2y /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⇒ //; (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]; 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 movex y; rewrite /= mem_enum. Qed.

Definition connect : rel T := fun x yy \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 ->]; p ⇒ //; rewrite (eq_path rgraphK) in e_p ×.
Qed.

Lemma connect_trans : transitive connect.
Proof.
movex y z /connectP[p e_p ->] /connectP[q e_q ->]; apply/connectP.
by (p ++ q); rewrite ?cat_path ?e_p ?last_cat.
Qed.

Lemma connect0 x : connect x x.
Proof. by apply/connectP; [::]. Qed.

Lemma eq_connect0 x y : x = yconnect x y.
Proof. move->; exact: connect0. Qed.

Lemma connect1 x y : e x yconnect x y.
Proof. by movee_xy; apply/connectP; [:: y]; rewrite /= ?e_xy. Qed.

Lemma path_connect x p : path e x psubpred (mem (x :: p)) (connect x).
Proof.
movee_p y p_y; case/splitPl: p / p_y e_pp q <-.
by rewrite cat_path ⇒ /andP[e_p _]; apply/connectP; p.
Qed.

Definition root x := odflt x (pick (connect x)).

Definition roots : pred T := fun xroot 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 yconnect x =1 connect y.
Proof. by move/connect1; exact: same_connect. Qed.

Lemma same_connect1r x y : e x yconnect^~ x =1 connect^~ y.
Proof. by move/connect1; exact: 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 := x y, e x yin_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)).

Prenex Implicits connect root roots.

Implicit Arguments dfsP [T g x y].
Implicit Arguments connectP [T e x y].
Implicit 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.
movee'e x _ /connectP[p e_p ->]; elim: p x e_p ⇒ //= y p IHp x /andP[exy].
by move/IHp; apply: connect_trans; exact: e'e.
Qed.

Lemma relU_sym e e' :
  connect_sym econnect_sym e'connect_sym (relU e e').
Proof.
movesym_e sym_e'; apply: symmetric_from_prex _ /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 xx y e_xy; rewrite connect1 //= e_xy ?orbT.
Qed.

Lemma eq_connect e e' : e =2 e'connect e =2 connect e'.
Proof.
moveeq_e x y; apply/connectP/connectP⇒ [] [p e_p ->];
  by p; rewrite // (eq_path eq_e) in e_p ×.
Qed.

Lemma eq_n_comp e e' : connect e =2 connect e'n_comp_mem e =1 n_comp_mem e'.
Proof.
moveeq_e [a]; apply: eq_cardx /=.
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 moveeq_a; apply: eq_cardx; 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_cardx; rewrite !inE andbC.
Qed.

Lemma eq_root e e' : e =2 e'root e =1 root e'.
Proof. by moveeq_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 moveeq_e x; rewrite /roots (eq_root eq_e). Qed.

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 ye y x).
Proof.
suff crev e': subrel (connect (fun x : Te'^~ x)) (fun x(connect e')^~x).
  by movex y; rewrite sym_e; apply/idP/idP; exact: crev.
movex y /connectP[p e_p p_y]; apply/connectP.
(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 intro_closed a : ( x y, e x yx \in ay \in a) → closed e a.
Proof.
movecl_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)]; exact: IHp.
Qed.

Lemma closed_connect a :
  closed e a x y, connect e x y(x \in a) = (y \in a).
Proof.
movecl_a x _ /connectP[p e_p ->].
by elim: p x e_p ⇒ //= y p IHp x /andP[/cl_a->]; exact: IHp.
Qed.

Lemma connect_closed x : closed e (connect e x).
Proof. by movey z /connect1/same_connect_r; exact. Qed.

Lemma predC_closed a : closed e aclosed e [predC a].
Proof. by movecl_a x y /cl_a; rewrite !inE ⇒ →. Qed.

Lemma closure_closed a : closed e (closure e a).
Proof.
apply: intro_closedx y /connect1 e_xy; congr (~~ _).
by apply: eq_disjoint; exact: same_connect.
Qed.

Lemma mem_closure a : {subset a closure e a}.
Proof. by movex a_x; apply/existsP; x; rewrite !inE connect0. Qed.

Lemma subset_closure a : a \subset closure e a.
Proof. by apply/subsetP; exact: 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_cardz.
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;
  [ x | 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_cardy.
apply/andP/eqP ⇒ [[/eqP r_y /rootP→ //] | ->] /=.
by rewrite inE connect_root roots_root.
Qed.

End Closure.

Section Orbit.

Variables (T : finType) (f : TT).

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 (traject f (f x) n); [ exact: 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 _ ->]; exact: 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; exact/loopingP/looping_order.
exact: fconnect_iter.
Qed.

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 {1}/n orderSpred /order -(size_traject f x n).
apply: (leq_trans (subset_leq_card _) (card_size _)); apply/subsetPz.
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 ⇒ [->|]; [ i | j].
Qed.

Lemma findex_max x y : fconnect f x yfindex x y < order x.
Proof. by rewrite [_ y]fconnect_orbit -index_mem size_orbit. Qed.

Lemma findex_iter x i : i < order xfindex x (iter i f x) = i.
Proof.
movelt_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 yiter (findex x y) f x = y.
Proof.
rewrite [_ y]fconnect_orbitfxy; 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 fconnect_invariant (T' : eqType) (k : TT') :
  invariant f k =1 xpredT x y, fconnect f x yk x = k y.
Proof.
moveeq_k_f x y /iter_findex <-; elim: {y}(findex x y) ⇒ //= n →.
by rewrite (eqP (eq_k_f _)).
Qed.

Section Loop.

Variable p : seq T.
Hypotheses (f_p : fcycle f p) (Up : uniq p).
Variable x : T.
Hypothesis 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_xn ->; rewrite !last_traject -iterSdef_x.
by apply: (@loopingP _ f x n.+1); rewrite /looping def_x /= mem_head.
Qed.

Lemma order_cycle : order x = size p.
Proof. by rewrite -(card_uniqP Up); exact (eq_card fconnect_cycle). Qed.

Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
Proof.
have [i q def_p] := rot_to p_x; i.
rewrite /orbit order_cycle -(size_rot i) def_p.
suffices /fpathP[j ->]: fpath f x q by rewrite /= size_traject.
by move: f_p; rewrite -(rot_cycle i) def_p (cycle_path x); case/andP.
Qed.

End Loop.

Hypothesis injf : injective f.

Lemma f_finv : cancel finv f.
Proof.
movex; 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 ⇒ /= /injf →.
by case/trajectP; i.
Qed.

Lemma finv_f : cancel f finv.
Proof. exact (inj_can_sym f_finv injf). Qed.

Lemma fin_inj_bij : bijective f.
Proof. finv; [ exact finv_f | exact f_finv ]. Qed.

Lemma finv_bij : bijective finv.
Proof. f; [ exact f_finv | exact 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.
suff{x y} Sf x y: fconnect f x yfconnect f y x by apply/idP/idP; auto.
case/connectPp f_p → {y}; elim: p x f_p ⇒ //= y p IHp x.
rewrite -{2}(finv_f x) ⇒ /andP[/eqP→ /IHp/connect_trans→ //].
exact: fconnect_finv.
Qed.
Let symf := fconnect_sym.

Lemma iter_order x : iter (order x) f x = x.
Proof. by rewrite -orderSpred iterS; exact (f_finv x). Qed.

Lemma iter_finv n x : n order xiter n finv x = iter (order x - n) f x.
Proof.
rewrite -{2}[x]iter_order ⇒ /subnKC {1}<-; move: (_ - n) ⇒ m.
by rewrite iter_add; elim: n ⇒ // n {2}<-; rewrite iterSr /= finv_f.
Qed.

Lemma cycle_orbit x : fcycle f (orbit x).
Proof.
rewrite /orbit -orderSpred (cycle_path x) /= last_traject -/(finv x).
by rewrite fpath_traject f_finv andbT /=.
Qed.

Lemma fpath_finv x p : fpath finv x p = fpath f (last x p) (rev (belast x p)).
Proof.
elim: p x ⇒ //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC /=.
rewrite (canF_eq finv_f) eq_sym; congr (_ && (_ == _)).
by case: p ⇒ //= z p; rewrite rev_cons last_rcons.
Qed.

Lemma same_fconnect_finv : fconnect finv =2 fconnect f.
Proof.
movex y; rewrite (same_connect_rev symf); apply: {x y}eq_connectx 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 nfclosed f afcard f a × n = #|a|.
Proof.
movea_n cl_a; rewrite /n_comp_mem; set b := [predI froots f & a].
symmetry; transitivity #|preim (froot f) b|.
  apply: eq_cardx; rewrite !inE (roots_root fconnect_sym).
  by rewrite -(closed_connect cl_a (connect_root _ x)).
have{cl_a a_n} (x): b xfroot 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; exact: (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_cardy.
  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 x, (x \in a) = (f x \in a).
Proof. by movecl_a x; exact: 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.

End Orbit.

Prenex Implicits order orbit findex finv order_set.

Section FconnectId.

Variable T : finType.

Lemma fconnect_id (x : T) : fconnect id x =1 xpred1 x.
Proof. by movey; 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; exact: froots_id. Qed.

Lemma fcard_id (a : pred T) : fcard id a = #|a|.
Proof. by apply: eq_cardx; rewrite inE froots_id. Qed.

End FconnectId.

Section FconnectEq.

Variables (T : finType) (f f' : TT).

Lemma finv_eq_can : cancel f f'finv f =1 f'.
Proof.
movefK; exact: (bij_can_eq (fin_inj_bij (can_inj fK)) (finv_f (can_inj fK))).
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 movex; 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.

Section FinvEq.

Variables (T : finType) (f : TT).
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 movex; exact: 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 movex; 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_aconnect 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' : x, x \in aT') :
   ( x a_x,
      [/\ connect e x (h (h' x a_x))
        & y a_y, e x yconnect 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.
Proof.
moveAee' Ae'e; split⇒ [y a_y | x' z' a_x].
  by (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/andPe_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 ha \subset codom hrel_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_adjunctionclosed 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_adjunctionn_comp e a = n_comp e' [preim h of a].
Proof.
caseAee' Ae'e.
have inj_h: {in predI (roots e') [preim h of a] &, injective (root e \o h)}.
  movex' 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_cardx.
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.
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.

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

Unset Implicit Arguments.