From 235c370f818aa355bca0f3cad7e3a8225bdd2644 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Mon, 27 Oct 2025 02:31:46 -0400
Subject: [PATCH 01/16] all defns

---
 src/Iris/BI/BUpdAlt.lean | 146 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 146 insertions(+)
 create mode 100644 src/Iris/BI/BUpdAlt.lean

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
new file mode 100644
index 00000000..a87f2cbd
--- /dev/null
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -0,0 +1,146 @@
+-- TODO: reduce import size?
+import Iris.BI.BI
+import Iris.BI.BIBase
+import Iris.BI.Classes
+import Iris.BI.DerivedLaws
+import Iris.Algebra
+import Iris.Algebra.Updates
+import Iris.Algebra.UPred
+import Iris.BI.Plainly
+import Iris.ProofMode
+import Iris.BI.Updates
+
+-- TODO: why in rocq I don't need to explicitly import this?
+-- I need to import this for "bupd_alt_bupd"
+import Iris.Instances.UPred.Instance
+
+namespace Iris
+open Iris.Std BI
+
+
+-- Note to self: all rocq code are in multiline comments
+--               All questions start with TODO:
+
+-- TODO: why in rocq this definition is not moved into the section?
+
+-- This file contains an alternative version of basic updates, that is
+-- expression in terms of just the plain modality [■]
+def bupd_alt [BI PROP] [BIPlainly PROP] (P : PROP) : PROP :=
+  iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
+
+
+
+section bupd_alt
+variable [BI PROP] [BIPlainly PROP]
+
+-- TODO: the following 4 global instance
+
+
+/- Implicit Types P Q R : PROP. -/
+
+/-
+Global Instance bupd_alt_ne : NonExpansive bupd_alt.
+Proof. solve_proper. Qed.
+Global Instance bupd_alt_proper : Proper ((≡) ==> (≡)) bupd_alt.
+Proof. solve_proper. Qed.
+Global Instance bupd_alt_mono' : Proper ((⊢) ==> (⊢)) bupd_alt.
+Proof. solve_proper. Qed.
+Global Instance bupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
+Proof. solve_proper. Qed.
+-/
+-- NonExpansive
+
+-- Proper
+
+-- mono'
+
+-- flip mono
+
+-- TODO: should I use `lemma`? and how?
+
+-- The Laws of the basica update modality hold
+theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
+  iintro Hp
+  unfold bupd_alt
+  iintro R H
+  -- TODO: can i use iapply now?
+  ispecialize H Hp as H1
+  iexact H1
+
+theorem bupt_alt_mono {P Q : PROP} : (P ⊢ Q) → (bupd_alt P ⊢ bupd_alt Q) := by
+  intro
+  unfold bupd_alt
+
+  sorry
+
+theorem bupd_alt_trans {P : PROP} : bupd_alt (bupd_alt P) ⊢ P := by
+  sorry
+
+-- TODO: why need to wrap `P ∗ Q` with an iprop
+theorem bupd_alt_frame_r {P Q : PROP} : bupd_alt P ∗ Q ⊢ (bupd_alt iprop(P ∗ Q)) := by
+  sorry
+
+theorem bupd_alt_plainly {P : PROP} : bupd_alt iprop(■ P) ⊢ (■ P) := by
+  sorry
+
+-- Any modality confirming with [BiBUpdPlainly] entails the alternative definition
+-- TODO: don't quite understand the typeclass mechanisms...
+theorem bupd_bupd_alt [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢  bupd_alt P := by
+  sorry
+
+-- We get the usual rule for frame preserving updates if we have an [own]
+-- connective satisfying the following rule w.r.t. interaction with plainly.
+
+  -- TODO: how to translate the following?
+
+-- TODO: How is context different from variable
+-- TODO: check if this is a faithful translation of
+/-
+  Context {M : ucmra} (own : M → PROP).
+  Context (own_updateP_plainly : ∀ x Φ R,
+    x ~~>: Φ →
+    own x ∗ (∀ y, ⌜Φ y⌝ -∗ own y -∗ ■ R) ⊢ ■ R).
+-/
+variable [UCMRA M] (own : M → PROP)
+variable (own_updateP_plainly :
+  ∀ (x : M) (Φ : M → Prop) (R : PROP),
+    (x ~~>: Φ) →
+    own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
+
+  -- Lemma own_updateP x (Φ : M → Prop) :
+  --   x ~~>: Φ → own x ⊢ bupd_alt (∃ y, ⌜Φ y⌝ ∧ own y).
+  -- Proof.
+  --   iIntros (Hup) "Hx"; iIntros (R) "H".
+  --   iApply (own_updateP_plainly with "[$Hx H]"); first done.
+  --   iIntros (y ?) "Hy". iApply "H"; auto.
+  -- Qed.
+theorem own_updateP {x : M} {Φ : M → Prop} :
+    (x ~~>: Φ) →
+    own x ⊢ bupd_alt iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
+  -- TODO: why i can't use iintro here?
+  intro Hup
+  iintro Hx
+  unfold bupd_alt
+  iintro R H
+  -- specialize own_updateP_plainly x Φ
+  -- ispecialize own_updateP_plainly x Φ R Hup as H1
+
+  sorry
+
+end bupd_alt
+
+-- The alternative definition entails the ordinary basic update
+theorem bupd_alt_bupd [UCMRA M] (P : UPred M) : bupd_alt P ⊢ |==> P := by
+  sorry
+
+
+theorem bupd_alt_bupd_iff [UCMRA M] (P : UPred M) : bupd_alt P ⊣⊢ |==> P := by
+  refine ⟨?_, ?_⟩
+  · apply bupd_alt_bupd
+  · apply bupd_bupd_alt
+
+-- The law about the interaction between [uPred_ownM] and plainly holds.
+theorem ownM_updateP [UCMRA M] (x : M) (Φ : M → Prop) (R : UPred M) :
+    (x ~~>: Φ) →
+    UPred.ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ UPred.ownM y -∗ ■ R) ⊢ ■ R := by
+  sorry

From dc2cf15932ed17a1ee21279f260121138d1caa59 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Sun, 2 Nov 2025 02:05:04 -0500
Subject: [PATCH 02/16] prove mono

---
 src/Iris/BI/BUpdAlt.lean | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index a87f2cbd..6a73788a 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -67,11 +67,25 @@ theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
   ispecialize H Hp as H1
   iexact H1
 
+
+
 theorem bupt_alt_mono {P Q : PROP} : (P ⊢ Q) → (bupd_alt P ⊢ bupd_alt Q) := by
-  intro
+  intros H
   unfold bupd_alt
+  iintro R HQR
+  iintro Hp
 
-  sorry
+  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
+    iintro H
+    iintro Hp
+    iapply H
+    apply H
+    done
+  iintro ⟨Ha, H2⟩
+  ispecialize Ha HQR
+  iapply Ha
+  iapply H1
+  iassumption
 
 theorem bupd_alt_trans {P : PROP} : bupd_alt (bupd_alt P) ⊢ P := by
   sorry

From a35270590e01f9f3e4bf03c44de43b585b24f801 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Tue, 25 Nov 2025 11:24:11 -0500
Subject: [PATCH 03/16] checkpoint

---
 src/Iris/BI/BUpdAlt.lean | 57 +++++++++++++++++++++++++++++++---------
 1 file changed, 45 insertions(+), 12 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index 6a73788a..dccdd593 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -87,26 +87,52 @@ theorem bupt_alt_mono {P Q : PROP} : (P ⊢ Q) → (bupd_alt P ⊢ bupd_alt Q) :
   iapply H1
   iassumption
 
-theorem bupd_alt_trans {P : PROP} : bupd_alt (bupd_alt P) ⊢ P := by
-  sorry
+theorem bupd_alt_trans {P : PROP} : bupd_alt (bupd_alt P) ⊢ bupd_alt P := by
+  unfold bupd_alt
+  iintro Hp R H
+  ispecialize Hp R as HpR
+  iapply HpR
+  iintro Hp
+  ispecialize Hp R as HpR2
+  iapply HpR2
+  iassumption
 
 -- TODO: why need to wrap `P ∗ Q` with an iprop
 theorem bupd_alt_frame_r {P Q : PROP} : bupd_alt P ∗ Q ⊢ (bupd_alt iprop(P ∗ Q)) := by
-  sorry
+  unfold bupd_alt
+  iintro ⟨Hp, Hq⟩ R H
+  ispecialize Hp R as HpR
+  iapply HpR
+  iintro Hp
+  iapply H
+  isplit l [Hp]
+  · iexact Hp
+  · iexact Hq
 
 theorem bupd_alt_plainly {P : PROP} : bupd_alt iprop(■ P) ⊢ (■ P) := by
-  sorry
+  unfold bupd_alt
+  iintro H
+  ispecialize H P as HP
+  iapply HP
+  iintro Hp
+  iexact Hp
 
 -- Any modality confirming with [BiBUpdPlainly] entails the alternative definition
 -- TODO: don't quite understand the typeclass mechanisms...
 theorem bupd_bupd_alt [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢  bupd_alt P := by
-  sorry
+  unfold bupd_alt
+  iintro HP (R) H
+  -- Eliminate the bupds (by hand, until iMod is implemented)
+  refine BIUpdate.frame_r.trans ?_
+  refine (BIUpdate.mono sep_symm).trans ?_
+  -- TODO: what gets filled in in the `_` here, namely what is of type `BI PROP`?
+  refine (BIUpdate.mono <| @wand_elim PROP _ iprop(P -∗ ■ R) P iprop(■R) .rfl).trans ?_
+  exact bupd_elim
 
 -- We get the usual rule for frame preserving updates if we have an [own]
 -- connective satisfying the following rule w.r.t. interaction with plainly.
 
-  -- TODO: how to translate the following?
-
+-- TODO: how to translate the following?
 -- TODO: How is context different from variable
 -- TODO: check if this is a faithful translation of
 /-
@@ -128,17 +154,24 @@ variable (own_updateP_plainly :
   --   iApply (own_updateP_plainly with "[$Hx H]"); first done.
   --   iIntros (y ?) "Hy". iApply "H"; auto.
   -- Qed.
-theorem own_updateP {x : M} {Φ : M → Prop} :
+theorem own_updateP {x : M} {Φ : M → Prop}
+    (own_updateP_plainly :
+      ∀ (x : M) (Φ : M → Prop) (R : PROP),
+        (x ~~>: Φ) →
+        own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R) :
     (x ~~>: Φ) →
     own x ⊢ bupd_alt iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
-  -- TODO: why i can't use iintro here?
   intro Hup
   iintro Hx
   unfold bupd_alt
   iintro R H
-  -- specialize own_updateP_plainly x Φ
-  -- ispecialize own_updateP_plainly x Φ R Hup as H1
-
+  iapply own_updateP_plainly x Φ R Hup
+  isplit l [Hx]
+  · iexact Hx
+  -- TODO: can't intro (HΦ) to pure context
+  iintro y (HΦ) Hy
+  iapply H
+  iexists y
   sorry
 
 end bupd_alt

From 552e5a355effd65dc04011774cac2eaac5881365 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Tue, 25 Nov 2025 14:41:19 -0500
Subject: [PATCH 04/16] im destroyed by the vibe coding machine

---
 src/Iris/BI/BUpdAlt.lean | 129 ++++++++++++++++++++++++++++++++++-----
 1 file changed, 113 insertions(+), 16 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index dccdd593..a09b697f 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -145,20 +145,12 @@ variable [UCMRA M] (own : M → PROP)
 variable (own_updateP_plainly :
   ∀ (x : M) (Φ : M → Prop) (R : PROP),
     (x ~~>: Φ) →
-    own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
-
-  -- Lemma own_updateP x (Φ : M → Prop) :
-  --   x ~~>: Φ → own x ⊢ bupd_alt (∃ y, ⌜Φ y⌝ ∧ own y).
-  -- Proof.
-  --   iIntros (Hup) "Hx"; iIntros (R) "H".
-  --   iApply (own_updateP_plainly with "[$Hx H]"); first done.
-  --   iIntros (y ?) "Hy". iApply "H"; auto.
-  -- Qed.
+    own x ∗ (∀ y, iprop(<affine> ⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
 theorem own_updateP {x : M} {Φ : M → Prop}
     (own_updateP_plainly :
       ∀ (x : M) (Φ : M → Prop) (R : PROP),
         (x ~~>: Φ) →
-        own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R) :
+        own x ∗ (∀ y, iprop(<affine> ⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R) :
     (x ~~>: Φ) →
     own x ⊢ bupd_alt iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
   intro Hup
@@ -168,17 +160,58 @@ theorem own_updateP {x : M} {Φ : M → Prop}
   iapply own_updateP_plainly x Φ R Hup
   isplit l [Hx]
   · iexact Hx
-  -- TODO: can't intro (HΦ) to pure context
-  iintro y (HΦ) Hy
+  -- TODO: can't intro HΦ to pure context
+  iintro y
+  iintro HΦ
+  icases HΦ with ⌜HQ⌝
+  iintro Hy
   iapply H
   iexists y
-  sorry
-
+  isplit
+  · ipure_intro
+    exact HQ
+  · iexact Hy
 end bupd_alt
 
+-- Helper predicate for bupd_alt_bupd proof
+private def bupd_alt_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
+  holds k _ := ∃ x'', ✓{k} (x'' • y) ∧ P k x''
+  mono {_} := fun ⟨z, Hz1, Hz2⟩ _ Hn =>
+    ⟨z, CMRA.validN_of_le Hn Hz1, P.mono Hz2 (CMRA.incN_refl z) Hn⟩
+
 -- The alternative definition entails the ordinary basic update
 theorem bupd_alt_bupd [UCMRA M] (P : UPred M) : bupd_alt P ⊢ |==> P := by
-  sorry
+  unfold bupd_alt bupd
+  -- Unseal
+  intro n x Hx H
+  -- Unfold bupd definition in `Instance.lean`
+  intro k y Hkn Hxy
+  -- Apply H to the custom predicate R
+  let R := bupd_alt_pred P y
+  -- H : iprop(∀ R, (P -∗ ■ R) -∗ ■ R).holds n x
+  -- This is sForall (fun p => ∃ R, (P -∗ ■ R) -∗ ■ R = p).holds n x
+  -- Which means: ∀ p, (∃ R', ...) → p n x
+  -- We instantiate with our R
+  have H_inst : (UPred.wand (UPred.wand P (UPred.plainly R)) (UPred.plainly R)).holds n x :=
+    H (UPred.wand (UPred.wand P (UPred.plainly R)) (UPred.plainly R)) ⟨R, rfl⟩
+  -- Now use mono to get it at k with y (not x • y!)
+  -- We need x ≼{k} y, but that's not generally true
+  -- Instead, apply H_inst directly at k with y
+  -- But we need ✓{k} (x • y) to apply the wand
+  -- Actually, let's just use H_inst as a wand and apply it
+  -- The wand says: ∀ k' y', k' ≤ n → ✓{k'} (x • y') → (P -∗ ■ R) k' y' → (■ R) k' (x • y')
+  have wand_holds : (UPred.wand P (UPred.plainly R)).holds k y := by
+    intro k' z Hk' Hvyz HP
+    -- Need to show: (■ R) k' (y • z), which is R k' UCMRA.unit
+    -- R k' UCMRA.unit = ∃ x'', ✓{k'} (x'' • y) ∧ P k' x''
+    refine ⟨z, ?_, HP⟩
+    -- Hvyz : ✓{k'} (y • z), need ✓{k'} (z • y)
+    exact CMRA.validN_ne CMRA.op_commN Hvyz
+  -- Now apply H_inst
+  have HR : (UPred.plainly R).holds k (x • y) := H_inst k y Hkn Hxy wand_holds
+  -- HR : (■ R) k (x • y), which unfolds to R k UCMRA.unit
+  -- R k UCMRA.unit = ∃ x', ✓{k} (x' • y) ∧ P k x'
+  exact HR
 
 
 theorem bupd_alt_bupd_iff [UCMRA M] (P : UPred M) : bupd_alt P ⊣⊢ |==> P := by
@@ -190,4 +223,68 @@ theorem bupd_alt_bupd_iff [UCMRA M] (P : UPred M) : bupd_alt P ⊣⊢ |==> P :=
 theorem ownM_updateP [UCMRA M] (x : M) (Φ : M → Prop) (R : UPred M) :
     (x ~~>: Φ) →
     UPred.ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ UPred.ownM y -∗ ■ R) ⊢ ■ R := by
-  sorry
+  intro Hup
+  -- Unfold to work at the representation level
+  intro n z Hv ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
+  -- Hv : ✓{n} z
+  -- Destructure the sep:
+  -- x1, z2 are the two parts
+  -- Hx : z ≡{n} x1 • z2
+  -- ⟨z1, Hz1⟩ : (ownM x) n x1, which means x ≼{n} x1, i.e., ∃ z1, x1 ≡{n} x • z1
+  -- HR : ForAll holds at z2
+
+  -- After ofe_subst, we have z ≡{n} (x • z1) • z2
+  have Hz_subst : z ≡{n}≡ (x • z1) • z2 := by
+    calc z ≡{n}≡ x1 • z2 := Hx
+         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
+
+  -- Apply the update with frame z1 • z2
+  have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
+    show ✓{n} (x • (z1 • z2))
+    refine CMRA.validN_ne ?_ Hv
+    calc z ≡{n}≡ (x • z1) • z2 := Hz_subst
+         _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
+
+  obtain ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
+
+  -- HR : ∀ p, (∃ y', p = ...) → p n z2
+  -- We need to instantiate with the wand
+  let p := UPred.wand (UPred.pure (Φ y)) (UPred.wand (UPred.ownM y) (UPred.plainly R))
+  have Hp : (UPred.wand (UPred.pure (Φ y)) (UPred.wand (UPred.ownM y) (UPred.plainly R))).holds n z2 :=
+    HR p ⟨y, rfl⟩
+
+  -- Apply Hp at step n with resource z1
+  -- First wand: (⌜Φ y⌝ -∗ (ownM y -∗ ■ R)).holds n z2
+  -- Means: ∀ n' x', n' ≤ n → ✓{n'} (z2 • x') → (⌜Φ y⌝) n' x' → (ownM y -∗ ■ R) n' (z2 • x')
+  -- We need ✓{n} (z2 • z1)
+  have Hv_z2z1 : ✓{n} (z2 • z1) := by
+    -- From Coq line 250: rewrite comm. by eapply cmra_validN_op_r.
+    -- We have Hvalid_y : ✓{n} (y •? some (z1 • z2)) = ✓{n} (y • (z1 • z2))
+    -- Need ✓{n} (z2 • z1)
+    have : ✓{n} (y • (z1 • z2)) := Hvalid_y
+    exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right this)
+
+  have Hp1 : (UPred.wand (UPred.ownM y) (UPred.plainly R)).holds n (z2 • z1) := Hp n z1 (Nat.le_refl _) Hv_z2z1 HΦy
+
+  -- Apply the second wand at step n with resource y
+  -- (ownM y -∗ ■ R).holds n (z2 • z1)
+  -- Means: ∀ n' x', n' ≤ n → ✓{n'} ((z2 • z1) • x') → (ownM y) n' x' → (■ R) n' ((z2 • z1) • x')
+  -- We want to apply this with x' = y at step n
+  -- Need: ✓{n} ((z2 • z1) • y)
+  have Hv_z2z1y : ✓{n} ((z2 • z1) • y) := by
+    -- From Coq line 251: by rewrite (comm _ _ y) (comm _ z2).
+    -- We have Hvalid_y : ✓{n} (y • (z1 • z2))
+    have : ✓{n} (y • (z1 • z2)) := Hvalid_y
+    refine CMRA.validN_ne ?_ this
+    calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
+         _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
+
+  -- Need: (ownM y) n y, which is y ≼{n} y
+  have Hy_incl : y ≼{n} y := CMRA.incN_refl y
+
+  have HR_goal : (UPred.plainly R).holds n ((z2 • z1) • y) :=
+    Hp1 n y (Nat.le_refl _) Hv_z2z1y Hy_incl
+
+  -- HR_goal : R n UCMRA.unit
+  -- We need to show: R n UCMRA.unit
+  exact HR_goal

From 7cd65bea093ee3fb61e738bf2607ab9e5f8410b3 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Tue, 2 Dec 2025 16:02:16 -0500
Subject: [PATCH 05/16] checkpoint

---
 src/Iris/BI/BUpdAlt.lean | 32 ++++++++------------------------
 1 file changed, 8 insertions(+), 24 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index a09b697f..f02f35a2 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -14,15 +14,11 @@ import Iris.BI.Updates
 -- I need to import this for "bupd_alt_bupd"
 import Iris.Instances.UPred.Instance
 
+set_option trace.Meta.synthInstance true
+
 namespace Iris
 open Iris.Std BI
 
-
--- Note to self: all rocq code are in multiline comments
---               All questions start with TODO:
-
--- TODO: why in rocq this definition is not moved into the section?
-
 -- This file contains an alternative version of basic updates, that is
 -- expression in terms of just the plain modality [■]
 def bupd_alt [BI PROP] [BIPlainly PROP] (P : PROP) : PROP :=
@@ -35,7 +31,6 @@ variable [BI PROP] [BIPlainly PROP]
 
 -- TODO: the following 4 global instance
 
-
 /- Implicit Types P Q R : PROP. -/
 
 /-
@@ -63,7 +58,6 @@ theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
   iintro Hp
   unfold bupd_alt
   iintro R H
-  -- TODO: can i use iapply now?
   ispecialize H Hp as H1
   iexact H1
 
@@ -74,7 +68,6 @@ theorem bupt_alt_mono {P Q : PROP} : (P ⊢ Q) → (bupd_alt P ⊢ bupd_alt Q) :
   unfold bupd_alt
   iintro R HQR
   iintro Hp
-
   have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
     iintro H
     iintro Hp
@@ -146,11 +139,12 @@ variable (own_updateP_plainly :
   ∀ (x : M) (Φ : M → Prop) (R : PROP),
     (x ~~>: Φ) →
     own x ∗ (∀ y, iprop(<affine> ⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
+
 theorem own_updateP {x : M} {Φ : M → Prop}
     (own_updateP_plainly :
       ∀ (x : M) (Φ : M → Prop) (R : PROP),
         (x ~~>: Φ) →
-        own x ∗ (∀ y, iprop(<affine> ⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R) :
+        own x ∗ (∀ y, <affine> iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R) :
     (x ~~>: Φ) →
     own x ⊢ bupd_alt iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
   intro Hup
@@ -182,32 +176,22 @@ private def bupd_alt_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
 -- The alternative definition entails the ordinary basic update
 theorem bupd_alt_bupd [UCMRA M] (P : UPred M) : bupd_alt P ⊢ |==> P := by
   unfold bupd_alt bupd
-  -- Unseal
   intro n x Hx H
   -- Unfold bupd definition in `Instance.lean`
   intro k y Hkn Hxy
-  -- Apply H to the custom predicate R
   let R := bupd_alt_pred P y
-  -- H : iprop(∀ R, (P -∗ ■ R) -∗ ■ R).holds n x
-  -- This is sForall (fun p => ∃ R, (P -∗ ■ R) -∗ ■ R = p).holds n x
-  -- Which means: ∀ p, (∃ R', ...) → p n x
-  -- We instantiate with our R
   have H_inst : (UPred.wand (UPred.wand P (UPred.plainly R)) (UPred.plainly R)).holds n x :=
+    -- TODO: why do i need to pass this wand into H..., why I also need to pass in this proof
     H (UPred.wand (UPred.wand P (UPred.plainly R)) (UPred.plainly R)) ⟨R, rfl⟩
-  -- Now use mono to get it at k with y (not x • y!)
-  -- We need x ≼{k} y, but that's not generally true
-  -- Instead, apply H_inst directly at k with y
-  -- But we need ✓{k} (x • y) to apply the wand
-  -- Actually, let's just use H_inst as a wand and apply it
-  -- The wand says: ∀ k' y', k' ≤ n → ✓{k'} (x • y') → (P -∗ ■ R) k' y' → (■ R) k' (x • y')
+
   have wand_holds : (UPred.wand P (UPred.plainly R)).holds k y := by
     intro k' z Hk' Hvyz HP
     -- Need to show: (■ R) k' (y • z), which is R k' UCMRA.unit
     -- R k' UCMRA.unit = ∃ x'', ✓{k'} (x'' • y) ∧ P k' x''
     refine ⟨z, ?_, HP⟩
-    -- Hvyz : ✓{k'} (y • z), need ✓{k'} (z • y)
     exact CMRA.validN_ne CMRA.op_commN Hvyz
-  -- Now apply H_inst
+
+  -- TODO: why do I need to pass in k, y, Hkn, Hxy, wand_holds again??
   have HR : (UPred.plainly R).holds k (x • y) := H_inst k y Hkn Hxy wand_holds
   -- HR : (■ R) k (x • y), which unfolds to R k UCMRA.unit
   -- R k UCMRA.unit = ∃ x', ✓{k} (x' • y) ∧ P k x'

From 5235dded015182db1b9db708d44cd8016e819000 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Thu, 4 Dec 2025 18:28:45 -0500
Subject: [PATCH 06/16] clean up

---
 src/Iris/BI/BUpdAlt.lean | 85 ++++++++++------------------------------
 1 file changed, 20 insertions(+), 65 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index f02f35a2..251b849a 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -14,7 +14,7 @@ import Iris.BI.Updates
 -- I need to import this for "bupd_alt_bupd"
 import Iris.Instances.UPred.Instance
 
-set_option trace.Meta.synthInstance true
+-- set_option trace.Meta.synthInstance true
 
 namespace Iris
 open Iris.Std BI
@@ -154,16 +154,13 @@ theorem own_updateP {x : M} {Φ : M → Prop}
   iapply own_updateP_plainly x Φ R Hup
   isplit l [Hx]
   · iexact Hx
-  -- TODO: can't intro HΦ to pure context
-  iintro y
-  iintro HΦ
-  icases HΦ with ⌜HQ⌝
+  iintro y ⌜HΦ⌝
   iintro Hy
   iapply H
   iexists y
   isplit
   · ipure_intro
-    exact HQ
+    exact HΦ
   · iexact Hy
 end bupd_alt
 
@@ -180,22 +177,13 @@ theorem bupd_alt_bupd [UCMRA M] (P : UPred M) : bupd_alt P ⊢ |==> P := by
   -- Unfold bupd definition in `Instance.lean`
   intro k y Hkn Hxy
   let R := bupd_alt_pred P y
-  have H_inst : (UPred.wand (UPred.wand P (UPred.plainly R)) (UPred.plainly R)).holds n x :=
-    -- TODO: why do i need to pass this wand into H..., why I also need to pass in this proof
-    H (UPred.wand (UPred.wand P (UPred.plainly R)) (UPred.plainly R)) ⟨R, rfl⟩
+  have H_inst : iprop((P -∗ ■ R) -∗ ■ R).holds n x := H _ ⟨R, rfl⟩
 
-  have wand_holds : (UPred.wand P (UPred.plainly R)).holds k y := by
+  have wand_holds : iprop(P -∗ ■ R).holds k y := by
     intro k' z Hk' Hvyz HP
-    -- Need to show: (■ R) k' (y • z), which is R k' UCMRA.unit
-    -- R k' UCMRA.unit = ∃ x'', ✓{k'} (x'' • y) ∧ P k' x''
     refine ⟨z, ?_, HP⟩
     exact CMRA.validN_ne CMRA.op_commN Hvyz
-
-  -- TODO: why do I need to pass in k, y, Hkn, Hxy, wand_holds again??
-  have HR : (UPred.plainly R).holds k (x • y) := H_inst k y Hkn Hxy wand_holds
-  -- HR : (■ R) k (x • y), which unfolds to R k UCMRA.unit
-  -- R k UCMRA.unit = ∃ x', ✓{k} (x' • y) ∧ P k x'
-  exact HR
+  exact H_inst k y Hkn Hxy wand_holds
 
 
 theorem bupd_alt_bupd_iff [UCMRA M] (P : UPred M) : bupd_alt P ⊣⊢ |==> P := by
@@ -208,67 +196,34 @@ theorem ownM_updateP [UCMRA M] (x : M) (Φ : M → Prop) (R : UPred M) :
     (x ~~>: Φ) →
     UPred.ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ UPred.ownM y -∗ ■ R) ⊢ ■ R := by
   intro Hup
-  -- Unfold to work at the representation level
-  intro n z Hv ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
-  -- Hv : ✓{n} z
-  -- Destructure the sep:
-  -- x1, z2 are the two parts
-  -- Hx : z ≡{n} x1 • z2
-  -- ⟨z1, Hz1⟩ : (ownM x) n x1, which means x ≼{n} x1, i.e., ∃ z1, x1 ≡{n} x • z1
-  -- HR : ForAll holds at z2
-
-  -- After ofe_subst, we have z ≡{n} (x • z1) • z2
+  intro n z
+  intro Hv
+  -- x1 z2 are introduced for separating conjunction
+  -- (ownM x).holds n x1 := x ≼{n} x1, namely x · z1 = x1
+  intro ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
+  -- manually having ofe_subst, z ≡{n} (x • z1) • z2
   have Hz_subst : z ≡{n}≡ (x • z1) • z2 := by
     calc z ≡{n}≡ x1 • z2 := Hx
          _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
 
-  -- Apply the update with frame z1 • z2
   have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
     show ✓{n} (x • (z1 • z2))
     refine CMRA.validN_ne ?_ Hv
     calc z ≡{n}≡ (x • z1) • z2 := Hz_subst
          _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
+  have ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
 
-  obtain ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
-
-  -- HR : ∀ p, (∃ y', p = ...) → p n z2
-  -- We need to instantiate with the wand
-  let p := UPred.wand (UPred.pure (Φ y)) (UPred.wand (UPred.ownM y) (UPred.plainly R))
-  have Hp : (UPred.wand (UPred.pure (Φ y)) (UPred.wand (UPred.ownM y) (UPred.plainly R))).holds n z2 :=
-    HR p ⟨y, rfl⟩
+  have Hp := HR (iprop(⌜Φ y⌝ -∗ (UPred.ownM y -∗ ■ R))) ⟨y, rfl⟩
 
-  -- Apply Hp at step n with resource z1
-  -- First wand: (⌜Φ y⌝ -∗ (ownM y -∗ ■ R)).holds n z2
-  -- Means: ∀ n' x', n' ≤ n → ✓{n'} (z2 • x') → (⌜Φ y⌝) n' x' → (ownM y -∗ ■ R) n' (z2 • x')
-  -- We need ✓{n} (z2 • z1)
   have Hv_z2z1 : ✓{n} (z2 • z1) := by
-    -- From Coq line 250: rewrite comm. by eapply cmra_validN_op_r.
-    -- We have Hvalid_y : ✓{n} (y •? some (z1 • z2)) = ✓{n} (y • (z1 • z2))
-    -- Need ✓{n} (z2 • z1)
-    have : ✓{n} (y • (z1 • z2)) := Hvalid_y
-    exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right this)
-
-  have Hp1 : (UPred.wand (UPred.ownM y) (UPred.plainly R)).holds n (z2 • z1) := Hp n z1 (Nat.le_refl _) Hv_z2z1 HΦy
-
-  -- Apply the second wand at step n with resource y
-  -- (ownM y -∗ ■ R).holds n (z2 • z1)
-  -- Means: ∀ n' x', n' ≤ n → ✓{n'} ((z2 • z1) • x') → (ownM y) n' x' → (■ R) n' ((z2 • z1) • x')
-  -- We want to apply this with x' = y at step n
-  -- Need: ✓{n} ((z2 • z1) • y)
+    exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
+
+  have Hp1 : iprop(UPred.ownM y -∗ ■ R).holds n (z2 • z1) := Hp n z1 (Nat.le_refl _) Hv_z2z1 HΦy
+
   have Hv_z2z1y : ✓{n} ((z2 • z1) • y) := by
-    -- From Coq line 251: by rewrite (comm _ _ y) (comm _ z2).
-    -- We have Hvalid_y : ✓{n} (y • (z1 • z2))
-    have : ✓{n} (y • (z1 • z2)) := Hvalid_y
-    refine CMRA.validN_ne ?_ this
+    apply CMRA.validN_ne ?_ Hvalid_y
     calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
          _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
 
-  -- Need: (ownM y) n y, which is y ≼{n} y
   have Hy_incl : y ≼{n} y := CMRA.incN_refl y
-
-  have HR_goal : (UPred.plainly R).holds n ((z2 • z1) • y) :=
-    Hp1 n y (Nat.le_refl _) Hv_z2z1y Hy_incl
-
-  -- HR_goal : R n UCMRA.unit
-  -- We need to show: R n UCMRA.unit
-  exact HR_goal
+  exact Hp1 n y (Nat.le_refl _) Hv_z2z1y Hy_incl

From 9b5d451726538ce64b3e87270c727583064e7c9f Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Thu, 4 Dec 2025 19:16:09 -0500
Subject: [PATCH 07/16] more clean up

---
 src/Iris/BI/BUpdAlt.lean | 25 +++----------------------
 1 file changed, 3 insertions(+), 22 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index 251b849a..fcc18f39 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -1,17 +1,4 @@
--- TODO: reduce import size?
-import Iris.BI.BI
-import Iris.BI.BIBase
-import Iris.BI.Classes
-import Iris.BI.DerivedLaws
-import Iris.Algebra
-import Iris.Algebra.Updates
-import Iris.Algebra.UPred
-import Iris.BI.Plainly
 import Iris.ProofMode
-import Iris.BI.Updates
-
--- TODO: why in rocq I don't need to explicitly import this?
--- I need to import this for "bupd_alt_bupd"
 import Iris.Instances.UPred.Instance
 
 -- set_option trace.Meta.synthInstance true
@@ -43,16 +30,13 @@ Proof. solve_proper. Qed.
 Global Instance bupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
 Proof. solve_proper. Qed.
 -/
--- NonExpansive
 
+-- NonExpansive
 -- Proper
-
 -- mono'
-
 -- flip mono
 
 -- TODO: should I use `lemma`? and how?
-
 -- The Laws of the basica update modality hold
 theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
   iintro Hp
@@ -61,8 +45,6 @@ theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
   ispecialize H Hp as H1
   iexact H1
 
-
-
 theorem bupt_alt_mono {P Q : PROP} : (P ⊢ Q) → (bupd_alt P ⊢ bupd_alt Q) := by
   intros H
   unfold bupd_alt
@@ -90,7 +72,6 @@ theorem bupd_alt_trans {P : PROP} : bupd_alt (bupd_alt P) ⊢ bupd_alt P := by
   iapply HpR2
   iassumption
 
--- TODO: why need to wrap `P ∗ Q` with an iprop
 theorem bupd_alt_frame_r {P Q : PROP} : bupd_alt P ∗ Q ⊢ (bupd_alt iprop(P ∗ Q)) := by
   unfold bupd_alt
   iintro ⟨Hp, Hq⟩ R H
@@ -98,7 +79,7 @@ theorem bupd_alt_frame_r {P Q : PROP} : bupd_alt P ∗ Q ⊢ (bupd_alt iprop(P 
   iapply HpR
   iintro Hp
   iapply H
-  isplit l [Hp]
+  isplitl [Hp]
   · iexact Hp
   · iexact Hq
 
@@ -152,7 +133,7 @@ theorem own_updateP {x : M} {Φ : M → Prop}
   unfold bupd_alt
   iintro R H
   iapply own_updateP_plainly x Φ R Hup
-  isplit l [Hx]
+  isplitl [Hx]
   · iexact Hx
   iintro y ⌜HΦ⌝
   iintro Hy

From 47ef8a95882a9033cd7c9f85d463bc74411d37a3 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Tue, 9 Dec 2025 22:59:03 -0500
Subject: [PATCH 08/16] checkpt

---
 src/Iris/BI/BUpdAlt.lean | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index fcc18f39..d15d6094 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -11,20 +11,27 @@ open Iris.Std BI
 def bupd_alt [BI PROP] [BIPlainly PROP] (P : PROP) : PROP :=
   iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
 
-
-
 section bupd_alt
 variable [BI PROP] [BIPlainly PROP]
 
--- TODO: the following 4 global instance
-
-/- Implicit Types P Q R : PROP. -/
-
+instance bupd_alt_ne : OFE.NonExpansive (bupd_alt (PROP := PROP)) where
+  ne n x1 x2 Hx := by
+    unfold bupd_alt
+    apply forall_ne
+    intro R
+    apply wand_ne.ne;
+    · apply wand_ne.ne
+      · exact Hx
+      · exact .rfl
+    · exact .rfl
 /-
 Global Instance bupd_alt_ne : NonExpansive bupd_alt.
 Proof. solve_proper. Qed.
+-- non-expansive is like Proper but wiht ≡n≡
+
 Global Instance bupd_alt_proper : Proper ((≡) ==> (≡)) bupd_alt.
 Proof. solve_proper. Qed.
+
 Global Instance bupd_alt_mono' : Proper ((⊢) ==> (⊢)) bupd_alt.
 Proof. solve_proper. Qed.
 Global Instance bupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
@@ -100,9 +107,10 @@ theorem bupd_bupd_alt [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==>
   refine BIUpdate.frame_r.trans ?_
   refine (BIUpdate.mono sep_symm).trans ?_
   -- TODO: what gets filled in in the `_` here, namely what is of type `BI PROP`?
-  refine (BIUpdate.mono <| @wand_elim PROP _ iprop(P -∗ ■ R) P iprop(■R) .rfl).trans ?_
-  exact bupd_elim
+  let AAA : BI PROP := by infer_instance
+  exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
 
+-- #print bupd_bupd_alt
 -- We get the usual rule for frame preserving updates if we have an [own]
 -- connective satisfying the following rule w.r.t. interaction with plainly.
 

From 0304ea98a21ffe72ac5e5df0400fc248256c9a05 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Thu, 11 Dec 2025 00:38:06 -0500
Subject: [PATCH 09/16] more clean up

---
 src/Iris/BI/BUpdAlt.lean | 37 ++-----------------------------------
 1 file changed, 2 insertions(+), 35 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index d15d6094..8d668fba 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -24,27 +24,8 @@ instance bupd_alt_ne : OFE.NonExpansive (bupd_alt (PROP := PROP)) where
       · exact Hx
       · exact .rfl
     · exact .rfl
-/-
-Global Instance bupd_alt_ne : NonExpansive bupd_alt.
-Proof. solve_proper. Qed.
--- non-expansive is like Proper but wiht ≡n≡
-
-Global Instance bupd_alt_proper : Proper ((≡) ==> (≡)) bupd_alt.
-Proof. solve_proper. Qed.
-
-Global Instance bupd_alt_mono' : Proper ((⊢) ==> (⊢)) bupd_alt.
-Proof. solve_proper. Qed.
-Global Instance bupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
-Proof. solve_proper. Qed.
--/
-
--- NonExpansive
--- Proper
--- mono'
--- flip mono
-
--- TODO: should I use `lemma`? and how?
--- The Laws of the basica update modality hold
+
+-- The Laws of the basic update modality hold
 theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
   iintro Hp
   unfold bupd_alt
@@ -99,30 +80,16 @@ theorem bupd_alt_plainly {P : PROP} : bupd_alt iprop(■ P) ⊢ (■ P) := by
   iexact Hp
 
 -- Any modality confirming with [BiBUpdPlainly] entails the alternative definition
--- TODO: don't quite understand the typeclass mechanisms...
 theorem bupd_bupd_alt [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢  bupd_alt P := by
   unfold bupd_alt
   iintro HP (R) H
   -- Eliminate the bupds (by hand, until iMod is implemented)
   refine BIUpdate.frame_r.trans ?_
   refine (BIUpdate.mono sep_symm).trans ?_
-  -- TODO: what gets filled in in the `_` here, namely what is of type `BI PROP`?
-  let AAA : BI PROP := by infer_instance
   exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
 
--- #print bupd_bupd_alt
 -- We get the usual rule for frame preserving updates if we have an [own]
 -- connective satisfying the following rule w.r.t. interaction with plainly.
-
--- TODO: how to translate the following?
--- TODO: How is context different from variable
--- TODO: check if this is a faithful translation of
-/-
-  Context {M : ucmra} (own : M → PROP).
-  Context (own_updateP_plainly : ∀ x Φ R,
-    x ~~>: Φ →
-    own x ∗ (∀ y, ⌜Φ y⌝ -∗ own y -∗ ■ R) ⊢ ■ R).
--/
 variable [UCMRA M] (own : M → PROP)
 variable (own_updateP_plainly :
   ∀ (x : M) (Φ : M → Prop) (R : PROP),

From f8f45829075d21519b766e4e60271892fdbbca41 Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Thu, 11 Dec 2025 02:02:35 -0500
Subject: [PATCH 10/16] good to go

---
 src/Iris/BI/BUpdAlt.lean | 15 ++++++---------
 src/Iris/BI/Plainly.lean |  4 ++++
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
index 8d668fba..8d351acc 100644
--- a/src/Iris/BI/BUpdAlt.lean
+++ b/src/Iris/BI/BUpdAlt.lean
@@ -1,8 +1,6 @@
 import Iris.ProofMode
 import Iris.Instances.UPred.Instance
 
--- set_option trace.Meta.synthInstance true
-
 namespace Iris
 open Iris.Std BI
 
@@ -16,7 +14,6 @@ variable [BI PROP] [BIPlainly PROP]
 
 instance bupd_alt_ne : OFE.NonExpansive (bupd_alt (PROP := PROP)) where
   ne n x1 x2 Hx := by
-    unfold bupd_alt
     apply forall_ne
     intro R
     apply wand_ne.ne;
@@ -94,13 +91,12 @@ variable [UCMRA M] (own : M → PROP)
 variable (own_updateP_plainly :
   ∀ (x : M) (Φ : M → Prop) (R : PROP),
     (x ~~>: Φ) →
-    own x ∗ (∀ y, iprop(<affine> ⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
+    own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
 
-theorem own_updateP {x : M} {Φ : M → Prop}
-    (own_updateP_plainly :
-      ∀ (x : M) (Φ : M → Prop) (R : PROP),
-        (x ~~>: Φ) →
-        own x ∗ (∀ y, <affine> iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R) :
+-- Since own_updateP doesn't use `own_updateP_plainly` in the type,
+-- need to explicitly include it
+include own_updateP_plainly
+theorem own_updateP {x : M} {Φ : M → Prop} :
     (x ~~>: Φ) →
     own x ⊢ bupd_alt iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
   intro Hup
@@ -118,6 +114,7 @@ theorem own_updateP {x : M} {Φ : M → Prop}
   · ipure_intro
     exact HΦ
   · iexact Hy
+
 end bupd_alt
 
 -- Helper predicate for bupd_alt_bupd proof
diff --git a/src/Iris/BI/Plainly.lean b/src/Iris/BI/Plainly.lean
index a897bd25..c327f37f 100644
--- a/src/Iris/BI/Plainly.lean
+++ b/src/Iris/BI/Plainly.lean
@@ -302,6 +302,10 @@ theorem impl_wand_plainly : (■ P → Q) ⊣⊢ (■ P -∗ Q) :=
 
 end AffineBI
 
+-- Typeclass instances
+instance plainly_absorbing (P : PROP) : Absorbing iprop(■ P) where
+  absorbing := absorbingly_elim_plainly.1
+
 end PlainlyLaws
 
 end Iris.BI

From c4a4156a31d1696df86d59eb8db3f1c77d607b0f Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 19 Dec 2025 08:55:57 -0500
Subject: [PATCH 11/16] Move files

---
 src/Iris/BI/BUpdAlt.lean               | 182 -------------------------
 src/Iris/BI/Plainly.lean               |   1 -
 src/Iris/Instances/UPred/Instance.lean |  75 ++++++++++
 src/Iris/ProofMode.lean                |   1 +
 4 files changed, 76 insertions(+), 183 deletions(-)
 delete mode 100644 src/Iris/BI/BUpdAlt.lean

diff --git a/src/Iris/BI/BUpdAlt.lean b/src/Iris/BI/BUpdAlt.lean
deleted file mode 100644
index 8d351acc..00000000
--- a/src/Iris/BI/BUpdAlt.lean
+++ /dev/null
@@ -1,182 +0,0 @@
-import Iris.ProofMode
-import Iris.Instances.UPred.Instance
-
-namespace Iris
-open Iris.Std BI
-
--- This file contains an alternative version of basic updates, that is
--- expression in terms of just the plain modality [■]
-def bupd_alt [BI PROP] [BIPlainly PROP] (P : PROP) : PROP :=
-  iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
-
-section bupd_alt
-variable [BI PROP] [BIPlainly PROP]
-
-instance bupd_alt_ne : OFE.NonExpansive (bupd_alt (PROP := PROP)) where
-  ne n x1 x2 Hx := by
-    apply forall_ne
-    intro R
-    apply wand_ne.ne;
-    · apply wand_ne.ne
-      · exact Hx
-      · exact .rfl
-    · exact .rfl
-
--- The Laws of the basic update modality hold
-theorem bupd_alt_intro {P : PROP} : P ⊢ bupd_alt P := by
-  iintro Hp
-  unfold bupd_alt
-  iintro R H
-  ispecialize H Hp as H1
-  iexact H1
-
-theorem bupt_alt_mono {P Q : PROP} : (P ⊢ Q) → (bupd_alt P ⊢ bupd_alt Q) := by
-  intros H
-  unfold bupd_alt
-  iintro R HQR
-  iintro Hp
-  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
-    iintro H
-    iintro Hp
-    iapply H
-    apply H
-    done
-  iintro ⟨Ha, H2⟩
-  ispecialize Ha HQR
-  iapply Ha
-  iapply H1
-  iassumption
-
-theorem bupd_alt_trans {P : PROP} : bupd_alt (bupd_alt P) ⊢ bupd_alt P := by
-  unfold bupd_alt
-  iintro Hp R H
-  ispecialize Hp R as HpR
-  iapply HpR
-  iintro Hp
-  ispecialize Hp R as HpR2
-  iapply HpR2
-  iassumption
-
-theorem bupd_alt_frame_r {P Q : PROP} : bupd_alt P ∗ Q ⊢ (bupd_alt iprop(P ∗ Q)) := by
-  unfold bupd_alt
-  iintro ⟨Hp, Hq⟩ R H
-  ispecialize Hp R as HpR
-  iapply HpR
-  iintro Hp
-  iapply H
-  isplitl [Hp]
-  · iexact Hp
-  · iexact Hq
-
-theorem bupd_alt_plainly {P : PROP} : bupd_alt iprop(■ P) ⊢ (■ P) := by
-  unfold bupd_alt
-  iintro H
-  ispecialize H P as HP
-  iapply HP
-  iintro Hp
-  iexact Hp
-
--- Any modality confirming with [BiBUpdPlainly] entails the alternative definition
-theorem bupd_bupd_alt [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢  bupd_alt P := by
-  unfold bupd_alt
-  iintro HP (R) H
-  -- Eliminate the bupds (by hand, until iMod is implemented)
-  refine BIUpdate.frame_r.trans ?_
-  refine (BIUpdate.mono sep_symm).trans ?_
-  exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
-
--- We get the usual rule for frame preserving updates if we have an [own]
--- connective satisfying the following rule w.r.t. interaction with plainly.
-variable [UCMRA M] (own : M → PROP)
-variable (own_updateP_plainly :
-  ∀ (x : M) (Φ : M → Prop) (R : PROP),
-    (x ~~>: Φ) →
-    own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
-
--- Since own_updateP doesn't use `own_updateP_plainly` in the type,
--- need to explicitly include it
-include own_updateP_plainly
-theorem own_updateP {x : M} {Φ : M → Prop} :
-    (x ~~>: Φ) →
-    own x ⊢ bupd_alt iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
-  intro Hup
-  iintro Hx
-  unfold bupd_alt
-  iintro R H
-  iapply own_updateP_plainly x Φ R Hup
-  isplitl [Hx]
-  · iexact Hx
-  iintro y ⌜HΦ⌝
-  iintro Hy
-  iapply H
-  iexists y
-  isplit
-  · ipure_intro
-    exact HΦ
-  · iexact Hy
-
-end bupd_alt
-
--- Helper predicate for bupd_alt_bupd proof
-private def bupd_alt_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
-  holds k _ := ∃ x'', ✓{k} (x'' • y) ∧ P k x''
-  mono {_} := fun ⟨z, Hz1, Hz2⟩ _ Hn =>
-    ⟨z, CMRA.validN_of_le Hn Hz1, P.mono Hz2 (CMRA.incN_refl z) Hn⟩
-
--- The alternative definition entails the ordinary basic update
-theorem bupd_alt_bupd [UCMRA M] (P : UPred M) : bupd_alt P ⊢ |==> P := by
-  unfold bupd_alt bupd
-  intro n x Hx H
-  -- Unfold bupd definition in `Instance.lean`
-  intro k y Hkn Hxy
-  let R := bupd_alt_pred P y
-  have H_inst : iprop((P -∗ ■ R) -∗ ■ R).holds n x := H _ ⟨R, rfl⟩
-
-  have wand_holds : iprop(P -∗ ■ R).holds k y := by
-    intro k' z Hk' Hvyz HP
-    refine ⟨z, ?_, HP⟩
-    exact CMRA.validN_ne CMRA.op_commN Hvyz
-  exact H_inst k y Hkn Hxy wand_holds
-
-
-theorem bupd_alt_bupd_iff [UCMRA M] (P : UPred M) : bupd_alt P ⊣⊢ |==> P := by
-  refine ⟨?_, ?_⟩
-  · apply bupd_alt_bupd
-  · apply bupd_bupd_alt
-
--- The law about the interaction between [uPred_ownM] and plainly holds.
-theorem ownM_updateP [UCMRA M] (x : M) (Φ : M → Prop) (R : UPred M) :
-    (x ~~>: Φ) →
-    UPred.ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ UPred.ownM y -∗ ■ R) ⊢ ■ R := by
-  intro Hup
-  intro n z
-  intro Hv
-  -- x1 z2 are introduced for separating conjunction
-  -- (ownM x).holds n x1 := x ≼{n} x1, namely x · z1 = x1
-  intro ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
-  -- manually having ofe_subst, z ≡{n} (x • z1) • z2
-  have Hz_subst : z ≡{n}≡ (x • z1) • z2 := by
-    calc z ≡{n}≡ x1 • z2 := Hx
-         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
-
-  have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
-    show ✓{n} (x • (z1 • z2))
-    refine CMRA.validN_ne ?_ Hv
-    calc z ≡{n}≡ (x • z1) • z2 := Hz_subst
-         _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
-  have ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
-
-  have Hp := HR (iprop(⌜Φ y⌝ -∗ (UPred.ownM y -∗ ■ R))) ⟨y, rfl⟩
-
-  have Hv_z2z1 : ✓{n} (z2 • z1) := by
-    exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
-
-  have Hp1 : iprop(UPred.ownM y -∗ ■ R).holds n (z2 • z1) := Hp n z1 (Nat.le_refl _) Hv_z2z1 HΦy
-
-  have Hv_z2z1y : ✓{n} ((z2 • z1) • y) := by
-    apply CMRA.validN_ne ?_ Hvalid_y
-    calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
-         _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
-
-  have Hy_incl : y ≼{n} y := CMRA.incN_refl y
-  exact Hp1 n y (Nat.le_refl _) Hv_z2z1y Hy_incl
diff --git a/src/Iris/BI/Plainly.lean b/src/Iris/BI/Plainly.lean
index c327f37f..c8b49fb4 100644
--- a/src/Iris/BI/Plainly.lean
+++ b/src/Iris/BI/Plainly.lean
@@ -302,7 +302,6 @@ theorem impl_wand_plainly : (■ P → Q) ⊣⊢ (■ P -∗ Q) :=
 
 end AffineBI
 
--- Typeclass instances
 instance plainly_absorbing (P : PROP) : Absorbing iprop(■ P) where
   absorbing := absorbingly_elim_plainly.1
 
diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index 3ee48c68..e39fb263 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -9,6 +9,7 @@ import Iris.Algebra.OFE
 import Iris.Algebra.CMRA
 import Iris.Algebra.UPred
 import Iris.Algebra.Updates
+import Iris.ProofMode.BupdPlain
 
 section UPredInstance
 
@@ -493,3 +494,77 @@ instance : BIAffine (UPred M) := ⟨by infer_instance⟩
 -- TODO: Port derived lemmas
 
 end UPred
+
+section UPredAlt
+
+open BUpdPlain
+
+/-
+## Compatibility between the UPred model of BUpd and the BUpd construction for generic BIPlainly instances
+-/
+
+-- Helper predicate for BUpdPlain_bupd proof
+private def BUpdPlain_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
+  holds k _ := ∃ x'', ✓{k} (x'' • y) ∧ P k x''
+  mono {_} := fun ⟨z, Hz1, Hz2⟩ _ Hn =>
+    ⟨z, CMRA.validN_of_le Hn Hz1, P.mono Hz2 (CMRA.incN_refl z) Hn⟩
+
+-- The alternative definition entails the ordinary basic update
+theorem BUpdPlain_bupd [UCMRA M] (P : UPred M) : BUpdPlain P ⊢ |==> P := by
+  unfold BUpdPlain bupd
+  intro n x Hx H
+  -- Unfold bupd definition in `Instance.lean`
+  intro k y Hkn Hxy
+  let R := BUpdPlain_pred P y
+  have H_inst : iprop((P -∗ ■ R) -∗ ■ R).holds n x := H _ ⟨R, rfl⟩
+
+  have wand_holds : iprop(P -∗ ■ R).holds k y := by
+    intro k' z Hk' Hvyz HP
+    refine ⟨z, ?_, HP⟩
+    exact CMRA.validN_ne CMRA.op_commN Hvyz
+  exact H_inst k y Hkn Hxy wand_holds
+
+
+theorem BUpdPlain_bupd_iff [UCMRA M] (P : UPred M) : BUpdPlain P ⊣⊢ |==> P := by
+  refine ⟨?_, ?_⟩
+  · apply BUpdPlain_bupd
+  · apply bupd_BUpdPlain
+
+-- The law about the interaction between [uPred_ownM] and plainly holds.
+theorem ownM_updateP [UCMRA M] (x : M) (Φ : M → Prop) (R : UPred M) :
+    (x ~~>: Φ) →
+    UPred.ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ UPred.ownM y -∗ ■ R) ⊢ ■ R := by
+  intro Hup
+  intro n z
+  intro Hv
+  -- x1 z2 are introduced for separating conjunction
+  -- (ownM x).holds n x1 := x ≼{n} x1, namely x · z1 = x1
+  intro ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
+  -- manually having ofe_subst, z ≡{n} (x • z1) • z2
+  have Hz_subst : z ≡{n}≡ (x • z1) • z2 := by
+    calc z ≡{n}≡ x1 • z2 := Hx
+         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
+
+  have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
+    show ✓{n} (x • (z1 • z2))
+    refine CMRA.validN_ne ?_ Hv
+    calc z ≡{n}≡ (x • z1) • z2 := Hz_subst
+         _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
+  have ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
+
+  have Hp := HR (iprop(⌜Φ y⌝ -∗ (UPred.ownM y -∗ ■ R))) ⟨y, rfl⟩
+
+  have Hv_z2z1 : ✓{n} (z2 • z1) := by
+    exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
+
+  have Hp1 : iprop(UPred.ownM y -∗ ■ R).holds n (z2 • z1) := Hp n z1 (Nat.le_refl _) Hv_z2z1 HΦy
+
+  have Hv_z2z1y : ✓{n} ((z2 • z1) • y) := by
+    apply CMRA.validN_ne ?_ Hvalid_y
+    calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
+         _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
+
+  have Hy_incl : y ≼{n} y := CMRA.incN_refl y
+  exact Hp1 n y (Nat.le_refl _) Hv_z2z1y Hy_incl
+
+section UPredAlt
diff --git a/src/Iris/ProofMode.lean b/src/Iris/ProofMode.lean
index 31024ef7..6c2814a0 100644
--- a/src/Iris/ProofMode.lean
+++ b/src/Iris/ProofMode.lean
@@ -5,3 +5,4 @@ import Iris.ProofMode.Instances
 import Iris.ProofMode.Patterns
 import Iris.ProofMode.Tactics
 import Iris.ProofMode.UnifHints
+import Iris.ProofMode.BupdPlain

From c5282a8670ad0514d576bf7132741dcb2ea4192c Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 19 Dec 2025 09:21:15 -0500
Subject: [PATCH 12/16] chore: cleanup

---
 src/Iris/Instances/UPred/Instance.lean | 70 +++++++-------------------
 1 file changed, 19 insertions(+), 51 deletions(-)

diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index e39fb263..d58d7db6 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -497,74 +497,42 @@ end UPred
 
 section UPredAlt
 
-open BUpdPlain
+open BUpdPlain CMRA UPred
 
 /-
 ## Compatibility between the UPred model of BUpd and the BUpd construction for generic BIPlainly instances
 -/
 
--- Helper predicate for BUpdPlain_bupd proof
-private def BUpdPlain_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
+def BUpdPlain_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
   holds k _ := ∃ x'', ✓{k} (x'' • y) ∧ P k x''
   mono {_} := fun ⟨z, Hz1, Hz2⟩ _ Hn =>
-    ⟨z, CMRA.validN_of_le Hn Hz1, P.mono Hz2 (CMRA.incN_refl z) Hn⟩
+    ⟨z, validN_of_le Hn Hz1, P.mono Hz2 (incN_refl z) Hn⟩
 
--- The alternative definition entails the ordinary basic update
+/-- The alternative definition entails the ordinary basic update -/
 theorem BUpdPlain_bupd [UCMRA M] (P : UPred M) : BUpdPlain P ⊢ |==> P := by
-  unfold BUpdPlain bupd
-  intro n x Hx H
-  -- Unfold bupd definition in `Instance.lean`
-  intro k y Hkn Hxy
-  let R := BUpdPlain_pred P y
-  have H_inst : iprop((P -∗ ■ R) -∗ ■ R).holds n x := H _ ⟨R, rfl⟩
-
-  have wand_holds : iprop(P -∗ ■ R).holds k y := by
-    intro k' z Hk' Hvyz HP
-    refine ⟨z, ?_, HP⟩
-    exact CMRA.validN_ne CMRA.op_commN Hvyz
-  exact H_inst k y Hkn Hxy wand_holds
-
-
-theorem BUpdPlain_bupd_iff [UCMRA M] (P : UPred M) : BUpdPlain P ⊣⊢ |==> P := by
-  refine ⟨?_, ?_⟩
-  · apply BUpdPlain_bupd
-  · apply bupd_BUpdPlain
-
--- The law about the interaction between [uPred_ownM] and plainly holds.
-theorem ownM_updateP [UCMRA M] (x : M) (Φ : M → Prop) (R : UPred M) :
-    (x ~~>: Φ) →
-    UPred.ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ UPred.ownM y -∗ ■ R) ⊢ ■ R := by
-  intro Hup
-  intro n z
-  intro Hv
-  -- x1 z2 are introduced for separating conjunction
-  -- (ownM x).holds n x1 := x ≼{n} x1, namely x · z1 = x1
-  intro ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
-  -- manually having ofe_subst, z ≡{n} (x • z1) • z2
-  have Hz_subst : z ≡{n}≡ (x • z1) • z2 := by
-    calc z ≡{n}≡ x1 • z2 := Hx
-         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
+  intro n x Hx H k y Hkn Hxy
+  refine (H _ ⟨BUpdPlain_pred P y, rfl⟩) k y Hkn Hxy ?_
+  intro _ z _ Hvyz HP
+  refine ⟨z, validN_ne op_commN Hvyz, HP⟩
+
+theorem BUpdPlain_bupd_iff [UCMRA M] (P : UPred M) : BUpdPlain P ⊣⊢ |==> P :=
+  ⟨BUpdPlain_bupd P, BUpd_BUpdPlain⟩
 
+theorem ownM_updateP [UCMRA M] {x : M} {R : UPred M} (Φ : M → Prop) (Hup : x ~~>: Φ) :
+    ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ ownM y -∗ ■ R) ⊢ ■ R := by
+  intro n z Hv ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
   have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
     show ✓{n} (x • (z1 • z2))
     refine CMRA.validN_ne ?_ Hv
-    calc z ≡{n}≡ (x • z1) • z2 := Hz_subst
+    calc z ≡{n}≡ x1 • z2 := Hx
+         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
          _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
   have ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
-
   have Hp := HR (iprop(⌜Φ y⌝ -∗ (UPred.ownM y -∗ ■ R))) ⟨y, rfl⟩
-
-  have Hv_z2z1 : ✓{n} (z2 • z1) := by
-    exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
-
-  have Hp1 : iprop(UPred.ownM y -∗ ■ R).holds n (z2 • z1) := Hp n z1 (Nat.le_refl _) Hv_z2z1 HΦy
-
-  have Hv_z2z1y : ✓{n} ((z2 • z1) • y) := by
-    apply CMRA.validN_ne ?_ Hvalid_y
+  refine Hp n z1 (Nat.le_refl _) ?_ HΦy n y (Nat.le_refl _) ?_ (incN_refl y)
+  · exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
+  · apply CMRA.validN_ne ?_ Hvalid_y
     calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
          _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
 
-  have Hy_incl : y ≼{n} y := CMRA.incN_refl y
-  exact Hp1 n y (Nat.le_refl _) Hv_z2z1y Hy_incl
-
 section UPredAlt

From f86ead6938037e9e586548821e687dc120b9fa83 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 19 Dec 2025 09:21:35 -0500
Subject: [PATCH 13/16] add new file

---
 src/Iris/ProofMode/BUpdPlain.lean | 116 ++++++++++++++++++++++++++++++
 1 file changed, 116 insertions(+)
 create mode 100644 src/Iris/ProofMode/BUpdPlain.lean

diff --git a/src/Iris/ProofMode/BUpdPlain.lean b/src/Iris/ProofMode/BUpdPlain.lean
new file mode 100644
index 00000000..b68d7c94
--- /dev/null
+++ b/src/Iris/ProofMode/BUpdPlain.lean
@@ -0,0 +1,116 @@
+import Iris.Std
+import Iris.BI
+import Iris.Algebra.Updates
+import Iris.ProofMode.Classes
+import Iris.ProofMode.Tactics
+import Iris.ProofMode.Display
+
+namespace Iris
+open Iris.Std BI
+
+/-! This file contains an alternative version of basic updates.
+
+Namely, this definition is an expression in terms of the plain modality [■],
+which can be used to instanstiate BUpd for any BIPlainly BI.
+
+cf. https://gitlab.mpi-sws.org/iris/iris/merge_requests/211
+-/
+
+namespace BUpdPlain
+
+def BUpdPlain [BIBase PROP] [Plainly PROP] (P : PROP) : PROP :=
+  iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
+
+section BupdPlainDef
+
+open OFE
+
+variable [BI PROP] [BIPlainly PROP]
+
+instance BUpdPlain_ne : NonExpansive (BUpdPlain (PROP := PROP)) where
+  ne _ _ _ H := forall_ne fun _ => wand_ne.ne (wand_ne.ne H .rfl) .rfl
+
+theorem BUpdPlain_intro {P : PROP} : P ⊢ BUpdPlain P := by
+  iintro Hp
+  unfold BUpdPlain
+  iintro _ H
+  iapply H
+  iexact Hp
+
+theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q) := by
+  intros H
+  unfold BUpdPlain
+  iintro R HQR
+  iintro Hp
+  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
+    iintro H
+    iintro Hp
+    iapply H
+    apply H
+  iintro ⟨Ha, H2⟩
+  ispecialize Ha HQR
+  iapply Ha
+  iapply H1
+  iexact H2
+
+theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
+  unfold BUpdPlain
+  iintro Hp R H
+  ispecialize Hp R as HpR
+  iapply HpR
+  iintro Hp
+  ispecialize Hp R as HpR2
+  iapply HpR2
+  iassumption
+
+theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(P ∗ Q)) := by
+  unfold BUpdPlain
+  iintro ⟨Hp, Hq⟩ R H
+  ispecialize Hp R as HpR
+  iapply HpR
+  iintro Hp
+  iapply H
+  isplitl [Hp]
+  · iexact Hp
+  · iexact Hq
+
+theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
+  unfold BUpdPlain
+  iintro H
+  ispecialize H P as HP
+  iapply HP
+  exact wand_rfl
+
+/- BiBUpdPlainly entails the alternative definition -/
+theorem BUpd_BUpdPlain [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢ BUpdPlain P := by
+  unfold BUpdPlain
+  iintro _ _ _
+  refine BIUpdate.frame_r.trans ?_
+  refine (BIUpdate.mono sep_symm).trans ?_
+  exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
+
+-- We get the usual rule for frame preserving updates if we have an [own]
+-- connective satisfying the following rule w.r.t. interaction with plainly.
+
+theorem own_updateP [UCMRA M] {own : M → PROP} {x : M} {Φ : M → Prop}
+  (own_updateP_plainly : ∀ (x : M) (Φ : M → Prop) (R : PROP),
+    (x ~~>: Φ) → own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
+  (Hup : x ~~>: Φ) :
+    own x ⊢ BUpdPlain iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
+  iintro Hx
+  unfold BUpdPlain
+  iintro R H
+  iapply own_updateP_plainly x Φ R Hup
+  isplitl [Hx]
+  · iexact Hx
+  iintro y ⌜HΦ⌝
+  iintro Hy
+  iapply H
+  iexists y
+  isplit
+  · ipure_intro
+    exact HΦ
+  · iexact Hy
+
+end BupdPlainDef
+end BUpdPlain

From c4cb3b79fc31bf4b41ca7b0480e9ebf2aeee7f7a Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 19 Dec 2025 09:34:28 -0500
Subject: [PATCH 14/16] fix: for CI

---
 src/Iris/Instances/UPred/Instance.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index d58d7db6..557720b4 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -9,7 +9,7 @@ import Iris.Algebra.OFE
 import Iris.Algebra.CMRA
 import Iris.Algebra.UPred
 import Iris.Algebra.Updates
-import Iris.ProofMode.BupdPlain
+import Iris.ProofMode.BUpdPlain
 
 section UPredInstance
 

From 9f7d25e0052fc9eace10d9d98babe493c9d0e8ab Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 19 Dec 2025 09:40:27 -0500
Subject: [PATCH 15/16] chore: fix build

---
 src/Iris/Examples/Resources.lean | 1 -
 src/Iris/ProofMode.lean          | 1 -
 2 files changed, 2 deletions(-)

diff --git a/src/Iris/Examples/Resources.lean b/src/Iris/Examples/Resources.lean
index b3f26e50..9fe30d7f 100644
--- a/src/Iris/Examples/Resources.lean
+++ b/src/Iris/Examples/Resources.lean
@@ -3,7 +3,6 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
-import Iris.BI
 import Iris.ProofMode
 import Iris.Algebra.IProp
 import Iris.Instances.UPred.Instance
diff --git a/src/Iris/ProofMode.lean b/src/Iris/ProofMode.lean
index 6c2814a0..31024ef7 100644
--- a/src/Iris/ProofMode.lean
+++ b/src/Iris/ProofMode.lean
@@ -5,4 +5,3 @@ import Iris.ProofMode.Instances
 import Iris.ProofMode.Patterns
 import Iris.ProofMode.Tactics
 import Iris.ProofMode.UnifHints
-import Iris.ProofMode.BupdPlain

From 6caa6e7a2c01303b234021d0145debf807fa4456 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 19 Dec 2025 23:01:24 -0500
Subject: [PATCH 16/16] move BUpdPlain to BI/Lib

---
 src/Iris/BI/Lib/BUpdPlain.lean         | 116 +++++++++++++++++++++++++
 src/Iris/Instances/UPred/Instance.lean |   2 +-
 2 files changed, 117 insertions(+), 1 deletion(-)
 create mode 100644 src/Iris/BI/Lib/BUpdPlain.lean

diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
new file mode 100644
index 00000000..b68d7c94
--- /dev/null
+++ b/src/Iris/BI/Lib/BUpdPlain.lean
@@ -0,0 +1,116 @@
+import Iris.Std
+import Iris.BI
+import Iris.Algebra.Updates
+import Iris.ProofMode.Classes
+import Iris.ProofMode.Tactics
+import Iris.ProofMode.Display
+
+namespace Iris
+open Iris.Std BI
+
+/-! This file contains an alternative version of basic updates.
+
+Namely, this definition is an expression in terms of the plain modality [■],
+which can be used to instanstiate BUpd for any BIPlainly BI.
+
+cf. https://gitlab.mpi-sws.org/iris/iris/merge_requests/211
+-/
+
+namespace BUpdPlain
+
+def BUpdPlain [BIBase PROP] [Plainly PROP] (P : PROP) : PROP :=
+  iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
+
+section BupdPlainDef
+
+open OFE
+
+variable [BI PROP] [BIPlainly PROP]
+
+instance BUpdPlain_ne : NonExpansive (BUpdPlain (PROP := PROP)) where
+  ne _ _ _ H := forall_ne fun _ => wand_ne.ne (wand_ne.ne H .rfl) .rfl
+
+theorem BUpdPlain_intro {P : PROP} : P ⊢ BUpdPlain P := by
+  iintro Hp
+  unfold BUpdPlain
+  iintro _ H
+  iapply H
+  iexact Hp
+
+theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q) := by
+  intros H
+  unfold BUpdPlain
+  iintro R HQR
+  iintro Hp
+  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
+    iintro H
+    iintro Hp
+    iapply H
+    apply H
+  iintro ⟨Ha, H2⟩
+  ispecialize Ha HQR
+  iapply Ha
+  iapply H1
+  iexact H2
+
+theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
+  unfold BUpdPlain
+  iintro Hp R H
+  ispecialize Hp R as HpR
+  iapply HpR
+  iintro Hp
+  ispecialize Hp R as HpR2
+  iapply HpR2
+  iassumption
+
+theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(P ∗ Q)) := by
+  unfold BUpdPlain
+  iintro ⟨Hp, Hq⟩ R H
+  ispecialize Hp R as HpR
+  iapply HpR
+  iintro Hp
+  iapply H
+  isplitl [Hp]
+  · iexact Hp
+  · iexact Hq
+
+theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
+  unfold BUpdPlain
+  iintro H
+  ispecialize H P as HP
+  iapply HP
+  exact wand_rfl
+
+/- BiBUpdPlainly entails the alternative definition -/
+theorem BUpd_BUpdPlain [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢ BUpdPlain P := by
+  unfold BUpdPlain
+  iintro _ _ _
+  refine BIUpdate.frame_r.trans ?_
+  refine (BIUpdate.mono sep_symm).trans ?_
+  exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
+
+-- We get the usual rule for frame preserving updates if we have an [own]
+-- connective satisfying the following rule w.r.t. interaction with plainly.
+
+theorem own_updateP [UCMRA M] {own : M → PROP} {x : M} {Φ : M → Prop}
+  (own_updateP_plainly : ∀ (x : M) (Φ : M → Prop) (R : PROP),
+    (x ~~>: Φ) → own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
+  (Hup : x ~~>: Φ) :
+    own x ⊢ BUpdPlain iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
+  iintro Hx
+  unfold BUpdPlain
+  iintro R H
+  iapply own_updateP_plainly x Φ R Hup
+  isplitl [Hx]
+  · iexact Hx
+  iintro y ⌜HΦ⌝
+  iintro Hy
+  iapply H
+  iexists y
+  isplit
+  · ipure_intro
+    exact HΦ
+  · iexact Hy
+
+end BupdPlainDef
+end BUpdPlain
diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index 557720b4..ceab2607 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -9,7 +9,7 @@ import Iris.Algebra.OFE
 import Iris.Algebra.CMRA
 import Iris.Algebra.UPred
 import Iris.Algebra.Updates
-import Iris.ProofMode.BUpdPlain
+import Iris.BI.Lib.BUpdPlain
 
 section UPredInstance