decidable.v 4.33 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
Require Export base.

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's avatar
Robbert Krebbers committed
18

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's avatar
Robbert Krebbers committed
22
  match goal with
23
24
  | H : context [@decide ?P ?dec] |- _ =>
    destruct (@decide P dec)
25
  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
26
27
28
    destruct (@decide_rel _ _ R x y dec)
  | |- context [@decide ?P ?dec] =>
    destruct (@decide P dec)
29
  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
30
    destruct (@decide_rel _ _ R x y dec)
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
  end.

33
34
(** 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
35
36
37
38
39
Ltac solve_trivial_decision :=
  match goal with
  | [ |- Decision (?P) ] => apply _
  | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
  end.
40
Ltac solve_decision :=
41
42
  intros; first [ solve_trivial_decision
                | unfold Decision; decide equality; solve_trivial_decision ].
Robbert Krebbers's avatar
Robbert Krebbers committed
43

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's avatar
Robbert Krebbers committed
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.

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]. *)
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 :=
  xbool_decide_pack _ p.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

65
Lemma dsig_eq {A} (P : A  Prop) {dec :  x, Decision (P x)}
66
  (x y : dsig P) : x = y  `x = `y.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Proof.
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's avatar
Robbert Krebbers committed
75
Qed.
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).