Library CoLoR.Util.Relation.RelSub

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Stephane Le Roux, 2007-02-20
sub-relation, restriction, etc.

Set Implicit Arguments.

Section On_Rel_Gen.

  Variable A : Type.

  Section restriction.

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

    Definition restriction x y := In x l /\ In y l /\ R x y.

    Definition is_restricted := forall x y, R x y -> In x l /\ In y l.

    Lemma incl_restriction : restriction << R.

    Lemma restriction_dec : eq_dec A -> rel_dec R -> rel_dec restriction.

    Lemma restriction_midex :
      eq_midex A -> rel_midex R -> rel_midex restriction.

  End restriction.

  Lemma restriction_monotonic : forall (R' R'' : relation A) l,
    R' << R'' -> restriction R' l << restriction R'' l.

  Lemma restricted_restriction : forall R l, is_restricted (restriction R l) l.

  Lemma restricted_clos_trans : forall R l,
    is_restricted R l -> is_restricted (clos_trans R) l.

  Lemma clos_trans_restricted_pair : forall R x y,
    is_restricted R (x::y::nil) -> clos_trans R x y -> R x y.

  Lemma clos_trans_restricted_pair_bis : forall R x y,
    is_restricted R (x::y::nil) -> clos_trans R y x -> R y x.

  Lemma clos_trans_restriction : forall (R : relation A) x y,
    R x y -> clos_trans (restriction R (x :: y :: nil)) x y.

End On_Rel_Gen.