Version of `negb` for proof mode.

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

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