Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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.forall (P : Prop) (H : Decidable P),
Decidable_witness = true -> P
Proof.forall (P : Prop) (H : Decidable P),
Decidable_witness = true -> P
intros P H Hp; apply -> Decidable_spec; assumption.
Qed.

Lemma Decidable_complete : forall P (H : Decidable P),
  P -> Decidable_witness = true.forall (P : Prop) (H : Decidable P),
P -> Decidable_witness = true
Proof.forall (P : Prop) (H : Decidable P),
P -> Decidable_witness = true
intros P H Hp; apply <- Decidable_spec; assumption.
Qed.

Lemma Decidable_sound_alt : forall P (H : Decidable P),
   ~ P -> Decidable_witness = false.forall (P : Prop) (H : Decidable P),
~ P -> Decidable_witness = false
Proof.forall (P : Prop) (H : Decidable P),
~ P -> Decidable_witness = false
intros P [wit spec] Hd; simpl; destruct wit; tauto.
Qed.

Lemma Decidable_complete_alt : forall P (H : Decidable P),
  Decidable_witness = false -> ~ P.forall (P : Prop) (H : Decidable P),
Decidable_witness = false -> ~ P
Proof.forall (P : Prop) (H : Decidable P),
Decidable_witness = false -> ~ P
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 (Decidable:=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.

Require Import Bool Arith ZArith.

Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
  Decidable_witness := Bool.eqb x y
}.
Next Obligation.x, y:bool
eqb x y = true <-> x = y
 apply eqb_true_iff.
Qed.

Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
  Decidable_witness := Nat.eqb x y
}.
Next Obligation.x, y:nat
(x =? y) = true <-> x = y
 apply Nat.eqb_eq.
Qed.

Instance Decidable_le_nat : forall (x y : nat), Decidable (x <= y) := {
  Decidable_witness := Nat.leb x y
}.
Next Obligation.x, y:nat
(x <=? y) = true <-> x <= y
 apply Nat.leb_le.
Qed.

Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
  Decidable_witness := Z.eqb x y
}.
Next Obligation.x, y:Z
(x =? y)%Z = true <-> x = y
 apply Z.eqb_eq.
Qed.