From febed0cb69a02ead87c5d707303812622a11f1a6 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 20 May 2026 14:57:29 +0200 Subject: [PATCH 01/19] Implement IsOp type class and its instances from algebra/proofmode_classes.v --- Iris/Iris/Algebra/IsOp.lean | 53 +++++++++++++++++++++++++++++++++++++ Iris/PORTING.md | 4 +-- 2 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 Iris/Iris/Algebra/IsOp.lean diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean new file mode 100644 index 00000000..cda44b03 --- /dev/null +++ b/Iris/Iris/Algebra/IsOp.lean @@ -0,0 +1,53 @@ +/- +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 +meta import Iris.Std.RocqPorting + +namespace Iris.Algebra + +open CMRA + +@[rocq_alias IsOp] +class IsOp [CMRA α] (a b1 b2 : α) where + is_op : a ≡ b1 • b2 + +@[rocq_alias is_op_op] +instance (priority := default + 100) isOp_op [CMRA α] (a b : α) : IsOp (a • b) a b where + is_op := .rfl + +@[rocq_alias IsOp'] +class IsOp' [CMRA α] (a b1 b2 : α) where + is_op' : IsOp a b1 b2 + +@[rocq_alias IsOp'LR] +class IsOp'LR [CMRA α] (a b1 b2 : α) where + is_op_lr : IsOp a b1 b2 + +@[rocq_alias is_op_lr_op] +instance isOp_lr_op [CMRA α] (a b : α) : IsOp'LR (a • b) a b where + is_op_lr := ⟨.rfl⟩ + +@[rocq_alias is_op_pair] +instance isOp_pair [CMRA α] (a b1 b2 : α) (a' b1' b2' : α) + [h1 : IsOp a b1 b2] [h2 : IsOp a' b1' b2'] : IsOp' (a, a') (b1, b1') (b2, b2') where + is_op' := ⟨⟨h1.is_op, h2.is_op⟩⟩ + +@[rocq_alias is_op_pair_core_id_l] +instance isOp_pair_core_id_l [CMRA α] [CMRA β] (a : α) (a' b1' b2' : β) + [h1 : CoreId a] [h2 : IsOp a' b1' b2'] : IsOp' (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 isOp_pair_core_id_r [CMRA α] [CMRA β] (a b1 b2 : α) (a' : β) + [h1 : CoreId a'] [h2 : IsOp a b1 b2] : IsOp' (a, a') (b1, a') (b2, a') where + is_op' := ⟨⟨h2.is_op, (op_self a').symm⟩⟩ + +@[rocq_alias is_op_Some] +instance isOp_some [CMRA α] (a b1 b2 : α) + [h : IsOp a b1 b2] : IsOp' (some a) (some b1) (some b2) where + is_op' := ⟨h.is_op⟩ diff --git a/Iris/PORTING.md b/Iris/PORTING.md index d3c20031..d4bca5ed 100644 --- a/Iris/PORTING.md +++ b/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 From e644c221916219710b12b79a6402e680d9d236af Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 20 May 2026 15:29:55 +0200 Subject: [PATCH 02/19] Add IsOp type class instances in FragAuth.lean --- Iris/Iris/Algebra/IsOp.lean | 10 +++++++++- Iris/Iris/Algebra/Lib/FracAuth.lean | 21 +++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index cda44b03..9296dca9 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -8,10 +8,14 @@ module public import Iris.Algebra.CMRA meta import Iris.Std.RocqPorting -namespace Iris.Algebra +@[expose] public section + +namespace Iris open CMRA +section IsOp + @[rocq_alias IsOp] class IsOp [CMRA α] (a b1 b2 : α) where is_op : a ≡ b1 • b2 @@ -51,3 +55,7 @@ instance isOp_pair_core_id_r [CMRA α] [CMRA β] (a b1 b2 : α) (a' : β) instance isOp_some [CMRA α] (a b1 b2 : α) [h : IsOp a b1 b2] : IsOp' (some a) (some b1) (some b2) where is_op' := ⟨h.is_op⟩ + +end IsOp + +end Iris diff --git a/Iris/Iris/Algebra/Lib/FracAuth.lean b/Iris/Iris/Algebra/Lib/FracAuth.lean index d8065402..af9c50d2 100644 --- a/Iris/Iris/Algebra/Lib/FracAuth.lean +++ b/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,26 @@ 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} {a a1 a2 : A} + [h1 : IsOp q q1 q2] [h2 : IsOp a a1 a2] : + IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where + is_op' := by + repeat constructor + apply h1.is_op + apply 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 q q1 q2] : + IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where + is_op' := by + repeat constructor + apply h2.is_op + apply (op_self a).symm + /-! ## Updates -/ @[rocq_alias frac_auth_update] From 4819f5df7cdb3911dac1a6c2daa42c65b1d081ee Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 10:54:21 +0200 Subject: [PATCH 03/19] Combine several IsOp, IsOp' and IsOp'LR type classes into one Instead of using multiple type classes, utilise InOut for type class synthesis --- Iris/Iris/Algebra/IsOp.lean | 49 +++++++++++++++++++++++-------------- 1 file changed, 31 insertions(+), 18 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 9296dca9..b6f17dab 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -16,45 +16,58 @@ open CMRA section IsOp + +/-- + A type class for splitting `a` into `b1` and `b2`, as well as to merge `b1` + and `b2` into `a`. +-/ @[rocq_alias IsOp] -class IsOp [CMRA α] (a b1 b2 : α) where +class IsOp [CMRA α] (a : outParam α) (b1 b2 : α) where is_op : a ≡ b1 • b2 @[rocq_alias is_op_op] instance (priority := default + 100) isOp_op [CMRA α] (a b : α) : IsOp (a • b) a b where is_op := .rfl -@[rocq_alias IsOp'] -class IsOp' [CMRA α] (a b1 b2 : α) where - is_op' : IsOp a b1 b2 +#rocq_ignore IsOp' "separate type class is no longer necessary" + +-- @[rocq_alias IsOp'] +-- class IsOp' [CMRA α] (a b1 b2 : α) where +-- is_op' : IsOp a b1 b2 + +#rocq_ignore IsOp'LR "seperate type class is no longer necessary" + +-- @[rocq_alias IsOp'LR] +-- class IsOp'LR [CMRA α] (a b1 b2 : α) where +-- is_op_lr : IsOp a b1 b2 + +#rocq_ignore is_op_lr_op "no longer necessary as IsOp'LR is not relevant" -@[rocq_alias IsOp'LR] -class IsOp'LR [CMRA α] (a b1 b2 : α) where - is_op_lr : IsOp a b1 b2 +-- @[rocq_alias is_op_lr_op] +-- instance isOp_lr_op [CMRA α] (a b : α) : IsOp'LR (a • b) a b where +-- is_op_lr := ⟨.rfl⟩ -@[rocq_alias is_op_lr_op] -instance isOp_lr_op [CMRA α] (a b : α) : IsOp'LR (a • b) a b where - is_op_lr := ⟨.rfl⟩ +/- The following type class instances were originally defined for `IsOp'`. -/ @[rocq_alias is_op_pair] instance isOp_pair [CMRA α] (a b1 b2 : α) (a' b1' b2' : α) - [h1 : IsOp a b1 b2] [h2 : IsOp a' b1' b2'] : IsOp' (a, a') (b1, b1') (b2, b2') where - is_op' := ⟨⟨h1.is_op, h2.is_op⟩⟩ + [h1 : IsOp a b1 b2] [h2 : IsOp a' b1' b2'] : IsOp (a, a') (b1, b1') (b2, b2') where + is_op := ⟨h1.is_op, h2.is_op⟩ @[rocq_alias is_op_pair_core_id_l] instance isOp_pair_core_id_l [CMRA α] [CMRA β] (a : α) (a' b1' b2' : β) - [h1 : CoreId a] [h2 : IsOp a' b1' b2'] : IsOp' (a, a') (a, b1') (a, b2') where - is_op' := ⟨⟨(op_self a).symm, h2.is_op⟩⟩ + [h1 : CoreId a] [h2 : IsOp a' b1' b2'] : IsOp (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 isOp_pair_core_id_r [CMRA α] [CMRA β] (a b1 b2 : α) (a' : β) - [h1 : CoreId a'] [h2 : IsOp a b1 b2] : IsOp' (a, a') (b1, a') (b2, a') where - is_op' := ⟨⟨h2.is_op, (op_self a').symm⟩⟩ + [h1 : CoreId a'] [h2 : IsOp a b1 b2] : IsOp (a, a') (b1, a') (b2, a') where + is_op := ⟨h2.is_op, (op_self a').symm⟩ @[rocq_alias is_op_Some] instance isOp_some [CMRA α] (a b1 b2 : α) - [h : IsOp a b1 b2] : IsOp' (some a) (some b1) (some b2) where - is_op' := ⟨h.is_op⟩ + [h : IsOp a b1 b2] : IsOp (some a) (some b1) (some b2) where + is_op := h.is_op end IsOp From c2fe097ce1e78ed612f10ab6e27628dba83ea208 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 10:55:20 +0200 Subject: [PATCH 04/19] Removing "missing token_combine_gives" comment in Token.lean --- Iris/Iris/Instances/Lib/Token.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Iris/Iris/Instances/Lib/Token.lean b/Iris/Iris/Instances/Lib/Token.lean index 522deaa7..594d27b7 100644 --- a/Iris/Iris/Instances/Lib/Token.lean +++ b/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) From caa21ea2987df87f227331e42f41c4812ca19226 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 10:55:53 +0200 Subject: [PATCH 05/19] Simplify proofs for isOp_frac_auth and isOp_frac_auth_core_id --- Iris/Iris/Algebra/Lib/FracAuth.lean | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/Iris/Iris/Algebra/Lib/FracAuth.lean b/Iris/Iris/Algebra/Lib/FracAuth.lean index af9c50d2..ee95de9d 100644 --- a/Iris/Iris/Algebra/Lib/FracAuth.lean +++ b/Iris/Iris/Algebra/Lib/FracAuth.lean @@ -219,22 +219,16 @@ theorem frag_op_valid {q1 q2 : Frac F} {a b : A} : /-! ## IsOp type class instances -/ @[rocq_alias frac_auth_is_op] -instance isOp_frac_auth {q q1 q2 : Frac F} {a a1 a2 : A} +instance isOp_frac_auth {q q1 q2 : Frac F} {a1 a2 : A} {a : outParam A} [h1 : IsOp q q1 q2] [h2 : IsOp a a1 a2] : - IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where - is_op' := by - repeat constructor - apply h1.is_op - apply h2.is_op + IsOp (◯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 q q1 q2] : - IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where - is_op' := by - repeat constructor - apply h2.is_op - apply (op_self a).symm + IsOp (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where + is_op := ⟨⟨⟩, ⟨h2.is_op, (op_self a).symm⟩⟩ /-! ## Updates -/ From 7bf3cbee4ae22d705eaab933eeeff39b0ad1fd73 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 13:06:40 +0200 Subject: [PATCH 06/19] Add IsOp-related type class instances for iOwn --- Iris/Iris/Algebra/IsOp.lean | 9 ++++-- Iris/Iris/Instances/IProp/Instance.lean | 41 +++++++++++++++++++++---- 2 files changed, 42 insertions(+), 8 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index b6f17dab..b45af746 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -18,8 +18,7 @@ section IsOp /-- - A type class for splitting `a` into `b1` and `b2`, as well as to merge `b1` - and `b2` into `a`. + A type class for splitting `a` into `b1` and `b2`. -/ @[rocq_alias IsOp] class IsOp [CMRA α] (a : outParam α) (b1 b2 : α) where @@ -29,6 +28,12 @@ class IsOp [CMRA α] (a : outParam α) (b1 b2 : α) where instance (priority := default + 100) isOp_op [CMRA α] (a b : α) : IsOp (a • b) a b where is_op := .rfl +/-- + A type class to merge `b1` and `b2` into `a`. +-/ +class IsOpMerge [CMRA α] (a : α) (b1 b2 : outParam α) where + is_op : a ≡ b1 • b2 + #rocq_ignore IsOp' "separate type class is no longer necessary" -- @[rocq_alias IsOp'] diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 6d1d24cf..ae59fac7 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/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 b1 b2 : F.ap (IProp GF)} [h : IsOpMerge 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 : IsOpMerge 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 : IsOpMerge 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 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 : IsOpMerge 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 From 861eb0e6ee13b7a0afb70dfbb0aa8a1251e6ee45 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 14:41:22 +0200 Subject: [PATCH 07/19] Port frac_is_op --- Iris/Iris/Algebra/Frac.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 2ba970d5..0204450f 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/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 [CMRA F] {q1 q2 : F} : IsOp (op q1 q2) q1 q2 where + is_op := .rfl + section NumericFraction /-- Generic fractional instance for types with comparison and 1 operators. -/ From c676b20229a1376bb38e8320278f4935fa828df2 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 15:11:52 +0200 Subject: [PATCH 08/19] IsOp type class instances for View.lean --- Iris/Iris/Algebra/DFrac.lean | 3 ++- Iris/Iris/Algebra/View.lean | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean index 30fe47d6..f4129eb2 100644 --- a/Iris/Iris/Algebra/DFrac.lean +++ b/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] diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index 93340cfb..1e130631 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -312,6 +312,12 @@ 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 dq dq1 dq2] : IsOp (●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 +355,10 @@ 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 [h : IsOp b b1 b2] : IsOp (◯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, _⟩ From a2f9fa5154d2b30ede53b9cb371e0792857f0494 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 21 May 2026 17:54:44 +0200 Subject: [PATCH 09/19] Port auth_flag_is_op, auth_auth_dfrac_is_op in Algebra/Auth.lean --- Iris/Iris/Algebra/Auth.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index ff13f4b6..6b5e647a 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -137,7 +137,11 @@ 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 dq dq1 dq2] : IsOp (●{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 +178,10 @@ 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 a b1 b2] : IsOp (◯ a : Auth F A) (◯ b1) (◯ b2) where + is_op := ⟨⟨⟩, h.is_op⟩ + -- TODO: auth_frag_sep_homomorphism /- TODO: BigOPs From 59f94a1fcd93303db8d7481891ba3fad0e44b231 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 22 May 2026 10:27:38 +0200 Subject: [PATCH 10/19] Port the type class instance dfrac_is_op and the lemma op_own --- Iris/Iris/Algebra/DFrac.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean index f4129eb2..42ddfd84 100644 --- a/Iris/Iris/Algebra/DFrac.lean +++ b/Iris/Iris/Algebra/DFrac.lean @@ -221,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 q q1 q2] : + IsOp (own q.car) (own q1.car) (own q2.car) where + is_op := by rw [h.is_op]; rfl + end DFrac From 51e2ac79cfff8d893edb42cdebd3c4483557246f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 22 May 2026 11:22:42 +0200 Subject: [PATCH 11/19] Correct isOp_frac --- Iris/Iris/Algebra/Frac.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 0204450f..2f0512d3 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -131,7 +131,7 @@ class UFraction (α : Type _) extends Fraction α, One α where one_whole : Fraction.Whole (1 : α) @[rocq_alias frac_is_op] -instance isOp_frac [CMRA F] {q1 q2 : F} : IsOp (op q1 q2) q1 q2 where +instance isOp_frac [Fraction α] {q1 q2 : Frac α} : IsOp (Add.add q1 q2) q1 q2 where is_op := .rfl section NumericFraction From 8eb46b17bba15942aab557a3dc98519667777230 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 22 May 2026 11:54:31 +0200 Subject: [PATCH 12/19] Correct type class synthesis direction --- Iris/Iris/Algebra/IsOp.lean | 43 +++++++++++-------------- Iris/Iris/Instances/IProp/Instance.lean | 10 +++--- 2 files changed, 24 insertions(+), 29 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index b45af746..69e9b565 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -17,42 +17,37 @@ open CMRA section IsOp -/-- - A type class for splitting `a` into `b1` and `b2`. --/ + @[rocq_alias IsOp] -class IsOp [CMRA α] (a : outParam α) (b1 b2 : α) where +class IsOp [CMRA α] (a b1 b2 : α) where is_op : 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 (a • b) a b where +instance (priority := default - 100) isOp_op [CMRA α] (a b : α) : IsOp (a • b) a b where is_op := .rfl /-- - A type class to merge `b1` and `b2` into `a`. + A type class for merging `b1` and `b2` into `a`. -/ -class IsOpMerge [CMRA α] (a : α) (b1 b2 : outParam α) where +@[rocq_alias IsOp'] +class IsOpMerge [CMRA α] (a : outParam α) (b1 b2 : α) where is_op : a ≡ b1 • b2 -#rocq_ignore IsOp' "separate type class is no longer necessary" - --- @[rocq_alias IsOp'] --- class IsOp' [CMRA α] (a b1 b2 : α) where --- is_op' : IsOp a b1 b2 - -#rocq_ignore IsOp'LR "seperate type class is no longer necessary" - --- @[rocq_alias IsOp'LR] --- class IsOp'LR [CMRA α] (a b1 b2 : α) where --- is_op_lr : IsOp a b1 b2 - -#rocq_ignore is_op_lr_op "no longer necessary as IsOp'LR is not relevant" +/-- + A type class for splitting `a` into `b1` and `b2`. +-/ +class IsOpSplit [CMRA α] (a : α) (b1 b2 : outParam α) where + is_op : a ≡ b1 • b2 --- @[rocq_alias is_op_lr_op] --- instance isOp_lr_op [CMRA α] (a b : α) : IsOp'LR (a • b) a b where --- is_op_lr := ⟨.rfl⟩ +@[rocq_alias is_op_lr_op] +instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) : + IsOpSplit (a • b) a b where + is_op := .rfl -/- The following type class instances were originally defined for `IsOp'`. -/ +/- The following type class instances were originally defined with `IsOp'`. -/ @[rocq_alias is_op_pair] instance isOp_pair [CMRA α] (a b1 b2 : α) (a' b1' b2' : α) diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index ae59fac7..089c3003 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -753,23 +753,23 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn exact BI.and_elim_r @[rocq_alias into_sep_own] -instance intoSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge a b1 b2] : +instance intoSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit 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 : IsOpMerge a b1 b2] : +instance intoAnd_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit 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 : IsOpMerge a b1 b2] : +instance fromSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit 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 {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp a b1 b2] : +instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge 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 @@ -779,7 +779,7 @@ instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} : combine_sep_gives := iOwn_cmraValid_op @[rocq_alias from_and_own_persistent] -instance fromAndOwn_persistent {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge a b1 b2] +instance fromAndOwn_persistent {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit 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` From 7c20b3cb1a6b50a48e83a48f4732b243b30acffb Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 22 May 2026 13:48:56 +0200 Subject: [PATCH 13/19] Reorganise IsOp type classes --- Iris/Iris/Algebra/Frac.lean | 2 +- Iris/Iris/Algebra/IsOp.lean | 43 ++++++++++++++++++++++--------------- 2 files changed, 27 insertions(+), 18 deletions(-) diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 2f0512d3..e0f0ff13 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -131,7 +131,7 @@ class UFraction (α : Type _) extends Fraction α, One α where one_whole : Fraction.Whole (1 : α) @[rocq_alias frac_is_op] -instance isOp_frac [Fraction α] {q1 q2 : Frac α} : IsOp (Add.add q1 q2) q1 q2 where +instance isOp_frac [Fraction α] {q1 q2 : Frac α} : IsOp (q1 + q2) q1 q2 where is_op := .rfl section NumericFraction diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 69e9b565..b2a1cd10 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -16,56 +16,65 @@ open CMRA section IsOp - - -@[rocq_alias IsOp] +/-- + A type class that allows merging `b1` and `b2` into `a` as well as + to split `a` into `b1` and `b2`. +-/ +@[rocq_alias IsOp'] class IsOp [CMRA α] (a b1 b2 : α) where is_op : a ≡ b1 • b2 +/-- + A type class for merging `b1` and `b2` into `a`. +-/ +@[rocq_alias IsOp] +class IsOpMerge [CMRA α] (a : outParam α) (b1 b2 : α) extends IsOp 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 (a • b) a b where +instance (priority := default - 100) isOp_op [CMRA α] (a b : α) : + IsOpMerge (a • b) a b where is_op := .rfl /-- - A type class for merging `b1` and `b2` into `a`. + A type class for splitting `a` into `b1` and `b2`. -/ -@[rocq_alias IsOp'] -class IsOpMerge [CMRA α] (a : outParam α) (b1 b2 : α) where - is_op : a ≡ b1 • b2 +@[rocq_alias IsOp'LR] +class IsOpSplit [CMRA α] (a : α) (b1 b2 : outParam α) extends IsOp a b1 b2 /-- - A type class for splitting `a` into `b1` and `b2`. + Splitting with `•` should have the highest priority. -/ -class IsOpSplit [CMRA α] (a : α) (b1 b2 : outParam α) where - is_op : a ≡ b1 • b2 - @[rocq_alias is_op_lr_op] instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) : IsOpSplit (a • b) a b where is_op := .rfl -/- The following type class instances were originally defined with `IsOp'`. -/ +/- + The following type class instances were originally defined for `IsOp'`. + The distinction between `IsOp` and `IsOp'` is no longe relevant in Lean, + so the following instances all concern `IsOp`. +-/ @[rocq_alias is_op_pair] -instance isOp_pair [CMRA α] (a b1 b2 : α) (a' b1' b2' : α) +instance isOpMerge_pair [CMRA α] (a b1 b2 : α) (a' b1' b2' : α) [h1 : IsOp a b1 b2] [h2 : IsOp a' b1' b2'] : IsOp (a, a') (b1, b1') (b2, b2') where is_op := ⟨h1.is_op, h2.is_op⟩ @[rocq_alias is_op_pair_core_id_l] -instance isOp_pair_core_id_l [CMRA α] [CMRA β] (a : α) (a' b1' b2' : β) +instance isOpMerge_pair_core_id_l [CMRA α] [CMRA β] (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp a' b1' b2'] : IsOp (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 isOp_pair_core_id_r [CMRA α] [CMRA β] (a b1 b2 : α) (a' : β) +instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] (a b1 b2 : α) (a' : β) [h1 : CoreId a'] [h2 : IsOp a b1 b2] : IsOp (a, a') (b1, a') (b2, a') where is_op := ⟨h2.is_op, (op_self a').symm⟩ @[rocq_alias is_op_Some] -instance isOp_some [CMRA α] (a b1 b2 : α) +instance isOpMerge_some [CMRA α] (a b1 b2 : α) [h : IsOp a b1 b2] : IsOp (some a) (some b1) (some b2) where is_op := h.is_op From 138c87c9424bb596a80eaa3ed97248b91fd2bde8 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Fri, 22 May 2026 18:10:32 +0200 Subject: [PATCH 14/19] Towards using single IsOp type class using semiOutParam --- Iris/Iris/Algebra/Auth.lean | 6 ++- Iris/Iris/Algebra/DFrac.lean | 4 +- Iris/Iris/Algebra/Frac.lean | 6 +-- Iris/Iris/Algebra/IsOp.lean | 56 ++++++++++++++----------- Iris/Iris/Algebra/Lib/FracAuth.lean | 8 ++-- Iris/Iris/Algebra/View.lean | 7 +++- Iris/Iris/Instances/IProp/Instance.lean | 10 ++--- Iris/Iris/Tests/Tactics.lean | 17 ++++++++ 8 files changed, 71 insertions(+), 43 deletions(-) diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index 6b5e647a..01978bd4 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -138,7 +138,8 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac F} {a : A} : auth_op_auth_eqv @[rocq_alias auth_auth_dfrac_is_op] -instance {dq dq1 dq2 : DFrac F} [h : IsOp dq dq1 dq2] : IsOp (●{dq} a : Auth F A) (●{dq1} a) (●{dq2} a) where +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 @@ -179,7 +180,8 @@ nonrec instance {a : A} {b : A} [CoreId b] : instCoreIdOpAuthDiscardFrag @[rocq_alias auth_frag_is_op] -instance {a b1 b2 : A} [h : IsOp a b1 b2] : IsOp (◯ a : Auth F A) (◯ b1) (◯ b2) where +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 diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean index 42ddfd84..3d3fef2d 100644 --- a/Iris/Iris/Algebra/DFrac.lean +++ b/Iris/Iris/Algebra/DFrac.lean @@ -225,8 +225,8 @@ theorem DFrac.update_acquire [IsSplitFraction F] : 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 q q1 q2] : - IsOp (own q.car) (own q1.car) (own q2.car) where +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 diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index e0f0ff13..424d1e72 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -130,9 +130,9 @@ 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 (q1 + q2) q1 q2 where - is_op := .rfl +-- @[rocq_alias frac_is_op] +-- instance isOp_frac [Fraction α] {q1 q2 : Frac α} : IsOp merge (q1 + q2) q1 q2 where +-- is_op := .rfl section NumericFraction diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index b2a1cd10..92940026 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -6,13 +6,14 @@ 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 +open CMRA ProofMode section IsOp @@ -20,62 +21,67 @@ section IsOp A type class that allows merging `b1` and `b2` into `a` as well as to split `a` into `b1` and `b2`. -/ -@[rocq_alias IsOp'] -class IsOp [CMRA α] (a b1 b2 : α) where +@[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 /-- - A type class for merging `b1` and `b2` into `a`. + Syntactic sugar for specifying whether `IsOp` is used for merging or splitting. -/ -@[rocq_alias IsOp] -class IsOpMerge [CMRA α] (a : outParam α) (b1 b2 : α) extends IsOp a b1 b2 +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 : α) : - IsOpMerge (a • b) a b where + IsOp merge (a • b) a b where is_op := .rfl -/-- - A type class for splitting `a` into `b1` and `b2`. --/ -@[rocq_alias IsOp'LR] -class IsOpSplit [CMRA α] (a : α) (b1 b2 : outParam α) extends IsOp a b1 b2 - /-- Splitting with `•` should have the highest priority. -/ @[rocq_alias is_op_lr_op] instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) : - IsOpSplit (a • b) a b where + IsOp split (a • b) a b where is_op := .rfl /- - The following type class instances were originally defined for `IsOp'`. - The distinction between `IsOp` and `IsOp'` is no longe relevant in Lean, - so the following instances all concern `IsOp`. + 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 α] (a b1 b2 : α) (a' b1' b2' : α) - [h1 : IsOp a b1 b2] [h2 : IsOp a' b1' b2'] : IsOp (a, a') (b1, b1') (b2, b2') where +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 β] (a : α) (a' b1' b2' : β) - [h1 : CoreId a] [h2 : IsOp a' b1' b2'] : IsOp (a, a') (a, b1') (a, b2') where +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 β] (a b1 b2 : α) (a' : β) - [h1 : CoreId a'] [h2 : IsOp a b1 b2] : IsOp (a, a') (b1, a') (b2, a') where +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 : α) - [h : IsOp a b1 b2] : IsOp (some a) (some b1) (some b2) where +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 diff --git a/Iris/Iris/Algebra/Lib/FracAuth.lean b/Iris/Iris/Algebra/Lib/FracAuth.lean index ee95de9d..a0668d65 100644 --- a/Iris/Iris/Algebra/Lib/FracAuth.lean +++ b/Iris/Iris/Algebra/Lib/FracAuth.lean @@ -220,14 +220,14 @@ theorem frag_op_valid {q1 q2 : Frac F} {a b : A} : @[rocq_alias frac_auth_is_op] instance isOp_frac_auth {q q1 q2 : Frac F} {a1 a2 : A} {a : outParam A} - [h1 : IsOp q q1 q2] [h2 : IsOp a a1 a2] : - IsOp (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where + [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 q q1 q2] : - IsOp (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where + [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 -/ diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index 1e130631..93bb629a 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -313,7 +313,9 @@ theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View F R) ≡ (●V{dq1} 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 dq dq1 dq2] : IsOp (●V{dq} a : View F R) (●V{dq1} a) (●V{dq2} a) where +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 @@ -356,7 +358,8 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b refine UCMRA.unit_left_id.symm @[rocq_alias view_frag_is_op] -instance [h : IsOp b b1 b2] : IsOp (◯V b : View F R) (◯V b1) (◯V b2) where +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] diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 089c3003..7c470885 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -753,23 +753,23 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn exact BI.and_elim_r @[rocq_alias into_sep_own] -instance intoSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit a b1 b2] : +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 : IsOpSplit a b1 b2] : +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 : IsOpSplit a b1 b2] : +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 {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge a b1 b2] : +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 @@ -779,7 +779,7 @@ instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} : combine_sep_gives := iOwn_cmraValid_op @[rocq_alias from_and_own_persistent] -instance fromAndOwn_persistent {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit a b1 b2] +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` diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 71bbf0ff..da36bfe8 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/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 From e9396bf6e008fcb54f8d0fe6869846fe8a93f123 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 24 May 2026 14:51:37 +0200 Subject: [PATCH 15/19] Use uncheckedInParam for b1 and b2 --- Iris/Iris/Algebra/IsOp.lean | 4 +++- Iris/Iris/Instances/IProp/Instance.lean | 6 +++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 92940026..67f70cda 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -22,7 +22,9 @@ section IsOp 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 +class IsOp [CMRA α] + (_ : InOut) (a : semiOutParam $ α) + (b1 : uncheckedInParam α) (b2 : uncheckedInParam α) where is_op : a ≡ b1 • b2 /-- diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 7c470885..a1709b09 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -752,17 +752,20 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn rintro rfl exact BI.and_elim_r +set_option synthInstance.checkSynthOrder false in @[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 +set_option synthInstance.checkSynthOrder false in @[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⟩) +set_option synthInstance.checkSynthOrder false in @[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 @@ -778,8 +781,9 @@ instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} : CombineSepGives (iOwn γ a1) (iOwn γ a2) (internalCmraValid (a1 • a2)) where combine_sep_gives := iOwn_cmraValid_op +set_option synthInstance.checkSynthOrder false in @[rocq_alias from_and_own_persistent] -instance fromAndOwn_persistent {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2] +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` From 1e4a8e7baae116df840da34f14a286b4cea836d3 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 24 May 2026 15:21:37 +0200 Subject: [PATCH 16/19] Remove frac_is_op: not ported yet --- Iris/Iris/Algebra/Frac.lean | 4 ---- Iris/Iris/Tests/Tactics.lean | 2 +- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 424d1e72..3dfebac8 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -130,10 +130,6 @@ 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. -/ diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index da36bfe8..5d8bcdfb 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2561,7 +2561,7 @@ example {F GF} [RFunctorContractive F] [ElemG GF F] {γ} 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 α)) γ a2 -∗ iOwn (F := constOF (Frac α)) γ a3 -∗ iOwn (F := constOF (Frac α)) γ (a1 • (a2 • a3)) ∗ internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • (a2 • a3)) := by From 2b04cbdee1c758e834e6efa12310a34d8d4d9805 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 24 May 2026 16:46:32 +0200 Subject: [PATCH 17/19] Add tests for icombine with IsOp instances --- Iris/Iris/Tests/Tactics.lean | 46 +++++++++++++++++++++--------------- 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 5d8bcdfb..39a12db9 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -10,11 +10,12 @@ public import Iris.ProofMode public import Iris.Instances.IProp public import Iris.Instances.Lib.LaterCredits public import Iris.Instances.Lib.Token +public import Iris.Algebra.CMRA @[expose] public section namespace Iris.Tests -open Iris.BI +open BI CMRA DFrac /- This file contains tests with various scenarios for all available tactics. -/ @@ -2543,36 +2544,43 @@ example [BI PROP] {P Q R : PROP} : ⊢ P -∗ Q -∗ □ R -∗ R ∗ P ∗ Q := iintro HP HQ #HR icombine %a as HNew1 -/-- Tests `icombine` for combining propositions involving `iOwn` -/ +/-- Tests `icombine` for combining propositions involving `iOwn`, where + `a2` and `a3` can be combined as `b` instead of `a2 • a3` as + the former takes higher precedence. Likewise, `a1` and `b` is merged + as `c` instead of `a1 • b`. -/ example {F GF} [RFunctorContractive F] [ElemG GF F] {γ} - {a1 a2 a3 : F.ap (IProp GF)} : + {a1 a2 a3 b c : F.ap (IProp GF)} [IsOp merge b a2 a3] [IsOp merge c a1 b] : ⊢ iOwn γ a1 -∗ iOwn γ a2 -∗ iOwn γ a3 -∗ - iOwn γ (a1 • (a2 • a3)) ∗ - internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • (a2 • a3)) := by + iOwn γ c ∗ + internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • b) := by iintro H1 H2 H3 icombine H1 H2 H3 as Hnew1 gives ⟨Hnew2, Hnew3⟩ isplitl · iexact Hnew1 · isplit - · iexact Hnew2 + · iexact Hnew2 -- `IsOp` is irrelevant to the `gives` syntax · 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 -∗ +/-- Tests `icombine` for combining propositions involving `iOwn`, `IsOp` + instances. -/ +example {GF} [UFraction α] [ElemG GF (constOF (DFrac α))] + [ElemG GF (constOF (Frac α))] {γ} + {a1 a2 a3 b : Frac α} [IsOp merge b a2 a3] [IsOp merge c a1 b] : + ⊢@{IProp GF} + iOwn (F := constOF (DFrac α)) γ (own a1.car) -∗ + iOwn (F := constOF (DFrac α)) γ (own a2.car) -∗ + iOwn (F := constOF (DFrac α)) γ (own a3.car) -∗ + 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 + iOwn (F := constOF (DFrac α)) γ (own c.car) ∗ + iOwn (F := constOF (Frac α)) γ c := by + iintro H1 H2 H3 H4 H5 H6 + icombine H1 H2 H3 as Hnew1 + icombine H4 H5 H6 as Hnew2 + isplitl [Hnew1] · iexact Hnew1 - · isplit - · iexact Hnew2 - · iexact Hnew3 + · iexact Hnew2 /-- Tests `icombine` for combining propositions involving later credits. -/ example {GF m n} [LcGS GF] : From e0402040965f4f8340771dbda5735c1d7b01a0ca Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 24 May 2026 17:12:09 +0200 Subject: [PATCH 18/19] Add tests for icombine and IsOp instances for authoritative CMRA --- Iris/Iris/Tests/Tactics.lean | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 39a12db9..80ae4cf0 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2561,11 +2561,11 @@ example {F GF} [RFunctorContractive F] [ElemG GF F] {γ} · iexact Hnew2 -- `IsOp` is irrelevant to the `gives` syntax · iexact Hnew3 -/-- Tests `icombine` for combining propositions involving `iOwn`, `IsOp` - instances. -/ -example {GF} [UFraction α] [ElemG GF (constOF (DFrac α))] +/-- Tests `icombine` for combining propositions involving `iOwn` and `IsOp` + instances for `DFrac` and `Frac`. -/ +example {GF α} [UFraction α] [ElemG GF (constOF (DFrac α))] [ElemG GF (constOF (Frac α))] {γ} - {a1 a2 a3 b : Frac α} [IsOp merge b a2 a3] [IsOp merge c a1 b] : + {a1 a2 a3 b c : Frac α} [IsOp merge b a2 a3] [IsOp merge c a1 b] : ⊢@{IProp GF} iOwn (F := constOF (DFrac α)) γ (own a1.car) -∗ iOwn (F := constOF (DFrac α)) γ (own a2.car) -∗ @@ -2582,6 +2582,24 @@ example {GF} [UFraction α] [ElemG GF (constOF (DFrac α))] · iexact Hnew1 · iexact Hnew2 +/-- Tests `icombine` for combining propositions involving `iOwn` and `IsOp` + instances for the authoritative CMRA. -/ +example {GF F A} [UFraction F] [UCMRA A] [ElemG GF (constOF (Auth F A))] {γ} + {a1 a2 a3 b c : A} {dq dq1 dq2 : DFrac F} + [IsOp merge b a2 a3] [IsOp merge c a1 b] [IsOp merge dq dq1 dq2] : + ⊢@{IProp GF} + iOwn (F := constOF (Auth F A)) γ (◯ a1) -∗ + iOwn (F := constOF (Auth F A)) γ (◯ a2) -∗ + iOwn (F := constOF (Auth F A)) γ (◯ a3) -∗ + iOwn (F := constOF (Auth F A)) γ (●{dq1} a1) -∗ + iOwn (F := constOF (Auth F A)) γ (●{dq2} a1) -∗ + iOwn (F := constOF (Auth F A)) γ ((◯ c) • ●{dq} a1) := by + iintro H1 H2 H3 H4 H5 + icombine H1 H2 H3 as HNew1 + icombine H4 H5 as HNew2 + icombine HNew1 HNew2 as HNew + iexact HNew + /-- 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 From b1d3bb2e59dda54c1568ac9a210e43d70e0d2b4f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Sun, 24 May 2026 17:19:00 +0200 Subject: [PATCH 19/19] Nested merging --- Iris/Iris/Tests/Tactics.lean | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 80ae4cf0..f152863a 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2551,8 +2551,7 @@ example [BI PROP] {P Q R : PROP} : ⊢ P -∗ Q -∗ □ R -∗ R ∗ P ∗ Q := example {F GF} [RFunctorContractive F] [ElemG GF F] {γ} {a1 a2 a3 b c : F.ap (IProp GF)} [IsOp merge b a2 a3] [IsOp merge c a1 b] : ⊢ iOwn γ a1 -∗ iOwn γ a2 -∗ iOwn γ a3 -∗ - iOwn γ c ∗ - internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • b) := by + iOwn γ c ∗ internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • b) := by iintro H1 H2 H3 icombine H1 H2 H3 as Hnew1 gives ⟨Hnew2, Hnew3⟩ isplitl @@ -2573,8 +2572,7 @@ example {GF α} [UFraction α] [ElemG GF (constOF (DFrac α))] iOwn (F := constOF (Frac α)) γ a1 -∗ iOwn (F := constOF (Frac α)) γ a2 -∗ iOwn (F := constOF (Frac α)) γ a3 -∗ - iOwn (F := constOF (DFrac α)) γ (own c.car) ∗ - iOwn (F := constOF (Frac α)) γ c := by + iOwn (F := constOF (DFrac α)) γ (own c.car) ∗ iOwn (F := constOF (Frac α)) γ c := by iintro H1 H2 H3 H4 H5 H6 icombine H1 H2 H3 as Hnew1 icombine H4 H5 H6 as Hnew2 @@ -2585,19 +2583,23 @@ example {GF α} [UFraction α] [ElemG GF (constOF (DFrac α))] /-- Tests `icombine` for combining propositions involving `iOwn` and `IsOp` instances for the authoritative CMRA. -/ example {GF F A} [UFraction F] [UCMRA A] [ElemG GF (constOF (Auth F A))] {γ} - {a1 a2 a3 b c : A} {dq dq1 dq2 : DFrac F} - [IsOp merge b a2 a3] [IsOp merge c a1 b] [IsOp merge dq dq1 dq2] : + {a1 a2 a3 b c : A} {dq' dq'' dq1 dq2 dq3 dq4 : DFrac F} + [IsOp merge b a2 a3] [IsOp merge c a1 b] + [IsOp merge dq' dq1 dq2] [IsOp merge dq'' dq3 dq4] : ⊢@{IProp GF} iOwn (F := constOF (Auth F A)) γ (◯ a1) -∗ iOwn (F := constOF (Auth F A)) γ (◯ a2) -∗ iOwn (F := constOF (Auth F A)) γ (◯ a3) -∗ iOwn (F := constOF (Auth F A)) γ (●{dq1} a1) -∗ iOwn (F := constOF (Auth F A)) γ (●{dq2} a1) -∗ - iOwn (F := constOF (Auth F A)) γ ((◯ c) • ●{dq} a1) := by - iintro H1 H2 H3 H4 H5 + iOwn (F := constOF (Auth F A)) γ (●{dq3} a1) -∗ + iOwn (F := constOF (Auth F A)) γ (●{dq4} a1) -∗ + iOwn (F := constOF (Auth F A)) γ ((◯ c) • ●{dq' • dq''} a1) := by + iintro H1 H2 H3 H4 H5 H6 H7 icombine H1 H2 H3 as HNew1 icombine H4 H5 as HNew2 - icombine HNew1 HNew2 as HNew + icombine H6 H7 as HNew3 + icombine HNew1 HNew2 HNew3 as HNew iexact HNew /-- Tests `icombine` for combining propositions involving later credits. -/