Merge PR #12420: [stdlib] Decidable instance for negation

Reviewed-by: Blaisorblade
Ack-by: SkySkimmer

1 files changed, 10 insertions, 0 deletions

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
 }.