From fe3f50a830a4b559b6293198e6ead688f386a676 Mon Sep 17 00:00:00 2001
From: Janggun Lee <leesisi123@naver.com>
Date: Fri, 23 Aug 2024 09:07:20 +0000
Subject: [PATCH] Add `discrete_function_update{P}`.

* `updateP` requires `Finite A`, similar to `discrete_fun_included_spec`.

* `update` has no such side conditions.
---
 iris/algebra/functions.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 6aa92d2f9..7f7bb4477 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -161,4 +161,22 @@ Section cmra.
     rewrite !cmra_update_updateP;
       eauto using discrete_fun_singleton_updateP_empty with subst.
   Qed.
+
+  Lemma discrete_fun_updateP `{Hfin: Finite A} f P :
+    (∀ a, f a ~~>: P a) → f ~~>: (λ f', ∀ a, P a (f' a)).
+  Proof.
+    rewrite cmra_total_updateP. setoid_rewrite cmra_total_updateP.
+    intros Hf n z Hfz.
+    destruct (finite_choice
+      (λ a y, P a y ∧ ✓{n} (y ⋅ (z a)))
+      ltac:(naive_solver)) as [f' Hf'].
+    naive_solver.
+  Qed.
+
+  Lemma discrete_fun_update f g :
+    (∀ a, f a ~~> g a) → f ~~> g.
+  Proof.
+    rewrite cmra_total_update. setoid_rewrite cmra_total_update.
+    intros Hfg n zf Hz a. apply (Hfg a), Hz.
+  Qed.
 End cmra.
-- 
GitLab