decidable.v 7.31 KB
Newer Older
 Robbert Krebbers committed Feb 19, 2013 1 ``````(* Copyright (c) 2012-2013, Robbert Krebbers. *) `````` 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 Mar 14, 2013 6 ``````Require Export proof_irrel. `````` Robbert Krebbers committed Oct 19, 2012 7 `````` `````` Robbert Krebbers committed Jan 05, 2013 8 9 ``````Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances. `````` Robbert Krebbers committed Oct 19, 2012 10 11 ``````Lemma dec_stable `{Decision P} : ¬¬P → P. Proof. firstorder. Qed. `````` Robbert Krebbers committed Jun 11, 2012 12 `````` `````` Robbert Krebbers committed Feb 19, 2013 13 14 15 ``````Lemma Is_true_reflect (b : bool) : reflect b b. Proof. destruct b. by left. right. intros []. Qed. `````` Robbert Krebbers committed Aug 29, 2012 16 17 18 19 20 21 22 23 24 ``````(** 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 Oct 19, 2012 25 ``````Proof. done. Qed. `````` Robbert Krebbers committed Jun 11, 2012 26 `````` `````` Robbert Krebbers committed Mar 14, 2013 27 28 29 30 31 32 33 ``````Lemma decide_true {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x. Proof. by destruct (decide P). Qed. Lemma decide_false {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y. Proof. by destruct (decide P). Qed. `````` Robbert Krebbers committed Feb 19, 2013 34 35 ``````(** 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 36 ``````Tactic Notation "destruct_decide" constr(dec) "as" ident(H) := `````` Robbert Krebbers committed Feb 19, 2013 37 38 39 40 `````` destruct dec as [H|H]; try match type of H with | ¬¬_ => apply dec_stable in H end. `````` Robbert Krebbers committed Mar 14, 2013 41 42 ``````Tactic Notation "destruct_decide" constr(dec) := let H := fresh in destruct_decide dec as H. `````` Robbert Krebbers committed Feb 19, 2013 43 `````` `````` Robbert Krebbers committed Aug 29, 2012 44 ``````(** The tactic [case_decide] performs case analysis on an arbitrary occurrence `````` Robbert Krebbers committed Oct 19, 2012 45 ``````of [decide] or [decide_rel] in the conclusion or hypotheses. *) `````` Robbert Krebbers committed Mar 14, 2013 46 ``````Tactic Notation "case_decide" "as" ident(Hd) := `````` Robbert Krebbers committed Jun 11, 2012 47 `````` match goal with `````` Robbert Krebbers committed Aug 29, 2012 48 `````` | H : context [@decide ?P ?dec] |- _ => `````` Robbert Krebbers committed Mar 14, 2013 49 `````` destruct_decide (@decide P dec) as Hd `````` Robbert Krebbers committed Aug 21, 2012 50 `````` | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => `````` Robbert Krebbers committed Mar 14, 2013 51 `````` destruct_decide (@decide_rel _ _ R x y dec) as Hd `````` Robbert Krebbers committed Aug 29, 2012 52 `````` | |- context [@decide ?P ?dec] => `````` Robbert Krebbers committed Mar 14, 2013 53 `````` destruct_decide (@decide P dec) as Hd `````` Robbert Krebbers committed Aug 21, 2012 54 `````` | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => `````` Robbert Krebbers committed Mar 14, 2013 55 `````` destruct_decide (@decide_rel _ _ R x y dec) as Hd `````` Robbert Krebbers committed Jun 11, 2012 56 `````` end. `````` Robbert Krebbers committed Mar 14, 2013 57 58 ``````Tactic Notation "case_decide" := let H := fresh in case_decide as H. `````` Robbert Krebbers committed Jun 11, 2012 59 `````` `````` Robbert Krebbers committed Aug 29, 2012 60 61 ``````(** 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 62 63 ``````Ltac solve_trivial_decision := match goal with `````` Robbert Krebbers committed Oct 19, 2012 64 65 `````` | |- Decision (?P) => apply _ | |- sumbool ?P (¬?P) => change (Decision P); apply _ `````` Robbert Krebbers committed Jun 11, 2012 66 `````` end. `````` Robbert Krebbers committed Oct 19, 2012 67 68 69 ``````Ltac solve_decision := intros; first [ solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision ]. `````` Robbert Krebbers committed Jun 11, 2012 70 `````` `````` Robbert Krebbers committed Feb 01, 2013 71 72 73 74 75 76 77 78 ``````(** The following combinators are useful to create Decision proofs in combination with the [refine] tactic. *) 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_or S1 S2 := (if S1 then left _ else cast_if S2). `````` Robbert Krebbers committed May 07, 2013 79 ``````Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3). `````` Robbert Krebbers committed Feb 01, 2013 80 81 82 ``````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 83 84 85 ``````(** 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 86 `````` `````` Robbert Krebbers committed Feb 19, 2013 87 88 89 90 91 92 93 94 95 96 97 ``````Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P). Proof. unfold bool_decide. destruct dec. by left. by right. Qed. Ltac case_bool_decide := match goal with | H : context [@bool_decide ?P ?dec] |- _ => destruct_decide (@bool_decide_reflect P dec) | |- context [@bool_decide ?P ?dec] => destruct_decide (@bool_decide_reflect P dec) end. `````` Robbert Krebbers committed Jun 11, 2012 98 ``````Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. `````` Robbert Krebbers committed Oct 19, 2012 99 ``````Proof. unfold bool_decide. by destruct dec. Qed. `````` Robbert Krebbers committed Jun 11, 2012 100 ``````Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. `````` Robbert Krebbers committed Oct 19, 2012 101 ``````Proof. unfold bool_decide. by destruct dec. Qed. `````` Robbert Krebbers committed Jun 11, 2012 102 `````` `````` Robbert Krebbers committed Aug 29, 2012 103 104 105 106 ``````(** * 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 19, 2013 107 108 109 ``````irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. Due to the absence of universe polymorpic definitions we also define a variant [dsigS] for types in [Set]. *) `````` Robbert Krebbers committed Aug 21, 2012 110 111 ``````Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} := { x | bool_decide (P x) }. `````` Robbert Krebbers committed Feb 19, 2013 112 113 114 ``````Definition dsigS {A : Set} (P : A → Prop) `{∀ x : A, Decision (P x)} : Set := { x | bool_decide (P x) }. `````` Robbert Krebbers committed Aug 21, 2012 115 116 117 118 ``````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 119 ``````Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)} `````` Robbert Krebbers committed Aug 29, 2012 120 `````` (x y : dsig P) : x = y ↔ `x = `y. `````` Robbert Krebbers committed Mar 14, 2013 121 ``````Proof. apply (sig_eq_pi _). Qed. `````` Robbert Krebbers committed Feb 01, 2013 122 123 124 ``````Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p : dexist (`x) p = x. Proof. by apply dsig_eq. Qed. `````` Robbert Krebbers committed Aug 29, 2012 125 126 127 `````` (** * Instances of Decision *) (** Instances of [Decision] for operators of propositional logic. *) `````` Robbert Krebbers committed Oct 19, 2012 128 129 130 131 132 133 ``````Instance True_dec: Decision True := left I. Instance False_dec: Decision False := right (False_rect False). Section prop_dec. Context `(P_dec : Decision P) `(Q_dec : Decision Q). `````` Robbert Krebbers committed Nov 12, 2012 134 135 `````` Global Instance not_dec: Decision (¬P). Proof. refine (cast_if_not P_dec); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 136 `````` Global Instance and_dec: Decision (P ∧ Q). `````` Robbert Krebbers committed Nov 12, 2012 137 `````` Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 138 `````` Global Instance or_dec: Decision (P ∨ Q). `````` Robbert Krebbers committed Nov 12, 2012 139 `````` Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 140 `````` Global Instance impl_dec: Decision (P → Q). `````` Robbert Krebbers committed Nov 12, 2012 141 `````` Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined. `````` Robbert Krebbers committed Oct 19, 2012 142 ``````End prop_dec. `````` Robbert Krebbers committed Aug 29, 2012 143 144 `````` (** Instances of [Decision] for common data types. *) `````` Robbert Krebbers committed Jan 05, 2013 145 146 ``````Instance bool_eq_dec (x y : bool) : Decision (x = y). Proof. solve_decision. Defined. `````` Robbert Krebbers committed Oct 19, 2012 147 148 149 ``````Instance unit_eq_dec (x y : unit) : Decision (x = y). Proof. refine (left _); by destruct x, y. Defined. Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) `````` Robbert Krebbers committed Jan 05, 2013 150 `````` `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y). `````` Robbert Krebbers committed Oct 19, 2012 151 152 153 154 155 ``````Proof. refine (cast_if_and (A_dec (fst x) (fst y)) (B_dec (snd x) (snd y))); abstract (destruct x, y; simpl in *; congruence). Defined. Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) `````` Robbert Krebbers committed Jan 05, 2013 156 `````` `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y). `````` Robbert Krebbers committed Oct 19, 2012 157 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Jan 05, 2013 158 159 160 161 162 163 164 165 `````` 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 uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y : Decision (uncurry P x y) := P_dec (x,y). `````` Robbert Krebbers committed Mar 14, 2013 166 167 168 169 `````` Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)} `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y). Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.``````