Library CoLoR.Util.Relation.RelDec

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Stephane Le Roux, 2007-02-23
decidability of a relation: In an arbitrary set with decidable (resp. middle-excluding) equality, a binary relation is decidable (resp. middle-excluding) iff the transitive closures of its finite restrictions are decidable (resp. middle-excluding)

Set Implicit Arguments.


Section S.

  Variable A : Type.

bound_path preserves middle exclusion and decidability for restrictions

  Section bp_restriction_midex_dec.

    Variable R : relation A.

    Lemma dec_lem : forall R' R'' x y l, rel_dec R' -> rel_dec R'' ->
      {z : A | In z l /\ R' x z /\ R'' z y}
      + {~exists z : A, In z l /\ R' x z /\ R'' z y}.

    Lemma midex_lem : forall R' R'' x y l, rel_midex R' -> rel_midex R'' ->
      (exists z : A, In z l /\ R' x z /\ R'' z y)
      \/ (~exists z : A, In z l /\ R' x z /\ R'' z y).

    Lemma bpath_dec : forall l n,
      is_restricted R l -> rel_dec R -> rel_dec (bpath R n).

    Lemma bpath_midex : forall l n,
      is_restricted R l -> rel_midex R -> rel_midex (bpath R n).

    Lemma restricted_dec_clos_trans_dec : eq_dec A -> rel_dec R ->
      forall l, is_restricted R l -> rel_dec (clos_trans R).

    Lemma restricted_midex_clos_trans_midex : eq_midex A -> rel_midex R ->
      forall l, is_restricted R l -> rel_midex (clos_trans R).

  End bp_restriction_midex_dec.

middle-excluding/decidability of a relation is equivalent to middle-excluding/decidability of the transitive closure of every finite restriction of the relation

  Section em_dec_clos_trans.

    Variable R : relation A.

    Lemma R_midex_clos_trans_restriction_midex : eq_midex A -> rel_midex R ->
      forall l, rel_midex (clos_trans (restriction R l)).

    Lemma R_dec_clos_trans_restriction_dec : eq_dec A -> rel_dec R ->
      forall l, rel_dec (clos_trans (restriction R l)).

    Lemma clos_trans_restriction_dec_R_dec :
      (forall l, rel_dec (clos_trans (restriction R l))) -> rel_dec R.

    Lemma clos_trans_restriction_midex_R_midex :
      (forall l, rel_midex (clos_trans (restriction R l))) -> rel_midex R.

  End em_dec_clos_trans.

End S.