feat: Port algebra/proofmode_classes.v (IsOp and related type classes)

Iris/Iris/Algebra/Auth.lean

@@ -137,7 +137,12 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac F} {a : A} :
     (●{dq1 • dq2} a) ≡ (●{dq1} a) • (●{dq2} a) :=
   auth_op_auth_eqv
 
--- TODO: auth_auth_dfrac_is_op
+@[rocq_alias auth_auth_dfrac_is_op]
+instance {dq dq1 dq2 : DFrac F} [h : IsOp merge dq dq1 dq2] :
+    IsOp io (●{dq} a : Auth F A) (●{dq1} a) (●{dq2} a) where
+  is_op := by
+    rw [h.is_op]
+    apply auth_dfrac_op
 
 @[rocq_alias auth_frag_op]
 theorem frag_op {b1 b2 : A} : (◯ (b1 • b2) : Auth F A) = ((◯ b1 : Auth F A) • ◯ b2) :=
@@ -174,7 +179,11 @@ nonrec instance {a : A} {b : A} [CoreId b] :
     CoreId ((●{.discard} a : Auth F A) • ◯ b) :=
   instCoreIdOpAuthDiscardFrag
 
--- TODO: auth_frag_is_op
+@[rocq_alias auth_frag_is_op]
+instance {a b1 b2 : A} [h : IsOp merge a b1 b2] :
+    IsOp io (◯ a : Auth F A) (◯ b1) (◯ b2) where
+  is_op := ⟨⟨⟩, h.is_op⟩
+
 -- TODO: auth_frag_sep_homomorphism
 
 /- TODO: BigOPs

Iris/Iris/Algebra/DFrac.lean

@@ -10,6 +10,7 @@ public import Iris.Algebra.OFE
 public import Iris.Algebra.Frac
 public import Iris.Algebra.Updates
 public import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.IsOp
 meta import Iris.Std.RocqPorting
 
 @[expose] public section
@@ -32,7 +33,7 @@ instance : OFE.Discrete (DFrac F) := ⟨congrArg id⟩
 
 namespace DFrac
 
-open DFrac Fraction OFE.Discrete
+open DFrac Fraction OFE.Discrete IsOp
 
 variable [UFraction F]
 
@@ -220,4 +221,12 @@ theorem DFrac.update_acquire [IsSplitFraction F] :
     rw [← add_assoc, IsSplitFraction.split_add]
     exact HP
 
+@[rocq_alias dfrac_op_own]
+theorem op_own (f f' : F) : own f • own f' = own (f + f') := rfl
+
+@[rocq_alias dfrac_is_op]
+instance isOp_dfrac_own {q q1 q2 : Frac F} [h : IsOp merge q q1 q2] :
+    IsOp io (own q.car) (own q1.car) (own q2.car) where
+  is_op := by rw [h.is_op]; rfl
+
 end DFrac

Iris/Iris/Algebra/Frac.lean

@@ -7,6 +7,7 @@ module
 
 public import Iris.Algebra.CMRA
 public import Iris.Algebra.OFE
+public import Iris.Algebra.IsOp
 
 /-!
 # The Frac CMRA
@@ -129,6 +130,10 @@ class UFraction (α : Type _) extends Fraction α, One α where
   -- whole_iff_one {a : α} : Fraction.Whole a ↔ a = 1
   one_whole : Fraction.Whole (1 : α)
 
+-- @[rocq_alias frac_is_op]
+-- instance isOp_frac [Fraction α] {q1 q2 : Frac α} : IsOp merge (q1 + q2) q1 q2 where
+--   is_op := .rfl
+
 section NumericFraction
 
 /-- Generic fractional instance for types with comparison and 1 operators. -/

Iris/Iris/Algebra/IsOp.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, Alvin Tang
+-/
+module
+
+public import Iris.Algebra.CMRA
+public import Iris.ProofMode.SynthInstanceAttr
+meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+namespace Iris
+
+open CMRA ProofMode
+
+section IsOp
+
+/--
+  A type class that allows merging `b1` and `b2` into `a` as well as
+  to split `a` into `b1` and `b2`.
+-/
+@[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR]
+class IsOp [CMRA α] (_ : InOut) (a : semiOutParam $ α) (b1 b2 : α) where
+  is_op : a ≡ b1 • b2
+
+/--
+  Syntactic sugar for specifying whether `IsOp` is used for merging or splitting.
+-/
+macro_rules
+  | `(IsOp merge $a $b1 $b2) => `(IsOp .out $a $b1 $b2)
+  | `(IsOp split $a $b1 $b2) => `(IsOp .in $a $b1 $b2)
+
+/--
+  Merging with `•` should have the lowest priority.
+-/
+@[rocq_alias is_op_op]
+instance (priority := default - 100) isOp_op [CMRA α] (a b : α) :
+    IsOp merge (a • b) a b where
+  is_op := .rfl
+
+/--
+  Splitting with `•` should have the highest priority.
+-/
+@[rocq_alias is_op_lr_op]
+instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) :
+    IsOp split (a • b) a b where
+  is_op := .rfl
+
+/-
+  The following type class instances were originally defined in terms of
+  both `IsOp` and `IsOp'`. The distinction between `IsOp` and `IsOp'` is no
+  longer relevant in Lean, and we use `InOut` instead.
+
+  Note that in the Rocq formulation, the assumptions use `IsOp` while
+  the conclusion use `IsOp'`. We therefore use `merge` for the assumptions
+  but allow any `InOut` value for the conclusion.
+-/
+
+@[rocq_alias is_op_pair]
+instance isOpMerge_pair [CMRA α] {io : InOut}
+    (a b1 b2 : α) (a' b1' b2' : α)
+    [h1 : IsOp merge a b1 b2] [h2 : IsOp merge a' b1' b2'] :
+    IsOp io (a, a') (b1, b1') (b2, b2') where
+  is_op := ⟨h1.is_op, h2.is_op⟩
+
+@[rocq_alias is_op_pair_core_id_l]
+instance isOpMerge_pair_core_id_l [CMRA α] [CMRA β] {io : InOut}
+    (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp merge a' b1' b2'] :
+    IsOp io (a, a') (a, b1') (a, b2') where
+  is_op := ⟨(op_self a).symm, h2.is_op⟩
+
+@[rocq_alias is_op_pair_core_id_r]
+instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {io : InOut}
+    (a b1 b2 : α) (a' : β)
+    [h1 : CoreId a'] [h2 : IsOp merge a b1 b2] :
+    IsOp io (a, a') (b1, a') (b2, a') where
+  is_op := ⟨h2.is_op, (op_self a').symm⟩
+
+@[rocq_alias is_op_Some]
+instance isOpMerge_some [CMRA α] (a b1 b2 : α) {io : InOut}
+    [h : IsOp merge a b1 b2] :
+    IsOp io (some a) (some b1) (some b2) where
+  is_op := h.is_op
+
+end IsOp
+
+end Iris

Iris/Iris/Algebra/Lib/FracAuth.lean

@@ -6,6 +6,7 @@ Authors: Markus de Medeiros
 module
 
 public import Iris.Algebra.Auth
+public import Iris.Algebra.IsOp
 import Iris.Algebra.LocalUpdates
 meta import Iris.Std.RocqPorting
 
@@ -215,6 +216,20 @@ theorem frag_op_valid {q1 q2 : Frac F} {a b : A} :
   show ✓ (◯F{q1 + q2} (a • b)) ↔ _
   exact frag_valid
 
+/-! ## IsOp type class instances -/
+
+@[rocq_alias frac_auth_is_op]
+instance isOp_frac_auth {q q1 q2 : Frac F} {a1 a2 : A} {a : outParam A}
+    [h1 : IsOp merge q q1 q2] [h2 : IsOp merge a a1 a2] :
+    IsOp io (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where
+  is_op := ⟨⟨⟩, ⟨h1.is_op, h2.is_op⟩⟩
+
+@[rocq_alias frac_auth_is_op_core_id]
+instance isOp_frac_auth_core_id {q q1 q2 : Frac F} {a : A}
+    [h1 : CoreId a] [h2 : IsOp merge q q1 q2] :
+    IsOp io (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where
+  is_op := ⟨⟨⟩, ⟨h2.is_op, (op_self a).symm⟩⟩
+
 /-! ## Updates -/
 
 @[rocq_alias frac_auth_update]

Iris/Iris/Algebra/View.lean

@@ -312,6 +312,14 @@ instance : UCMRA (View F R) where
 theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View F R) ≡ (●V{dq1} a) • ●V{dq2} a :=
   ⟨⟨rfl, Agree.idemp.symm⟩, UCMRA.unit_left_id.symm⟩
 
+@[rocq_alias view_auth_dfrac_is_op]
+instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac F} {a : A}
+    [h : IsOp merge dq dq1 dq2] :
+    IsOp io (●V{dq} a : View F R) (●V{dq1} a) (●V{dq2} a) where
+  is_op := by
+    rw [h.is_op]
+    apply auth_op_auth_eqv
+
 @[rocq_alias view_frag_op]
 theorem frag_op_eq : (◯V (b1 • b2) : View F R) = ((◯V b1) • ◯V b2 : View F R) := rfl
 
@@ -349,6 +357,11 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b
     refine (CMRA.coreId_iff_core_eqv_self.mp (by trivial)).trans ?_
     refine UCMRA.unit_left_id.symm
 
+@[rocq_alias view_frag_is_op]
+instance {b b1 b2 : B} [h : IsOp merge b b1 b2] :
+    IsOp io (◯V b : View F R) (◯V b1) (◯V b2) where
+  is_op := NonExpansive.eqv h.is_op
+
 @[rocq_alias view_auth_dfrac_op_invN]
 theorem dist_of_validN_auth (H : ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡{n}≡ a2 := by
   rcases H with ⟨_, _, H, _⟩

Iris/Iris/Instances/IProp/Instance.lean

@@ -14,7 +14,7 @@ public meta import Iris.Std.RocqPorting
 @[expose] public section
 namespace Iris
 
-open COFE
+open COFE Std CMRA
 
 /-- Apply an OFunctor at a fixed type -/
 abbrev COFE.OFunctorPre.ap (F : OFunctorPre) (T : Type _) [OFE T] :=
@@ -752,16 +752,45 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn
     rintro rfl
     exact BI.and_elim_r
 
+@[rocq_alias into_sep_own]
+instance intoSep_own {γ} {a : F.ap (IProp GF)} [h : IsOp split a b1 b2] :
+    IntoSep (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  into_sep := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mp.trans iOwn_op.mp
+
+@[rocq_alias into_and_own]
+instance intoAnd_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2] :
+    IntoAnd false (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  into_and := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mp.trans <|
+    and_intro (iOwn_mono ⟨b2, .rfl⟩) (iOwn_mono ⟨b1, CMRA.comm⟩)
+
+@[rocq_alias from_sep_own]
+instance fromSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2] :
+    FromSep (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  from_sep := iOwn_op.mpr.trans (equiv_iff.mp <| NonExpansive.eqv h.is_op).mpr
+
 @[rocq_alias combine_sep_as_own]
-instance combineSepAs_iOwn {γ} {a1 a2 : F.ap (IProp GF)} :
-  -- TODO: Add IsOp premise once it is ported
-  CombineSepAs (iOwn γ a1) (iOwn γ a2) (iOwn γ (a1 • a2)) where
-  combine_sep_as := iOwn_op.mpr
+instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp merge a b1 b2] :
+    CombineSepAs (iOwn γ b1) (iOwn γ b2) (iOwn γ a) where
+  combine_sep_as := iOwn_op.mpr.trans (equiv_iff.mp <| NonExpansive.eqv h.is_op.symm).mp
 
 @[rocq_alias combine_sep_gives_own]
 instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} :
-  CombineSepGives (iOwn γ a1) (iOwn γ a2) (internalCmraValid (a1 • a2)) where
+    CombineSepGives (iOwn γ a1) (iOwn γ a2) (internalCmraValid (a1 • a2)) where
   combine_sep_gives := iOwn_cmraValid_op
 
+@[rocq_alias from_and_own_persistent]
+instance fromAndOwn_persistent {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2]
+    [TCOr (CoreId b1) (CoreId b2)] : FromAnd (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  from_and := by
+    -- Infer from `CoreId b1` that `iOwn γ b1` is persistent, likewise for `b2`
+    have _ : TCOr (Persistent (iOwn γ b1)) (Persistent (iOwn γ b2)) := by
+      cases (inferInstance : TCOr (CoreId b1) (CoreId b2))
+      · infer_instance
+      · infer_instance
+    calc
+      _ ⊢ iOwn γ b1 ∗ iOwn γ b2 := persistent_and_sep_1
+      _ ⊢ iOwn γ (b1 • b2)      := iOwn_op.mpr
+      _ ⊢ iOwn γ a              := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mpr
+
 end iOwn
 end Iris

Iris/Iris/Instances/Lib/Token.lean

@@ -19,8 +19,6 @@ open BI CMRA Excl OFE UPred IProp Std ProofMode
 This library provides assertions that represent "unique tokens".
 The `token γ` assertion provides ownership of the token named `γ`,
 and the key lemma `token_exclusive` proves only one token exists.
-
-FIXME: missing token_combine_gives
 -/
 
 abbrev TokenF : COFE.OFunctorPre := constOF (Excl Unit)

Iris/Iris/Tests/Tactics.lean

@@ -2557,6 +2557,23 @@ example {F GF} [RFunctorContractive F] [ElemG GF F] {γ}
     · iexact Hnew2
     · iexact Hnew3
 
+/-- Tests `icombine` for combining propositions involving `iOwn` -/
+example {GF} [Fraction α] [ElemG GF (constOF (Frac α))] {γ}
+    {a1 a2 a3 : Frac α} :
+    ⊢@{IProp GF} iOwn (F := constOF (Frac α)) γ a1 -∗
+      iOwn (F := constOF (Frac α))  γ a2 -∗
+      iOwn (F := constOF (Frac α)) γ a3 -∗
+      iOwn (F := constOF (Frac α)) γ (a1 • (a2 • a3)) ∗
+      internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • (a2 • a3)) := by
+  iintro H1 H2 H3
+  set_option trace.Meta.synthInstance true in
+    icombine H1 H2 H3 as Hnew1 gives ⟨Hnew2, Hnew3⟩
+  isplitl
+  · iexact Hnew1
+  · isplit
+    · iexact Hnew2
+    · iexact Hnew3
+
 /-- Tests `icombine` for combining propositions involving later credits. -/
 example {GF m n} [LcGS GF] :
     ⊢@{IProp GF} £ n -∗ £ 1 -∗ £ m -∗ £ 1 -∗ £ n + (1 + (m + 1)) := by

Iris/PORTING.md

@@ -95,8 +95,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] Discrete functions
   - [x] Isomorphisms
   - [ ] Sigma 
-- [ ] `proofmode_classes.v`
-  - [ ] IsOp
+- [x] `proofmode_classes.v`
+  - [x] IsOp
 - [ ] `reservation_map.v`
   - [ ] CMRA
   - [ ] Updates