- -

Library mathcomp.ssreflect.fingraph

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

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