Library CoLoR.Util.Relation.Path

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Stephane Le Roux, 2006-10-17
  • Frederic Blanqui, 2007-01-22
  • Sidi Ould-Biha, 2010-04-27

Set Implicit Arguments.

in the following, we assume given a type A and a relation R on A

Section S.

  Variables (A : Type) (R : relation A).

(path x y z1;..;zn) if x R z1 R .. R zn R y

  Fixpoint path (x y : A) (l : list A) : Prop :=
    match l with
      | nil => R x y
      | z::l' => R x z /\ path z y l'

  Lemma path_clos_trans : forall y l x, path x y l -> R! x y.

  Lemma path_app : forall y z l' l x,
    path x y l -> path y z l' -> path x z (l++y::l').

  Lemma clos_trans_path : forall x y, R! x y -> exists l, path x y l.

  Lemma path_app_elim_right : forall y z l l' x,
    path x z (l++y::l') -> path y z l'.

  Lemma path_nodup_length :
    eq_midex A -> forall y l x, path x y l ->
      exists l', ~In x l' /\ ~In y l' /\ nodup l'
        /\ length l'<= length l /\ l' [= l /\ path x y l'.

  Lemma path_restricted_incl : forall y l l' x,
    is_restricted R l -> path x y l' -> l' [= l.

  Lemma path_nth_inP : forall l x y k,
    path x y l -> S k < length l -> R (nth k l y) (nth (S k) l y).

  Lemma path_lastP : forall k x y l,
    path x y l -> S k = length l -> R (nth k l y) y.

  Lemma path_headP : forall l x y, path x y l -> R x (nth 0 l y).

paths of bounded length

  Inductive bpath n : relation A :=
  | bp_intro : forall x y l, length l <= n -> path x y l -> bpath n x y.

  Lemma bpath_clos_trans : forall n, bpath n << R!.

  Lemma clos_trans_bpath : eq_midex A -> forall l,
    is_restricted R l -> R! << bpath (length l).

  Lemma bpath_n_Sn : forall n x y, bpath n x y -> bpath (S n) x y.

  Lemma bpath_Sn_n_or_Rn : forall n x y,
    bpath (S n) x y -> bpath n x y \/ exists z : A, R x z /\ bpath n z y.

  Lemma R_bpath_n_Sn : forall x y z n,
    R x y -> bpath n y z -> bpath (S n) x z.

properties when the equality is decidable

  Variables eqdec : eq_dec A.

  Lemma path_app_elim : forall l x y z m,
    path x y (l++z::m) -> path x z l /\ path z y m.

  Lemma sub_path : forall l x y x' y' l' m p,
    x::l++y::nil = m++x'::l'++y'::p -> path x y l -> path x' y' l'.

  Lemma path_suffix : forall y z l' l'' x,
    path x y l' -> suffix (z::l'') l' -> path z y l''.

  Lemma path_cut : forall y l' x,
    In x l' -> path x y l' -> path x y (tail(cut eqdec x l')).

  Lemma path_cut_bis : forall l' x y z,
    In z l' -> R x z -> path z y l' -> path x y (cut eqdec z l').

  Lemma path_shrink : forall y l' x, path x y l' -> path x y (shrink eqdec l').

End S.

paths and sub-relations

Section inclusion.

  Variable A : Type.

  Lemma path_preserved : forall R R' (y : A) l x,
    R << R' -> path R x y l -> path R' x y l.

  Lemma path_restriction : forall R (y : A) l x,
    path R x y l -> path (restriction R (x::y::l)) x y l.

End inclusion.


Section restriction.

  Variables (A : Type) (R : relation A) (l : list A).

  Lemma restricted_path_incl : is_restricted R l ->
    forall m x y, path R x y m -> x :: m ++ y :: nil [= l.

  Variable eqdec : eq_dec A.

  Lemma long_path_occur : is_restricted R l ->
    forall x y m, path R x y m -> length m >= length l - 1 ->
      exists z, occur eqdec z (x :: m ++ y :: nil) >= 2.

  Lemma path_restriction_In_left : forall (x y : A) l',
    path (restriction R l) x y l' -> In x l.

End restriction.