decidable.v 9.94 KB
 Robbert Krebbers committed Jan 29, 2019 1 ``````(* Copyright (c) 2012-2019, Coq-std++ developers. *) `````` Robbert Krebbers committed Aug 29, 2012 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 Feb 13, 2016 6 ``````From stdpp Require Export proof_irrel. `````` Ralf Jung committed Jan 31, 2017 7 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Oct 19, 2012 8 9 10 `````` Lemma dec_stable `{Decision P} : ¬¬P → P. Proof. firstorder. Qed. `````` Robbert Krebbers committed Jun 11, 2012 11 `````` `````` Robbert Krebbers committed Feb 19, 2013 12 ``````Lemma Is_true_reflect (b : bool) : reflect b b. `````` Robbert Krebbers committed Mar 03, 2016 13 ``````Proof. destruct b. left; constructor. right. intros []. Qed. `````` Robbert Krebbers committed Feb 11, 2016 14 ``````Instance: Inj (=) (↔) Is_true. `````` 15 ``````Proof. intros [] []; simpl; intuition. Qed. `````` Robbert Krebbers committed Feb 19, 2013 16 `````` `````` Robbert Krebbers committed Jun 24, 2013 17 ``````Lemma decide_True {A} `{Decision P} (x y : A) : `````` Robbert Krebbers committed Mar 14, 2013 18 `````` P → (if decide P then x else y) = x. `````` Robbert Krebbers committed Mar 03, 2016 19 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed Jun 24, 2013 20 ``````Lemma decide_False {A} `{Decision P} (x y : A) : `````` Robbert Krebbers committed Mar 14, 2013 21 `````` ¬P → (if decide P then x else y) = y. `````` Robbert Krebbers committed Mar 03, 2016 22 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed May 22, 2014 23 24 ``````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 25 ``````Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed. `````` Robbert Krebbers committed Mar 14, 2013 26 `````` `````` Robbert Krebbers committed May 30, 2017 27 28 29 30 ``````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 committed Jan 31, 2017 31 `````` `````` Robbert Krebbers committed Feb 19, 2013 32 33 ``````(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the components is double negated, it will try to remove the double negation. *) `````` Robbert Krebbers committed Mar 14, 2013 34 ``````Tactic Notation "destruct_decide" constr(dec) "as" ident(H) := `````` Robbert Krebbers committed Feb 19, 2013 35 36 37 38 `````` destruct dec as [H|H]; try match type of H with | ¬¬_ => apply dec_stable in H end. `````` Robbert Krebbers committed Mar 14, 2013 39 40 ``````Tactic Notation "destruct_decide" constr(dec) := let H := fresh in destruct_decide dec as H. `````` Robbert Krebbers committed Feb 19, 2013 41 `````` `````` Robbert Krebbers committed Aug 29, 2012 42 ``````(** The tactic [case_decide] performs case analysis on an arbitrary occurrence `````` Robbert Krebbers committed Oct 19, 2012 43 ``````of [decide] or [decide_rel] in the conclusion or hypotheses. *) `````` Robbert Krebbers committed Mar 14, 2013 44 ``````Tactic Notation "case_decide" "as" ident(Hd) := `````` Robbert Krebbers committed Jun 11, 2012 45 `````` match goal with `````` Robbert Krebbers committed Aug 29, 2012 46 `````` | H : context [@decide ?P ?dec] |- _ => `````` Robbert Krebbers committed Mar 14, 2013 47 `````` destruct_decide (@decide P dec) as Hd `````` Robbert Krebbers committed Aug 21, 2012 48 `````` | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => `````` Robbert Krebbers committed Mar 14, 2013 49 `````` destruct_decide (@decide_rel _ _ R x y dec) as Hd `````` Robbert Krebbers committed Aug 29, 2012 50 `````` | |- context [@decide ?P ?dec] => `````` Robbert Krebbers committed Mar 14, 2013 51 `````` destruct_decide (@decide P dec) as Hd `````` Robbert Krebbers committed Aug 21, 2012 52 `````` | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => `````` Robbert Krebbers committed Mar 14, 2013 53 `````` destruct_decide (@decide_rel _ _ R x y dec) as Hd `````` Robbert Krebbers committed Jun 11, 2012 54 `````` end. `````` Robbert Krebbers committed Mar 14, 2013 55 56 ``````Tactic Notation "case_decide" := let H := fresh in case_decide as H. `````` Robbert Krebbers committed Jun 11, 2012 57 `````` `````` Robbert Krebbers committed Aug 29, 2012 58 59 ``````(** The tactic [solve_decision] uses Coq's [decide equality] tactic together with instance resolution to automatically generate decision procedures. *) `````` Robbert Krebbers committed Jun 11, 2012 60 61 ``````Ltac solve_trivial_decision := match goal with `````` Robbert Krebbers committed Oct 19, 2012 62 63 `````` | |- Decision (?P) => apply _ | |- sumbool ?P (¬?P) => change (Decision P); apply _ `````` Robbert Krebbers committed Jun 11, 2012 64 `````` end. `````` 65 66 67 68 ``````Ltac solve_decision := unfold EqDecision; intros; first [ solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision ]. `````` Robbert Krebbers committed Jun 11, 2012 69 `````` `````` Robbert Krebbers committed Feb 01, 2013 70 71 ``````(** The following combinators are useful to create Decision proofs in combination with the [refine] tactic. *) `````` Robbert Krebbers committed May 02, 2014 72 ``````Notation swap_if S := (match S with left H => right H | right H => left H end). `````` Robbert Krebbers committed Feb 01, 2013 73 74 75 76 77 ``````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 _). `````` Robbert Krebbers committed May 21, 2013 78 79 ``````Notation cast_if_and5 S1 S2 S3 S4 S5 := (if S1 then cast_if_and4 S2 S3 S4 S5 else right _). `````` Robbert Krebbers committed May 02, 2014 80 81 ``````Notation cast_if_and6 S1 S2 S3 S4 S5 S6 := (if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _). `````` Robbert Krebbers committed Feb 01, 2013 82 ``````Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2). `````` Robbert Krebbers committed May 07, 2013 83 ``````Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3). `````` Robbert Krebbers committed Feb 01, 2013 84 85 86 ``````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 _). `````` Robbert Krebbers committed Aug 29, 2012 87 88 89 ``````(** We can convert decidable propositions to booleans. *) Definition bool_decide (P : Prop) {dec : Decision P} : bool := if dec then true else false. `````` Robbert Krebbers committed Jun 11, 2012 90 `````` `````` Robbert Krebbers committed Feb 19, 2013 91 ``````Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P). `````` Robbert Krebbers committed Mar 03, 2016 92 ``````Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed. `````` Robbert Krebbers committed Feb 19, 2013 93 `````` `````` Ralf Jung committed Jun 18, 2019 94 95 96 ``````Lemma bool_decide_decide P `{!Decision P} : bool_decide P = if decide P then true else false. Proof. reflexivity. Qed. `````` Ralf Jung committed Jul 13, 2019 97 98 99 ``````Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X): (if decide P then x1 else x2) = (if bool_decide P then x1 else x2). Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed. `````` Ralf Jung committed Jun 18, 2019 100 `````` `````` Robbert Krebbers committed May 21, 2013 101 ``````Tactic Notation "case_bool_decide" "as" ident (Hd) := `````` Robbert Krebbers committed Feb 19, 2013 102 103 `````` match goal with | H : context [@bool_decide ?P ?dec] |- _ => `````` Robbert Krebbers committed May 21, 2013 104 `````` destruct_decide (@bool_decide_reflect P dec) as Hd `````` Robbert Krebbers committed Feb 19, 2013 105 `````` | |- context [@bool_decide ?P ?dec] => `````` Robbert Krebbers committed May 21, 2013 106 `````` destruct_decide (@bool_decide_reflect P dec) as Hd `````` Robbert Krebbers committed Feb 19, 2013 107 `````` end. `````` Robbert Krebbers committed May 21, 2013 108 109 ``````Tactic Notation "case_bool_decide" := let H := fresh in case_bool_decide as H. `````` Robbert Krebbers committed Feb 19, 2013 110 `````` `````` 111 ``````Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P ↔ P. `````` Robbert Krebbers committed Mar 03, 2016 112 ``````Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed. `````` 113 ``````Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. `````` Robbert Krebbers committed Mar 03, 2016 114 ``````Proof. rewrite bool_decide_spec; trivial. Qed. `````` Robbert Krebbers committed Jun 11, 2012 115 ``````Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. `````` Robbert Krebbers committed Mar 03, 2016 116 ``````Proof. rewrite bool_decide_spec; trivial. Qed. `````` Tej Chajed committed Nov 28, 2018 117 ``````Hint Resolve bool_decide_pack : core. `````` Ralf Jung committed Jun 30, 2019 118 119 120 121 122 `````` Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P. Proof. case_bool_decide; intuition discriminate. Qed. Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P. Proof. case_bool_decide; intuition discriminate. Qed. `````` Robbert Krebbers committed Dec 23, 2014 123 124 125 ``````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 committed Jun 11, 2012 126 `````` `````` Ralf Jung committed Jun 30, 2019 127 128 129 130 131 132 133 134 135 136 137 138 139 140 ``````Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P. Proof. apply bool_decide_eq_true. Qed. Lemma bool_decide_eq_true_2 P `{!Decision P}: P → bool_decide P = true. Proof. apply bool_decide_eq_true. Qed. Lemma bool_decide_eq_false_1 P `{!Decision P}: bool_decide P = false → ¬P. Proof. apply bool_decide_eq_false. Qed. Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false. Proof. apply bool_decide_eq_false. Qed. (** Backwards compatibility notations. *) Notation bool_decide_true := bool_decide_eq_true_2. Notation bool_decide_false := bool_decide_eq_false_2. `````` Robbert Krebbers committed Aug 29, 2012 141 142 143 144 ``````(** * 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 committed Feb 01, 2017 145 ``````irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *) `````` Robbert Krebbers committed Aug 21, 2012 146 147 ``````Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} := { x | bool_decide (P x) }. `````` Robbert Krebbers committed Feb 19, 2013 148 `````` `````` Robbert Krebbers committed Aug 21, 2012 149 150 151 152 ``````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. `````` Robbert Krebbers committed Feb 01, 2013 153 ``````Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)} `````` Robbert Krebbers committed Aug 29, 2012 154 `````` (x y : dsig P) : x = y ↔ `x = `y. `````` Robbert Krebbers committed Mar 14, 2013 155 ``````Proof. apply (sig_eq_pi _). Qed. `````` Robbert Krebbers committed Feb 01, 2013 156 157 ``````Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p : dexist (`x) p = x. `````` Robbert Krebbers committed Mar 03, 2016 158 ``````Proof. apply dsig_eq; reflexivity. Qed. `````` Robbert Krebbers committed Aug 29, 2012 159 `````` `````` Robbert Krebbers committed May 10, 2019 160 ``````(** * Instances of [Decision] *) `````` Robbert Krebbers committed Aug 29, 2012 161 ``````(** Instances of [Decision] for operators of propositional logic. *) `````` Robbert Krebbers committed Oct 19, 2012 162 163 ``````Instance True_dec: Decision True := left I. Instance False_dec: Decision False := right (False_rect False). `````` Robbert Krebbers committed May 02, 2014 164 ``````Instance Is_true_dec b : Decision (Is_true b). `````` Jacques-Henri Jourdan committed Sep 14, 2016 165 ``````Proof. destruct b; simpl; apply _. Defined. `````` Robbert Krebbers committed Oct 19, 2012 166 167 168 169 `````` Section prop_dec. Context `(P_dec : Decision P) `(Q_dec : Decision Q). `````` Robbert Krebbers committed Nov 12, 2012 170 171 `````` Global Instance not_dec: Decision (¬P). Proof. refine (cast_if_not P_dec); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 172 `````` Global Instance and_dec: Decision (P ∧ Q). `````` Robbert Krebbers committed Nov 12, 2012 173 `````` Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 174 `````` Global Instance or_dec: Decision (P ∨ Q). `````` Robbert Krebbers committed Nov 12, 2012 175 `````` Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 176 `````` Global Instance impl_dec: Decision (P → Q). `````` Robbert Krebbers committed Nov 12, 2012 177 `````` Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 178 ``````End prop_dec. `````` Robbert Krebbers committed May 02, 2014 179 180 ``````Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ↔ Q) := and_dec _ _. `````` Robbert Krebbers committed Aug 29, 2012 181 182 `````` (** Instances of [Decision] for common data types. *) `````` Robbert Krebbers committed Sep 20, 2016 183 ``````Instance bool_eq_dec : EqDecision bool. `````` Robbert Krebbers committed Jan 05, 2013 184 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 185 ``````Instance unit_eq_dec : EqDecision unit. `````` Robbert Krebbers committed May 02, 2014 186 ``````Proof. solve_decision. Defined. `````` Ralf Jung committed Aug 26, 2019 187 188 ``````Instance Empty_set_eq_dec : EqDecision Empty_set. Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 189 ``````Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B). `````` Robbert Krebbers committed May 02, 2014 190 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Sep 20, 2016 191 ``````Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B). `````` Robbert Krebbers committed Oct 19, 2012 192 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Jan 05, 2013 193 194 195 196 197 198 `````` 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 Mar 14, 2013 199 `````` `````` Robbert Krebbers committed Sep 20, 2016 200 201 202 203 204 ``````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 Aug 21, 2013 205 206 `````` (** Some laws for decidable propositions *) `````` Robbert Krebbers committed May 02, 2014 207 208 209 210 211 ``````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). `````` Robbert Krebbers committed Aug 21, 2013 212 ``````Proof. destruct (decide P); tauto. Qed. `````` Robbert Krebbers committed May 02, 2014 213 ``````Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q. `````` Robbert Krebbers committed Aug 21, 2013 214 ``````Proof. destruct (decide Q); tauto. Qed. `````` Hai Dang committed Jul 05, 2017 215 `````` `````` Robbert Krebbers committed Aug 02, 2017 216 217 218 ``````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. `````` Robbert Krebbers committed May 10, 2019 219 220 221 222 223 224 225 226 `````` (** * Instances of [RelDecision] *) Definition flip_dec {A} (R : relation A) `{!RelDecision R} : RelDecision (flip R) := λ x y, decide_rel R y x. (** We do not declare this as an actual instance since Coq can unify [flip ?R] with any relation. Coq's standard library is carrying out the same approach for the [Reflexive], [Transitive], etc, instance of [flip]. *) Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.``````