decidable.v 9.17 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
2 3 4 5
(* 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 stdpp Require Export proof_irrel.
7
Set Default Proof Using "Type*".
8

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.

11 12
Lemma dec_stable `{Decision P} : ¬¬P  P.
Proof. firstorder. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14
Lemma Is_true_reflect (b : bool) : reflect b b.
15
Proof. destruct b. left; constructor. right. intros []. Qed.
16
Instance: Inj (=) () Is_true.
17
Proof. intros [] []; simpl; intuition. Qed.
18

19 20 21 22 23 24 25 26 27
(** 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).
28
Proof. reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

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

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

45 46
(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
components is double negated, it will try to remove the double negation. *)
47
Tactic Notation "destruct_decide" constr(dec) "as" ident(H) :=
48 49 50 51
  destruct dec as [H|H];
  try match type of H with
  | ¬¬_ => apply dec_stable in H
  end.
52 53
Tactic Notation "destruct_decide" constr(dec) :=
  let H := fresh in destruct_decide dec as H.
54

55
(** The tactic [case_decide] performs case analysis on an arbitrary occurrence
56
of [decide] or [decide_rel] in the conclusion or hypotheses. *)
57
Tactic Notation "case_decide" "as" ident(Hd) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  match goal with
59
  | H : context [@decide ?P ?dec] |- _ =>
60
    destruct_decide (@decide P dec) as Hd
61
  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
62
    destruct_decide (@decide_rel _ _ R x y dec) as Hd
63
  | |- context [@decide ?P ?dec] =>
64
    destruct_decide (@decide P dec) as Hd
65
  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
66
    destruct_decide (@decide_rel _ _ R x y dec) as Hd
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  end.
68 69
Tactic Notation "case_decide" :=
  let H := fresh in case_decide as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
70

71 72
(** The tactic [solve_decision] uses Coq's [decide equality] tactic together
with instance resolution to automatically generate decision procedures. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74
Ltac solve_trivial_decision :=
  match goal with
75 76
  | |- Decision (?P) => apply _
  | |- sumbool ?P (¬?P) => change (Decision P); apply _
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  end.
78 79 80
Ltac solve_decision := intros; first
  [ solve_trivial_decision
  | unfold Decision; decide equality; solve_trivial_decision ].
Robbert Krebbers's avatar
Robbert Krebbers committed
81

82 83
(** The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)
84
Notation swap_if S := (match S with left H => right H | right H => left H end).
85 86 87 88 89
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 _).
90 91
Notation cast_if_and5 S1 S2 S3 S4 S5 :=
  (if S1 then cast_if_and4 S2 S3 S4 S5 else right _).
92 93
Notation cast_if_and6 S1 S2 S3 S4 S5 S6 :=
  (if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _).
94
Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
95
Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
96 97 98
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 _).

99 100 101
(** We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
  if dec then true else false.
Robbert Krebbers's avatar
Robbert Krebbers committed
102

103
Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
104
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
105

106
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
107 108
  match goal with
  | H : context [@bool_decide ?P ?dec] |- _ =>
109
    destruct_decide (@bool_decide_reflect P dec) as Hd
110
  | |- context [@bool_decide ?P ?dec] =>
111
    destruct_decide (@bool_decide_reflect P dec) as Hd
112
  end.
113 114
Tactic Notation "case_bool_decide" :=
  let H := fresh in case_bool_decide as H.
115

116
Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P  P.
117
Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
118
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P  P.
119
Proof. rewrite bool_decide_spec; trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P  bool_decide P.
121
Proof. rewrite bool_decide_spec; trivial. Qed.
122
Hint Resolve bool_decide_pack.
123
Lemma bool_decide_true (P : Prop) `{Decision P} : P  bool_decide P = true.
124
Proof. case_bool_decide; tauto. Qed.
125
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P  bool_decide P = false.
126
Proof. case_bool_decide; tauto. Qed.
127 128 129
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
130

131 132 133 134
(** * 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
Robbert Krebbers's avatar
Robbert Krebbers committed
135
irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *)
136 137
Definition dsig `(P : A  Prop) `{ x : A, Decision (P x)} :=
  { x | bool_decide (P x) }.
138

139 140 141 142
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.
143
Lemma dsig_eq `(P : A  Prop) `{ x, Decision (P x)}
144
  (x y : dsig P) : x = y  `x = `y.
145
Proof. apply (sig_eq_pi _). Qed.
146 147
Lemma dexists_proj1 `(P : A  Prop) `{ x, Decision (P x)} (x : dsig P) p :
  dexist (`x) p = x.
148
Proof. apply dsig_eq; reflexivity. Qed.
149 150 151

(** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *)
152 153
Instance True_dec: Decision True := left I.
Instance False_dec: Decision False := right (False_rect False).
154
Instance Is_true_dec b : Decision (Is_true b).
155
Proof. destruct b; simpl; apply _. Defined.
156 157 158 159

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

160 161
  Global Instance not_dec: Decision (¬P).
  Proof. refine (cast_if_not P_dec); intuition. Defined.
162
  Global Instance and_dec: Decision (P  Q).
163
  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
164
  Global Instance or_dec: Decision (P  Q).
165
  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
166
  Global Instance impl_dec: Decision (P  Q).
167
  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
168
End prop_dec.
169 170
Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
  Decision (P  Q) := and_dec _ _.
171 172

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

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 192
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.
193 194

(** Some laws for decidable propositions *)
195 196 197 198 199
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).
200
Proof. destruct (decide P); tauto. Qed.
201
Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P  Q)  (¬P  Q)  ¬Q.
202
Proof. destruct (decide Q); tauto. Qed.
Hai Dang's avatar
Hai Dang committed
203

204 205 206
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B  A)
  `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.