# Library mathcomp.ssreflect.fingraph

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
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].

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

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

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

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

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

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.

Variables (T T' : finType) (h : T' T) (e : rel T) (e' : rel T').
Hypotheses (sym_e : connect_sym e) (sym_e' : connect_sym e').

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

injective h a \subset codom h rel_base h e e' [predC a]

Let ccl_a := closed_connect cl_a.

rel_adjunction n_comp e a = n_comp e' [preim h of a].

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.