Library CoLoR.Util.FGraph.FGraph

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


Set Implicit Arguments.

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

  Module Export S := FSetUtil.Make XSet.
  Module Export M := FMapUtil.Make XMap.

  Module R := RelUtil.
  Module Import X := E.

  Lemma eq_com x y : eq x y <-> eq y x.

A finite graph on X.t is represented by its successor map: a finite map from X.t to the type of finite sets on X.t. Since an element can be mapped to the empty set, this representation is not unique and the setoid equality on maps based on the setoid equality on sets (meq) does not identify a map with no mapping for x and a map mapping x to the empty set. We therefore have to consider another equivalence (geq). We will consider that two graphs are equivalent if they define the same relation. See below for more details.

  Definition graph := XMap.t XSet.t.

  Implicit Type g h : graph.

  Definition meq : relation graph := XMap.Equiv XSet.Equal.

  Instance Equal_meq : subrelation Equal meq.


relation corresponding to a graph

  SubClass relation_on_X := relation X.t.

  Definition rel g : relation_on_X :=
    fun x y => exists s, find x g = Some s /\ XSet.In y s.

  Coercion rel : graph >-> relation_on_X.

  Lemma rel_empty : rel empty == empty_rel.

  Instance rel_meq_ext' : Proper (meq ==> eq ==> eq ==> impl) rel.


  Instance rel_meq_ext : Proper (meq ==> eq ==> eq ==> iff) rel.


  Lemma find_Some_rel {g x s} : find x g = Some s ->
    XSet.is_empty s = false -> exists y, rel g x y.

singleton relation

  Definition id x y a b := eq a x /\ eq b y.

relation defined by an element and a set of successors

  Definition succ x s a b := eq a x /\ XSet.In b s.

  Instance succ_m_ext' : Proper (eq ==> XSet.Equal ==> eq ==> eq ==> impl) succ.


  Instance succ_m' : Proper (eq ==> XSet.Equal ==> inclusion) succ.


  Instance succ_m : Proper (eq ==> XSet.Equal ==> same) succ.


  Lemma succ_empty : forall x, succ x XSet.empty == empty_rel.

  Lemma succ_add : forall x y s, succ x (XSet.add y s) == id x y U succ x s.

  Lemma rel_add : forall x g s, ~In x g -> rel (add x s g) == succ x s U g.

relation defined by an element and a list of successors

  Definition succ_list x s a (b : X.t) := eq a x /\ InA eq b s.

  Instance succ_list_m_ext' :
    Proper (eq ==> eqlistA eq ==> eq ==> eq ==> impl) succ_list.


  Lemma succ_list_nil : forall x, succ_list x nil == empty_rel.

  Lemma succ_list_cons : forall x y l,
    succ_list x (y :: l) == id x y U succ_list x l.

product relation

  Definition prod s t a b := XSet.In a s /\ XSet.In b t.

  Lemma prod_m_ext :
    Proper (XSet.Equal ==> XSet.Equal ==> eq ==> eq ==> iff) prod.

ordering on graphs: g is smaller than g' if rel g is included in rel g'

  Definition gle g h := g << h.

  Instance gle_PreOrder : PreOrder gle.


  Lemma empty_gle : forall g, rel empty << g.

equality on graphs: two graphs are equivalent if they define the same relation

  Definition geq g h := g == h.

  Instance geq_Equivalence : Equivalence geq.


  Lemma meq_geq : meq << geq.

  Instance geq_meq : Proper (meq ==> meq ==> iff) geq.


  Instance geq_Equal : Proper (Equal ==> Equal ==> iff) geq.


  Lemma Equal_geq : Equal << geq.

relations between gle and geq

  Lemma gle_antisym : forall g h, geq g h <-> (gle g h /\ gle h g).

  Instance gle_geq' : Proper (geq ==> geq ==> impl) gle.


properties of rel

  Instance rel_gle_ext : Proper (gle ==> eq ==> eq ==> impl) rel.


  Instance rel_geq_ext' : Proper (geq ==> eq ==> eq ==> impl) rel.


successors of a node

  Definition succs x g :=
    match find x g with
      | Some s => s
      | None => XSet.empty
    end.

  Lemma In_succs_rel : forall g x y, XSet.In y (succs x g) <-> rel g x y.

  Lemma mem_succs_rel : forall g x y,
    XSet.mem y (succs x g) = true <-> rel g x y.

  Lemma succs_empty : forall x, succs x empty = XSet.empty.

  Lemma succs_add : forall x y s g,
    succs x (add y s g) = if eq_dec y x then s else succs x g.

  Lemma succs_add_id : forall x s g, succs x (add x s g) = s.

  Instance succs_gle : Proper (eq ==> gle ==> XSet.Subset) succs.


  Instance succs_geq : Proper (eq ==> geq ==> XSet.Equal) succs.


  Lemma mem_succs_id : forall g x y,
    XSet.mem y (succs x g) = true -> g U id x y == g.

g is smaller then g' iff the successors of g are included in the successors of g'

  Lemma gle_succs : forall g g',
    gle g g' <-> forall x, succs x g [<=] succs x g'.

two graphs are equivalent iff they have the same successors

  Lemma geq_succs : forall g g',
    geq g g' <-> forall x, succs x g [=] succs x g'.

properties of geq wrt add

  Lemma geq_add_remove : forall y s g g', ~In y g -> geq (add y s g) g' ->
    geq g (if XSet.is_empty s then g' else remove y g').

  Lemma geq_add : forall y s g g', ~In y g -> geq (add y s g) g' ->
    if XSet.is_empty s then geq g' g else Add y (succs y g') (remove y g') g'.

predecessors of a node

  Definition preds_aux x y sy s := if XSet.mem x sy then XSet.add y s else s.

  Instance preds_aux_m :
    Proper (eq ==> eq ==> XSet.Equal ==> XSet.Equal ==> XSet.Equal) preds_aux.


  Instance preds_aux_m' :
    Proper (Logic.eq ==> eq ==> Logic.eq ==> XSet.Equal ==> XSet.Equal)
    preds_aux.


  Lemma preds_aux_transp : forall x, transpose_neqkey XSet.Equal (preds_aux x).

  Definition preds x g := fold (preds_aux x) g XSet.empty.

  Instance preds_Equal : Proper (eq ==> Equal ==> XSet.Equal) preds.


  Lemma preds_empty : forall x, preds x empty [=] XSet.empty.

  Lemma preds_add : forall x y s g, ~In y g -> preds x (add y s g)
    [=] if XSet.mem x s then XSet.add y (preds x g) else preds x g.

  Lemma preds_geq_empty : forall x g,
    geq g empty -> preds x g [=] XSet.empty.

  Instance preds_geq : Proper (eq ==> geq ==> XSet.Equal) preds.


  Lemma In_preds_rel : forall x y g, XSet.In x (preds y g) <-> rel g x y.

  Lemma prod_add_incl_tc_id : forall x y g,
    prod (XSet.add x (preds x g)) (XSet.add y (succs y g)) << (g U id x y)!.

add an edge into a graph

  Definition add_edge x y g : graph := add x (XSet.add y (succs x g)) g.

  Instance add_edge_gle : Proper (eq ==> eq ==> gle ==> gle) add_edge.


  Instance add_edge_geq : Proper (eq ==> eq ==> geq ==> geq) add_edge.


  Lemma rel_add_edge : forall x y g, add_edge x y g == g U id x y.

  Lemma add_edge_transp_geq : forall x, transpose geq (add_edge x).

set iteration of (add_edge x)

  Lemma rel_set_fold_add_edge : forall x s g0,
    XSet.fold (add_edge x) s g0 == succ x s U g0.

  Lemma rel_set_fold_add_edge_ext : forall x s g0 a b,
    rel (XSet.fold (add_edge x) s g0) a b <-> succ x s a b \/ rel g0 a b.

list iteration of (add_edge x)

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

  Lemma rel_list_fold_left_add_edge : forall x l g0,
    fold_left (add_edge' x) l g0 == succ_list x l U g0.

building graphs by list iteration

  Section list_fold_left.

    Variables (A : Type) (F : graph -> A -> graph)
      (hF : forall g a, F g a == F empty a U g).

    Lemma rel_list_fold_left : forall l g x y, rel (fold_left F l g) x y
      <-> (rel g x y \/ exists a, List.In a l /\ rel (F empty a) x y).

  End list_fold_left.

End Make.