Library CoLoR.Util.FGraph.TransClos

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2011-01-18
Transitive closure of a finite graph.


Set Implicit Arguments.

Module Make (XSet : FSetInterface.S)
       (XMap : FMapInterface.S with Module E := XSet.E).

  Module Export G := FGraph.Make XSet XMap.

  Implicit Type g h : graph.

  Import X.

  Module R := RelUtil.

(a,b) in (pred x s g) if a is a predecessor of x in g and b in s

  Definition pred x s g a b := rel g a x /\ XSet.In b s.

  Instance pred_geq' :
    Proper (eq ==> XSet.Equal ==> geq ==> inclusion) pred.


  Instance pred_geq :
    Proper (eq ==> XSet.Equal ==> geq ==> same) pred.


  Instance pred_geq_ext' :
    Proper (eq ==> XSet.Equal ==> geq ==> eq ==> eq ==> impl) pred.


  Instance pred_geq_ext :
    Proper (eq ==> XSet.Equal ==> geq ==> eq ==> eq ==> iff) pred.


  Lemma pred_empty : forall x s, pred x s empty == empty_rel.

  Lemma pred_succ_prod : forall x y g,
    let ysy := XSet.add y (succs y g) in
      let xpx := XSet.add x (preds x g) in
        pred x ysy g U succ x ysy == prod xpx ysy.

if x is in sw, then add a pair (w,z) for every z in s

  Definition add_pred x s w sw g :=
    if XSet.mem x sw then XSet.fold (add_edge w) s g else g.

  Instance add_pred_geq :
    Proper (eq ==> XSet.Equal ==> eq ==> XSet.Equal ==> geq ==> geq) add_pred.


  Lemma rel_map_fold_add_pred : forall x s g g0,
    fold (add_pred x s) g g0 == pred x s g U g0.

  Lemma rel_map_fold_add_pred_ext : forall x s g g0 a b,
    rel (fold (add_pred x s) g g0) a b <-> pred x s g a b \/ rel g0 a b.

  Lemma add_pred_transp_geq : forall x s, transpose_neqkey geq (add_pred x s).

given a transitive graph g, add x y g adds edges to g to get the transitive closure of id x y U g

  Definition trans_add_edge x y g :=
    
    if XSet.mem y (succs x g) then g
    
      else let ysy := XSet.add y (succs y g) in
        fold (add_pred x ysy) g
        
          (XSet.fold (add_edge x) ysy g).

  Instance trans_add_edge_geq :
    Proper (eq ==> eq ==> geq ==> geq) trans_add_edge.


  Lemma rel_trans_add_edge_pred_succ : forall x y g,
    trans_add_edge x y g == if XSet.mem y (succs x g) then g
      else let ysy := XSet.add y (succs y g) in pred x ysy g U (succ x ysy U g).

  Lemma rel_trans_add_edge_prod : forall x y g,
    trans_add_edge x y g == if XSet.mem y (succs x g) then g
      else prod (XSet.add x (preds x g)) (XSet.add y (succs y g)) U g.

  Lemma add_edge_incl_trans : forall x y g,
    add_edge x y g << trans_add_edge x y g.

  Lemma transitive_trans_add_edge : forall x y g,
    Transitive g -> Transitive (trans_add_edge x y g).

  Lemma rel_trans_add_edge : forall x y g,
    Transitive g -> trans_add_edge x y g == add_edge x y g!.

  Lemma succs_trans_add_edge_id : forall x y g,
    succs x (trans_add_edge x y g)
    [=] if XSet.mem y (succs x g) then succs x g
      else XSet.union (XSet.add y (succs y g)) (succs x g).

  Lemma preds_trans_add_edge_id : forall x y g,
    preds x (trans_add_edge x y g)
    [=] if XSet.mem y (succs x g) then preds x g
      else if XSet.mem x (XSet.add y (succs y g)) then XSet.add x (preds x g)
        else preds x g.

building a transitive graph using list iteration

  Import ListUtil.

  Definition trans_add_edge' x g y := trans_add_edge x y g.

  Lemma transitive_list_fold_left_trans_add_edge : forall x l g,
    Transitive g -> Transitive (fold_left (trans_add_edge' x) l g).

In the following, we assume given a type A (e.g. rule) and a function f on A returning either None or some pair x,l where x is an element of X.t (e.g. a symbol) and l is a list of elements of X.t.

  Section list.

    Variable (A : Type) (f : A -> option (X.t * list X.t)).

graph obtained by extending g with the arcs provided by f a

    Definition add_edge_list g a :=
      match f a with
        | None => g
        | Some (x,l) => fold_left (add_edge' x) l g
      end.

    Lemma rel_add_edge_list : forall g a, add_edge_list g a ==
      match f a with
        | None => g
        | Some (x,l) => succ_list x l U g
      end.

    Global Instance add_edge_list_gle :
      Proper (gle ==> Logic.eq ==> gle) add_edge_list.


    Global Instance add_edge_list_geq :
      Proper (geq ==> Logic.eq ==> geq) add_edge_list.


iteration of add_edge_list on a list of elements of A
graph obtained by extending g with the arcs provided by f a using the function trans_add_edge now

    Definition trans_add_edge_list g a :=
      match f a with
        | None => g
        | Some (x,l) => fold_left (trans_add_edge' x) l g
      end.

    Lemma transitive_trans_add_edge_list : forall g a,
      Transitive g -> Transitive (trans_add_edge_list g a).

    Lemma rel_trans_add_edge_list : forall g a, Transitive g ->
      trans_add_edge_list g a == add_edge_list g a!.

    Lemma transitive_list_fold_left_trans_add_edge_list : forall l g,
      Transitive g -> Transitive (fold_left trans_add_edge_list l g).

iteration of trans_add_edge_list on a list of elements of A
transitive closure of a graph defined by a list of elements of A

    Definition trans_clos_list l := fold_left trans_add_edge_list l empty.

    Lemma transitive_empty : Transitive (rel empty).

    Lemma transitive_trans_clos_list : forall l, Transitive (trans_clos_list l).

    Lemma rel_trans_clos_list : forall l,
      trans_clos_list l == fold_left add_edge_list l empty!.

  End list.

building a transitive graph using set iteration

  Lemma transitive_set_fold_trans_add_edge : forall x g,
    Transitive g -> forall s, Transitive (XSet.fold (trans_add_edge x) s g).

End Make.