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

Require Import Relations.

Set Implicit Arguments.

Section relation.

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

Definition rel_midex := x y, R x y ¬R x y.

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

Lemma rel_dec_midex : rel_decrel_midex.

Proof.
do 3 intro. destruct (X x y); tauto.
Qed.

Definition fun_rel_dec (f : AAbool) :=
x y, if f x y then R x y else ¬R x y.

Lemma bool_rel_dec : {f : AAbool | fun_rel_dec f}rel_dec.

Proof.
intros (f,H) x y. generalize (H x y). case (f x y) ; intros ; tauto.
Qed.

Lemma rel_dec_bool : rel_dec{f : AAbool | fun_rel_dec f}.

Proof.
intro H. (fun x y : Aif H x y then true else false).
intros x y. destruct (H x y) ; trivial.
Qed.

Lemma fun_rel_dec_true : f x y, fun_rel_dec ff x y = trueR x y.

Proof.
intros. set (w := H x y). rewrite H0 in w. assumption.
Qed.

Lemma fun_rel_dec_false : f x y,
fun_rel_dec ff x y = false¬R x y.

Proof.
intros. set (w := H x y). rewrite H0 in w. assumption.
Qed.

End relation.

equality relation

Section identity.

Variable A : Type.

Definition eq_midex := x y : A, x=y xy.

Definition eq_dec := x y : A, {x=y}+{xy}.

Lemma eq_dec_midex : eq_deceq_midex.

Proof.
do 3 intro. destruct (X x y); tauto.
Qed.

End identity.