Library mathcomp.ssreflect.fingraph
(* (c) Copyright 2006-2015 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).
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)).
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 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)).
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 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.
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.
Implicit Arguments intro_adjunction [T T' h e e' a].
Implicit Arguments adjunction_n_comp [T T' e e' a].
Unset Implicit Arguments.
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.
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.
Implicit Arguments intro_adjunction [T T' h e e' a].
Implicit Arguments adjunction_n_comp [T T' e e' a].
Unset Implicit Arguments.