Big ops

src/Iris/Algebra.lean

@@ -1,8 +1,10 @@
 import Iris.Algebra.Agree
+import Iris.Algebra.BigOp
 import Iris.Algebra.CMRA
 import Iris.Algebra.COFESolver
 import Iris.Algebra.OFE
 import Iris.Algebra.Frac
 import Iris.Algebra.Heap
 import Iris.Algebra.View
 import Iris.Algebra.HeapView
+import Iris.Algebra.Monoid

src/Iris/Algebra/CMRA.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Сухарик (@suhr), Markus de Medeiros
 -/
 import Iris.Algebra.OFE
+import Iris.Algebra.Monoid
 
 namespace Iris
 open OFE
@@ -731,6 +732,12 @@ instance empty_cancelable : Cancelable (unit : α) where
 theorem _root_.Iris.OFE.Dist.to_incN {n} {x y : α} (H : x ≡{n}≡ y) : x ≼{n} y :=
   ⟨unit, ((equiv_dist.mp unit_right_id n).trans H).symm⟩
 
+instance cmra_monoid : Algebra.Monoid α (@op α _) unit where
+  op_ne.ne := fun {_n} {_x₁ _x₂} hx {_y₁ _y₂} hy => Dist.op hx hy
+  op_assoc _ _ _ := assoc.symm
+  op_comm _ _ := comm
+  op_left_id _ := unit_left_id
+
 end ucmra
 
 

src/Iris/Algebra/Monoid.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2025 Zongyuan Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zongyuan Liu
+-/
+import Iris.Algebra.OFE
+
+namespace Iris.Algebra
+
+/-! # Monoids for Big Operators
+
+This file defines monoid structures for big operators, following the Iris/Rocq approach.
+
+The key design decisions (matching Rocq):
+- `Monoid` contains the laws and requires an OFE structure
+- The operation must be non-expansive (`NonExpansive₂`)
+- We use explicit `op` and `unit` parameters to support multiple monoids on the same type
+  (e.g., on BIs we have monoids for `∗`/`emp`, `∧`/`True`, and `∨`/`False`)
+-/
+
+open OFE
+
+/-! ## Monoid Class -/
+
+/-- A commutative monoid on an OFE, used for big operators.
+The operation must be non-expansive, associative, commutative, and have a left identity.
+
+The operation `op` and unit `unit` are explicit parameters (not fields) to support
+multiple monoids on the same type. -/
+class Monoid (M : Type u) [OFE M] (op : M → M → M) (unit : outParam M) where
+  /-- The operation is non-expansive in both arguments -/
+  op_ne : NonExpansive₂ op
+  /-- Associativity up to equivalence -/
+  op_assoc : ∀ a b c : M, op (op a b) c ≡ op a (op b c)
+  /-- Commutativity up to equivalence -/
+  op_comm : ∀ a b : M, op a b ≡ op b a
+  /-- Left identity up to equivalence -/
+  op_left_id : ∀ a : M, op unit a ≡ a
+
+namespace Monoid
+
+attribute [simp] op_left_id
+
+variable {M : Type u} [OFE M] {op : M → M → M}
+
+/-- The operation is proper with respect to equivalence. -/
+theorem op_proper {unit : M} [Monoid M op unit] {a a' b b' : M}
+    (ha : a ≡ a') (hb : b ≡ b') : op a b ≡ op a' b' := by
+  haveI : NonExpansive₂ op := op_ne
+  exact NonExpansive₂.eqv ha hb
+
+/-- Right identity follows from commutativity and left identity. -/
+@[simp] theorem op_right_id {unit : M} [Monoid M op unit] (a : M) : op a unit ≡ a :=
+  Equiv.trans (op_comm (unit := unit) a unit) (op_left_id a)
+
+/-- Congruence on the left argument. -/
+theorem op_congr_l {unit : M} [Monoid M op unit] {a a' b : M} (h : a ≡ a') : op a b ≡ op a' b :=
+  op_proper (unit := unit) h Equiv.rfl
+
+/-- Congruence on the right argument. -/
+theorem op_congr_r {unit : M} [Monoid M op unit] {a b b' : M} (h : b ≡ b') : op a b ≡ op a b' :=
+  op_proper (unit := unit) Equiv.rfl h
+
+/-- Rearrange `(a * b) * (c * d)` to `(a * c) * (b * d)`. -/
+theorem op_op_swap {unit : M} [Monoid M op unit] {a b c d : M} :
+    op (op a b) (op c d) ≡ op (op a c) (op b d) :=
+  calc op (op a b) (op c d)
+      _ ≡ op a (op b (op c d)) := op_assoc a b (op c d)
+      _ ≡ op a (op (op b c) d) := op_congr_r (Equiv.symm (op_assoc b c d))
+      _ ≡ op a (op (op c b) d) := op_congr_r (op_congr_l (op_comm b c))
+      _ ≡ op a (op c (op b d)) := op_congr_r (op_assoc c b d)
+      _ ≡ op (op a c) (op b d) := Equiv.symm (op_assoc a c (op b d))
+
+/-- Swap inner elements: `a * (b * c)` to `b * (a * c)`. -/
+theorem op_swap_inner {unit : M} [Monoid M op unit] {a b c : M} :
+    op a (op b c) ≡ op b (op a c) :=
+  calc op a (op b c)
+      _ ≡ op (op a b) c := Equiv.symm (op_assoc a b c)
+      _ ≡ op (op b a) c := op_congr_l (op_comm a b)
+      _ ≡ op b (op a c) := op_assoc b a c
+
+/-- Non-expansiveness for dist. -/
+theorem op_ne_dist {unit : M} [Monoid M op unit] {n : Nat} {a a' b b' : M}
+    (ha : a ≡{n}≡ a') (hb : b ≡{n}≡ b') : op a b ≡{n}≡ op a' b' := by
+  haveI : NonExpansive₂ op := op_ne
+  exact NonExpansive₂.ne ha hb
+
+end Monoid
+
+/-! ## Monoid Homomorphisms -/
+
+/-- A weak monoid homomorphism preserves the operation but not necessarily the unit.
+This is useful for connectives like `own` where we only have `True ==∗ own γ ∅`,
+not `True ↔ own γ ∅`. -/
+class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]
+    (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂)
+    [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂]
+    (R : M₂ → M₂ → Prop) (f : M₁ → M₂) where
+  /-- The relation is reflexive -/
+  rel_refl : ∀ a : M₂, R a a
+  /-- The relation is transitive -/
+  rel_trans : ∀ {a b c : M₂}, R a b → R b c → R a c
+  /-- The relation is proper with respect to equivalence -/
+  rel_proper : ∀ {a a' b b' : M₂}, a ≡ a' → b ≡ b' → (R a b ↔ R a' b')
+  /-- The operation is proper with respect to R -/
+  op_proper : ∀ {a a' b b' : M₂}, R a a' → R b b' → R (op₂ a b) (op₂ a' b')
+  /-- The function is non-expansive -/
+  f_ne : NonExpansive f
+  /-- The homomorphism property -/
+  homomorphism : ∀ x y, R (f (op₁ x y)) (op₂ (f x) (f y))
+
+/-- A monoid homomorphism preserves both the operation and the unit. -/
+class MonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]
+    (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂)
+    [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂]
+    (R : M₂ → M₂ → Prop) (f : M₁ → M₂)
+    extends WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f where
+  /-- The unit is preserved -/
+  map_unit : R (f unit₁) unit₂
+
+end Iris.Algebra

src/Iris/BI.lean

@@ -5,3 +5,4 @@ import Iris.BI.Instances
 import Iris.BI.BI
 import Iris.BI.Notation
 import Iris.BI.Updates
+import Iris.BI.BigOps

src/Iris/BI/BI.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Mario Carneiro
+Authors: Lars König, Mario Carneiro, Zongyuan Liu
 -/
 import Iris.Algebra.OFE
 import Iris.BI.BIBase
@@ -18,6 +18,8 @@ theorem liftRel_eq : liftRel (@Eq α) A B ↔ A = B := by
 
 /-- Require that a separation logic with carrier type `PROP` fulfills all necessary axioms. -/
 class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
+  -- Iris-Rocq defines BI equiv `≡` as OFE equiv, `⊣⊢` as two directions of bi-entailment,
+  -- and uses `bi_mixin_equiv_entails`. The two implementations are equivalent.
   Equiv P Q := P ⊣⊢ Q
 
   entails_preorder : Preorder Entails
@@ -102,7 +104,7 @@ export BIBase (
   Entails emp pure and or imp sForall sExists «forall» «exists» sep wand
   persistently BiEntails iff wandIff affinely absorbingly
   intuitionistically later persistentlyIf affinelyIf absorbinglyIf
-  intuitionisticallyIf bigAnd bigOr bigSep Entails.trans BiEntails.trans)
+  intuitionisticallyIf Entails.trans BiEntails.trans)
 
 attribute [rw_mono_rule] BI.sep_mono
 attribute [rw_mono_rule] BI.persistently_mono

src/Iris/BI/BIBase.lean

@@ -7,7 +7,6 @@ import Iris.BI.Notation
 import Iris.Std.Classes
 import Iris.Std.DelabRule
 import Iris.Std.Rewrite
-import Iris.Std.BigOp
 
 namespace Iris.BI
 open Iris.Std
@@ -256,18 +255,6 @@ delab_rule absorbinglyIf
 delab_rule intuitionisticallyIf
   | `($_ $p $P) => do ``(iprop(□?$p $(← unpackIprop P)))
 
-/-- Fold the conjunction `∧` over a list of separation logic propositions. -/
-def bigAnd [BIBase PROP] (Ps : List PROP) : PROP := bigOp and iprop(True) Ps
-/-- Fold the disjunction `∨` over a list of separation logic propositions. -/
-def bigOr [BIBase PROP] (Ps : List PROP) : PROP := bigOp or iprop(False) Ps
-/-- Fold the separating conjunction `∗` over a list of separation logic propositions. -/
-def bigSep [BIBase PROP] (Ps : List PROP) : PROP := bigOp sep iprop(emp) Ps
-
-notation:40 "[∧] " Ps:max => bigAnd Ps
-notation:40 "[∨] " Ps:max => bigOr Ps
-notation:40 "[∗] " Ps:max => bigSep Ps
-
-
 /-- Iterated later modality. -/
 syntax:max "▷^[" term:45 "]" term:40 : term