# Library Coq.Classes.DecidableClass

# A typeclass to ease the handling of decidable properties.

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.

Lemma Decidable_complete : forall P (H : Decidable P),

P -> Decidable_witness = true.

Lemma Decidable_sound_alt : forall P (H : Decidable P),

~ P -> Decidable_witness = false.

Lemma Decidable_complete_alt : forall P (H : Decidable P),

Decidable_witness = false -> ~ P.

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

}.