From 6dd5b57094d3245186b0ff7d904f08da03650b26 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Dec 2019 12:10:42 +0100
Subject: [PATCH] Version of `negb` for proof mode.

---
 theories/proofmode/base.v      | 4 ++++
 theories/proofmode/reduction.v | 3 ++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index c28fbbe9d..bc251fe25 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -17,6 +17,10 @@ the actual operations that may appear in users' proofs. *)
 Lemma lazy_andb_true (b1 b2 : bool) : b1 &&& b2 = true ↔ b1 = true ∧ b2 = true.
 Proof. destruct b1, b2; intuition congruence. Qed.
 
+Definition negb (b : bool) : bool := if b then false else true.
+Lemma negb_true b : negb b = true ↔ b = false.
+Proof. by destruct b. Qed.
+
 Fixpoint Pos_succ (x : positive) : positive :=
   match x with
   | (p~1)%positive => ((Pos_succ p)~0)%positive
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index ba3090367..0cfc07623 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -6,7 +6,8 @@ From iris.proofmode Require Import base environments.
     do not reduce e.g. before unification happens in [iApply].*)
 Declare Reduction pm_eval := cbv [
   (* base *)
-  base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
+  base.negb base.beq
+  base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
-- 
GitLab