Bupdalt

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

src/Iris/BI/Plainly.lean

@@ -302,6 +302,9 @@ theorem impl_wand_plainly : (■ P → Q) ⊣⊢ (■ P -∗ Q) :=
 
 end AffineBI
 
+instance plainly_absorbing (P : PROP) : Absorbing iprop(■ P) where
+  absorbing := absorbingly_elim_plainly.1
+
 end PlainlyLaws
 
 end Iris.BI

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

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.BI.Lib.BUpdPlain
 
 section UPredInstance
 
@@ -493,3 +494,45 @@ instance : BIAffine (UPred M) := ⟨by infer_instance⟩
 -- TODO: Port derived lemmas
 
 end UPred
+
+section UPredAlt
+
+open BUpdPlain CMRA UPred
+
+/-
+## Compatibility between the UPred model of BUpd and the BUpd construction for generic BIPlainly instances
+-/
+
+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, validN_of_le Hn Hz1, P.mono Hz2 (incN_refl z) Hn⟩
+
+/-- The alternative definition entails the ordinary basic update -/
+theorem BUpdPlain_bupd [UCMRA M] (P : UPred M) : BUpdPlain P ⊢ |==> P := by
+  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}≡ 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⟩
+  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
+
+section UPredAlt

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