decidable.v 8.81 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 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185

(** * 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).
Proof. destruct b; apply _. Defined.

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. *)
Instance bool_eq_dec (x y : bool) : Decision (x = y).
Proof. solve_decision. Defined.
Instance unit_eq_dec (x y : unit) : Decision (x = y).
Proof. solve_decision. Defined.
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).
Proof. solve_decision. Defined.
Instance sum_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).
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.

Instance sig_eq_dec `(P : A  Prop) `{ x, ProofIrrel (P x)}
  `{ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
186
Proof. refine (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.