Library CoLoR.Util.Relation.SCCTopoOrdering

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Leo Ducas, 2007-08-06
We build here the quotient graph by the relation SCC, which is Topo Sortable. We represent the quotient of the Domain by SCC with a function to nat.

Set Implicit Arguments.

Section SCC_quotient.

  Variable hyps : SCC_dec_hyps.

  Notation A := (hyp_A hyps).
  Notation eq_dec := (hyp_eq_dec hyps).
  Notation Dom := (hyp_Dom hyps).
  Notation R := (hyp_R hyps).
  Notation restriction := (hyp_restriction hyps).
  Notation Dom_nodup := (hyp_nodup hyps).
  Notation R_dec := (hyp_R_dec hyps).
  Notation dim := (length Dom).

  Variables (M : matrix dim dim) (HM : M = SCC_mat_effective hyps).

  Notation SCC := (SCC R).
  Notation SCC_dec := (SCC_effective_dec hyps HM).

Reflexive closure of SCC: isolated points are also considered as SCC

  Definition SCC' x y := (SCC%) x y /\ In x Dom /\ In y Dom.

  Lemma SCC'_dec : forall x y, {SCC' x y} + {~SCC' x y}.

  Lemma SCC'_trans : forall x y z, SCC' x y -> SCC' y z -> SCC' x z.

  Lemma SCC'_sym : forall x y ,SCC' x y -> SCC' y x.

SCC'_tag map each vertex of the graph to its SCC number

  Definition SCC'_tag x := find_first (SCC' x) (SCC'_dec x) Dom.

  Lemma SCC'_tag_exact : forall x y,
      SCC' x y <-> SCC'_tag x = SCC'_tag y /\ SCC'_tag x <> None.

faster way to compute SCC'_tag but not certified

  Fixpoint bools_find_first n (v : vector bool n) :=
    match v with
    | Vnil => None
    | Vcons true w => Some 0
    | Vcons false w =>
      match bools_find_first w with
      | None => None
      | Some r => Some (S r)

  Definition SCC_tag_fast M t :=
    let oi := find_first (eq t) (eq_dec t) Dom in
    match oi with
    | None => None
    | Some i =>
      match le_gt_dec dim i with
      | right Hi => @bools_find_first dim (Vnth M Hi)
      | left _ => None

quotient relation

  Definition Rquo x y :=
    exists r, SCC'_tag r = Some x /\ exists s, SCC'_tag s = Some y /\ R r s.

  Lemma Rquo_restricted : is_restricted Rquo (nats_decr_lt dim).

  Lemma Rquo_dec : forall x y, {Rquo x y} + {~Rquo x y}.

irreflexive version of Rquo

  Definition Rquo' x y := Rquo x y /\ x <> y.

  Lemma Rquo'_dec x y : {Rquo' x y} + {~Rquo' x y}.

  Lemma Rquo'_path : forall l x y, path Rquo' x y l ->
    exists r, SCC'_tag r = Some x /\ exists s, SCC'_tag s = Some y /\ R! r s.

  Lemma irrefl_tc_Rquo' : irreflexive (Rquo'!).

  Lemma topo_sortable_Rquo' : topo_sortable Rquo'.

  Definition RT x y :=
    proj1_sig topo_sortable_Rquo' (nats_decr_lt dim) x y = true.

  Lemma Rquo'_incl_RT : Rquo' << RT.

  Lemma sorted_SCC' :
    {m : list nat | sort RT m & permutation eq_nat_dec (nats_decr_lt dim) m}.

End SCC_quotient.