decidable.v 8.98 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
6
From iris.prelude Require Export proof_irrel.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13

Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.

Lemma dec_stable `{Decision P} : ¬¬P  P.
Proof. firstorder. Qed.

Lemma Is_true_reflect (b : bool) : reflect b b.
14
Proof. destruct b. left; constructor. right. intros []. Qed.
15
Instance: Inj (=) () Is_true.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
21
22
23
24
25
26
Proof. intros [] []; simpl; intuition. Qed.

(** We introduce [decide_rel] to avoid inefficienct computation due to eager
evaluation of propositions by [vm_compute]. This inefficiency occurs if
[(x = y) := (f x = f y)] as [decide (x = y)] evaluates to [decide (f x = f y)]
which then might lead to evaluation of [f x] and [f y]. Using [decide_rel]
we hide [f] under a lambda abstraction to avoid this unnecessary evaluation. *)
Definition decide_rel {A B} (R : A  B  Prop) {dec :  x y, Decision (R x y)}
  (x : A) (y : B) : Decision (R x y) := dec x y.
Lemma decide_rel_correct {A B} (R : A  B  Prop) `{ x y, Decision (R x y)}
  (x : A) (y : B) : decide_rel R x y = decide (R x y).
27
Proof. reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30

Lemma decide_True {A} `{Decision P} (x y : A) :
  P  (if decide P then x else y) = x.
31
Proof. destruct (decide P); tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
Lemma decide_False {A} `{Decision P} (x y : A) :
  ¬P  (if decide P then x else y) = y.
34
Proof. destruct (decide P); tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
  (P  Q)  (if decide P then x else y) = (if decide Q then x else y).
37
Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

Ralf Jung's avatar
Ralf Jung committed
39
40
41
42
43
Lemma decide_left`{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Proof. destruct (decide P) as [?|?]; [|contradiction]. f_equal. apply proof_irrel. Qed.
Lemma decide_right`{Decision P} `{!ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
Proof. destruct (decide P) as [?|?]; [contradiction|]. f_equal. apply proof_irrel. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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
(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
components is double negated, it will try to remove the double negation. *)
Tactic Notation "destruct_decide" constr(dec) "as" ident(H) :=
  destruct dec as [H|H];
  try match type of H with
  | ¬¬_ => apply dec_stable in H
  end.
Tactic Notation "destruct_decide" constr(dec) :=
  let H := fresh in destruct_decide dec as H.

(** The tactic [case_decide] performs case analysis on an arbitrary occurrence
of [decide] or [decide_rel] in the conclusion or hypotheses. *)
Tactic Notation "case_decide" "as" ident(Hd) :=
  match goal with
  | H : context [@decide ?P ?dec] |- _ =>
    destruct_decide (@decide P dec) as Hd
  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
    destruct_decide (@decide_rel _ _ R x y dec) as Hd
  | |- context [@decide ?P ?dec] =>
    destruct_decide (@decide P dec) as Hd
  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
    destruct_decide (@decide_rel _ _ R x y dec) as Hd
  end.
Tactic Notation "case_decide" :=
  let H := fresh in case_decide as H.

(** The tactic [solve_decision] uses Coq's [decide equality] tactic together
with instance resolution to automatically generate decision procedures. *)
Ltac solve_trivial_decision :=
  match goal with
  | |- Decision (?P) => apply _
  | |- sumbool ?P (¬?P) => change (Decision P); apply _
  end.
Ltac solve_decision := intros; first
  [ solve_trivial_decision
  | unfold Decision; decide equality; solve_trivial_decision ].

(** The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)
Notation swap_if S := (match S with left H => right H | right H => left H end).
Notation cast_if S := (if S then left _ else right _).
Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
Notation cast_if_and4 S1 S2 S3 S4 :=
  (if S1 then cast_if_and3 S2 S3 S4 else right _).
Notation cast_if_and5 S1 S2 S3 S4 S5 :=
  (if S1 then cast_if_and4 S2 S3 S4 S5 else right _).
Notation cast_if_and6 S1 S2 S3 S4 S5 S6 :=
  (if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _).
Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
Notation cast_if_not S := (if S then right _ else left _).

(** We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
  if dec then true else false.

Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
103
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
109
110
111
112
113
114
115

Tactic Notation "case_bool_decide" "as" ident (Hd) :=
  match goal with
  | H : context [@bool_decide ?P ?dec] |- _ =>
    destruct_decide (@bool_decide_reflect P dec) as Hd
  | |- context [@bool_decide ?P ?dec] =>
    destruct_decide (@bool_decide_reflect P dec) as Hd
  end.
Tactic Notation "case_bool_decide" :=
  let H := fresh in case_bool_decide as H.

Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P  P.
116
Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P  P.
118
Proof. rewrite bool_decide_spec; trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P  bool_decide P.
120
Proof. rewrite bool_decide_spec; trivial. Qed.
121
Hint Resolve bool_decide_pack.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Lemma bool_decide_true (P : Prop) `{Decision P} : P  bool_decide P = true.
123
Proof. case_bool_decide; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P  bool_decide P = false.
125
Proof. case_bool_decide; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
  (P  Q)  bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed.

(** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we
propositions we define the type [dsig P] whose Leibniz equality is proof
irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *)
Definition dsig `(P : A  Prop) `{ x : A, Decision (P x)} :=
  { x | bool_decide (P x) }.

Definition proj2_dsig `{ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
  bool_decide_unpack _ (proj2_sig x).
Definition dexist `{ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
  xbool_decide_pack _ p.
Lemma dsig_eq `(P : A  Prop) `{ x, Decision (P x)}
  (x y : dsig P) : x = y  `x = `y.
Proof. apply (sig_eq_pi _). Qed.
Lemma dexists_proj1 `(P : A  Prop) `{ x, Decision (P x)} (x : dsig P) p :
  dexist (`x) p = x.
147
Proof. apply dsig_eq; reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
151
152
153

(** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *)
Instance True_dec: Decision True := left I.
Instance False_dec: Decision False := right (False_rect False).
Instance Is_true_dec b : Decision (Is_true b).
154
Proof. destruct b; simpl; apply _. Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171

Section prop_dec.
  Context `(P_dec : Decision P) `(Q_dec : Decision Q).

  Global Instance not_dec: Decision (¬P).
  Proof. refine (cast_if_not P_dec); intuition. Defined.
  Global Instance and_dec: Decision (P  Q).
  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
  Global Instance or_dec: Decision (P  Q).
  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
  Global Instance impl_dec: Decision (P  Q).
  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
End prop_dec.
Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
  Decision (P  Q) := and_dec _ _.

(** Instances of [Decision] for common data types. *)
172
Instance bool_eq_dec : EqDecision bool.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
Proof. solve_decision. Defined.
174
Instance unit_eq_dec : EqDecision unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
Proof. solve_decision. Defined.
176
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Robbert Krebbers's avatar
Robbert Krebbers committed
177
Proof. solve_decision. Defined.
178
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
181
182
183
184
185
186
Proof. solve_decision. Defined.

Instance curry_dec `(P_dec :  (x : A) (y : B), Decision (P x y)) p :
    Decision (curry P p) :=
  match p as p return Decision (curry P p) with
  | (x,y) => P_dec x y
  end.

187
188
189
190
191
Instance sig_eq_dec `(P : A  Prop) `{ x, ProofIrrel (P x), EqDecision A} :
  EqDecision (sig P).
Proof.
 refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
195
196
197
198
199
200
201

(** Some laws for decidable propositions *)
Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P  Q)  ¬P  ¬Q.
Proof. destruct (decide P); tauto. Qed.
Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P  Q)  ¬P  ¬Q.
Proof. destruct (decide Q); tauto. Qed.
Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P  Q)  ¬P  (¬Q  P).
Proof. destruct (decide P); tauto. Qed.
Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P  Q)  (¬P  Q)  ¬Q.
Proof. destruct (decide Q); tauto. Qed.