Library CoLoR.Util.Relation.RelMidex

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Stephane Le Roux, 2007-02-20
excluded middle and decidability for relations.



Set Implicit Arguments.

Section S.

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

  Definition rel_midex := forall x y : A, R x y \/ ~R x y.

  Definition rel_dec := forall x y, {R x y} + {~R x y}.

  Lemma rel_dec_midex : rel_dec -> rel_midex.

  Definition fun_rel_dec (f : A->A->bool) :=
    forall x y, if f x y then R x y else ~R x y.

  Lemma bool_rel_dec : {f : A->A->bool | fun_rel_dec f} -> rel_dec.

  Lemma rel_dec_bool : rel_dec -> {f : A->A->bool | fun_rel_dec f}.

  Lemma fun_rel_dec_true : forall f x y, fun_rel_dec f -> f x y = true -> R x y.

  Lemma fun_rel_dec_false : forall f x y,
    fun_rel_dec f -> f x y = false -> ~R x y.

Leibniz equality relation

  Definition eq_midex := forall x y : A, x=y \/ x<>y.

  Definition eq_dec := forall x y : A, {x=y}+{x<>y}.

  Lemma eq_dec_midex : eq_dec -> eq_midex.

End S.