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
|
Require Import
MathClasses.interfaces.canonical_names MathClasses.misc.util.
Require Bool.
Class Decision P := decide: sumbool P (¬P).
Arguments decide _ {Decision}.
#[global]
Instance: ∀ P, Decision P → Stable P.
Proof. firstorder. Qed.
Ltac case_decide := match goal with
| H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in *
| |- context [@decide ?P ?dec] => case (@decide P dec) in *
end.
Ltac solve_trivial_decision :=
match goal with
| [ |- Decision (?P) ] => apply _
| [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
end.
Ltac solve_decision :=
first [solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision].
(* We cannot state this as Proper (iff ==> iffT) Decision due to the lack of setoid rewriting in Type *)
Program Definition decision_proper (P Q : Prop) (PiffQ : P ↔ Q) (P_dec : Decision P) : Decision Q :=
match P_dec with
| left _ => left _
| right _ => right _
end.
Solve Obligations with (program_simpl; tauto).
Definition bool_decide (P : Prop) `{dec : !Decision P} : bool := if dec then true else false.
Lemma bool_decide_true `{dec : Decision P} : bool_decide P ≡ true ↔ P.
Proof. unfold bool_decide. split; intro; destruct dec; firstorder with bool. Qed.
Lemma bool_decide_false `{dec : !Decision P} : bool_decide P ≡ false ↔ ¬P.
Proof. unfold bool_decide. split; intro; destruct dec; firstorder with bool. Qed.
(*
Because [vm_compute] evaluates terms in [Prop] eagerly and does not remove dead code we
need the decide_rel hack. Suppose we have [(x = y) =def (f x = f y)], now:
bool_decide (x = y) → bool_decide (f x = f y) → ...
As we see, the dead code [f x] and [f y] is actually evaluated, which is of course an utter waste.
Therefore we introduce decide_rel and bool_decide_rel.
bool_decide_rel (=) x y → bool_decide_rel (λ a b, f a = f b) x y → ...
Now the definition of equality remains under a lambda and our problem does not occur anymore!
*)
Definition decide_rel `(R : A → B → Prop) {dec : ∀ x y, Decision (R x y)} (x : A) (y : B) : Decision (R x y)
:= dec x y.
Definition bool_decide_rel `(R : relation A) {dec : ∀ x y, Decision (R x y)} : A → A → bool
:= λ x y, if dec x y then true else false.
Lemma bool_decide_rel_true `(R : relation A) {dec : ∀ x y, Decision (R x y)} :
∀ x y, bool_decide_rel R x y ≡ true ↔ R x y.
Proof. unfold bool_decide_rel. split; intro; destruct dec; firstorder with bool. Qed.
Lemma bool_decide_rel_false `(R : relation A)`{dec : ∀ x y, Decision (R x y)} :
∀ x y, bool_decide_rel R x y ≡ false ↔ ¬R x y.
Proof. unfold bool_decide_rel. split; intro; destruct dec; firstorder with bool. Qed.
Program Definition decision_from_bool_decide {P b} (prf : b ≡ true ↔ P) :
Decision P := match b with true => left _ | false => right _ end.
Next Obligation. now apply prf. Qed.
Next Obligation. rewrite <-prf. discriminate. Qed.
#[global]
Program Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x ≡ y))
`(B_dec : ∀ x y : B, Decision (x ≡ y)) : ∀ x y : A * B, Decision (x ≡ y) := λ x y,
match A_dec (fst x) (fst y) with
| left _ => match B_dec (snd x) (snd y) with left _ => left _ | right _ => right _ end
| right _ => right _
end.
Solve Obligations with (program_simpl; f_equal; firstorder).
#[global]
Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∧ Q) :=
match P_dec with
| left _ => match Q_dec with left _ => left _ | right _ => right _ end
| right _ => right _
end.
Solve Obligations with (program_simpl; tauto).
#[global]
Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∨ Q) :=
match P_dec with
| left _ => left _
| right _ => match Q_dec with left _ => left _ | right _ => right _ end
end.
Solve Obligations with (program_simpl; firstorder).
#[global]
Program Instance is_Some_dec `(x : option A) : Decision (is_Some x) :=
match x with
| None => right _
| Some _ => left _
end.
#[global]
Program Instance is_None_dec `(x : option A) : Decision (is_None x) :=
match x with
| None => left _
| Some _ => right _
end.
#[global]
Program Instance option_eq_dec `(A_dec : ∀ x y : A, Decision (x ≡ y))
: ∀ x y : option A, Decision (x ≡ y) := λ x y,
match x with
| Some r =>
match y with
| Some s => match A_dec r s with left _ => left _ | right _ => right _ end
| None => right _
end
| None =>
match y with
| Some s => right _
| None => left _
end
end.
#[global]
Program Instance True_dec: Decision True := left _.
#[global]
Program Instance False_dec: Decision False := right _.
|
