Library CoLoR.Util.Relation.Cycle

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-02-06

Set Implicit Arguments.

Section S.

Variables (A : Type) (R : relation A) (eq_dec : forall x y : A, {x=y}+{~x=y}).


Definition cycle x := path R x x.

Lemma path_cycle : forall x y l, path R x y l -> In x l ->
  exists m, exists p, l = m ++ x :: p /\ cycle x m.

cycles of minimum length

Definition cycle_min x l := cycle x l /\ ~In x l /\ nodup l.

Lemma cycle_min_intro : forall x l, cycle x l ->
  exists m, exists y, exists p, exists q,
    x :: l = m ++ y :: p ++ q /\ cycle_min y p.

End S.

implicit arguments