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.

Require Import Cycle.
Require Import Path.
Require Import ListUtil.
Require Import RelUtil.

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 : x y z, SCC x y SCC y z SCC x z.

Proof.
intros. unfold SCC in ×. destruct H; destruct H0.
split; eapply t_trans; eauto; auto.
Qed.

Lemma SCC_sym : x y, SCC x y SCC y x.

Proof.
intros. unfold SCC in ×. destruct H; split; assumption.
Qed.

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

Proof.
intros. unfold SCC. unfold cycle in H.
generalize (in_elim H0); intros.
destruct H1; destruct H1; subst.
apply path_app_elim in H.
destruct H.
apply path_clos_trans in H; apply path_clos_trans in H1.
split; auto.
Qed.

Lemma SCC_in_cycle : x y, SCC x y l, cycle R x l In y l.

Proof.
intros.
destruct H.
apply clos_trans_path in H; apply clos_trans_path in H0.
destruct H; destruct H0.
(x0++y::x1).
split; auto with ×.
unfold cycle.
apply path_app; auto.
Qed.

Lemma cycle_in_SCC_bound : x l, cycle R x l SCC x x.

Proof.
intros; unfold SCC; unfold cycle in H.
split; apply path_clos_trans in H; auto.
Qed.

End definition.

Section inclusion.

Variables R1 R2 : relation A.

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

Proof.
intros.
unfold inclusion; unfold SCC.
intros.
destruct H0.
assert (R1! << R2!).
apply incl_tc; assumption.
split; unfold inclusion in H2.
apply (H2 x y); assumption.
apply (H2 y x); assumption.
Qed.

End inclusion.

End S.