1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** * A typeclass to ease the handling of decidable properties. *)
(** A proposition is decidable whenever it is reflected by a boolean. *)
Class Decidable (P : Prop) := {
Decidable_witness : bool;
Decidable_spec : Decidable_witness = true <-> P
}.
(** Alternative ways of specifying the reflection property. *)
Lemma Decidable_sound : forall P (H : Decidable P),
Decidable_witness = true -> P.
Proof.
intros P H Hp; apply -> Decidable_spec; assumption.
Qed.
Lemma Decidable_complete : forall P (H : Decidable P),
P -> Decidable_witness = true.
Proof.
intros P H Hp; apply <- Decidable_spec; assumption.
Qed.
Lemma Decidable_sound_alt : forall P (H : Decidable P),
~ P -> Decidable_witness = false.
Proof.
intros P [wit spec] Hd; simpl; destruct wit; tauto.
Qed.
Lemma Decidable_complete_alt : forall P (H : Decidable P),
Decidable_witness = false -> ~ P.
Proof.
intros P [wit spec] Hd Hc; simpl in *; intuition congruence.
Qed.
(** The generic function that should be used to program, together with some
useful tactics. *)
Definition decide P {H : Decidable P} := @Decidable_witness _ H.
Ltac _decide_ P H :=
let b := fresh "b" in
set (b := decide P) in *;
assert (H : decide P = b) by reflexivity;
clearbody b;
destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H].
Tactic Notation "decide" constr(P) "as" ident(H) :=
_decide_ P H.
Tactic Notation "decide" constr(P) :=
let H := fresh "H" in _decide_ P H.
(** Some usual instances. *)
#[global,refine]
Instance Decidable_not {P} `{Decidable P} : Decidable (~ P) := {
Decidable_witness := negb Decidable_witness
}.
Proof.
abstract (specialize Decidable_spec; case Decidable_witness; intuition discriminate).
Defined.
|
