From 9d63d29f508ad4a86088344f041645632c64b638 Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Wed, 27 May 2020 14:14:33 -0400
Subject: [stdlib] Decidable instance for negation

Added Changelog
---
 theories/Classes/DecidableClass.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'theories/Classes/DecidableClass.v')

diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 94fcd55aa5..7169aa673d 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -65,6 +65,16 @@ Tactic Notation "decide" constr(P) :=
 
 Require Import Bool Arith ZArith.
 
+Program Instance Decidable_not {P} `{Decidable P} : Decidable (~ P) := {
+  Decidable_witness := negb Decidable_witness
+}.
+Next Obligation.
+  split; intro Heq.
+  - apply negb_true_iff in Heq.
+    eapply Decidable_complete_alt; intuition.
+  - erewrite Decidable_sound_alt; intuition.
+Qed.
+
 Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
   Decidable_witness := Bool.eqb x y
 }.
-- 
cgit v1.2.3