Library CoLoR.Util.Relation.Cycle

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

Set Implicit Arguments.


Section S.

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

cycles

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