Library CoLoR.Util.Relation.Iter

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-02-07
  • Ducas Leo 2007-08-06
iteration of a relation

Set Implicit Arguments.


Section S.

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

Fixpoint iter (n : nat) : relation A :=
  match n with
    | O => R
    | S p => R @ iter p
  end.

properties

Lemma iter_tc : forall n, iter n << R!.

Lemma iter_iter : forall p q, iter p @ iter q << iter (p+q+1).

Lemma iter_plus_1 : forall p q, iter (p+q+1) << iter p @ iter q.

Lemma iter_commut : forall p q, iter p @ iter q << iter q @ iter p.

unions of iterated relations

Definition Iter_ge k x y := exists n, n >= k /\ iter n x y.

Definition Iter := Iter_ge 0.

Fixpoint iter_le (n : nat) : relation A :=
  match n with
    | O => R
    | S p => iter n U iter_le p
  end.

properties

Lemma tc_iter : R! << Iter.

Lemma Iter_split : forall n, Iter << iter_le n U Iter_ge (S n).

Lemma Iter_ge_split : forall n, Iter_ge n << iter n U Iter_ge (S n).

Lemma iter_Iter_ge_commut : forall n p,
  iter n @ Iter_ge p << Iter_ge p @ iter n.

Lemma iter_Iter_ge : forall n p, iter n @ Iter_ge p << Iter_ge (n+p+1).

Lemma incl_Iter_ge : forall n p, p <= n -> Iter_ge n << Iter_ge p.

Alternative definitions of iter_le

Fixpoint iter_le2 n :=
  match n with
    | O => R
    | S i => (R @ iter_le2 i) U iter_le2 i
  end.

Fixpoint iter_le_fast n :=
  match n with
    | O => R
    | S i => let R' := iter_le_fast i in R' @ R' U R'
  end.

Equivalence between the different definitions

Lemma iter_le_spec : forall n x y,
  iter_le n x y <-> exists p, p <= n /\ iter p x y.

Lemma iter_le2_spec : forall n x y,
  iter_le2 n x y <-> exists p, p <= n /\ iter p x y.

Lemma iter_compose : forall p q, iter p @ iter q << iter (p+q+1).


Lemma iter_le_fast_spec : forall n x y,
  iter_le_fast n x y <-> exists p,(S p) <= exp2 n /\ iter p x y.

Lemma iter_le_same n x y : iter_le2 n x y <-> iter_le n x y.

Lemma iter_le_fast_exp2_same n x y :
  iter_le_fast n x y <-> iter_le ((exp2 n)-1) x y.

relation with paths

Lemma iter_path : forall n x y,
  iter n x y -> exists l, length l = n /\ path R x y l.

Lemma path_iter : forall l x y, path R x y l -> iter (length l) x y.

Lemma bpath_iter_le : forall n x y, bpath R n x y -> iter_le n x y.

Lemma iter_le_bpath : forall n x y, iter_le n x y -> bpath R n x y .

End S.

implicit arguments