Library connect

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
This file develops the theory of transitive closure in a finType T.       
For e : rel T and f : T -> T we define:                                   
                                                                          
dfs e n a x    == the list of points traversed by a depth-first search of 
                  the graph of e, at depth n, starting from x, and        
                  prepended to a                                          
connect e      == the transitive closure of e (computed by dfs)           
connect_sym e  <=> connect e is symmetric, hence an equivalence relation  
root e x       == pick a representative of connect e x, the component of  
                  x in the transitive closure of e                        
roots e        == the codomain predicate of root e                        
n_comp e       == number of components of connect e, i.e., the number of  
                  equivalence classes of connect e if connect_sym e holds 
closed e a     == the predicate a is e-invariant                          
closure e a    == closure under e 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) == connected under f iteration         
froot f x      == root (frel f) x == 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 orbit of x under f               
order_set f n  == elements of f-order n                                   
finv f         == the inverse of f, if f is a permutation; specifically,  
                  finv f x == iter (order x).-1 f x                       
fcard f        == number of orbits of f                                   
fclosed f a    == closed under iteration of f                             
fclosure f a   == closure under f iteration                               
fun_adjunction == rel_adjunction (frel f)                                 

Import Prenex Implicits.

Decidable connectivity in finite types.                                  

Section Connect.

Variables (T : finType) (e : rel T).

Fixpoint dfs (n : nat) (a : seq T) (x : T) {struct n} :=
  if n is n'.+1 then
    if x \in a then a else foldl (dfs n') (x :: a) (enum (e x))
  else a.

Definition connect : rel T := fun x y => y \in dfs #|T| [::] x.

Lemma subset_dfs : forall n (a b : seq T), a \subset foldl (dfs n) a b.

Inductive dfs_path x y (a : seq T) : Prop :=
  DfsPath p of path e x p & y = last x p & [disjoint x :: p & a].

Lemma dfsP : forall n x y (a : seq T),
  #|T| <= #|a| + n -> y \notin a -> reflect (dfs_path x y a) (y \in dfs n a x).

Lemma connectP : forall x y,
  reflect (exists2 p, path e x p & y = last x p) (connect x y).

Lemma connect_trans : forall x1 x2 x3,
  connect x1 x2 -> connect x2 x3 -> connect x1 x3.

Lemma connect0 : forall x, connect x x.

Lemma eq_connect0 : forall x y : T, x = y -> connect x y.

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

Lemma path_connect : forall x p, path e x p ->
  subpred (mem (x :: p)) (connect x).

Definition root x := if pick (connect x) is Some y then y else x.

Definition roots : pred T := fun x => root x == x.

Definition n_comp a := #|predI roots a|.

Lemma connect_root : forall x, connect x (root x).

Definition connect_sym := forall x y, connect x y = connect y x.

Lemma same_connect : connect_sym -> forall x y,
  connect x y -> connect x =1 connect y.

Lemma same_connect_r : connect_sym -> forall x y,
  connect x y -> forall z, connect z x = connect z y.

Lemma rootP : forall x y,
  connect_sym -> reflect (root x = root y) (connect x y).

Lemma root_root : connect_sym -> forall x, root (root x) = root x.

Lemma roots_root : connect_sym -> forall x, roots (root x).

Lemma root_connect :
  connect_sym -> forall x y, (root x == root y) = connect x y.

End Connect.


Implicit Arguments connectP [T e x y].
Implicit Arguments rootP [T e x y].

Notation "'fconnect' f" := (connect (frel f))
  (at level 10, f at level 8) : seq_scope.

Notation "'froot' f" := (root (frel f))
  (at level 10, f at level 8) : seq_scope.

Notation "'froots' f" := (roots (frel f))
  (at level 10, f at level 8) : seq_scope.

Notation "'fcard' f" := (n_comp (frel f))
  (at level 10, f at level 8) : seq_scope.

Section EqConnect.

Variable T : finType.

Lemma connect_sub : forall e e' : rel T,
  subrel e (connect e') -> subrel (connect e) (connect e').

Lemma relU_sym : forall e e' : rel T,
  connect_sym e -> connect_sym e' -> connect_sym (relU e e').

Lemma eq_connect : forall e e' : rel T, e =2 e' -> connect e =2 connect e'.

Lemma eq_n_comp : forall e e' : rel T,
  connect e =2 connect e' -> n_comp e =1 n_comp e'.

Lemma eq_n_comp_r : forall a a' : pred T, a =1 a' ->
  forall e, n_comp e a = n_comp e a'.

Lemma n_compC : forall a e, n_comp e T = n_comp e a + n_comp e (predC a).

Lemma eq_root : forall e1 e2 : rel T, e1 =2 e2 -> root e1 =1 root e2.

Lemma eq_roots : forall e1 e2 : rel T, e1 =2 e2 -> roots e1 =1 roots e2.

End EqConnect.

Section Closure.

Variables (T : finType) (e : rel T).
Hypothesis He : connect_sym e.

Lemma same_connect_rev : connect e =2 connect (fun x y => e y x).

Definition closed (a : pred T) := forall x y, e x y -> a x = a y.

Lemma intro_closed : forall a : pred T,
  (forall x y, e x y -> a x -> a y) -> closed a.

Lemma closed_connect : forall a, closed a ->
  forall x y, connect e x y -> a x = a y.

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

Lemma predC_closed : forall a, closed a -> closed (predC a).

Definition closure (a : pred T) : pred T :=
  fun x => ~~ [disjoint connect e x & a].

Lemma closure_closed : forall a, closed (closure a).

Lemma subset_closure : forall a : pred T, a \subset (closure a).

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

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

End Closure.

Notation "'fclosed' f" := (closed (frel f))
  (at level 10, f at level 8) : seq_scope.

Notation "'fclosure' f" := (closure (frel f))
  (at level 10, f at level 8) : seq_scope.


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 : forall n x, fconnect f x (iter n f x).

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

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

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

Lemma size_orbit : forall x : T, size (orbit x) = order x.

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

Lemma fconnect_orbit : forall x, fconnect f x =i orbit x.

Lemma orbit_uniq : forall x, uniq (orbit x).

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

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

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

Lemma findex0 : forall x, findex x x = 0.

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

Section Loop.

Variable p : seq T.
Hypotheses (Hp : fcycle f p) (Up : uniq p).
Variable x : T.
Hypothesis Hx : x \in p.

The first lemma does not depend on Up : (uniq p) 
Lemma fconnect_cycle : fconnect f x =i p.

Lemma order_cycle : order x = size p.

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

End Loop.

Hypothesis Hf : 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 : forall x y, fconnect f x y = fconnect f y x.

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

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

Lemma cycle_orbit : forall x, fcycle f (orbit x).

Lemma fpath_finv : forall 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 finv =1 fcard f.

Definition order_set n : pred T := fun x => order x == n.

Lemma order_div_card : forall n a,
    subpred a (order_set n) -> fclosed f a -> 0 < n ->
  forall m, (#|a| == n * m) = (fcard f a == m).

Lemma fclosed1 : forall a, fclosed f a -> forall x, a x = a (f x).

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

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

End Orbit.


Section FinCancel.

Variables (T : finType) (f f' : T -> T).
Hypothesis Ef : cancel f f'.

Let Hf := can_inj Ef.

Lemma finv_eq_can : finv f =1 f'.

End FinCancel.

Section FconnectEq.

Variables (T : finType) (f f' : T -> T).
Hypothesis Eff' : f =1 f'.

Lemma eq_pred1 : frel f =2 frel f'.

Lemma eq_fpath : fpath f =2 fpath f'.

Lemma eq_fconnect : fconnect f =2 fconnect f'.

Lemma eq_fcard : fcard f =1 fcard 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'.

Hypothesis Hf : injective f.

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

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

Lemma order_set_finv : order_set (finv f) =2 order_set f.

End FconnectEq.

Section RelAdjunction.

Variables (T T' : finType) (h : T' -> T) (e : rel T) (e' : rel T').
Hypotheses (He : connect_sym e) (He' : connect_sym e').

Variable a : pred T.
Hypothesis Ha : closed e a.

Record rel_adjunction : Type := RelAdjunction {
  rel_unit : forall x, a x -> {x' : T' | connect e x (h x')};
  rel_functor : forall x' y',
    a (h x') -> connect e' x' y' = connect e (h x') (h y')
}.

Lemma intro_adjunction : forall h' : (forall x, a x -> T'),
   (forall x Hx, connect e x (h (h' x Hx))
             /\ (forall y Hy, e x y -> connect e' (h' x Hx) (h' y Hy))) ->
   (forall x' Hx, connect e' x' (h' (h x') Hx)
             /\ (forall 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.

Lemma adjunction_closed : rel_adjunction -> closed e' (preim h a).

Lemma adjunction_n_comp : rel_adjunction -> n_comp e a = n_comp e' (preim h a).

End RelAdjunction.

Definition fun_adjunction T T' h f f' :=
  @rel_adjunction T T' h (frel f) (frel f').

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