From f6ab476374f379625c5de44976ae2a7fa93c5a15 Mon Sep 17 00:00:00 2001
From: Janggun Lee <leesisi123@naver.com>
Date: Thu, 29 Aug 2024 20:40:27 +0900
Subject: [PATCH] Add some `discrete_fun_singleton` helpers.

---
 iris/algebra/functions.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 210c1bffe..4b0c2dc03 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -86,6 +86,16 @@ Section cmra.
       rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
     by apply ucmra_unit_validN.
   Qed.
+  Lemma discrete_fun_singleton_valid x (y : B x) : ✓ discrete_fun_singleton x y ↔ ✓ y.
+  Proof.
+    by rewrite !cmra_valid_validN; setoid_rewrite discrete_fun_singleton_validN.
+  Qed.
+
+  Lemma discrete_fun_singleton_unit x : discrete_fun_singleton x (ε : B x) ≡ ε.
+  Proof.
+    move=>x'; destruct (decide (x = x')) as [->|];
+      by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
+  Qed.
 
   Lemma discrete_fun_singleton_core x (y : B x) :
     core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).
-- 
GitLab