decidable.v 4.91 KB
Newer Older
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. *)
6 7 8 9
Require Export base tactics.

Lemma dec_stable `{Decision P} : ¬¬P  P.
Proof. firstorder. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11 12 13 14 15 16 17 18 19
(** 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).
20
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22
(** The tactic [case_decide] performs case analysis on an arbitrary occurrence
23
of [decide] or [decide_rel] in the conclusion or hypotheses. *)
24
Ltac case_decide :=
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  match goal with
26 27
  | H : context [@decide ?P ?dec] |- _ =>
    destruct (@decide P dec)
28
  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
29 30 31
    destruct (@decide_rel _ _ R x y dec)
  | |- context [@decide ?P ?dec] =>
    destruct (@decide P dec)
32
  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
33
    destruct (@decide_rel _ _ R x y dec)
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
  end.

36 37
(** The tactic [solve_decision] uses Coq's [decide equality] tactic together
with instance resolution to automatically generate decision procedures. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39
Ltac solve_trivial_decision :=
  match goal with
40 41
  | |- Decision (?P) => apply _
  | |- sumbool ?P (¬?P) => change (Decision P); apply _
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  end.
43 44 45
Ltac solve_decision := intros; first
  [ solve_trivial_decision
  | unfold Decision; decide equality; solve_trivial_decision ].
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47 48 49
(** We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
  if dec then true else false.
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51

Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P  P.
52
Proof. unfold bool_decide. by destruct dec. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P  bool_decide P.
54
Proof. unfold bool_decide. by destruct dec. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55

56 57 58 59 60
(** * 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]. *)
61 62 63 64 65 66
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 :=
  xbool_decide_pack _ p.
Robbert Krebbers's avatar
Robbert Krebbers committed
67

68
Lemma dsig_eq {A} (P : A  Prop) {dec :  x, Decision (P x)}
69
  (x y : dsig P) : x = y  `x = `y.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof.
71 72 73 74 75
  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)).
76 77
    + by intros [] [].
    + done.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Qed.
79

80 81 82 83 84 85 86 87
(** 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_or S1 S2 := (if S1 then left _ else cast_if S2).
Notation cast_if_not S := (if S then right _ else left _).

88 89
(** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *)
90 91 92 93 94 95 96 97 98 99 100 101 102
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).

  Global Instance and_dec: Decision (P  Q).
  Proof. refine (cast_if_and P_dec Q_dec); intuition. Qed.
  Global Instance or_dec: Decision (P  Q).
  Proof. refine (cast_if_or P_dec Q_dec); intuition. Qed.
  Global Instance impl_dec: Decision (P  Q).
  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Qed.
End prop_dec.
103 104

(** Instances of [Decision] for common data types. *)
105 106 107 108 109 110 111 112 113 114 115
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))
    `(B_dec :  x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
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))
    `(B_dec :  x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
Proof. solve_decision. Defined.