1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
Require Import Coq.Bool.Bool.
Require Import Coq.Classes.RelationClasses.
Require Coq.Setoids.Setoid.
Set Implicit Arguments.
Set Strict Implicit.
Class RelDec (T : Type) (equ : T -> T -> Prop) : Type :=
{ rel_dec : T -> T -> bool }.
Arguments rel_dec {_} {equ} {_} _ _.
Arguments rel_dec _ _ _ !x !y.
Class RelDec_Correct T (equ : T -> T -> Prop) (ED : RelDec equ) : Prop :=
{ rel_dec_correct : forall x y : T, rel_dec x y = true <-> equ x y }.
Notation "a ?[ r ] b" := (@rel_dec _ r _ a b) (at level 30, b at next level).
Definition eq_dec {T : Type} {ED : RelDec (@eq T)} := rel_dec.
Section neg_rel_dec_correct.
Context {T} {R:T -> T -> Prop} {RD:RelDec R} {RDC:RelDec_Correct RD}.
Definition neg_rel_dec_correct : forall {x y}, ~R x y <-> rel_dec x y = false.
Proof. intros x y. destruct (bool_dec (rel_dec x y) true) ; constructor ; intros ;
repeat
match goal with
| [ |- ~ _ ] => unfold not ; intros
| [ H1 : ?P, H2 : ~?P |- _ ] => specialize (H2 H1) ; contradiction
| [ H1 : ?P = true, H2 : ?P = false |- _ ] => rewrite H1 in H2 ; discriminate
| [ H1 : ?P <> true |- ?P = false ] => apply not_true_is_false ; exact H1
| [ H1 : ?rel_dec ?a ?b = true, H2 : ~?R ?a ?b |- _ ] =>
apply rel_dec_correct in H1
| [ H1 : ?rel_dec ?a ?b = false, H2 : ?R ?a ?b |- _ ] =>
apply rel_dec_correct in H2
end.
Qed.
End neg_rel_dec_correct.
Section rel_dec_p.
Context {T} {R:T -> T -> Prop} {RD:RelDec R} {RDC:RelDec_Correct RD}.
Definition rel_dec_p (x:T) (y:T) : {R x y} + {~R x y}.
Proof. destruct (bool_dec (rel_dec x y) true) as [H | H].
apply rel_dec_correct in H ; eauto.
apply not_true_is_false in H ; apply neg_rel_dec_correct in H ; eauto.
Qed.
Definition neg_rel_dec_p (x:T) (y:T) : {~R x y} + {R x y}.
Proof. destruct (rel_dec_p x y) ; [ right | left ] ; auto. Qed.
End rel_dec_p.
Section lemmas.
Variable T : Type.
Variable eqt : T -> T -> Prop.
Variable r : RelDec eqt.
Variable rc : RelDec_Correct r.
Theorem rel_dec_eq_true : forall x y,
eqt x y -> rel_dec x y = true.
Proof.
intros. eapply rel_dec_correct in H. assumption.
Qed.
Theorem rel_dec_neq_false : forall x y,
~eqt x y -> rel_dec x y = false.
Proof.
intros. remember (x ?[ eqt ] y).
symmetry in Heqb.
destruct b; try reflexivity.
exfalso. eapply (@rel_dec_correct _ _ _ rc) in Heqb. auto.
Qed.
Theorem rel_dec_sym : Symmetric eqt -> forall x y,
x ?[ eqt ] y = y ?[ eqt ] x.
Proof.
intros.
remember (x ?[ eqt ] y); remember (y ?[ eqt ] x); intuition.
destruct b; destruct b0; auto.
{ symmetry in Heqb; symmetry in Heqb0.
eapply (@rel_dec_correct _ _ _ rc) in Heqb.
symmetry in Heqb.
eapply (@rel_dec_correct _ _ _ rc) in Heqb.
congruence. }
{ symmetry in Heqb; symmetry in Heqb0.
eapply (@rel_dec_correct _ _ _ rc) in Heqb0.
symmetry in Heqb0.
eapply (@rel_dec_correct _ _ _ rc) in Heqb0.
congruence. }
Qed.
End lemmas.
Section RelDec_from_dec.
Context {T} (R : T -> T -> Prop).
Variable (f : forall a b : T, {R a b} + {~R a b}).
Definition RelDec_from_dec
: RelDec R :=
{| rel_dec := fun a b =>
match f a b with
| left _ => true
| right _ => false
end |}.
Global Instance RelDec_Correct_eq_typ : RelDec_Correct RelDec_from_dec.
Proof.
constructor.
intros.
unfold rel_dec; simpl.
destruct (f x y).
- tauto.
- split.
+ inversion 1.
+ intro. apply n in H. tauto.
Qed.
End RelDec_from_dec.
(*
Section SumEq.
Variable T : Type.
Variable U : Type.
Variable EDT : RelDec (@eq T).
Variable EDU : RelDec (@eq U).
(** Specialization for equality **)
Global Instance RelDec_eq_sum : RelDec (@eq (T + U)) :=
{ rel_dec := fun x y =>
match x , y with
| inl x , inl y => eq_dec x y
| inr x , inr y => eq_dec x y
| _ , _ => false
end }.
Variable EDCT : RelDec_Correct EDT.
Variable EDCU : RelDec_Correct EDU.
Global Instance RelDec_Correct_eq_sum : RelDec_Correct RelDec_eq_sum.
Proof.
constructor; destruct x; destruct y; split; simpl in *; intros; try congruence;
f_equal; try match goal with
| [ H : context [ eq_dec ?X ?Y ] |- _ ] =>
consider (eq_dec X Y)
| [ |- context [ eq_dec ?X ?Y ] ] =>
consider (eq_dec X Y)
end; auto; congruence.
Qed.
End SumEq.
*)
|
