decidable.v 8.64 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
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

(** 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).
98
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
105
106
107
108
109
110

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.
111
Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P  P.
113
Proof. rewrite bool_decide_spec; trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P  bool_decide P.
115
Proof. rewrite bool_decide_spec; trivial. Qed.
116
Hint Resolve bool_decide_pack.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Lemma bool_decide_true (P : Prop) `{Decision P} : P  bool_decide P = true.
118
Proof. case_bool_decide; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P  bool_decide P = false.
120
Proof. case_bool_decide; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
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.
142
Proof. apply dsig_eq; reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
146
147
148

(** * 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).
149
Proof. destruct b; simpl; apply _. Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166

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. *)
167
Instance bool_eq_dec : EqDecision bool.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Proof. solve_decision. Defined.
169
Instance unit_eq_dec : EqDecision unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Proof. solve_decision. Defined.
171
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Proof. solve_decision. Defined.
173
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
176
177
178
179
180
181
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.

182
183
184
185
186
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
187
188
189
190
191
192
193
194
195
196

(** 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.