feat: SBI (#181)

Author: markusdemedeiros

PORTING.md

@@ -454,11 +454,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 ## Examples
 
 - SI Logic 
-  - [ ] `si_logic/siprop.v`
-  - [ ] `si_logic/bi.v`
-    - [ ] BI instance 
-    - [ ] BI Persistently instance
-    - [ ] BI Later instance
+  - [x] `si_logic/siprop.v`
+  - [x] `si_logic/bi.v`
+    - [x] BI instance 
+    - [x] BI Persistently instance
+    - [x] BI Later instance
 
 - Program Logic
   - Final decisions about what to port from this folder have not been made yet.

src/Iris/BI.lean

@@ -8,3 +8,4 @@ public import Iris.BI.Instances
 public import Iris.BI.BI
 public import Iris.BI.Notation
 public import Iris.BI.Updates
+public import Iris.BI.Cmra

src/Iris/BI/BIBase.lean

@@ -309,3 +309,28 @@ macro_rules
 
 delab_rule except0
   | `($_ $P) => do ``(iprop(◇ $(← unpackIprop P)))
+
+
+/-- Plainly modality -/
+class Plainly (PROP : Type _) where
+  plainly : PROP → PROP
+export Plainly (plainly)
+
+syntax "■ " term:40 : term
+
+macro_rules
+  | `(iprop(■ $P))  => ``(Plainly.plainly iprop($P))
+
+delab_rule Plainly.plainly
+  | `($_ $P) => do ``(iprop(■ $(← Iris.BI.unpackIprop P)))
+
+def Plainly.plainlyIf [BIBase PROP] [Plainly PROP] (p : Bool) (P : PROP) : PROP :=
+  iprop(if p then ■ P else P)
+
+syntax:max "■?" term:max ppHardSpace term:40 : term
+
+macro_rules
+  | `(iprop(■? $p $P))  => ``(Plainly.plainlyIf $p iprop($P))
+
+delab_rule Plainly.plainlyIf
+  | `($_ $p $P) => do ``(iprop(■? $p $(← Iris.BI.unpackIprop P)))

src/Iris/BI/Cmra.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.BI.Sbi
+public import Iris.BI.Plainly
+public import Iris.Std.RocqAlias
+
+@[expose] public section
+
+/-!
+# Generic CMRA validity in a BI logic
+
+This file defines the generic internal CMRA validity for any `Sbi PROP`,
+as `<si_pure> cmraValid a`.
+-/
+
+namespace Iris
+open BI OFE SiProp CMRA Sbi
+
+section CmraValid
+
+variable [Sbi PROP] [CMRA A]
+
+@[rocq_alias internal_cmra_valid]
+def internalCmraValid (a : A) : PROP := siPure (cmraValid a)
+
+@[rocq_alias internal_cmra_valid_ne]
+instance internalCmraValid_ne : NonExpansive (internalCmraValid (PROP := PROP) (A := A)) where
+  ne _ _ _ h := siPure_ne.ne (instNonExpansiveCmraValid.ne h)
+
+@[rocq_alias internal_cmra_valid_intro]
+theorem internalCmraValid_intro {P : PROP} {a : A} (h : Valid a) :
+    P ⊢ internalCmraValid a :=
+  calc (P : PROP)
+    _ ⊢ True := true_intro
+    _ ⊢ <si_pure> True := siPure_pure.mpr
+    _ ⊢ internalCmraValid a := siPure_mono (cmraValid_intro h)
+
+@[rocq_alias internal_cmra_valid_elim]
+theorem internalCmraValid_elim (a : A) : internalCmraValid a ⊢@{PROP} ⌜✓{0} a⌝ :=
+  calc internalCmraValid a
+    _ ⊢ <si_pure> ⌜✓{0} a⌝ := siPure_mono cmraValid_elim
+    _ ⊢ ⌜✓{0} a⌝ := siPure_pure.mp
+
+@[rocq_alias internal_cmra_valid_weaken]
+theorem internalCmraValid_weaken {a b : A} :
+    internalCmraValid (a • b) ⊢@{PROP} internalCmraValid a :=
+  siPure_mono cmraValid_weaken
+
+@[rocq_alias internal_cmra_valid_entails]
+theorem internalCmraValid_entails [CMRA B] {a : A} {b : B} :
+    (internalCmraValid a ⊢@{PROP} internalCmraValid b) ↔ ∀ n, ✓{n} a → ✓{n} b :=
+  siPure_entails.trans cmraValid_entails_iff
+
+@[rocq_alias si_pure_internal_cmra_valid]
+theorem siPure_internalCmraValid {a : A} : <si_pure> cmraValid a ⊣⊢@{PROP} internalCmraValid a :=
+  .rfl
+
+@[rocq_alias persistently_internal_cmra_valid]
+theorem persistently_internalCmraValid {a : A} :
+    <pers> internalCmraValid a ⊣⊢@{PROP} internalCmraValid a :=
+  persistently_siPure
+
+@[rocq_alias plainly_internal_cmra_valid]
+theorem plainly_internalCmraValid (a : A) :
+    ■ internalCmraValid a ⊣⊢@{PROP} internalCmraValid a :=
+  plainly_siPure
+
+@[rocq_alias intuitionistically_internal_cmra_valid]
+theorem intuitionistically_internalCmraValid [BIAffine PROP] {a : A} :
+    □ internalCmraValid a ⊣⊢@{PROP} internalCmraValid a :=
+  intuitionistically_iff_persistently.trans persistently_internalCmraValid
+
+@[rocq_alias internal_cmra_valid_discrete]
+theorem internalCmraValid_discrete [CMRA.Discrete A] {a : A} :
+    internalCmraValid a ⊣⊢@{PROP} ⌜✓ a⌝ :=
+  ⟨(internalCmraValid_elim a).trans <| pure_mono (discrete_valid ·),
+   pure_elim' internalCmraValid_intro⟩
+
+@[rocq_alias internal_cmra_valid_persistent]
+instance internalCmraValid_persistent (a : A) :
+    Persistent (PROP := PROP) (internalCmraValid a) where
+  persistent := persistently_internalCmraValid.mpr
+
+@[rocq_alias internal_cmra_valid_absorbing]
+instance internalCmraValid_absorbing (a : A) :
+    Absorbing (PROP := PROP) (internalCmraValid a) :=
+  siPure_absorbing _
+
+@[rocq_alias internal_cmra_valid_plain]
+instance internalCmraValid_plain (a : A) :
+    Plain (PROP := PROP) (internalCmraValid a) where
+  plain := plainly_internalCmraValid a |>.mpr
+
+end CmraValid
+
+end Iris

src/Iris/BI/Extensions.lean

@@ -27,6 +27,9 @@ class BILoeb (PROP : Type _) [BI PROP] where
 
 class BILaterContractive (PROP : Type _) [BI PROP] extends OFE.Contractive later (α := PROP)
 
+class BIPureForall (PROP : Type _) [BI PROP] where
+  pure_forall_2 : ∀ {α : Sort _} (φ : α → Prop), (∀ a, ⌜φ a⌝) ⊢@{PROP} ⌜∀ a, φ a⌝
+
 class BIPersistentlyForall (PROP : Type _) [BI PROP] where
   persistently_sForall_2 (Ψ : PROP → Prop) : (∀ p, ⌜Ψ p⌝ → <pers> p) ⊢ <pers> (sForall Ψ)
 

src/Iris/BI/Lib/BUpdPlain.lean

@@ -16,21 +16,21 @@ 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.
+which can be used to instantiate BUpd for any Sbi BI.
 
 cf. https://gitlab.mpi-sws.org/iris/iris/merge_requests/211
 -/
 
 namespace BUpdPlain
 
-def BUpdPlain [BIBase PROP] [Plainly PROP] (P : PROP) : PROP :=
+def BUpdPlain [BIBase PROP] [BIBase.Plainly PROP] (P : PROP) : PROP :=
   iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
 
 section BupdPlainDef
 
 open OFE
 
-variable [BI PROP] [BIPlainly PROP]
+variable [Sbi PROP]
 
 instance BUpdPlain_ne : NonExpansive (BUpdPlain (PROP := PROP)) where
   ne _ _ _ H := forall_ne fun _ => wand_ne.ne (wand_ne.ne H .rfl) .rfl