decidable.v 8.64 KB
 Robbert Krebbers committed Nov 11, 2015 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. *) `````` Robbert Krebbers committed Mar 10, 2016 6 ``````From iris.prelude Require Export proof_irrel. `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Mar 03, 2016 14 ``````Proof. destruct b. left; constructor. right. intros []. Qed. `````` Robbert Krebbers committed Feb 11, 2016 15 ``````Instance: Inj (=) (↔) Is_true. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Robbert Krebbers committed Mar 03, 2016 27 ``````Proof. reflexivity. Qed. `````` Robbert Krebbers committed Nov 11, 2015 28 29 30 `````` Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x. `````` Robbert Krebbers committed Mar 03, 2016 31 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 32 33 ``````Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y. `````` Robbert Krebbers committed Mar 03, 2016 34 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Robbert Krebbers committed Mar 03, 2016 37 ``````Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Robbert Krebbers committed Mar 03, 2016 98 ``````Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Mar 03, 2016 111 ``````Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 112 ``````Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. `````` Robbert Krebbers committed Mar 03, 2016 113 ``````Proof. rewrite bool_decide_spec; trivial. Qed. `````` Robbert Krebbers committed Nov 11, 2015 114 ``````Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. `````` Robbert Krebbers committed Mar 03, 2016 115 ``````Proof. rewrite bool_decide_spec; trivial. Qed. `````` Robbert Krebbers committed Apr 07, 2016 116 ``````Hint Resolve bool_decide_pack. `````` Robbert Krebbers committed Nov 11, 2015 117 ``````Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true. `````` Robbert Krebbers committed Mar 03, 2016 118 ``````Proof. case_bool_decide; tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 119 ``````Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false. `````` Robbert Krebbers committed Mar 03, 2016 120 ``````Proof. case_bool_decide; tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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 := x↾bool_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. `````` Robbert Krebbers committed Mar 03, 2016 142 ``````Proof. apply dsig_eq; reflexivity. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Jacques-Henri Jourdan committed Sep 14, 2016 149 ``````Proof. destruct b; simpl; apply _. Defined. `````` Robbert Krebbers committed Nov 11, 2015 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. *) `````` Robbert Krebbers committed Sep 20, 2016 167 ``````Instance bool_eq_dec : EqDecision bool. `````` Robbert Krebbers committed Nov 11, 2015 168 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 169 ``````Instance unit_eq_dec : EqDecision unit. `````` Robbert Krebbers committed Nov 11, 2015 170 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 171 ``````Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B). `````` Robbert Krebbers committed Nov 11, 2015 172 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 173 ``````Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B). `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Sep 20, 2016 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 committed Nov 11, 2015 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.``````