# 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.