decidable.v 4.33 KB
 Robbert Krebbers committed Aug 29, 2012 1 2 3 4 5 ``````(* Copyright (c) 2012, 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 Jun 11, 2012 6 7 ``````Require Export base. `````` Robbert Krebbers committed Aug 29, 2012 8 9 10 11 12 13 14 15 16 17 ``````(** 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). Proof. easy. Qed. `````` Robbert Krebbers committed Jun 11, 2012 18 `````` `````` Robbert Krebbers committed Aug 29, 2012 19 20 21 ``````(** The tactic [case_decide] performs case analysis on an arbitrary occurrence of [decide] or [decide_rel] in the conclusion or assumptions. *) Ltac case_decide := `````` Robbert Krebbers committed Jun 11, 2012 22 `````` match goal with `````` Robbert Krebbers committed Aug 29, 2012 23 24 `````` | H : context [@decide ?P ?dec] |- _ => destruct (@decide P dec) `````` Robbert Krebbers committed Aug 21, 2012 25 `````` | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => `````` Robbert Krebbers committed Aug 29, 2012 26 27 28 `````` destruct (@decide_rel _ _ R x y dec) | |- context [@decide ?P ?dec] => destruct (@decide P dec) `````` Robbert Krebbers committed Aug 21, 2012 29 `````` | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => `````` Robbert Krebbers committed Aug 29, 2012 30 `````` destruct (@decide_rel _ _ R x y dec) `````` Robbert Krebbers committed Jun 11, 2012 31 32 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 33 34 ``````(** 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 35 36 37 38 39 ``````Ltac solve_trivial_decision := match goal with | [ |- Decision (?P) ] => apply _ | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _ end. `````` Robbert Krebbers committed Aug 29, 2012 40 ``````Ltac solve_decision := `````` Robbert Krebbers committed Aug 21, 2012 41 42 `````` intros; first [ solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision ]. `````` Robbert Krebbers committed Jun 11, 2012 43 `````` `````` Robbert Krebbers committed Aug 29, 2012 44 45 46 ``````(** 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 47 48 49 50 51 52 `````` Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. Proof. unfold bool_decide. now destruct dec. Qed. Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. Proof. unfold bool_decide. now destruct dec. Qed. `````` Robbert Krebbers committed Aug 29, 2012 53 54 55 56 57 ``````(** * 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]. *) `````` Robbert Krebbers committed Aug 21, 2012 58 59 60 61 62 63 ``````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. `````` Robbert Krebbers committed Jun 11, 2012 64 `````` `````` Robbert Krebbers committed Aug 21, 2012 65 ``````Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)} `````` Robbert Krebbers committed Aug 29, 2012 66 `````` (x y : dsig P) : x = y ↔ `x = `y. `````` Robbert Krebbers committed Jun 11, 2012 67 ``````Proof. `````` Robbert Krebbers committed Aug 29, 2012 68 69 70 71 72 73 74 `````` split. * destruct x, y. apply proj1_sig_inj. * intro. destruct x as [x Hx], y as [y Hy]. simpl in *. subst. f_equal. revert Hx Hy. case (bool_decide (P y)). + now intros [] []. + easy. `````` Robbert Krebbers committed Jun 11, 2012 75 ``````Qed. `````` Robbert Krebbers committed Aug 29, 2012 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 104 105 106 107 `````` (** * Instances of Decision *) (** Instances of [Decision] for operators of propositional logic. *) Program Instance True_dec: Decision True := left _. Program Instance False_dec: Decision False := right _. Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∧ Q) := match P_dec with | left _ => match Q_dec with left _ => left _ | right _ => right _ end | right _ => right _ end. Solve Obligations using intuition. Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∨ Q) := match P_dec with | left _ => left _ | right _ => match Q_dec with left _ => left _ | right _ => right _ end end. Solve Obligations using intuition. (** Instances of [Decision] for common data types. *) Program Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y) := match A_dec (fst x) (fst y) with | left _ => match B_dec (snd x) (snd y) with | left _ => left _ | right _ => right _ end | right _ => right _ end. Solve Obligations using intuition (simpl;congruence).``````