decidable.v 9.01 KB
 Robbert Krebbers committed Jan 24, 2017 1 ``````(* Copyright (c) 2012-2017, Robbert Krebbers. *) `````` Robbert Krebbers committed Nov 11, 2015 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. *) `````` Robbert Krebbers committed Mar 10, 2016 6 ``````From iris.prelude Require Export proof_irrel. `````` Ralf Jung committed Jan 03, 2017 7 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Mar 03, 2016 15 ``````Proof. destruct b. left; constructor. right. intros []. Qed. `````` Robbert Krebbers committed Feb 11, 2016 16 ``````Instance: Inj (=) (↔) Is_true. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Robbert Krebbers committed Mar 03, 2016 28 ``````Proof. reflexivity. Qed. `````` Robbert Krebbers committed Nov 11, 2015 29 30 31 `````` Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x. `````` Robbert Krebbers committed Mar 03, 2016 32 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 33 34 ``````Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y. `````` Robbert Krebbers committed Mar 03, 2016 35 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Robbert Krebbers committed Mar 03, 2016 38 ``````Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 39 `````` `````` Ralf Jung committed Dec 19, 2016 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 committed Nov 11, 2015 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). `````` Robbert Krebbers committed Mar 03, 2016 104 ``````Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Mar 03, 2016 117 ``````Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 118 ``````Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. `````` Robbert Krebbers committed Mar 03, 2016 119 ``````Proof. rewrite bool_decide_spec; trivial. Qed. `````` Robbert Krebbers committed Nov 11, 2015 120 ``````Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. `````` Robbert Krebbers committed Mar 03, 2016 121 ``````Proof. rewrite bool_decide_spec; trivial. Qed. `````` Robbert Krebbers committed Apr 07, 2016 122 ``````Hint Resolve bool_decide_pack. `````` Robbert Krebbers committed Nov 11, 2015 123 ``````Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true. `````` Robbert Krebbers committed Mar 03, 2016 124 ``````Proof. case_bool_decide; tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 125 ``````Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false. `````` Robbert Krebbers committed Mar 03, 2016 126 ``````Proof. case_bool_decide; tauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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 := 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 148 ``````Proof. apply dsig_eq; reflexivity. Qed. `````` Robbert Krebbers committed Nov 11, 2015 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). `````` Jacques-Henri Jourdan committed Sep 14, 2016 155 ``````Proof. destruct b; simpl; apply _. Defined. `````` Robbert Krebbers committed Nov 11, 2015 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. *) `````` Robbert Krebbers committed Sep 20, 2016 173 ``````Instance bool_eq_dec : EqDecision bool. `````` Robbert Krebbers committed Nov 11, 2015 174 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 175 ``````Instance unit_eq_dec : EqDecision unit. `````` Robbert Krebbers committed Nov 11, 2015 176 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 177 ``````Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B). `````` Robbert Krebbers committed Nov 11, 2015 178 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 179 ``````Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B). `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Sep 20, 2016 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 committed Nov 11, 2015 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.``````