Library CoLoR.Util.Relation.SCC

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Leo Ducas, 2007-08-06
Strongly Connected Components (SCC) of a graph seen as a relation

Set Implicit Arguments.

Section S.

  Variable A : Type.

  Section definition.

    Variable R : relation A.

Definition of SCC seen as a relation : are x and y in the same SCC ?

    Definition SCC x y := R! x y /\ R! y x.

Basic properties

    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.

    Lemma cycle_in_SCC : forall x l, cycle R x l -> forall y, In y l -> SCC x y.

    Lemma SCC_in_cycle : forall x y, SCC x y -> exists l, cycle R x l /\ In y l.

    Lemma cycle_in_SCC_bound : forall x l, cycle R x l -> SCC x x.

  End definition.

  Section inclusion.

    Variables R1 R2 : relation A.

    Lemma SCC_incl : R1 << R2 -> SCC R1 << SCC R2.

  End inclusion.

End S.