decidable.v 9.01 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.
7
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11 12 13 14

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.
15
Proof. destruct b. left; constructor. right. intros []. Qed.
16
Instance: Inj (=) () Is_true.
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18 19 20 21 22 23 24 25 26 27
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).
28
Proof. reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31

Lemma decide_True {A} `{Decision P} (x y : A) :
  P  (if decide P then x else y) = x.
32
Proof. destruct (decide P); tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
Lemma decide_False {A} `{Decision P} (x y : A) :
  ¬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.
Robbert Krebbers's avatar
Robbert Krebbers committed
39

40 41 42 43 44
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
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
(** 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).
104
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107 108 109 110 111 112 113 114 115 116

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.
117
Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Lemma bool_decide_true (P : Prop) `{Decision P} : P  bool_decide P = true.
124
Proof. case_bool_decide; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P  bool_decide P = false.
126
Proof. case_bool_decide; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
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.
148
Proof. apply dsig_eq; reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150 151 152 153 154

(** * 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).
155
Proof. destruct b; simpl; apply _. Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172

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. *)
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Proof. solve_decision. Defined.
177
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Proof. solve_decision. Defined.
179
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182 183 184 185 186 187
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.

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197 198 199 200 201 202

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