# 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)
end
end.

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
end
end.

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.