From 8262fdfd7f233dd5155be727e257f35d7af33d3f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 14:44:24 +0200 Subject: [PATCH 01/26] Implement `semiOutParamPos` and `semiOutParamNeg` --- Iris/Iris/Algebra/Agree.lean | 3 +- Iris/Iris/Algebra/Auth.lean | 9 +- Iris/Iris/Algebra/DFrac.lean | 4 +- Iris/Iris/Algebra/Frac.lean | 4 +- Iris/Iris/Algebra/HeapView.lean | 6 +- Iris/Iris/Algebra/IsOp.lean | 35 ++++--- Iris/Iris/Algebra/Lib/FracAuth.lean | 8 +- Iris/Iris/Algebra/Lib/MonoNat.lean | 9 +- Iris/Iris/Algebra/UFrac.lean | 2 +- Iris/Iris/Algebra/View.lean | 8 +- Iris/Iris/Instances/IProp/Instance.lean | 1 + Iris/Iris/ProofMode/Classes.lean | 28 +++--- Iris/Iris/ProofMode/Instances.lean | 14 +-- Iris/Iris/ProofMode/ProofModeM.lean | 2 +- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 101 +++++++++++++++------ Iris/Iris/ProofMode/Tactics/Cases.lean | 8 +- Iris/Iris/ProofMode/Tactics/HaveCore.lean | 4 +- Iris/Iris/ProofMode/Tactics/Intro.lean | 8 +- 18 files changed, 151 insertions(+), 103 deletions(-) diff --git a/Iris/Iris/Algebra/Agree.lean b/Iris/Iris/Algebra/Agree.lean index 42f732acc..c95fcd4f4 100644 --- a/Iris/Iris/Algebra/Agree.lean +++ b/Iris/Iris/Algebra/Agree.lean @@ -512,8 +512,7 @@ theorem valid_included {x y : Agree α} : ✓ y → x ≼ y → x ≡ y := by _ ≡ x • z := .op_r <| op_inv <| (CMRA.valid_iff heq).mp hval _ ≡ y := heq.symm -set_option synthInstance.checkSynthOrder false in -instance {x : Agree α} : IsOp io1 x io2 x io3 x where +instance {x : Agree α} : IsOp io x x x where is_op := idemp.symm end Agree diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index 2b44c1daa..915ca4b6a 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -137,10 +137,9 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac} {a : A} : (●{dq1 • dq2} a) ≡ (●{dq1} a) • (●{dq2} a) := auth_op_auth_eqv -set_option synthInstance.checkSynthOrder false in @[rocq_alias auth_auth_dfrac_is_op] -instance {dq dq1 dq2 : DFrac} [h : IsOp io1 dq io2 dq1 io3 dq2] : - IsOp io1 (●{dq} a : Auth A) io2 (●{dq1} a) io3 (●{dq2} a) where +instance {dq dq1 dq2 : DFrac} {a : A} [h : IsOp io dq dq1 dq2] : + IsOp io (●{dq} a : Auth A) (●{dq1} a) (●{dq2} a) where is_op := by rw [h.is_op.to_eq] apply auth_dfrac_op @@ -181,8 +180,8 @@ nonrec instance {a : A} {b : A} [CoreId b] : instCoreIdOpAuthDiscardFrag @[rocq_alias auth_frag_is_op] -instance {a b1 b2 : A} [h : IsOp io1 a io2 b1 io3 b2] : - IsOp io1 (◯ a : Auth A) io2 (◯ b1) io3 (◯ b2) where +instance {a b1 b2 : A} [h : IsOp io a b1 b2] : + IsOp io (◯ a : Auth A) (◯ b1) (◯ b2) where is_op := NonExpansive₂.eqv .rfl h.is_op -- TODO: auth_frag_sep_homomorphism diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean index ed1e1b76f..1efb2a8bc 100644 --- a/Iris/Iris/Algebra/DFrac.lean +++ b/Iris/Iris/Algebra/DFrac.lean @@ -227,8 +227,8 @@ theorem own_included {p q : Qp} : own p ≼ own q ↔ ∃ r, q = p + r := by exact ⟨r, Qp.ext_iff.mpr hz⟩ @[rocq_alias dfrac_is_op] -instance isOp_dfrac_own {q q1 q2 : Qp} [h : IsOp io1 q io2 q1 io3 q2] : - IsOp io1 (own q) io2 (own q1) io3 (own q2) where +instance isOp_dfrac_own {q q1 q2 : Qp} [h : IsOp io q q1 q2] : + IsOp io (own q) (own q1) (own q2) where is_op := by rw [h.is_op.to_eq]; rfl end DFrac diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 7595f2357..6e257904e 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -153,13 +153,11 @@ theorem Frac.op_eq (p q : Qp) : p • q = p + q := rfl @[rocq_alias frac_valid] theorem Frac.valid_iff {p : Qp} : ✓ p ↔ p.val ≤ 1 := .rfl -set_option synthInstance.checkSynthOrder false in @[rocq_alias frac_is_op] instance (priority := default - 10) (q1 q2 : Qp) : IsOpMerge (q1 + q2 : Qp) q1 q2 where is_op := .rfl -set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_frac] -instance (q : Qp) : IsOp io1 q io2 q.half io3 q.half where +instance (q : Qp) : IsOp io q q.half q.half where is_op := by refine OFE.Equiv.of_eq (q.ext ?_); grind diff --git a/Iris/Iris/Algebra/HeapView.lean b/Iris/Iris/Algebra/HeapView.lean index 9ba37b22a..0f3cebea1 100644 --- a/Iris/Iris/Algebra/HeapView.lean +++ b/Iris/Iris/Algebra/HeapView.lean @@ -194,9 +194,9 @@ theorem frag_op_eqv : Frag (H := H) k (dp • dq) (v1 • v2) ≡ Frag k dp v1 set_option synthInstance.checkSynthOrder false in instance - [hdp : IsOp io1 dp io2 dp1 io3 dp2] - [hv : IsOp io1 v io2 v1 io3 v2] : - IsOp io1 (Frag k dp v) io2 (Frag k dp1 v1) io3 (Frag (H := H) k dp2 v2) where + [hdp : IsOp io dp dp1 dp2] + [hv : IsOp io v v1 v2] : + IsOp io (Frag k dp v) (Frag k dp1 v1) (Frag (H := H) k dp2 v2) where is_op := by rw [hdp.is_op.to_eq] exact (NonExpansive.eqv hv.is_op).trans frag_op_eqv diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 63567a0c7..89be115d7 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -23,17 +23,16 @@ section IsOp -/ @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR] class IsOp [CMRA α] - (_ : InOut) (a : semiOutParam α) - (_ : InOut) (b1 : semiOutParam α) - (_ : InOut) (b2 : semiOutParam α) where + (io : InOut) (a : semiOutParamPos io α) + (b1 : semiOutParamNeg io α) + (b2 : semiOutParamNeg io α) where is_op : a ≡ b1 • b2 /-- Syntactic sugar for specifying whether `IsOp` is used for merging or splitting. -/ -abbrev IsOpMerge [CMRA α] (a b1 b2 : semiOutParam α) := IsOp .out a .in b1 .in b2 -abbrev IsOpSplit [CMRA α] (a b1 b2 : semiOutParam α) := IsOp .in a .out b1 .out b2 - +abbrev IsOpMerge [CMRA α] (a b1 b2 : α) := IsOp .out a b1 b2 +abbrev IsOpSplit [CMRA α] (a b1 b2 : α) := IsOp .in a b1 b2 set_option synthInstance.checkSynthOrder false in /-- @@ -60,31 +59,31 @@ instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) : -/ @[rocq_alias is_op_pair] -instance isOp_pair [CMRA α] {ioa iob1 iob2 : InOut} +instance isOp_pair [CMRA α] {io : InOut} (a b1 b2 : α) (a' b1' b2' : α) - [h1 : IsOp ioa a iob1 b1 iob2 b2] [h2 : IsOp ioa a' iob1 b1' iob2 b2'] : - IsOp ioa (a, a') iob1 (b1, b1') iob2 (b2, b2') where + [h1 : IsOp io a b1 b2] [h2 : IsOp io a' b1' b2'] : + IsOp io (a, a') (b1, b1') (b2, b2') where is_op := OFE.equiv_prod_ext h1.is_op h2.is_op set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_pair_core_id_l] -instance isOp_pair_core_id_l [CMRA α] [CMRA β] {ioa iob1 iob2 : InOut} - (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp ioa a' iob1 b1' iob2 b2'] : - IsOp ioa (a, a') iob1 (a, b1') iob2 (a, b2') where +instance isOp_pair_core_id_l [CMRA α] [CMRA β] {io : InOut} + (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp io a' b1' b2'] : + IsOp io (a, a') (a, b1') (a, b2') where is_op := OFE.equiv_prod_ext (op_self a).symm h2.is_op set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_pair_core_id_r] -instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {ioa iob1 iob2 : InOut} +instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {io : InOut} (a b1 b2 : α) (a' : β) - [h1 : CoreId a'] [h2 : IsOp ioa a iob1 b1 iob2 b2] : - IsOp ioa (a, a') iob1 (b1, a') iob2 (b2, a') where + [h1 : CoreId a'] [h2 : IsOp io a b1 b2] : + IsOp io (a, a') (b1, a') (b2, a') where is_op := OFE.equiv_prod_ext h2.is_op (op_self a').symm @[rocq_alias is_op_Some] -instance isOp_some [CMRA α] (a b1 b2 : α) {ioa iob1 iob2 : InOut} - [h : IsOp ioa a iob1 b1 iob2 b2] : - IsOp ioa (some a) iob1 (some b1) iob2 (some b2) where +instance isOp_some [CMRA α] (a b1 b2 : α) {io : InOut} + [h : IsOp io 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 78e8b3e3a..df88fcce5 100644 --- a/Iris/Iris/Algebra/Lib/FracAuth.lean +++ b/Iris/Iris/Algebra/Lib/FracAuth.lean @@ -229,15 +229,15 @@ theorem frag_op_valid {q1 q2 : Qp} {a b : A} : @[rocq_alias frac_auth_is_op] instance isOp_frac_auth {q q1 q2 : Qp} {a1 a2 : A} {a : outParam A} - [h1 : IsOp io1 q io2 q1 io3 q2] [h2 : IsOp io1 a io2 a1 io3 a2] : - IsOp io1 (◯F{q} a) io2 (◯F{q1} a1) io3 (◯F{q2} a2) where + [h1 : IsOp io q q1 q2] [h2 : IsOp io a a1 a2] : + IsOp io (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where is_op := NonExpansive.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv h1.is_op h2.is_op)) set_option synthInstance.checkSynthOrder false in @[rocq_alias frac_auth_is_op_core_id] instance isOp_frac_auth_core_id {q q1 q2 : Qp} {a : A} - [h1 : CoreId a] [h2 : IsOp io1 q io2 q1 io3 q2] : - IsOp io1 (◯F{q} a) io2 (◯F{q1} a) io3 (◯F{q2} a) where + [h1 : CoreId a] [h2 : IsOp io q q1 q2] : + IsOp io (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where is_op := NonExpansive.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv h2.is_op (op_self a).symm)) /-! ## Updates -/ diff --git a/Iris/Iris/Algebra/Lib/MonoNat.lean b/Iris/Iris/Algebra/Lib/MonoNat.lean index 6bab26468..1a6ad71a0 100644 --- a/Iris/Iris/Algebra/Lib/MonoNat.lean +++ b/Iris/Iris/Algebra/Lib/MonoNat.lean @@ -187,17 +187,16 @@ theorem auth_unpersist (n : MaxNat) : (●MN□ n : MonoNat) ~~>: (fun k => ∃ q, k = ●MN{DFrac.own q} n) := Auth.auth_updateP_both_unpersist -set_option synthInstance.checkSynthOrder false in @[rocq_alias mono_nat_auth_dfrac_is_op] instance {dq dq1 dq2 : DFrac} {n : MaxNat} - [h : IsOp io1 dq io2 dq1 io3 dq2] : - IsOp io1 (●MN{dq} n) io2 (●MN{dq1} n) io3 (●MN{dq2} n) where + [h : IsOp io dq dq1 dq2] : + IsOp io (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n) where is_op := by rw [h.is_op.to_eq]; apply auth_dfrac_op @[rocq_alias mono_nat_lb_max_is_op] instance {n n1 n2 : MaxNat} - [h : IsOp io1 n io2 n1 io3 n2] : - IsOp io1 (◯MN n : MonoNat) io2 (◯MN n1) io3 (◯MN n2) where + [h : IsOp io n n1 n2] : + IsOp io (◯MN n : MonoNat) (◯MN n1) (◯MN n2) where is_op := by rw [h.is_op.to_eq]; exact .rfl end MonoNat diff --git a/Iris/Iris/Algebra/UFrac.lean b/Iris/Iris/Algebra/UFrac.lean index 79d7d2214..947a5548f 100644 --- a/Iris/Iris/Algebra/UFrac.lean +++ b/Iris/Iris/Algebra/UFrac.lean @@ -96,7 +96,7 @@ instance {q : UFrac} : CMRA.IdFree q where set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_ufrac] -instance (q : UFrac) : IsOp io1 q io2 ⟨q.frac.half⟩ io3 ⟨q.frac.half⟩ where +instance (q : UFrac) : IsOp io q ⟨q.frac.half⟩ ⟨q.frac.half⟩ where is_op := OFE.Equiv.of_eq <| ext_iff.mpr (Qp.half_add_half q.frac).symm end UFrac diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index 0e5a65f57..c845c4a56 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -334,8 +334,8 @@ theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View R) ≡ (●V{dq1} a) • set_option synthInstance.checkSynthOrder false in @[rocq_alias view_auth_dfrac_is_op] instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac} {a : A} - [h : IsOp io1 dq io2 dq1 io3 dq2] : - IsOp io1 (●V{dq} a : View R) io2 (●V{dq1} a) io3 (●V{dq2} a) where + [h : IsOp io dq dq1 dq2] : + IsOp io (●V{dq} a : View R) (●V{dq1} a) (●V{dq2} a) where is_op := by rw [h.is_op.to_eq] apply auth_op_auth_eqv @@ -378,8 +378,8 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View R) • ◯V b) refine UCMRA.unit_left_id.symm @[rocq_alias view_frag_is_op] -instance {b b1 b2 : B} [h : IsOp io1 b io2 b1 io3 b2] : - IsOp io1 (◯V b : View R) io2 (◯V b1) io3 (◯V b2) where +instance {b b1 b2 : B} [h : IsOp io b b1 b2] : + IsOp io (◯V b : View 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 4816c965e..651313bc5 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -791,6 +791,7 @@ 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 +set_option synthInstance.checkSynthOrder false in @[rocq_alias combine_sep_as_own] instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge a b1 b2] : CombineSepAs (iOwn γ b1) (iOwn γ b2) (iOwn γ a) where diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index ac2ca161b..faac957bb 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -27,16 +27,19 @@ inductive AsEmpValid.Direction where | from @[ipm_class, rocq_alias AsEmpValid] -class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : semiOutParam $ Type _) -(_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam $ PROP) where +class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (io : InOut) + (PROP : semiOutParamPos io $ Type _) + (bi : semiOutParamPos io $ BI PROP) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) @[rocq_alias as_emp_valid_1] -theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) [AsEmpValid .into φ .in PROP .in bi P] -: φ → ⊢ P := (AsEmpValid.as_emp_valid .in .in).1 rfl +theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) + [inst : AsEmpValid .into φ .in PROP bi P] : φ → ⊢ P := + inst.as_emp_valid.left rfl @[rocq_alias as_emp_valid_2] -theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) [AsEmpValid .from φ .out PROP .out bi P] -: (⊢ P) → φ := (AsEmpValid.as_emp_valid .out .out).2 rfl +theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) + [inst : AsEmpValid .from φ .out PROP bi P] : (⊢ P) → φ := + inst.as_emp_valid.right rfl /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes with the prefix `From` are used to generate one or more propositions *from* which the original @@ -50,7 +53,8 @@ class FromImp {PROP} [BI PROP] (P : PROP) (Q1 Q2 : outParam $ PROP) where export FromImp (from_imp) @[ipm_class, rocq_alias FromWand] -class FromWand {PROP} [BI PROP] (P : PROP) (_ : InOut) (Q1 : semiOutParam PROP) (Q2 : outParam $ PROP) where +class FromWand {PROP} [BI PROP] (P : PROP) (io : InOut) + (Q1 : semiOutParamPos io PROP) (Q2 : outParam $ PROP) where from_wand : (Q1 -∗ Q2) ⊢ P export FromWand (from_wand) @@ -58,8 +62,8 @@ export FromWand (from_wand) @[ipm_class, rocq_alias IntoWand] class IntoWand {PROP} [BI PROP] (p q : Bool) (R : PROP) - (ioP : InOut) (P : semiOutParam PROP) - (ioQ : InOut) (Q : semiOutParam PROP) where + (ioP : InOut) (P : semiOutParamPos ioP PROP) + (ioQ : InOut) (Q : semiOutParamPos ioQ PROP) where into_wand : □?p R ⊢ □?q P -∗ Q export IntoWand (into_wand) @@ -134,7 +138,8 @@ class IntoAbsorbingly {PROP} [BI PROP] (P : outParam $ PROP) (Q : PROP) where export IntoAbsorbingly (into_absorbingly) @[ipm_class, rocq_alias FromAssumption, rocq_alias KnownLFromAssumption, rocq_alias KnownRFromAssumption] -class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut) (P : semiOutParam $ PROP) (Q : PROP) where +class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut) + (P : semiOutParamPos ioP PROP) (Q : PROP) where from_assumption : □?p P ⊢ Q export FromAssumption (from_assumption) @@ -146,7 +151,8 @@ export IntoPure (into_pure) #rocq_ignore into_pureT_hint "IntoPureT is not necessary in Lean" @[ipm_class, rocq_alias FromPure, rocq_alias FromPureT] -class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut) (φ : semiOutParam $ Prop) where +class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut) + (φ : semiOutParamPos ioφ Prop) where from_pure : ?a ⌜φ⌝ ⊢ P export FromPure (from_pure) diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean index 8ebc6aa25..ee0d85d28 100644 --- a/Iris/Iris/ProofMode/Instances.lean +++ b/Iris/Iris/ProofMode/Instances.lean @@ -20,26 +20,26 @@ open Iris.BI Iris.Std @[rocq_alias as_emp_valid_emp_valid] instance (priority := default + 10) asEmpValidEmpValid [bi : BI PROP] d (P : PROP) : - AsEmpValid d (⊢ P) io1 PROP io2 bi P := ⟨by simp⟩ + AsEmpValid d (⊢ P) io PROP bi P := ⟨by simp⟩ @[rocq_alias as_emp_valid_entails] instance asEmpValid_entails [bi : BI PROP] d (P Q : PROP) -: AsEmpValid d (P ⊢ Q) io1 PROP io2 bi iprop(P -∗ Q) where +: AsEmpValid d (P ⊢ Q) io PROP bi iprop(P -∗ Q) where as_emp_valid := ⟨λ _ => entails_wand, λ _ => wand_entails⟩ instance asEmpValid_bientails [bi : BI PROP] (P Q : PROP) -: AsEmpValid d (P ⊣⊢ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where +: AsEmpValid d (P ⊣⊢ Q) io PROP bi iprop(P ∗-∗ Q) where as_emp_valid := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩ @[rocq_alias as_emp_valid_equiv] instance asEmpValid_equiv [bi : BI PROP] (P Q : PROP) -: AsEmpValid d (P ≡ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where +: AsEmpValid d (P ≡ Q) io PROP bi iprop(P ∗-∗ Q) where as_emp_valid := ⟨λ _ h => equiv_wandIff (equiv_iff.1 h), λ _ h => (equiv_iff.2 (wandIff_equiv h))⟩ @[rocq_alias as_emp_valid_forall] instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP) - [hP : ∀ x, AsEmpValid d (Φ x) io1 PROP io2 bi iprop(P x)] -: AsEmpValid d (∀ x, Φ x) io1 PROP io2 bi iprop(∀ x, P x) where + [hP : ∀ x, AsEmpValid d (Φ x) io PROP bi iprop(P x)] +: AsEmpValid d (∀ x, Φ x) io PROP bi iprop(∀ x, P x) where as_emp_valid := ⟨λ hd h => forall_intro λ x => (hP x).1.1 hd (h x), λ hd h x => (hP x).1.2 hd $ h.trans (forall_elim x)⟩ @@ -173,6 +173,7 @@ instance intoForall_persistently [BI PROP] [BIPersistentlyForall PROP] (P : PROP [h : IntoForall P Φ] : IntoForall iprop( P) (fun a => iprop( (Φ a))) where into_forall := (persistently_mono h.1).trans persistently_forall_mp +set_option synthInstance.checkSynthOrder false in @[ipm_backtrack, rocq_alias into_forall_wand_pure] instance intoForall_wand_pure [BI PROP] (P Q : PROP) Φ [h : FromPure a P .out Φ] : IntoForall iprop(P -∗ Q) (fun _ : Φ => Q) where @@ -678,6 +679,7 @@ instance intoPure_pure_or (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∨ P2) (φ1 ∨ φ2) where into_pure := (or_mono h1.1 h2.1).trans pure_or.1 +set_option synthInstance.checkSynthOrder false in @[rocq_alias into_pure_pure_impl] instance intoPure_pure_imp (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : FromPure a P1 .out φ1] [or : TCOr (TCEq a false) (BIAffine PROP)] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 → P2) (φ1 → φ2) where diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean index f20e854f6..13af6d40c 100644 --- a/Iris/Iris/ProofMode/ProofModeM.lean +++ b/Iris/Iris/ProofMode/ProofModeM.lean @@ -123,7 +123,7 @@ def startProofMode (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withCont let prop ← mkFreshExprMVarQ q(Type u) let P ← mkFreshExprMVarQ q($prop) let bi ← mkFreshExprMVarQ q(BI $prop) - let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal .out $prop .out $bi $P) + let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal .out $prop $bi $P) | throwError "istart: {goal} is not an emp valid" if !mvars.isEmpty then throwError "istart does not support creating mvars" diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index a779ecc05..58875bb19 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -62,7 +62,7 @@ checking synthesis order checking, which is useful (though not perfect).) inductive ParamKind | in | out - | semiOut + | semiOut (idx : Nat) (negate : Bool) | uncheckedIn | inout deriving Inhabited @@ -71,7 +71,7 @@ instance : ToString ParamKind where toString | .in => "in" | .out => "out" - | .semiOut => "semiOut" + | .semiOut idx negate => s!"semiOut {idx} {negate}" | .uncheckedIn => "uncheckedIn" | .inout => "inout" @@ -122,30 +122,68 @@ initialize ipmClassesExt : private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Array ParamKind) := (ipmClassesExt.getState env).paramMap.find? declName -private partial def computeParamKinds (params : Array ParamKind) (wasInOut : Bool) (type : Expr) : +/-- + Analogous to `semiOutParam`, with the *negation* of the `InOut` value + indicating whether this is an input parameter or an output paramter for + the purpose of type class synthesis. + + This should be used instead of `semiOutParam` when the custom IPM type + class synthesiser is used. +-/ +@[reducible, expose] +def semiOutParamPos (_io : InOut) (α : Sort u) : Sort u := α + +/-- + Analogous to `semiOutParam`, with the *negation* of the `InOut` value + indicating whether this is an input parameter or an output paramter for + the purpose of type class synthesis. + + This should be used instead of `semiOutParam` when the custom IPM type + class synthesiser is used. +-/ +@[reducible, expose] +def semiOutParamNeg (_io : InOut) (α : Sort u) : Sort u := α + +/-- If `d` is `semiOutParam self α` or `semiOutParamNeg self α`, return `(negate, self)`. -/ +private def semiOutParamGoverning? (d : Expr) : Option (Bool × Expr) := + if d.isAppOfArity ``semiOutParamPos 2 then + some (false, d.getAppArgs[0]!) + else if d.isAppOfArity ``semiOutParamNeg 2 then + some (true, d.getAppArgs[0]!) + else + none + +private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : Except MessageData (Array ParamKind) := match type with | .forallE _ d b _ => - if wasInOut then - if d.isSemiOutParam then - computeParamKinds (params.push .semiOut) false b + -- we need to check this before outParam since `outParam (uncheckedInParam _)` should be + -- an `uncheckedInParam` + if isUncheckedInParam d then + computeParamKinds (params.push .uncheckedIn) b + else if d.isOutParam then + computeParamKinds (params.push .out) b + else if let some ⟨negate, self⟩ := semiOutParamGoverning? d then + if !self.isBVar then + Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ + `semiOutParamNeg` whose governing argument is not a direct reference to an earlier parameter" + else if self.bvarIdx! ≥ params.size then + Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ + `semiOutParamNeg` with an out-of-range governing reference" else - Except.error m!"invalid ipm_class, parameter #{params.size} is a `InOut` that is not followed \ - by a `semiOutParam`" + let govIdx := params.size - 1 - self.bvarIdx! + if params[govIdx]! matches .inout then + computeParamKinds (params.push (.semiOut govIdx negate)) b + else + Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ + `semiOutParamNeg` referencing parameter #{govIdx}, which is not an `InOut` parameter" + else if d.isSemiOutParam then + Except.error m!"invalid ipm_class, parameter #{params.size+1} is a `semiOutParam` that is \ + not preceded by an `InOut`" + else if d.isAppOfArity ``InOut 0 then + computeParamKinds (params.push .inout) b else - -- we need to check this before outParam since `outParam (uncheckedInParam _)` should be - -- an `uncheckedInParam` - if isUncheckedInParam d then - computeParamKinds (params.push .uncheckedIn) false b - else if d.isOutParam then - computeParamKinds (params.push .out) false b - else if d.isSemiOutParam then - Except.error m!"invalid ipm_class, parameter #{params.size+1} is a `semiOutParam` that is \ - not preceded by an `InOut`" - else if d.isAppOfArity ``InOut 0 then - computeParamKinds (params.push .inout) true b - else - computeParamKinds (params.push .in) false b + computeParamKinds (params.push .in) b | _ => return params /-- @@ -164,14 +202,19 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do let args := typeBody.getAppArgs if args.size != params.size then throwError "mismatched number of arguments" - let mut inoutIsIn := false + + let mut resolved : Std.HashMap Nat Bool := {} let mut mvarInputs := #[] + for i in 0...args.size do let param := params[i]! let arg := args[i]! - let param := if param matches .semiOut then - if inoutIsIn then .in else .out - else param + + let param : ParamKind := match param with + | .semiOut idx negate => + if resolved[idx]! ^^ negate then ParamKind.in else ParamKind.out + | p => p + match param with | .uncheckedIn => pure () | .in => if arg.getAppFn.isMVar then mvarInputs := mvarInputs.push i @@ -179,12 +222,12 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do throwError "parameter #{i} {arg} of {type} is an out parameter that is not an mvar" | .inout => if arg.isAppOfArity ``InOut.in 0 then - inoutIsIn := true + resolved := resolved.insert i true else if arg.isAppOfArity ``InOut.out 0 then - inoutIsIn := false + resolved := resolved.insert i false else throwError "parameter #{i} {arg} of {type} is an inout parameter that is not .in nor .out" - | .semiOut => unreachable! + | .semiOut _ _ => unreachable! return some mvarInputs syntax (name := ipm_class) "ipm_class" : attr @@ -198,7 +241,7 @@ initialize registerBuiltinAttribute { let some decl := env.find? declName | throwError "unknown declaration '{declName}'" unless kind == AttributeKind.global do throwAttrMustBeGlobal `ipm_class kind - let params ← ofExcept <| computeParamKinds #[] false decl.type + let params ← ofExcept <| computeParamKinds #[] decl.type trace[Meta.synthInstance.ipmParamKinds] m!"IPM params of {declName}: {params}" let env := ipmClassesExt.addEntry env {name := declName, params} setEnv env diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index 9f5ec3854..2c1fae59f 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -117,10 +117,10 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) let goal' := q(iprop(□ $A2 -∗ $goal)) let pf ← k1 hyps goal' A1 fun hyps goal' => do let goal'' ← mkFreshExprMVarQ q($prop) - let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in iprop(□ $A2) $goal'') + let .some inst ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in iprop(□ $A2) $goal'') | throwError "icases: internal error: {goal'} is not a wand" let pf ← k2 hyps goal'' A2 k - return q((wand_intro $pf).trans (from_wand .in (Q1:=iprop(□ $A2)))) + return q((wand_intro $pf).trans $(inst).from_wand) return q(and_elim_intuitionistic $pf) | .inr _ => let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A $A1 $A2) @@ -128,10 +128,10 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) let goal' := q(iprop($A2 -∗ $goal)) let pf ← k1 hyps goal' A1 fun hyps goal' => do let goal'' ← mkFreshExprMVarQ q($prop) - let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in $A2 $goal'') + let .some inst ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in $A2 $goal'') | throwError "icases: internal error: {goal'} is not a wand" let pf ← k2 hyps goal'' A2 k - return q((wand_intro $pf).trans (from_wand .in (Q1:=$A2))) + return q((wand_intro $pf).trans $(inst).from_wand) return q(sep_elim_spatial (A := $A) $pf) /-- Destruct a disjunction hypothesis [A] into two cases and continue separately on each branch. -/ diff --git a/Iris/Iris/ProofMode/Tactics/HaveCore.lean b/Iris/Iris/ProofMode/Tactics/HaveCore.lean index 83e5f6aed..49d27ace6 100644 --- a/Iris/Iris/ProofMode/Tactics/HaveCore.lean +++ b/Iris/Iris/ProofMode/Tactics/HaveCore.lean @@ -24,7 +24,7 @@ public section open BI theorem have_asEmpValid [bi : BI PROP] {φ} {P Q : PROP} - [h1 : AsEmpValid .into φ .in PROP .in bi P] (h : φ) : Q ⊢ Q ∗ □ P := + [h1 : AsEmpValid .into φ .in PROP bi P] (h : φ) : Q ⊢ Q ∗ □ P := sep_emp.2.trans (sep_mono_right $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h))) public meta section @@ -83,7 +83,7 @@ private def iHaveCore {e} (hyps : @Hyps u prop bi e) have val : Q($ty) := val let hyp ← mkFreshExprMVarQ q($prop) - let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty .in $prop .in $bi $hyp) + let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty .in $prop $bi $hyp) | throwError m!"ihave: {ty} is not an entailment" return ⟨_, hyps, q(true), hyp, q(have_asEmpValid $val)⟩ diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index f6cf3fd62..917f0175d 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -28,9 +28,10 @@ theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} exact (and_mono_right inst.1).trans <| persistently_and_intuitionistically_sep_right.1.trans h theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} - [FromWand Q .out A1 A2] [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)] + [instFromWand : FromWand Q .out A1 A2] + [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)] (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by - refine (wand_intro ?_).trans (from_wand .out (Q1:=A1)) + refine (wand_intro ?_).trans instFromWand.from_wand exact match or with | TCOr.l => (sep_mono_right <| (affine_affinely A1).2.trans (affinely_mono inst.1)).trans h | TCOr.r => (sep_mono_right <| inst.1.trans absorbingly_intuitionistically.2).trans <| @@ -48,7 +49,8 @@ theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP} persistently_and_intuitionistically_sep_left.1.trans <| sep_mono_left intuitionistically_elim theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} - [FromWand Q .out A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans (from_wand .out (Q1:=A1)) + [inst : FromWand Q .out A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := + (wand_intro h).trans inst.from_wand public meta section open Lean Elab Tactic Meta Qq BI Std From e9dc50bfe50a21d7a6711610bdd2215e2cdf567f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 14:47:30 +0200 Subject: [PATCH 02/26] Bug fix within `SynthInstance.lean` --- Iris/Iris/ProofMode/SynthInstance.lean | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/SynthInstance.lean b/Iris/Iris/ProofMode/SynthInstance.lean index fa24d8ecc..202564b45 100644 --- a/Iris/Iris/ProofMode/SynthInstance.lean +++ b/Iris/Iris/ProofMode/SynthInstance.lean @@ -129,8 +129,20 @@ partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do let some (mctx', subgoals) ← withAssignableSyntheticOpaque (SynthInstance.tryResolve mvar inst) | return (none, false) setMCtx mctx' - for g in subgoals do - let some _ ← synthInstanceMainCore g | return (none, true) + let mut pending := subgoals + let mut progress := true + while progress && !pending.isEmpty do + progress := false + let mut stillPending := [] + for g in pending do + let mctxBefore ← getMCtx + if let some _ ← synthInstanceMainCore g then + progress := true + else + setMCtx mctxBefore + stillPending := stillPending.cons g + pending := stillPending + if !pending.isEmpty then return (none, true) return (some (), true) if res.isSome then return res From e03356c355ab2ccf7e20c733d54e73a3094c5077 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 14:47:52 +0200 Subject: [PATCH 03/26] Update test for Issue #456 in `Tests/Instances.lean` --- Iris/Iris/Tests/Instances.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 612fba582..35f91dd6f 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -304,11 +304,11 @@ section issue_456 -- test for https://github.com/leanprover-community/iris-lean/issues/456 @[ipm_class] -class C (_ : InOut) (a : semiOutParam Nat) (_ : InOut) (b : semiOutParam Nat) : Prop where +class C (io : InOut) (a : semiOutParamPos io Nat) (b : semiOutParamNeg io Nat) : Prop where -abbrev CMerge (a b : semiOutParam Nat) := C .out a .in b +abbrev CMerge (a b : Nat) := C .out a b -abbrev CSplit (a b : semiOutParam Nat) := C .in a .out b +abbrev CSplit (a b : Nat) := C .in a b set_option synthInstance.checkSynthOrder false in instance instMerge (b : Nat) : CMerge (b + 1) b := ⟨⟩ From 82ef8840ecf2d38cf87ae0b156dd9f1e0c5ec8a6 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 14:56:28 +0200 Subject: [PATCH 04/26] Update error message in `SynthInstanceAttr.lean` and more tests --- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 4 ++-- Iris/Iris/Tests/Instances.lean | 23 ++++++++++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index 58875bb19..1a8e68e39 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -178,8 +178,8 @@ Except MessageData (Array ParamKind) := Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ `semiOutParamNeg` referencing parameter #{govIdx}, which is not an `InOut` parameter" else if d.isSemiOutParam then - Except.error m!"invalid ipm_class, parameter #{params.size+1} is a `semiOutParam` that is \ - not preceded by an `InOut`" + Except.error m!"invalid ipm_class, parameter #{params.size+1} is a `semiOutParam`. Use \ + `semiOutParamPos`/`semiOutParamNeg` instead" else if d.isAppOfArity ``InOut 0 then computeParamKinds (params.push .inout) b else diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 35f91dd6f..4fb53fd11 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -327,3 +327,26 @@ instance instSplit (k : Nat) : CSplit (k + 1) k := ⟨⟩ #ipm_synth CSplit _ _ end issue_456 + +section semiOutParam + +/-- +error: invalid ipm_class, parameter #2 is a `semiOutParam`. +Use `semiOutParamPos`/`semiOutParamNeg` instead +-/ +#guard_msgs in +@[ipm_class] +class C1 (io : InOut) (a : semiOutParam Nat) : Prop where + +/-- +error: invalid ipm_class, parameter #2 is a `semiOutParamPos`/`semiOutParamNeg` +whose governing argument is not a direct reference to an earlier parameter +-/ +#guard_msgs in +@[ipm_class] +class C2 {α} (a : α) (a : semiOutParamPos .in Nat) : Prop where + +/- The attribute `semiOutParam` is still relevant for regular type classes -/ +class C3 (io : InOut) (a : semiOutParam Nat) : Prop where + +end semiOutParam From 464675cb849cebe89c0e5cd66b051b9af068b31f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 15:47:45 +0200 Subject: [PATCH 05/26] Fix `IsOp` usage and synthesis order check --- Iris/Iris/Algebra/ReservationMap.lean | 5 ++--- Iris/Iris/Instances/Lib/FUpd.lean | 1 + 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/Algebra/ReservationMap.lean b/Iris/Iris/Algebra/ReservationMap.lean index bebc94a68..888f69633 100644 --- a/Iris/Iris/Algebra/ReservationMap.lean +++ b/Iris/Iris/Algebra/ReservationMap.lean @@ -389,10 +389,9 @@ theorem singleton_mono {k} {a b : A} (Hab : a ≼ b) : singleton (H := H) k a let ⟨z, hz⟩ := Hab ⟨singleton k z, (NonExpansive.eqv hz).trans (singleton_op k a z)⟩ -set_option synthInstance.checkSynthOrder false in @[rocq_alias reservation_map_data_is_op] -instance {ia ib₁ ib₂ : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp ia a ib₁ b₁ ib₂ b₂] : - IsOp ia (singleton (H := H) k a) ib₁ (singleton k b₁) ib₂ (singleton k b₂) where +instance {io : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp io a b₁ b₂] : + IsOp io (singleton (H := H) k a) (singleton k b₁) (singleton k b₂) where is_op := .trans (NonExpansive.eqv hv.is_op ) (singleton_op k b₁ b₂) @[rocq_alias reservation_map_token_union] diff --git a/Iris/Iris/Instances/Lib/FUpd.lean b/Iris/Iris/Instances/Lib/FUpd.lean index b150420b0..df02d1bb1 100644 --- a/Iris/Iris/Instances/Lib/FUpd.lean +++ b/Iris/Iris/Instances/Lib/FUpd.lean @@ -485,6 +485,7 @@ instance fromPure_fupd_finally (a : Bool) (E : CoPset) (P : IProp GF) (φ : Prop refine .trans ?_ (fupd_finally_intro E _) cases a <;> simp only [affinelyIf_false, affinelyIf_true] <;> exact Plain.plain +set_option synthInstance.checkSynthOrder false in @[rocq_alias from_forall_fupd_pure] instance fromForall_fupd_pure {A : Type _} (E : CoPset) (P : IProp GF) (Φ : A → IProp GF) (φ : A → Prop) [h : FromForall P Φ] [hp : ∀ x, FromPure false (Φ x) .out (φ x)] : From 20fb4fbc31a75be723876b4982ca2f0a46d03302 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 16:04:53 +0200 Subject: [PATCH 06/26] Combine `semiOutParamPos` and `semiOutParamNeg` as `semiOutParamIPM` with a Boolean value indicating negation --- Iris/Iris/Algebra/IsOp.lean | 5 +-- Iris/Iris/ProofMode/Classes.lean | 14 +++---- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 48 ++++++++++------------ Iris/Iris/Tests/Instances.lean | 17 ++++---- 4 files changed, 37 insertions(+), 47 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 89be115d7..c3ce6bdfa 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -23,9 +23,8 @@ section IsOp -/ @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR] class IsOp [CMRA α] - (io : InOut) (a : semiOutParamPos io α) - (b1 : semiOutParamNeg io α) - (b2 : semiOutParamNeg io α) where + (io : InOut) (a : semiOutParamIPM io α) + (b1 : semiOutParamIPM io α true) (b2 : semiOutParamIPM io α true) where is_op : a ≡ b1 • b2 /-- diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index faac957bb..0f5af00e0 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -28,8 +28,8 @@ inductive AsEmpValid.Direction where @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (io : InOut) - (PROP : semiOutParamPos io $ Type _) - (bi : semiOutParamPos io $ BI PROP) (P : outParam $ PROP) where + (PROP : semiOutParamIPM io $ Type _) + (bi : semiOutParamIPM io $ BI PROP) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) @[rocq_alias as_emp_valid_1] @@ -54,7 +54,7 @@ export FromImp (from_imp) @[ipm_class, rocq_alias FromWand] class FromWand {PROP} [BI PROP] (P : PROP) (io : InOut) - (Q1 : semiOutParamPos io PROP) (Q2 : outParam $ PROP) where + (Q1 : semiOutParamIPM io PROP) (Q2 : outParam $ PROP) where from_wand : (Q1 -∗ Q2) ⊢ P export FromWand (from_wand) @@ -62,8 +62,8 @@ export FromWand (from_wand) @[ipm_class, rocq_alias IntoWand] class IntoWand {PROP} [BI PROP] (p q : Bool) (R : PROP) - (ioP : InOut) (P : semiOutParamPos ioP PROP) - (ioQ : InOut) (Q : semiOutParamPos ioQ PROP) where + (ioP : InOut) (P : semiOutParamIPM ioP PROP) + (ioQ : InOut) (Q : semiOutParamIPM ioQ PROP) where into_wand : □?p R ⊢ □?q P -∗ Q export IntoWand (into_wand) @@ -139,7 +139,7 @@ export IntoAbsorbingly (into_absorbingly) @[ipm_class, rocq_alias FromAssumption, rocq_alias KnownLFromAssumption, rocq_alias KnownRFromAssumption] class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut) - (P : semiOutParamPos ioP PROP) (Q : PROP) where + (P : semiOutParamIPM ioP PROP) (Q : PROP) where from_assumption : □?p P ⊢ Q export FromAssumption (from_assumption) @@ -152,7 +152,7 @@ export IntoPure (into_pure) @[ipm_class, rocq_alias FromPure, rocq_alias FromPureT] class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut) - (φ : semiOutParamPos ioφ Prop) where + (φ : semiOutParamIPM ioφ Prop) where from_pure : ?a ⌜φ⌝ ⊢ P export FromPure (from_pure) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index 1a8e68e39..6413b28cf 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Michael Sammler +Authors: Michael Sammler, Alvin Tang -/ module @@ -123,18 +123,10 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar (ipmClassesExt.getState env).paramMap.find? declName /-- - Analogous to `semiOutParam`, with the *negation* of the `InOut` value - indicating whether this is an input parameter or an output paramter for - the purpose of type class synthesis. + Analogous to `semiOutParam`, with - This should be used instead of `semiOutParam` when the custom IPM type - class synthesiser is used. --/ -@[reducible, expose] -def semiOutParamPos (_io : InOut) (α : Sort u) : Sort u := α -/-- - Analogous to `semiOutParam`, with the *negation* of the `InOut` value + with the *negation* of the `InOut` value indicating whether this is an input parameter or an output paramter for the purpose of type class synthesis. @@ -142,16 +134,18 @@ def semiOutParamPos (_io : InOut) (α : Sort u) : Sort u := α class synthesiser is used. -/ @[reducible, expose] -def semiOutParamNeg (_io : InOut) (α : Sort u) : Sort u := α +def semiOutParamIPM (_io : InOut) (α : Sort u) (_negate : Bool := false) : Sort u := semiOutParam α /-- If `d` is `semiOutParam self α` or `semiOutParamNeg self α`, return `(negate, self)`. -/ -private def semiOutParamGoverning? (d : Expr) : Option (Bool × Expr) := - if d.isAppOfArity ``semiOutParamPos 2 then - some (false, d.getAppArgs[0]!) - else if d.isAppOfArity ``semiOutParamNeg 2 then - some (true, d.getAppArgs[0]!) - else - none +private def semiOutParamGoverning? (d : Expr) : Option <| Bool × Expr := do + if d.isAppOfArity ``semiOutParamIPM 3 then + let negate := d.getAppArgs[2]! + if negate.isConstOf ``Bool.true then + some (true, d.getAppArgs[0]!) + else if negate.isConstOf ``Bool.false then + some (false, d.getAppArgs[0]!) + else none + else none private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : Except MessageData (Array ParamKind) := @@ -165,21 +159,21 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .out) b else if let some ⟨negate, self⟩ := semiOutParamGoverning? d then if !self.isBVar then - Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ - `semiOutParamNeg` whose governing argument is not a direct reference to an earlier parameter" + Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamIPM` \ + with the `InOut` argument not directly referencing to an earlier parameter" else if self.bvarIdx! ≥ params.size then - Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ - `semiOutParamNeg` with an out-of-range governing reference" + Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamIPM` \ + with an out-of-range governing reference" else let govIdx := params.size - 1 - self.bvarIdx! if params[govIdx]! matches .inout then computeParamKinds (params.push (.semiOut govIdx negate)) b else - Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamPos`/\ - `semiOutParamNeg` referencing parameter #{govIdx}, which is not an `InOut` parameter" + Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamIPM` \ + referencing parameter #{govIdx}, which is not an `InOut` parameter" else if d.isSemiOutParam then - Except.error m!"invalid ipm_class, parameter #{params.size+1} is a `semiOutParam`. Use \ - `semiOutParamPos`/`semiOutParamNeg` instead" + Except.error m!"invalid ipm_class, parameter #{params.size + 1} is a `semiOutParam`. Use \ + `semiOutParamIPM` instead" else if d.isAppOfArity ``InOut 0 then computeParamKinds (params.push .inout) b else diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 4fb53fd11..423c445d5 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -304,7 +304,7 @@ section issue_456 -- test for https://github.com/leanprover-community/iris-lean/issues/456 @[ipm_class] -class C (io : InOut) (a : semiOutParamPos io Nat) (b : semiOutParamNeg io Nat) : Prop where +class C (io : InOut) (a : semiOutParamIPM io Nat) (b : semiOutParamIPM io Nat true) : Prop where abbrev CMerge (a b : Nat) := C .out a b @@ -328,25 +328,22 @@ instance instSplit (k : Nat) : CSplit (k + 1) k := ⟨⟩ end issue_456 -section semiOutParam +section semiOutParamIPM -/-- -error: invalid ipm_class, parameter #2 is a `semiOutParam`. -Use `semiOutParamPos`/`semiOutParamNeg` instead --/ +/-- error: invalid ipm_class, parameter #2 is a `semiOutParam`. Use `semiOutParamIPM` instead -/ #guard_msgs in @[ipm_class] class C1 (io : InOut) (a : semiOutParam Nat) : Prop where /-- -error: invalid ipm_class, parameter #2 is a `semiOutParamPos`/`semiOutParamNeg` -whose governing argument is not a direct reference to an earlier parameter +error: invalid ipm_class, parameter #2 is a `semiOutParamIPM` with the `InOut` +argument not directly referencing to an earlier parameter -/ #guard_msgs in @[ipm_class] -class C2 {α} (a : α) (a : semiOutParamPos .in Nat) : Prop where +class C2 {α} (a : α) (a : semiOutParamIPM .in Nat false) : Prop where /- The attribute `semiOutParam` is still relevant for regular type classes -/ class C3 (io : InOut) (a : semiOutParam Nat) : Prop where -end semiOutParam +end semiOutParamIPM From bc8f2be7f6f4daf75052354162468ceb10b6cfce Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 16:11:21 +0200 Subject: [PATCH 07/26] Remove unnecessary `set_option synthInstance.checkSynthOrder false` --- Iris/Iris/Algebra/IsOp.lean | 12 ++---------- Iris/Iris/Algebra/UFrac.lean | 1 - Iris/Iris/Algebra/View.lean | 1 - 3 files changed, 2 insertions(+), 12 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index c3ce6bdfa..1b76b9556 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -33,19 +33,13 @@ class IsOp [CMRA α] abbrev IsOpMerge [CMRA α] (a b1 b2 : α) := IsOp .out a b1 b2 abbrev IsOpSplit [CMRA α] (a b1 b2 : α) := IsOp .in a b1 b2 -set_option synthInstance.checkSynthOrder false in -/-- - Merging with `•` should have the lowest priority. --/ +/-- Merging with `•` should have the lowest priority. -/ @[rocq_alias is_op_op] instance (priority := default - 100) isOpMerge_op [CMRA α] (a b : α) : IsOpMerge (a • b) a b where is_op := .rfl -set_option synthInstance.checkSynthOrder false in -/-- - Splitting with `•` should have the highest priority. --/ +/-- 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 @@ -64,14 +58,12 @@ instance isOp_pair [CMRA α] {io : InOut} IsOp io (a, a') (b1, b1') (b2, b2') where is_op := OFE.equiv_prod_ext h1.is_op h2.is_op -set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_pair_core_id_l] instance isOp_pair_core_id_l [CMRA α] [CMRA β] {io : InOut} (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp io a' b1' b2'] : IsOp io (a, a') (a, b1') (a, b2') where is_op := OFE.equiv_prod_ext (op_self a).symm h2.is_op -set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_pair_core_id_r] instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {io : InOut} (a b1 b2 : α) (a' : β) diff --git a/Iris/Iris/Algebra/UFrac.lean b/Iris/Iris/Algebra/UFrac.lean index 947a5548f..3902a9c7f 100644 --- a/Iris/Iris/Algebra/UFrac.lean +++ b/Iris/Iris/Algebra/UFrac.lean @@ -94,7 +94,6 @@ instance {q : UFrac} : CMRA.IdFree q where id_free0_r b _ H := by have := b.frac.2; simp only [dist_iff, ext_iff, frac_op] at H; grind -set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_ufrac] instance (q : UFrac) : IsOp io q ⟨q.frac.half⟩ ⟨q.frac.half⟩ where is_op := OFE.Equiv.of_eq <| ext_iff.mpr (Qp.half_add_half q.frac).symm diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index c845c4a56..000a2ced3 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -331,7 +331,6 @@ theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View R) ≡ (●V{dq1} a) • NonExpansive₂.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv .rfl Agree.idemp.symm)) UCMRA.unit_left_id.symm -set_option synthInstance.checkSynthOrder false in @[rocq_alias view_auth_dfrac_is_op] instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac} {a : A} [h : IsOp io dq dq1 dq2] : From 2f0df331922e49039f02fa6cdcddd45d5f67afd4 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 16:46:00 +0200 Subject: [PATCH 08/26] Further generalisation such that the `InOut` argument for `semiOutParamIPM` may involve pattern matching, conditionals, etc. --- Iris/Iris/Algebra/IsOp.lean | 2 +- Iris/Iris/ProofMode/Classes.lean | 11 ++-- Iris/Iris/ProofMode/Instances.lean | 20 +++---- Iris/Iris/ProofMode/ProofModeM.lean | 2 +- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 62 ++++++++++------------ Iris/Iris/ProofMode/Tactics/HaveCore.lean | 4 +- Iris/Iris/Tests/Instances.lean | 16 +++--- 7 files changed, 55 insertions(+), 62 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 1b76b9556..1789972d4 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -24,7 +24,7 @@ section IsOp @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR] class IsOp [CMRA α] (io : InOut) (a : semiOutParamIPM io α) - (b1 : semiOutParamIPM io α true) (b2 : semiOutParamIPM io α true) where + (b1 : semiOutParamIPM io.negate α) (b2 : semiOutParamIPM io.negate α) where is_op : a ≡ b1 • b2 /-- diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index 0f5af00e0..beab230f2 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -27,18 +27,19 @@ inductive AsEmpValid.Direction where | from @[ipm_class, rocq_alias AsEmpValid] -class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (io : InOut) - (PROP : semiOutParamIPM io $ Type _) - (bi : semiOutParamIPM io $ BI PROP) (P : outParam $ PROP) where +class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) + (PROP : semiOutParamIPM (match d with | .into => .in | .from => .out) $ Type _) + (bi : semiOutParamIPM (match d with | .into => .in | .from => .out) $ BI PROP) + (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) @[rocq_alias as_emp_valid_1] theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) - [inst : AsEmpValid .into φ .in PROP bi P] : φ → ⊢ P := + [inst : AsEmpValid .into φ PROP bi P] : φ → ⊢ P := inst.as_emp_valid.left rfl @[rocq_alias as_emp_valid_2] theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) - [inst : AsEmpValid .from φ .out PROP bi P] : (⊢ P) → φ := + [inst : AsEmpValid .from φ PROP bi P] : (⊢ P) → φ := inst.as_emp_valid.right rfl /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean index ee0d85d28..d4bdcf545 100644 --- a/Iris/Iris/ProofMode/Instances.lean +++ b/Iris/Iris/ProofMode/Instances.lean @@ -19,27 +19,27 @@ open Iris.BI Iris.Std -- AsEmpValid @[rocq_alias as_emp_valid_emp_valid] instance (priority := default + 10) asEmpValidEmpValid - [bi : BI PROP] d (P : PROP) : - AsEmpValid d (⊢ P) io PROP bi P := ⟨by simp⟩ + [bi : BI PROP] d (P : PROP) : AsEmpValid d (⊢ P) PROP bi P where + as_emp_valid := by simp @[rocq_alias as_emp_valid_entails] -instance asEmpValid_entails [bi : BI PROP] d (P Q : PROP) -: AsEmpValid d (P ⊢ Q) io PROP bi iprop(P -∗ Q) where +instance asEmpValid_entails [bi : BI PROP] d (P Q : PROP) : + AsEmpValid d (P ⊢ Q) PROP bi iprop(P -∗ Q) where as_emp_valid := ⟨λ _ => entails_wand, λ _ => wand_entails⟩ -instance asEmpValid_bientails [bi : BI PROP] (P Q : PROP) -: AsEmpValid d (P ⊣⊢ Q) io PROP bi iprop(P ∗-∗ Q) where +instance asEmpValid_bientails [bi : BI PROP] (P Q : PROP) : + AsEmpValid d (P ⊣⊢ Q) PROP bi iprop(P ∗-∗ Q) where as_emp_valid := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩ @[rocq_alias as_emp_valid_equiv] -instance asEmpValid_equiv [bi : BI PROP] (P Q : PROP) -: AsEmpValid d (P ≡ Q) io PROP bi iprop(P ∗-∗ Q) where +instance asEmpValid_equiv [bi : BI PROP] (P Q : PROP) : + AsEmpValid d (P ≡ Q) PROP bi iprop(P ∗-∗ Q) where as_emp_valid := ⟨λ _ h => equiv_wandIff (equiv_iff.1 h), λ _ h => (equiv_iff.2 (wandIff_equiv h))⟩ @[rocq_alias as_emp_valid_forall] instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP) - [hP : ∀ x, AsEmpValid d (Φ x) io PROP bi iprop(P x)] -: AsEmpValid d (∀ x, Φ x) io PROP bi iprop(∀ x, P x) where + [hP : ∀ x, AsEmpValid d (Φ x) PROP bi iprop(P x)] : + AsEmpValid d (∀ x, Φ x) PROP bi iprop(∀ x, P x) where as_emp_valid := ⟨λ hd h => forall_intro λ x => (hP x).1.1 hd (h x), λ hd h x => (hP x).1.2 hd $ h.trans (forall_elim x)⟩ diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean index 13af6d40c..3f04a1998 100644 --- a/Iris/Iris/ProofMode/ProofModeM.lean +++ b/Iris/Iris/ProofMode/ProofModeM.lean @@ -123,7 +123,7 @@ def startProofMode (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withCont let prop ← mkFreshExprMVarQ q(Type u) let P ← mkFreshExprMVarQ q($prop) let bi ← mkFreshExprMVarQ q(BI $prop) - let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal .out $prop $bi $P) + let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $prop $bi $P) | throwError "istart: {goal} is not an emp valid" if !mvars.isEmpty then throwError "istart does not support creating mvars" diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index 6413b28cf..ad053b37d 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -21,6 +21,12 @@ inductive InOut where | in | out +/-- `InOut.negate` converts `.in` into `.out`, and vice versa. -/ +@[reducible, expose] +def InOut.negate : InOut → InOut + | .in => .out + | .out => .in + /-- Marker for an unchecked input parameter. -/ @[reducible, expose] def uncheckedInParam (α : Sort u) : Sort u := α @@ -62,7 +68,7 @@ checking synthesis order checking, which is useful (though not perfect).) inductive ParamKind | in | out - | semiOut (idx : Nat) (negate : Bool) + | semiOut (expr : Expr) | uncheckedIn | inout deriving Inhabited @@ -71,7 +77,7 @@ instance : ToString ParamKind where toString | .in => "in" | .out => "out" - | .semiOut idx negate => s!"semiOut {idx} {negate}" + | .semiOut expr => s!"semiOut {expr}" | .uncheckedIn => "uncheckedIn" | .inout => "inout" @@ -123,28 +129,22 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar (ipmClassesExt.getState env).paramMap.find? declName /-- - Analogous to `semiOutParam`, with - + Analogous to `semiOutParam`, with the explicit argument `_io` being an + `InOut` value, which determines whether this is is an input parameter or an + output paramter for the purpose of type class synthesis. - with the *negation* of the `InOut` value - indicating whether this is an input parameter or an output paramter for - the purpose of type class synthesis. + One can use `InOut.negate` to negate the `InOut` value. This should be used instead of `semiOutParam` when the custom IPM type class synthesiser is used. -/ @[reducible, expose] -def semiOutParamIPM (_io : InOut) (α : Sort u) (_negate : Bool := false) : Sort u := semiOutParam α +def semiOutParamIPM (_io : InOut) (α : Sort u) : Sort u := semiOutParam α /-- If `d` is `semiOutParam self α` or `semiOutParamNeg self α`, return `(negate, self)`. -/ -private def semiOutParamGoverning? (d : Expr) : Option <| Bool × Expr := do - if d.isAppOfArity ``semiOutParamIPM 3 then - let negate := d.getAppArgs[2]! - if negate.isConstOf ``Bool.true then - some (true, d.getAppArgs[0]!) - else if negate.isConstOf ``Bool.false then - some (false, d.getAppArgs[0]!) - else none +private def semiOutParamGoverning? (d : Expr) : Option Expr := do + if d.isAppOfArity ``semiOutParamIPM 2 then + some d.getAppArgs[0]! else none private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : @@ -157,20 +157,8 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .uncheckedIn) b else if d.isOutParam then computeParamKinds (params.push .out) b - else if let some ⟨negate, self⟩ := semiOutParamGoverning? d then - if !self.isBVar then - Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamIPM` \ - with the `InOut` argument not directly referencing to an earlier parameter" - else if self.bvarIdx! ≥ params.size then - Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamIPM` \ - with an out-of-range governing reference" - else - let govIdx := params.size - 1 - self.bvarIdx! - if params[govIdx]! matches .inout then - computeParamKinds (params.push (.semiOut govIdx negate)) b - else - Except.error m!"invalid ipm_class, parameter #{params.size} is a `semiOutParamIPM` \ - referencing parameter #{govIdx}, which is not an `InOut` parameter" + else if let some expr := semiOutParamGoverning? d then + computeParamKinds (params.push (.semiOut expr)) b else if d.isSemiOutParam then Except.error m!"invalid ipm_class, parameter #{params.size + 1} is a `semiOutParam`. Use \ `semiOutParamIPM` instead" @@ -204,10 +192,14 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do let param := params[i]! let arg := args[i]! - let param : ParamKind := match param with - | .semiOut idx negate => - if resolved[idx]! ^^ negate then ParamKind.in else ParamKind.out - | p => p + let param : ParamKind ← match param with + | .semiOut expr => + let expr ← whnf (expr.instantiateRev (args.extract 0 i)) + if expr.isAppOfArity ``InOut.in 0 then pure ParamKind.in + else if expr.isAppOfArity ``InOut.out 0 then pure ParamKind.out + else + throwError m!"error with expr: {expr}" + | p => pure p match param with | .uncheckedIn => pure () @@ -221,7 +213,7 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do resolved := resolved.insert i false else throwError "parameter #{i} {arg} of {type} is an inout parameter that is not .in nor .out" - | .semiOut _ _ => unreachable! + | .semiOut _ => unreachable! return some mvarInputs syntax (name := ipm_class) "ipm_class" : attr diff --git a/Iris/Iris/ProofMode/Tactics/HaveCore.lean b/Iris/Iris/ProofMode/Tactics/HaveCore.lean index 49d27ace6..236770120 100644 --- a/Iris/Iris/ProofMode/Tactics/HaveCore.lean +++ b/Iris/Iris/ProofMode/Tactics/HaveCore.lean @@ -24,7 +24,7 @@ public section open BI theorem have_asEmpValid [bi : BI PROP] {φ} {P Q : PROP} - [h1 : AsEmpValid .into φ .in PROP bi P] (h : φ) : Q ⊢ Q ∗ □ P := + [h1 : AsEmpValid .into φ PROP bi P] (h : φ) : Q ⊢ Q ∗ □ P := sep_emp.2.trans (sep_mono_right $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h))) public meta section @@ -83,7 +83,7 @@ private def iHaveCore {e} (hyps : @Hyps u prop bi e) have val : Q($ty) := val let hyp ← mkFreshExprMVarQ q($prop) - let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty .in $prop $bi $hyp) + let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty $prop $bi $hyp) | throwError m!"ihave: {ty} is not an entailment" return ⟨_, hyps, q(true), hyp, q(have_asEmpValid $val)⟩ diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 423c445d5..9f90c7929 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -304,7 +304,7 @@ section issue_456 -- test for https://github.com/leanprover-community/iris-lean/issues/456 @[ipm_class] -class C (io : InOut) (a : semiOutParamIPM io Nat) (b : semiOutParamIPM io Nat true) : Prop where +class C (io : InOut) (a : semiOutParamIPM io Nat) (b : semiOutParamIPM io.negate Nat) : Prop where abbrev CMerge (a b : Nat) := C .out a b @@ -335,15 +335,15 @@ section semiOutParamIPM @[ipm_class] class C1 (io : InOut) (a : semiOutParam Nat) : Prop where -/-- -error: invalid ipm_class, parameter #2 is a `semiOutParamIPM` with the `InOut` -argument not directly referencing to an earlier parameter --/ -#guard_msgs in +/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by pattern matching. -/ +@[ipm_class] +class C2 (a : Bool) (a : semiOutParamIPM (match a with | false => .in | true => .out) Nat) : Prop where + +/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by conditional branching. -/ @[ipm_class] -class C2 {α} (a : α) (a : semiOutParamIPM .in Nat false) : Prop where +class C3 (a : Bool) (a : semiOutParamIPM (if a then .in else .out) Nat) : Prop where /- The attribute `semiOutParam` is still relevant for regular type classes -/ -class C3 (io : InOut) (a : semiOutParam Nat) : Prop where +class C4 (io : InOut) (a : semiOutParam Nat) : Prop where end semiOutParamIPM From 153b5189ab64a7ea1e207f826151848615437a78 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 16:56:40 +0200 Subject: [PATCH 09/26] `IsOp` code refactoring: use `IsOp.Direction` --- Iris/Iris/Algebra/Agree.lean | 2 +- Iris/Iris/Algebra/Auth.lean | 8 +++--- Iris/Iris/Algebra/DFrac.lean | 4 +-- Iris/Iris/Algebra/Frac.lean | 2 +- Iris/Iris/Algebra/HeapView.lean | 7 +++-- Iris/Iris/Algebra/IsOp.lean | 39 ++++++++++++++------------- Iris/Iris/Algebra/Lib/FracAuth.lean | 8 +++--- Iris/Iris/Algebra/Lib/MonoNat.lean | 8 +++--- Iris/Iris/Algebra/ReservationMap.lean | 6 ++--- Iris/Iris/Algebra/UFrac.lean | 2 +- Iris/Iris/Algebra/View.lean | 8 +++--- 11 files changed, 48 insertions(+), 46 deletions(-) diff --git a/Iris/Iris/Algebra/Agree.lean b/Iris/Iris/Algebra/Agree.lean index c95fcd4f4..666ba38a0 100644 --- a/Iris/Iris/Algebra/Agree.lean +++ b/Iris/Iris/Algebra/Agree.lean @@ -512,7 +512,7 @@ theorem valid_included {x y : Agree α} : ✓ y → x ≼ y → x ≡ y := by _ ≡ x • z := .op_r <| op_inv <| (CMRA.valid_iff heq).mp hval _ ≡ y := heq.symm -instance {x : Agree α} : IsOp io x x x where +instance {x : Agree α} : IsOp d x x x where is_op := idemp.symm end Agree diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index 915ca4b6a..3a37eeec4 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -138,8 +138,8 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac} {a : A} : auth_op_auth_eqv @[rocq_alias auth_auth_dfrac_is_op] -instance {dq dq1 dq2 : DFrac} {a : A} [h : IsOp io dq dq1 dq2] : - IsOp io (●{dq} a : Auth A) (●{dq1} a) (●{dq2} a) where +instance {dq dq1 dq2 : DFrac} {a : A} [h : IsOp d dq dq1 dq2] : + IsOp d (●{dq} a : Auth A) (●{dq1} a) (●{dq2} a) where is_op := by rw [h.is_op.to_eq] apply auth_dfrac_op @@ -180,8 +180,8 @@ nonrec instance {a : A} {b : A} [CoreId b] : instCoreIdOpAuthDiscardFrag @[rocq_alias auth_frag_is_op] -instance {a b1 b2 : A} [h : IsOp io a b1 b2] : - IsOp io (◯ a : Auth A) (◯ b1) (◯ b2) where +instance {a b1 b2 : A} [h : IsOp d a b1 b2] : + IsOp d (◯ a : Auth A) (◯ b1) (◯ b2) where is_op := NonExpansive₂.eqv .rfl h.is_op -- TODO: auth_frag_sep_homomorphism diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean index 1efb2a8bc..db3a84c06 100644 --- a/Iris/Iris/Algebra/DFrac.lean +++ b/Iris/Iris/Algebra/DFrac.lean @@ -227,8 +227,8 @@ theorem own_included {p q : Qp} : own p ≼ own q ↔ ∃ r, q = p + r := by exact ⟨r, Qp.ext_iff.mpr hz⟩ @[rocq_alias dfrac_is_op] -instance isOp_dfrac_own {q q1 q2 : Qp} [h : IsOp io q q1 q2] : - IsOp io (own q) (own q1) (own q2) where +instance isOp_dfrac_own {q q1 q2 : Qp} [h : IsOp d q q1 q2] : + IsOp d (own q) (own q1) (own q2) where is_op := by rw [h.is_op.to_eq]; rfl end DFrac diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 6e257904e..3a5c03f02 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -159,5 +159,5 @@ instance (priority := default - 10) (q1 q2 : Qp) : is_op := .rfl @[rocq_alias is_op_frac] -instance (q : Qp) : IsOp io q q.half q.half where +instance (q : Qp) : IsOp d q q.half q.half where is_op := by refine OFE.Equiv.of_eq (q.ext ?_); grind diff --git a/Iris/Iris/Algebra/HeapView.lean b/Iris/Iris/Algebra/HeapView.lean index 0f3cebea1..078ab40d5 100644 --- a/Iris/Iris/Algebra/HeapView.lean +++ b/Iris/Iris/Algebra/HeapView.lean @@ -192,11 +192,10 @@ theorem frag_op_eqv : Frag (H := H) k (dp • dq) (v1 • v2) ≡ Frag k dp v1 refine .trans ?_ (eqv_of_Equiv <| Heap.singleton_op_singleton).symm exact .rfl -set_option synthInstance.checkSynthOrder false in instance - [hdp : IsOp io dp dp1 dp2] - [hv : IsOp io v v1 v2] : - IsOp io (Frag k dp v) (Frag k dp1 v1) (Frag (H := H) k dp2 v2) where + [hdp : IsOp d dp dp1 dp2] + [hv : IsOp d v v1 v2] : + IsOp d (Frag k dp v) (Frag k dp1 v1) (Frag (H := H) k dp2 v2) where is_op := by rw [hdp.is_op.to_eq] exact (NonExpansive.eqv hv.is_op).trans frag_op_eqv diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 1789972d4..d88a33d9c 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -17,21 +17,27 @@ open CMRA ProofMode section IsOp +inductive IsOp.Direction +| merge +| split + /-- 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 α] - (io : InOut) (a : semiOutParamIPM io α) - (b1 : semiOutParamIPM io.negate α) (b2 : semiOutParamIPM io.negate α) where + (direction : IsOp.Direction) + (a : semiOutParamIPM (match direction with | .merge => .out | .split => .in) α) + (b1 : semiOutParamIPM (match direction with | .merge => .in | .split => .out) α) + (b2 : semiOutParamIPM (match direction with | .merge => .in | .split => .out) α) where is_op : a ≡ b1 • b2 /-- Syntactic sugar for specifying whether `IsOp` is used for merging or splitting. -/ -abbrev IsOpMerge [CMRA α] (a b1 b2 : α) := IsOp .out a b1 b2 -abbrev IsOpSplit [CMRA α] (a b1 b2 : α) := IsOp .in a b1 b2 +abbrev IsOpMerge [CMRA α] (a b1 b2 : α) := IsOp .merge a b1 b2 +abbrev IsOpSplit [CMRA α] (a b1 b2 : α) := IsOp .split a b1 b2 /-- Merging with `•` should have the lowest priority. -/ @[rocq_alias is_op_op] @@ -52,29 +58,26 @@ instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) : -/ @[rocq_alias is_op_pair] -instance isOp_pair [CMRA α] {io : InOut} - (a b1 b2 : α) (a' b1' b2' : α) - [h1 : IsOp io a b1 b2] [h2 : IsOp io a' b1' b2'] : - IsOp io (a, a') (b1, b1') (b2, b2') where +instance isOp_pair [CMRA α] {d : IsOp.Direction} (a b1 b2 : α) (a' b1' b2' : α) + [h1 : IsOp d a b1 b2] [h2 : IsOp d a' b1' b2'] : + IsOp d (a, a') (b1, b1') (b2, b2') where is_op := OFE.equiv_prod_ext h1.is_op h2.is_op @[rocq_alias is_op_pair_core_id_l] -instance isOp_pair_core_id_l [CMRA α] [CMRA β] {io : InOut} - (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp io a' b1' b2'] : - IsOp io (a, a') (a, b1') (a, b2') where +instance isOp_pair_core_id_l [CMRA α] [CMRA β] {d : IsOp.Direction} + (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp d a' b1' b2'] : + IsOp d (a, a') (a, b1') (a, b2') where is_op := OFE.equiv_prod_ext (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 io a b1 b2] : - IsOp io (a, a') (b1, a') (b2, a') where +instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {d : IsOp.Direction} + (a b1 b2 : α) (a' : β) [h1 : CoreId a'] [h2 : IsOp d a b1 b2] : + IsOp d (a, a') (b1, a') (b2, a') where is_op := OFE.equiv_prod_ext h2.is_op (op_self a').symm @[rocq_alias is_op_Some] -instance isOp_some [CMRA α] (a b1 b2 : α) {io : InOut} - [h : IsOp io a b1 b2] : - IsOp io (some a) (some b1) (some b2) where +instance isOp_some [CMRA α] (a b1 b2 : α) {d : IsOp.Direction} + [h : IsOp d a b1 b2] : IsOp d (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 df88fcce5..1a09f18ed 100644 --- a/Iris/Iris/Algebra/Lib/FracAuth.lean +++ b/Iris/Iris/Algebra/Lib/FracAuth.lean @@ -229,15 +229,15 @@ theorem frag_op_valid {q1 q2 : Qp} {a b : A} : @[rocq_alias frac_auth_is_op] instance isOp_frac_auth {q q1 q2 : Qp} {a1 a2 : A} {a : outParam A} - [h1 : IsOp io q q1 q2] [h2 : IsOp io a a1 a2] : - IsOp io (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where + [h1 : IsOp d q q1 q2] [h2 : IsOp d a a1 a2] : + IsOp d (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where is_op := NonExpansive.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv h1.is_op h2.is_op)) set_option synthInstance.checkSynthOrder false in @[rocq_alias frac_auth_is_op_core_id] instance isOp_frac_auth_core_id {q q1 q2 : Qp} {a : A} - [h1 : CoreId a] [h2 : IsOp io q q1 q2] : - IsOp io (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where + [h1 : CoreId a] [h2 : IsOp d q q1 q2] : + IsOp d (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where is_op := NonExpansive.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv h2.is_op (op_self a).symm)) /-! ## Updates -/ diff --git a/Iris/Iris/Algebra/Lib/MonoNat.lean b/Iris/Iris/Algebra/Lib/MonoNat.lean index 1a6ad71a0..5d86c2c52 100644 --- a/Iris/Iris/Algebra/Lib/MonoNat.lean +++ b/Iris/Iris/Algebra/Lib/MonoNat.lean @@ -189,14 +189,14 @@ theorem auth_unpersist (n : MaxNat) : @[rocq_alias mono_nat_auth_dfrac_is_op] instance {dq dq1 dq2 : DFrac} {n : MaxNat} - [h : IsOp io dq dq1 dq2] : - IsOp io (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n) where + [h : IsOp d dq dq1 dq2] : + IsOp d (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n) where is_op := by rw [h.is_op.to_eq]; apply auth_dfrac_op @[rocq_alias mono_nat_lb_max_is_op] instance {n n1 n2 : MaxNat} - [h : IsOp io n n1 n2] : - IsOp io (◯MN n : MonoNat) (◯MN n1) (◯MN n2) where + [h : IsOp d n n1 n2] : + IsOp d (◯MN n : MonoNat) (◯MN n1) (◯MN n2) where is_op := by rw [h.is_op.to_eq]; exact .rfl end MonoNat diff --git a/Iris/Iris/Algebra/ReservationMap.lean b/Iris/Iris/Algebra/ReservationMap.lean index 888f69633..955b66f3c 100644 --- a/Iris/Iris/Algebra/ReservationMap.lean +++ b/Iris/Iris/Algebra/ReservationMap.lean @@ -390,9 +390,9 @@ theorem singleton_mono {k} {a b : A} (Hab : a ≼ b) : singleton (H := H) k a ⟨singleton k z, (NonExpansive.eqv hz).trans (singleton_op k a z)⟩ @[rocq_alias reservation_map_data_is_op] -instance {io : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp io a b₁ b₂] : - IsOp io (singleton (H := H) k a) (singleton k b₁) (singleton k b₂) where - is_op := .trans (NonExpansive.eqv hv.is_op ) (singleton_op k b₁ b₂) +instance {d : IsOp.Direction} {a b₁ b₂ : A} [hv : IsOp d a b₁ b₂] : + IsOp d (singleton (H := H) k a) (singleton k b₁) (singleton k b₂) where + is_op := .trans (NonExpansive.eqv hv.is_op) (singleton_op k b₁ b₂) @[rocq_alias reservation_map_token_union] theorem token_union {e₁ e₂} (he : e₁ ## e₂) : diff --git a/Iris/Iris/Algebra/UFrac.lean b/Iris/Iris/Algebra/UFrac.lean index 3902a9c7f..c84e362e4 100644 --- a/Iris/Iris/Algebra/UFrac.lean +++ b/Iris/Iris/Algebra/UFrac.lean @@ -95,7 +95,7 @@ instance {q : UFrac} : CMRA.IdFree q where have := b.frac.2; simp only [dist_iff, ext_iff, frac_op] at H; grind @[rocq_alias is_op_ufrac] -instance (q : UFrac) : IsOp io q ⟨q.frac.half⟩ ⟨q.frac.half⟩ where +instance (q : UFrac) : IsOp d q ⟨q.frac.half⟩ ⟨q.frac.half⟩ where is_op := OFE.Equiv.of_eq <| ext_iff.mpr (Qp.half_add_half q.frac).symm end UFrac diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index 000a2ced3..06436a946 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -333,8 +333,8 @@ theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View R) ≡ (●V{dq1} a) • @[rocq_alias view_auth_dfrac_is_op] instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac} {a : A} - [h : IsOp io dq dq1 dq2] : - IsOp io (●V{dq} a : View R) (●V{dq1} a) (●V{dq2} a) where + [h : IsOp d dq dq1 dq2] : + IsOp d (●V{dq} a : View R) (●V{dq1} a) (●V{dq2} a) where is_op := by rw [h.is_op.to_eq] apply auth_op_auth_eqv @@ -377,8 +377,8 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View R) • ◯V b) refine UCMRA.unit_left_id.symm @[rocq_alias view_frag_is_op] -instance {b b1 b2 : B} [h : IsOp io b b1 b2] : - IsOp io (◯V b : View R) (◯V b1) (◯V b2) where +instance {b b1 b2 : B} [h : IsOp d b b1 b2] : + IsOp d (◯V b : View R) (◯V b1) (◯V b2) where is_op := NonExpansive.eqv h.is_op @[rocq_alias view_auth_dfrac_op_invN] From 4b68a767006480610baed8e51986277b89fbf79b Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 17:00:01 +0200 Subject: [PATCH 10/26] `IsOpMerge` and `IsOpSplit` are now redundant --- Iris/Iris/Algebra/Frac.lean | 2 +- Iris/Iris/Algebra/IsOp.lean | 10 ++-------- Iris/Iris/Instances/IProp/Instance.lean | 10 +++++----- Iris/Iris/Tests/Tactics.lean | 8 ++++---- 4 files changed, 12 insertions(+), 18 deletions(-) diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 3a5c03f02..677b2700e 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -155,7 +155,7 @@ theorem Frac.valid_iff {p : Qp} : ✓ p ↔ p.val ≤ 1 := .rfl @[rocq_alias frac_is_op] instance (priority := default - 10) (q1 q2 : Qp) : - IsOpMerge (q1 + q2 : Qp) q1 q2 where + IsOp .merge (q1 + q2 : Qp) q1 q2 where is_op := .rfl @[rocq_alias is_op_frac] diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index d88a33d9c..ae7a0246f 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -33,22 +33,16 @@ class IsOp [CMRA α] (b2 : semiOutParamIPM (match direction with | .merge => .in | .split => .out) α) where is_op : a ≡ b1 • b2 -/-- - Syntactic sugar for specifying whether `IsOp` is used for merging or splitting. --/ -abbrev IsOpMerge [CMRA α] (a b1 b2 : α) := IsOp .merge a b1 b2 -abbrev IsOpSplit [CMRA α] (a b1 b2 : α) := IsOp .split a b1 b2 - /-- Merging with `•` should have the lowest priority. -/ @[rocq_alias is_op_op] instance (priority := default - 100) isOpMerge_op [CMRA α] (a b : α) : - IsOpMerge (a • b) a b where + 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 : α) : - IsOpSplit (a • b) a b where + IsOp .split (a • b) a b where is_op := .rfl /- diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 651313bc5..2242e2d31 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -774,26 +774,26 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn set_option synthInstance.checkSynthOrder false in @[rocq_alias into_sep_own] -instance intoSep_own {γ} {a : 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 set_option synthInstance.checkSynthOrder false in @[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⟩) set_option synthInstance.checkSynthOrder false in @[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 set_option synthInstance.checkSynthOrder false in @[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 @@ -804,7 +804,7 @@ instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} : set_option synthInstance.checkSynthOrder false in @[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 fb8509a5f..de8a7e0e4 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2562,7 +2562,7 @@ example [BI PROP] {P Q R : PROP} : ⊢ P -∗ Q -∗ □ R -∗ R ∗ P ∗ Q := 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 b c : F.ap (IProp GF)} [IsOpMerge b a2 a3] [IsOpMerge c a1 b] : + {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 iintro H1 H2 H3 @@ -2577,7 +2577,7 @@ example {F GF} [RFunctorContractive F] [ElemG GF F] {γ} instances for `DFrac` and `Frac`. -/ example {GF} [ElemG GF (constOF DFrac)] [ElemG GF (constOF Qp)] {γ} - {a1 a2 a3 b c : Qp} [IsOpMerge b a2 a3] [IsOpMerge c a1 b] : + {a1 a2 a3 b c : Qp} [IsOp .merge b a2 a3] [IsOp .merge c a1 b] : ⊢@{IProp GF} iOwn (F := constOF DFrac) γ (own a1) -∗ iOwn (F := constOF DFrac) γ (own a2) -∗ @@ -2597,8 +2597,8 @@ example {GF} [ElemG GF (constOF DFrac)] instances for the authoritative CMRA. -/ example {GF A} [UCMRA A] [ElemG GF (constOF (Auth A))] {γ} {a1 a2 a3 b c : A} {q1 q2 : Qp} {dq'' dq3 dq4 : DFrac} - [IsOpMerge b a2 a3] [IsOpMerge c a1 b] - [IsOpMerge dq'' dq3 dq4] : + [IsOp .merge b a2 a3] [IsOp .merge c a1 b] + [IsOp .merge dq'' dq3 dq4] : ⊢@{IProp GF} iOwn (F := constOF (Auth A)) γ (◯ a1) -∗ iOwn (F := constOF (Auth A)) γ (◯ a2) -∗ From 6c7ec842a07ddcf6ab53cb94413b170970f4415b Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 17:03:27 +0200 Subject: [PATCH 11/26] Define `IsOp.Direction.mapToInOut` --- Iris/Iris/Algebra/IsOp.lean | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index ae7a0246f..cc25fbffe 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -21,16 +21,25 @@ inductive IsOp.Direction | merge | split +meta section + +@[reducible] +def IsOp.Direction.mapToInOut (d : IsOp.Direction) : InOut := + match d with + | merge => .out + | split => .in + +end + /-- 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 α] - (direction : IsOp.Direction) - (a : semiOutParamIPM (match direction with | .merge => .out | .split => .in) α) - (b1 : semiOutParamIPM (match direction with | .merge => .in | .split => .out) α) - (b2 : semiOutParamIPM (match direction with | .merge => .in | .split => .out) α) where + (d : IsOp.Direction) (a : semiOutParamIPM d.mapToInOut α) + (b1 : semiOutParamIPM d.mapToInOut.negate α) + (b2 : semiOutParamIPM d.mapToInOut.negate α) where is_op : a ≡ b1 • b2 /-- Merging with `•` should have the lowest priority. -/ From b1cda212827b08b0d859449806c4f5fa5b59abfc Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 17:10:33 +0200 Subject: [PATCH 12/26] Simplify `AsEmpValid` --- Iris/Iris/Algebra/IsOp.lean | 4 +--- Iris/Iris/ProofMode/Classes.lean | 12 ++++++++++-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index cc25fbffe..c01fc2247 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -25,9 +25,7 @@ meta section @[reducible] def IsOp.Direction.mapToInOut (d : IsOp.Direction) : InOut := - match d with - | merge => .out - | split => .in + match d with | merge => .out | split => .in end diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index beab230f2..b0fe47594 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -26,10 +26,18 @@ inductive AsEmpValid.Direction where | into | from +meta section + +@[reducible] +def AsEmpValid.Direction.mapToInOut (d : AsEmpValid.Direction) : InOut := + match d with | .into => .in | .from => .out + +end + @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) - (PROP : semiOutParamIPM (match d with | .into => .in | .from => .out) $ Type _) - (bi : semiOutParamIPM (match d with | .into => .in | .from => .out) $ BI PROP) + (PROP : semiOutParamIPM d.mapToInOut $ Type _) + (bi : semiOutParamIPM d.mapToInOut $ BI PROP) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) From b8d47d6409538bd8f8bd91fbd542300a45422d0c Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Mon, 13 Jul 2026 17:22:58 +0200 Subject: [PATCH 13/26] Minor improvements, typo fix --- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index ad053b37d..0f7359dd3 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -130,13 +130,13 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar /-- Analogous to `semiOutParam`, with the explicit argument `_io` being an - `InOut` value, which determines whether this is is an input parameter or an + `InOut` value, which determines whether this is an input parameter or an output paramter for the purpose of type class synthesis. One can use `InOut.negate` to negate the `InOut` value. - This should be used instead of `semiOutParam` when the custom IPM type - class synthesiser is used. + This should be used instead of `semiOutParam` for any type class with + the annotation `ipm_class`. -/ @[reducible, expose] def semiOutParamIPM (_io : InOut) (α : Sort u) : Sort u := semiOutParam α @@ -192,13 +192,13 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do let param := params[i]! let arg := args[i]! - let param : ParamKind ← match param with + let param ← match param with | .semiOut expr => - let expr ← whnf (expr.instantiateRev (args.extract 0 i)) - if expr.isAppOfArity ``InOut.in 0 then pure ParamKind.in - else if expr.isAppOfArity ``InOut.out 0 then pure ParamKind.out - else - throwError m!"error with expr: {expr}" + -- Reduce the `InOut` argument and determine whether it is `.in` or `.out` + let expr ← whnf <| expr.instantiateRev <| args.extract 0 i + if expr.isAppOfArity ``InOut.in 0 then pure .in + else if expr.isAppOfArity ``InOut.out 0 then pure .out + else throwError m!"unable to parse the Boolean expression {expr}" | p => pure p match param with From b43d67ebc4c785aec7be2af15c76903938236ed9 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 14:41:16 +0200 Subject: [PATCH 14/26] Function renaming: `AsEmpValid.Direction.toInOut` --- Iris/Iris/ProofMode/Classes.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index 4c770283e..abe8252e1 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -29,15 +29,16 @@ inductive AsEmpValid.Direction where meta section @[reducible] -def AsEmpValid.Direction.mapToInOut (d : AsEmpValid.Direction) : InOut := - match d with | .into => .in | .from => .out +def AsEmpValid.Direction.toInOut : AsEmpValid.Direction → InOut + | .into => .in + | .from => .out end @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) - (PROP : semiOutParamIPM d.mapToInOut $ Type _) - (bi : semiOutParamIPM d.mapToInOut $ BI PROP) + (PROP : semiOutParamIPM d.toInOut $ Type _) + (bi : semiOutParamIPM d.toInOut $ BI PROP) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) From 36527e4b86757a1d32920ddf5095652cbefbf69d Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 14:42:55 +0200 Subject: [PATCH 15/26] Remove outdated comment --- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index 0f7359dd3..e64c62040 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -141,8 +141,7 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar @[reducible, expose] def semiOutParamIPM (_io : InOut) (α : Sort u) : Sort u := semiOutParam α -/-- If `d` is `semiOutParam self α` or `semiOutParamNeg self α`, return `(negate, self)`. -/ -private def semiOutParamGoverning? (d : Expr) : Option Expr := do +private def semiOutParamExpr (d : Expr) : Option Expr := do if d.isAppOfArity ``semiOutParamIPM 2 then some d.getAppArgs[0]! else none @@ -157,7 +156,7 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .uncheckedIn) b else if d.isOutParam then computeParamKinds (params.push .out) b - else if let some expr := semiOutParamGoverning? d then + else if let some expr := semiOutParamExpr d then computeParamKinds (params.push (.semiOut expr)) b else if d.isSemiOutParam then Except.error m!"invalid ipm_class, parameter #{params.size + 1} is a `semiOutParam`. Use \ From 4d256468500b11b9a35c640437f30543135d9b03 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 14:45:52 +0200 Subject: [PATCH 16/26] Remove the `inout : ParamKind` and residual code --- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index e64c62040..cb193c84f 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -49,7 +49,6 @@ The parameters of a class declared with `ipm_class` are categorized into the fol or an output. 4. uncheckedIn: These are parameters marked with `uncheckedInParam`. These behave like `in` parameters, but allow mvars to match terms (see below). -5. inout: Parameters of type `InOut`, must appear before semiOut parameters (see above). The following constraints apply to the parameters: (In the following, semiOut parameters are treated as inputs if the preceding `InOut` is `in` and as @@ -70,7 +69,6 @@ inductive ParamKind | out | semiOut (expr : Expr) | uncheckedIn - | inout deriving Inhabited instance : ToString ParamKind where @@ -79,7 +77,6 @@ instance : ToString ParamKind where | .out => "out" | .semiOut expr => s!"semiOut {expr}" | .uncheckedIn => "uncheckedIn" - | .inout => "inout" section IPMClasses structure ClassEntry where @@ -161,8 +158,6 @@ Except MessageData (Array ParamKind) := else if d.isSemiOutParam then Except.error m!"invalid ipm_class, parameter #{params.size + 1} is a `semiOutParam`. Use \ `semiOutParamIPM` instead" - else if d.isAppOfArity ``InOut 0 then - computeParamKinds (params.push .inout) b else computeParamKinds (params.push .in) b | _ => return params @@ -184,7 +179,6 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do if args.size != params.size then throwError "mismatched number of arguments" - let mut resolved : Std.HashMap Nat Bool := {} let mut mvarInputs := #[] for i in 0...args.size do @@ -205,13 +199,6 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do | .in => if arg.getAppFn.isMVar then mvarInputs := mvarInputs.push i | .out => if !arg.getAppFn.isMVar then throwError "parameter #{i} {arg} of {type} is an out parameter that is not an mvar" - | .inout => - if arg.isAppOfArity ``InOut.in 0 then - resolved := resolved.insert i true - else if arg.isAppOfArity ``InOut.out 0 then - resolved := resolved.insert i false - else - throwError "parameter #{i} {arg} of {type} is an inout parameter that is not .in nor .out" | .semiOut _ => unreachable! return some mvarInputs From 30e665afa7f38f7520f5f7d308e2760b34323c60 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 15:42:01 +0200 Subject: [PATCH 17/26] Define `semiOutParamIPM` as a macro that involves `semiOutParam` --- Iris/Iris/Algebra/Agree.lean | 1 + Iris/Iris/Algebra/Auth.lean | 1 + Iris/Iris/Algebra/Frac.lean | 2 ++ Iris/Iris/Algebra/HeapView.lean | 1 + Iris/Iris/Algebra/IsOp.lean | 4 +++ Iris/Iris/Algebra/ReservationMap.lean | 1 + Iris/Iris/Algebra/UFrac.lean | 1 + Iris/Iris/Algebra/View.lean | 1 + Iris/Iris/ProofMode/Classes.lean | 4 +-- Iris/Iris/ProofMode/SynthInstance.lean | 16 ++-------- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 35 ++++++++++++++-------- Iris/Iris/Tests/Instances.lean | 11 +++++-- 12 files changed, 46 insertions(+), 32 deletions(-) diff --git a/Iris/Iris/Algebra/Agree.lean b/Iris/Iris/Algebra/Agree.lean index 666ba38a0..2dc2626a5 100644 --- a/Iris/Iris/Algebra/Agree.lean +++ b/Iris/Iris/Algebra/Agree.lean @@ -512,6 +512,7 @@ theorem valid_included {x y : Agree α} : ✓ y → x ≼ y → x ≡ y := by _ ≡ x • z := .op_r <| op_inv <| (CMRA.valid_iff heq).mp hval _ ≡ y := heq.symm +set_option synthInstance.checkSynthOrder false in instance {x : Agree α} : IsOp d x x x where is_op := idemp.symm diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index 3a37eeec4..3c7a76cd4 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -137,6 +137,7 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac} {a : A} : (●{dq1 • dq2} a) ≡ (●{dq1} a) • (●{dq2} a) := auth_op_auth_eqv +set_option synthInstance.checkSynthOrder false in @[rocq_alias auth_auth_dfrac_is_op] instance {dq dq1 dq2 : DFrac} {a : A} [h : IsOp d dq dq1 dq2] : IsOp d (●{dq} a : Auth A) (●{dq1} a) (●{dq2} a) where diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 677b2700e..c197350e8 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -153,11 +153,13 @@ theorem Frac.op_eq (p q : Qp) : p • q = p + q := rfl @[rocq_alias frac_valid] theorem Frac.valid_iff {p : Qp} : ✓ p ↔ p.val ≤ 1 := .rfl +set_option synthInstance.checkSynthOrder false in @[rocq_alias frac_is_op] instance (priority := default - 10) (q1 q2 : Qp) : IsOp .merge (q1 + q2 : Qp) q1 q2 where is_op := .rfl +set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_frac] instance (q : Qp) : IsOp d q q.half q.half where is_op := by refine OFE.Equiv.of_eq (q.ext ?_); grind diff --git a/Iris/Iris/Algebra/HeapView.lean b/Iris/Iris/Algebra/HeapView.lean index 078ab40d5..0c336cbe8 100644 --- a/Iris/Iris/Algebra/HeapView.lean +++ b/Iris/Iris/Algebra/HeapView.lean @@ -192,6 +192,7 @@ theorem frag_op_eqv : Frag (H := H) k (dp • dq) (v1 • v2) ≡ Frag k dp v1 refine .trans ?_ (eqv_of_Equiv <| Heap.singleton_op_singleton).symm exact .rfl +set_option synthInstance.checkSynthOrder false in instance [hdp : IsOp d dp dp1 dp2] [hv : IsOp d v v1 v2] : diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index c01fc2247..0cd65cd86 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -40,12 +40,14 @@ class IsOp [CMRA α] (b2 : semiOutParamIPM d.mapToInOut.negate α) where is_op : a ≡ b1 • b2 +set_option synthInstance.checkSynthOrder false in /-- Merging with `•` should have the lowest priority. -/ @[rocq_alias is_op_op] instance (priority := default - 100) isOpMerge_op [CMRA α] (a b : α) : IsOp .merge (a • b) a b where is_op := .rfl +set_option synthInstance.checkSynthOrder false in /-- Splitting with `•` should have the highest priority. -/ @[rocq_alias is_op_lr_op] instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) : @@ -64,12 +66,14 @@ instance isOp_pair [CMRA α] {d : IsOp.Direction} (a b1 b2 : α) (a' b1' b2' : IsOp d (a, a') (b1, b1') (b2, b2') where is_op := OFE.equiv_prod_ext h1.is_op h2.is_op +set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_pair_core_id_l] instance isOp_pair_core_id_l [CMRA α] [CMRA β] {d : IsOp.Direction} (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp d a' b1' b2'] : IsOp d (a, a') (a, b1') (a, b2') where is_op := OFE.equiv_prod_ext (op_self a).symm h2.is_op +set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_pair_core_id_r] instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {d : IsOp.Direction} (a b1 b2 : α) (a' : β) [h1 : CoreId a'] [h2 : IsOp d a b1 b2] : diff --git a/Iris/Iris/Algebra/ReservationMap.lean b/Iris/Iris/Algebra/ReservationMap.lean index 955b66f3c..7068131fd 100644 --- a/Iris/Iris/Algebra/ReservationMap.lean +++ b/Iris/Iris/Algebra/ReservationMap.lean @@ -389,6 +389,7 @@ theorem singleton_mono {k} {a b : A} (Hab : a ≼ b) : singleton (H := H) k a let ⟨z, hz⟩ := Hab ⟨singleton k z, (NonExpansive.eqv hz).trans (singleton_op k a z)⟩ +set_option synthInstance.checkSynthOrder false in @[rocq_alias reservation_map_data_is_op] instance {d : IsOp.Direction} {a b₁ b₂ : A} [hv : IsOp d a b₁ b₂] : IsOp d (singleton (H := H) k a) (singleton k b₁) (singleton k b₂) where diff --git a/Iris/Iris/Algebra/UFrac.lean b/Iris/Iris/Algebra/UFrac.lean index c84e362e4..4b1b934c9 100644 --- a/Iris/Iris/Algebra/UFrac.lean +++ b/Iris/Iris/Algebra/UFrac.lean @@ -94,6 +94,7 @@ instance {q : UFrac} : CMRA.IdFree q where id_free0_r b _ H := by have := b.frac.2; simp only [dist_iff, ext_iff, frac_op] at H; grind +set_option synthInstance.checkSynthOrder false in @[rocq_alias is_op_ufrac] instance (q : UFrac) : IsOp d q ⟨q.frac.half⟩ ⟨q.frac.half⟩ where is_op := OFE.Equiv.of_eq <| ext_iff.mpr (Qp.half_add_half q.frac).symm diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index 06436a946..869214ea7 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -331,6 +331,7 @@ theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View R) ≡ (●V{dq1} a) • NonExpansive₂.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv .rfl Agree.idemp.symm)) UCMRA.unit_left_id.symm +set_option synthInstance.checkSynthOrder false in @[rocq_alias view_auth_dfrac_is_op] instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac} {a : A} [h : IsOp d dq dq1 dq2] : diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index abe8252e1..65933a180 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -37,8 +37,8 @@ end @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) - (PROP : semiOutParamIPM d.toInOut $ Type _) - (bi : semiOutParamIPM d.toInOut $ BI PROP) + (PROP : semiOutParamIPM d.toInOut (Type _)) + (bi : semiOutParamIPM d.toInOut (BI PROP)) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) diff --git a/Iris/Iris/ProofMode/SynthInstance.lean b/Iris/Iris/ProofMode/SynthInstance.lean index 202564b45..fa24d8ecc 100644 --- a/Iris/Iris/ProofMode/SynthInstance.lean +++ b/Iris/Iris/ProofMode/SynthInstance.lean @@ -129,20 +129,8 @@ partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do let some (mctx', subgoals) ← withAssignableSyntheticOpaque (SynthInstance.tryResolve mvar inst) | return (none, false) setMCtx mctx' - let mut pending := subgoals - let mut progress := true - while progress && !pending.isEmpty do - progress := false - let mut stillPending := [] - for g in pending do - let mctxBefore ← getMCtx - if let some _ ← synthInstanceMainCore g then - progress := true - else - setMCtx mctxBefore - stillPending := stillPending.cons g - pending := stillPending - if !pending.isEmpty then return (none, true) + for g in subgoals do + let some _ ← synthInstanceMainCore g | return (none, true) return (some (), true) if res.isSome then return res diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index cb193c84f..a80f201d1 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -125,22 +125,28 @@ initialize ipmClassesExt : private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Array ParamKind) := (ipmClassesExt.getState env).paramMap.find? declName +@[reducible, expose] +def semiOutParamCore (_io : InOut) (α : Sort u) : Sort u := α + /-- - Analogous to `semiOutParam`, with the explicit argument `_io` being an - `InOut` value, which determines whether this is an input parameter or an - output paramter for the purpose of type class synthesis. + The keyword `semiOutParamIPM` is analogous to `semiOutParam`, with + an `InOut` value as an explicit argument, which determines whether this is an + input parameter or an output paramter for the purpose of type class synthesis. One can use `InOut.negate` to negate the `InOut` value. This should be used instead of `semiOutParam` for any type class with - the annotation `ipm_class`. + the annotation `[ipm_class]`. -/ -@[reducible, expose] -def semiOutParamIPM (_io : InOut) (α : Sort u) : Sort u := semiOutParam α - -private def semiOutParamExpr (d : Expr) : Option Expr := do - if d.isAppOfArity ``semiOutParamIPM 2 then - some d.getAppArgs[0]! +macro "semiOutParamIPM" io:term:max α:term:max : term => + `(semiOutParam (semiOutParamCore $io $α)) + +private def parseSemiOutParamIPM (d : Expr) : Option Expr := do + if d.isAppOfArity ``semiOutParam 1 then + let expr := d.getAppArgs[0]! + if expr.isAppOfArity ``semiOutParamCore 2 then + some expr.getAppArgs[0]! + else none else none private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : @@ -153,11 +159,14 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .uncheckedIn) b else if d.isOutParam then computeParamKinds (params.push .out) b - else if let some expr := semiOutParamExpr d then + else if let some expr := parseSemiOutParamIPM d then computeParamKinds (params.push (.semiOut expr)) b + else if d.isAppOfArity ``semiOutParamCore 2 then + Except.error m!"invalid ipm_class, `semiOutParamCore` used directly \ + in parameter #{params.size + 1}. Use `semiOutParamIPM` instead" else if d.isSemiOutParam then - Except.error m!"invalid ipm_class, parameter #{params.size + 1} is a `semiOutParam`. Use \ - `semiOutParamIPM` instead" + Except.error m!"invalid ipm_class, `semiOutParam` used directly \ + in parameter #{params.size + 1}. Use `semiOutParamIPM` instead" else computeParamKinds (params.push .in) b | _ => return params diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 9f90c7929..882876713 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -328,9 +328,9 @@ instance instSplit (k : Nat) : CSplit (k + 1) k := ⟨⟩ end issue_456 -section semiOutParamIPM +section semiOutParam -/-- error: invalid ipm_class, parameter #2 is a `semiOutParam`. Use `semiOutParamIPM` instead -/ +/-- error: invalid ipm_class, `semiOutParam` used directly in parameter #2. Use `semiOutParamIPM` instead -/ #guard_msgs in @[ipm_class] class C1 (io : InOut) (a : semiOutParam Nat) : Prop where @@ -346,4 +346,9 @@ class C3 (a : Bool) (a : semiOutParamIPM (if a then .in else .out) Nat) : Prop w /- The attribute `semiOutParam` is still relevant for regular type classes -/ class C4 (io : InOut) (a : semiOutParam Nat) : Prop where -end semiOutParamIPM +/-- error: invalid ipm_class, `semiOutParamCore` used directly in parameter #2. Use `semiOutParamIPM` instead -/ +#guard_msgs in +@[ipm_class] +class C5 (io : InOut) (a : semiOutParamCore .in Nat) : Prop where + +end semiOutParam From f905106bdf58feb6c76d278dd2b110016b3c64ba Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 16:22:36 +0200 Subject: [PATCH 18/26] Replace `semiOutParamIPM` with `semiOutParam (inOutParam ...)` --- Iris/Iris/Algebra/IsOp.lean | 6 ++--- Iris/Iris/ProofMode/Classes.lean | 14 +++++------ Iris/Iris/ProofMode/SynthInstanceAttr.lean | 28 +++++++--------------- Iris/Iris/Tests/Instances.lean | 17 ++++++------- 4 files changed, 27 insertions(+), 38 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 0cd65cd86..c62d38d76 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -35,9 +35,9 @@ end -/ @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR] class IsOp [CMRA α] - (d : IsOp.Direction) (a : semiOutParamIPM d.mapToInOut α) - (b1 : semiOutParamIPM d.mapToInOut.negate α) - (b2 : semiOutParamIPM d.mapToInOut.negate α) where + (d : IsOp.Direction) (a : semiOutParam <| inOutParam d.mapToInOut α) + (b1 : semiOutParam <| inOutParam d.mapToInOut.negate α) + (b2 : semiOutParam <| inOutParam d.mapToInOut.negate α) where is_op : a ≡ b1 • b2 set_option synthInstance.checkSynthOrder false in diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index 65933a180..08c221c63 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -37,8 +37,8 @@ end @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) - (PROP : semiOutParamIPM d.toInOut (Type _)) - (bi : semiOutParamIPM d.toInOut (BI PROP)) + (PROP : semiOutParam <| inOutParam d.toInOut (Type _)) + (bi : semiOutParam <| inOutParam d.toInOut (BI PROP)) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) @@ -64,7 +64,7 @@ export FromImp (from_imp) @[ipm_class, rocq_alias FromWand] class FromWand {PROP} [BI PROP] (P : PROP) (io : InOut) - (Q1 : semiOutParamIPM io PROP) (Q2 : outParam $ PROP) where + (Q1 : semiOutParam <| inOutParam io PROP) (Q2 : outParam $ PROP) where from_wand : (Q1 -∗ Q2) ⊢ P export FromWand (from_wand) @@ -72,8 +72,8 @@ export FromWand (from_wand) @[ipm_class, rocq_alias IntoWand] class IntoWand {PROP} [BI PROP] (p q : Bool) (R : PROP) - (ioP : InOut) (P : semiOutParamIPM ioP PROP) - (ioQ : InOut) (Q : semiOutParamIPM ioQ PROP) where + (ioP : InOut) (P : semiOutParam <| inOutParam ioP PROP) + (ioQ : InOut) (Q : semiOutParam <| inOutParam ioQ PROP) where into_wand : □?p R ⊢ □?q P -∗ Q export IntoWand (into_wand) @@ -149,7 +149,7 @@ export IntoAbsorbingly (into_absorbingly) @[ipm_class, rocq_alias FromAssumption, rocq_alias KnownLFromAssumption, rocq_alias KnownRFromAssumption] class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut) - (P : semiOutParamIPM ioP PROP) (Q : PROP) where + (P : semiOutParam <| inOutParam ioP PROP) (Q : PROP) where from_assumption : □?p P ⊢ Q export FromAssumption (from_assumption) @@ -162,7 +162,7 @@ export IntoPure (into_pure) @[ipm_class, rocq_alias FromPure, rocq_alias FromPureT] class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut) - (φ : semiOutParamIPM ioφ Prop) where + (φ : semiOutParam <| inOutParam ioφ Prop) where from_pure : ?a ⌜φ⌝ ⊢ P export FromPure (from_pure) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index a80f201d1..7ed90981d 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -126,25 +126,12 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar (ipmClassesExt.getState env).paramMap.find? declName @[reducible, expose] -def semiOutParamCore (_io : InOut) (α : Sort u) : Sort u := α - -/-- - The keyword `semiOutParamIPM` is analogous to `semiOutParam`, with - an `InOut` value as an explicit argument, which determines whether this is an - input parameter or an output paramter for the purpose of type class synthesis. - - One can use `InOut.negate` to negate the `InOut` value. - - This should be used instead of `semiOutParam` for any type class with - the annotation `[ipm_class]`. --/ -macro "semiOutParamIPM" io:term:max α:term:max : term => - `(semiOutParam (semiOutParamCore $io $α)) +def inOutParam (_io : InOut) (α : Sort u) : Sort u := α private def parseSemiOutParamIPM (d : Expr) : Option Expr := do if d.isAppOfArity ``semiOutParam 1 then let expr := d.getAppArgs[0]! - if expr.isAppOfArity ``semiOutParamCore 2 then + if expr.isAppOfArity ``inOutParam 2 then some expr.getAppArgs[0]! else none else none @@ -161,12 +148,13 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .out) b else if let some expr := parseSemiOutParamIPM d then computeParamKinds (params.push (.semiOut expr)) b - else if d.isAppOfArity ``semiOutParamCore 2 then - Except.error m!"invalid ipm_class, `semiOutParamCore` used directly \ - in parameter #{params.size + 1}. Use `semiOutParamIPM` instead" + else if d.isAppOfArity ``inOutParam 2 then + Except.error m!"invalid ipm_class, `inOutParam` used in parameter \ + #{params.size + 1} but not within `semiOutParam`. \ + Use `semiOutParam (inOutParam …)` instead." else if d.isSemiOutParam then - Except.error m!"invalid ipm_class, `semiOutParam` used directly \ - in parameter #{params.size + 1}. Use `semiOutParamIPM` instead" + Except.error m!"invalid ipm_class, `semiOutParam` used without `inOutParam` \ + in parameter #{params.size + 1}. Use `semiOutParam (inOutParam …)` instead." else computeParamKinds (params.push .in) b | _ => return params diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 882876713..3cb528802 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -304,7 +304,8 @@ section issue_456 -- test for https://github.com/leanprover-community/iris-lean/issues/456 @[ipm_class] -class C (io : InOut) (a : semiOutParamIPM io Nat) (b : semiOutParamIPM io.negate Nat) : Prop where +class C (io : InOut) (a : semiOutParam <| inOutParam io Nat) + (b : semiOutParam <| inOutParam io.negate Nat) : Prop where abbrev CMerge (a b : Nat) := C .out a b @@ -330,25 +331,25 @@ end issue_456 section semiOutParam -/-- error: invalid ipm_class, `semiOutParam` used directly in parameter #2. Use `semiOutParamIPM` instead -/ +/-- error: invalid ipm_class, `semiOutParam` used without `inOutParam` in parameter #2. Use `semiOutParam (inOutParam …)` instead. -/ #guard_msgs in @[ipm_class] class C1 (io : InOut) (a : semiOutParam Nat) : Prop where -/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by pattern matching. -/ +/-- Tests `semiOutParam (inOutParam …)` where the `InOut` value depends on another argument by pattern matching. -/ @[ipm_class] -class C2 (a : Bool) (a : semiOutParamIPM (match a with | false => .in | true => .out) Nat) : Prop where +class C2 (a : Bool) (a : semiOutParam <| inOutParam (match a with | false => .in | true => .out) Nat) : Prop where -/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by conditional branching. -/ +/-- Tests `semiOutParam (inOutParam …)` where the `InOut` value depends on another argument by conditional branching. -/ @[ipm_class] -class C3 (a : Bool) (a : semiOutParamIPM (if a then .in else .out) Nat) : Prop where +class C3 (a : Bool) (a : semiOutParam <| inOutParam (if a then .in else .out) Nat) : Prop where /- The attribute `semiOutParam` is still relevant for regular type classes -/ class C4 (io : InOut) (a : semiOutParam Nat) : Prop where -/-- error: invalid ipm_class, `semiOutParamCore` used directly in parameter #2. Use `semiOutParamIPM` instead -/ +/-- error: invalid ipm_class, `inOutParam` used in parameter #2 but not within `semiOutParam`. Use `semiOutParam (inOutParam …)` instead. -/ #guard_msgs in @[ipm_class] -class C5 (io : InOut) (a : semiOutParamCore .in Nat) : Prop where +class C5 (io : InOut) (a : inOutParam .in Nat) : Prop where end semiOutParam From c377e21060b9d5a92c44ec5af16a6b02b87afa6c Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 16:28:49 +0200 Subject: [PATCH 19/26] Update `dyn_reservation_map_data_is_op` --- Iris/Iris/Algebra/DynReservationMap.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/Algebra/DynReservationMap.lean b/Iris/Iris/Algebra/DynReservationMap.lean index 9e138f089..1c1d1a523 100644 --- a/Iris/Iris/Algebra/DynReservationMap.lean +++ b/Iris/Iris/Algebra/DynReservationMap.lean @@ -385,8 +385,8 @@ theorem mkData_mono {k} {a b : A} (Hab : a ≼ b) : set_option synthInstance.checkSynthOrder false in @[rocq_alias dyn_reservation_map_data_is_op] -instance {ia ib₁ ib₂ : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp ia a ib₁ b₁ ib₂ b₂] : - IsOp ia (mkData (H := H) k a) ib₁ (mkData k b₁) ib₂ (mkData k b₂) where +instance {d : IsOp.Direction} {a b₁ b₂ : A} [hv : IsOp d a b₁ b₂] : + IsOp d (mkData (H := H) k a) (mkData k b₁) (mkData k b₂) where is_op := .trans (NonExpansive.eqv hv.is_op) (mkData_op k b₁ b₂) @[rocq_alias dyn_reservation_map_token_union] From 771c2616e817993632fbd338afb73da1fce0ced5 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Tue, 21 Jul 2026 16:35:20 +0200 Subject: [PATCH 20/26] Add missing `set_option synthInstance.checkSynthOrder false` --- Iris/Iris/Algebra/Lib/MonoNat.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Iris/Iris/Algebra/Lib/MonoNat.lean b/Iris/Iris/Algebra/Lib/MonoNat.lean index 5d86c2c52..4e6e4a504 100644 --- a/Iris/Iris/Algebra/Lib/MonoNat.lean +++ b/Iris/Iris/Algebra/Lib/MonoNat.lean @@ -187,6 +187,7 @@ theorem auth_unpersist (n : MaxNat) : (●MN□ n : MonoNat) ~~>: (fun k => ∃ q, k = ●MN{DFrac.own q} n) := Auth.auth_updateP_both_unpersist +set_option synthInstance.checkSynthOrder false in @[rocq_alias mono_nat_auth_dfrac_is_op] instance {dq dq1 dq2 : DFrac} {n : MaxNat} [h : IsOp d dq dq1 dq2] : From 5838c10e6940863711d60bc89dcd21c93b89cbe5 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Wed, 22 Jul 2026 10:04:49 +0200 Subject: [PATCH 21/26] cleanup --- Iris/Iris/Algebra/IsOp.lean | 8 ++++---- Iris/Iris/Instances/Lib/FUpd.lean | 1 - Iris/Iris/ProofMode/Instances.lean | 2 -- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 4 ++-- 4 files changed, 6 insertions(+), 9 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index c62d38d76..6985ec9d3 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -24,7 +24,7 @@ inductive IsOp.Direction meta section @[reducible] -def IsOp.Direction.mapToInOut (d : IsOp.Direction) : InOut := +def IsOp.Direction.toInOut (d : IsOp.Direction) : InOut := match d with | merge => .out | split => .in end @@ -35,9 +35,9 @@ end -/ @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR] class IsOp [CMRA α] - (d : IsOp.Direction) (a : semiOutParam <| inOutParam d.mapToInOut α) - (b1 : semiOutParam <| inOutParam d.mapToInOut.negate α) - (b2 : semiOutParam <| inOutParam d.mapToInOut.negate α) where + (d : IsOp.Direction) (a : semiOutParam <| inOutParam d.toInOut α) + (b1 : semiOutParam <| inOutParam d.toInOut.negate α) + (b2 : semiOutParam <| inOutParam d.toInOut.negate α) where is_op : a ≡ b1 • b2 set_option synthInstance.checkSynthOrder false in diff --git a/Iris/Iris/Instances/Lib/FUpd.lean b/Iris/Iris/Instances/Lib/FUpd.lean index 2df749aed..9fcc8dab9 100644 --- a/Iris/Iris/Instances/Lib/FUpd.lean +++ b/Iris/Iris/Instances/Lib/FUpd.lean @@ -483,7 +483,6 @@ instance fromPure_fupd_finally (a : Bool) (E : CoPset) (P : IProp GF) (φ : Prop refine .trans ?_ (fupd_finally_intro E _) cases a <;> simp only [affinelyIf_false, affinelyIf_true] <;> exact Plain.plain -set_option synthInstance.checkSynthOrder false in @[rocq_alias from_forall_fupd_pure] instance fromForall_fupd_pure {A : Type _} (E : CoPset) (P : IProp GF) (Φ : A → IProp GF) (φ : A → Prop) [h : FromForall P Φ] [hp : ∀ x, FromPure false (Φ x) .out (φ x)] : diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean index 60a345d37..8d9052f52 100644 --- a/Iris/Iris/ProofMode/Instances.lean +++ b/Iris/Iris/ProofMode/Instances.lean @@ -175,7 +175,6 @@ instance intoForall_persistently [BI PROP] [BIPersistentlyForall PROP] (P : PROP [h : IntoForall P Φ] : IntoForall iprop( P) (fun a => iprop( (Φ a))) where into_forall := (persistently_mono h.1).trans persistently_forall_mp -set_option synthInstance.checkSynthOrder false in @[ipm_backtrack, rocq_alias into_forall_wand_pure] instance intoForall_wand_pure [BI PROP] (P Q : PROP) Φ [h : FromPure a P .out Φ] : IntoForall iprop(P -∗ Q) (fun _ : Φ => Q) where @@ -681,7 +680,6 @@ instance intoPure_pure_or (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∨ P2) (φ1 ∨ φ2) where into_pure := (or_mono h1.1 h2.1).trans pure_or.1 -set_option synthInstance.checkSynthOrder false in @[rocq_alias into_pure_pure_impl] instance intoPure_pure_imp (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : FromPure a P1 .out φ1] [or : TCOr (TCEq a false) (BIAffine PROP)] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 → P2) (φ1 → φ2) where diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index 7ed90981d..655feb94a 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -128,7 +128,7 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar @[reducible, expose] def inOutParam (_io : InOut) (α : Sort u) : Sort u := α -private def parseSemiOutParamIPM (d : Expr) : Option Expr := do +private def parseInOutParam (d : Expr) : Option Expr := do if d.isAppOfArity ``semiOutParam 1 then let expr := d.getAppArgs[0]! if expr.isAppOfArity ``inOutParam 2 then @@ -146,7 +146,7 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .uncheckedIn) b else if d.isOutParam then computeParamKinds (params.push .out) b - else if let some expr := parseSemiOutParamIPM d then + else if let some expr := parseInOutParam d then computeParamKinds (params.push (.semiOut expr)) b else if d.isAppOfArity ``inOutParam 2 then Except.error m!"invalid ipm_class, `inOutParam` used in parameter \ From 0407b2d3cf999f4f068a854b52253f4a54a5e8a8 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 22 Jul 2026 11:56:37 +0200 Subject: [PATCH 22/26] Minor formatting --- Iris/Iris/ProofMode/Classes.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index d1fbf5dc8..ef423e0c2 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -37,14 +37,16 @@ end @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (io : InOut) - (PROP : semiOutParam <| inOutParam io (Type _)) - (bi : semiOutParam <| inOutParam d.toInOut (BI PROP)) + (PROP : semiOutParam <| inOutParam io <| Type _) + (bi : semiOutParam <| inOutParam d.toInOut <| BI PROP) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) + @[rocq_alias as_emp_valid_1] theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) (inst : AsEmpValid .into φ io PROP bi P) : φ → ⊢ P := inst.as_emp_valid.left rfl + @[rocq_alias as_emp_valid_2] theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) (inst : AsEmpValid .from φ io PROP bi P) : (⊢ P) → φ := From ae757dad9af2651a6f199a56ffe7b948fbbc03eb Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 22 Jul 2026 12:57:04 +0200 Subject: [PATCH 23/26] More consistent explicit/implicit arguments --- Iris/Iris/ProofMode/Classes.lean | 8 ++++---- Iris/Iris/ProofMode/Instances.lean | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index ef423e0c2..f780abc78 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -36,24 +36,24 @@ def AsEmpValid.Direction.toInOut : AsEmpValid.Direction → InOut end @[ipm_class, rocq_alias AsEmpValid] -class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (io : InOut) +class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) io (PROP : semiOutParam <| inOutParam io <| Type _) (bi : semiOutParam <| inOutParam d.toInOut <| BI PROP) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) @[rocq_alias as_emp_valid_1] -theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) +theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) {io} (inst : AsEmpValid .into φ io PROP bi P) : φ → ⊢ P := inst.as_emp_valid.left rfl @[rocq_alias as_emp_valid_2] -theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) +theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) {io} (inst : AsEmpValid .from φ io PROP bi P) : (⊢ P) → φ := inst.as_emp_valid.right rfl @[ipm_class, rocq_alias AsEmpValid0] -class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (io : InOut) +class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (io : InOut := d.toInOut) (PROP : semiOutParam $ inOutParam io <| Type _) (bi : semiOutParam $ inOutParam d.toInOut <| BI PROP) (P : outParam PROP) where as_emp_valid_0 : AsEmpValid d φ io PROP bi P diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean index e4a93a884..0bff74e2a 100644 --- a/Iris/Iris/ProofMode/Instances.lean +++ b/Iris/Iris/ProofMode/Instances.lean @@ -21,25 +21,25 @@ open Iris.BI Iris.Std -- AsEmpValid @[rocq_alias as_emp_valid_emp_valid] instance (priority := default + 10) asEmpValidEmpValid - [bi : BI PROP] d (P : PROP) : AsEmpValid0 d (⊢ P) io PROP bi P where + [bi : BI PROP] d (P : PROP) io : AsEmpValid0 d (⊢ P) io PROP bi P where as_emp_valid_0 := ⟨by simp⟩ @[rocq_alias as_emp_valid_entails] -instance asEmpValid_entails [bi : BI PROP] d (P Q : PROP) : +instance asEmpValid_entails [bi : BI PROP] d io (P Q : PROP) : AsEmpValid0 d (P ⊢ Q) io PROP bi iprop(P -∗ Q) where as_emp_valid_0 := ⟨λ _ => entails_wand, λ _ => wand_entails⟩ -instance asEmpValid_bientails [bi : BI PROP] (P Q : PROP) : +instance asEmpValid_bientails [bi : BI PROP] d io (P Q : PROP) : AsEmpValid0 d (P ⊣⊢ Q) io PROP bi iprop(P ∗-∗ Q) where as_emp_valid_0 := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩ @[rocq_alias as_emp_valid_equiv] -instance asEmpValid_equiv [bi : BI PROP] (P Q : PROP) : +instance asEmpValid_equiv [bi : BI PROP] d io (P Q : PROP) : AsEmpValid0 d (P ≡ Q) io PROP bi iprop(P ∗-∗ Q) where as_emp_valid_0 := ⟨λ _ h => equiv_wandIff (equiv_iff.1 h), λ _ h => (equiv_iff.2 (wandIff_equiv h))⟩ @[rocq_alias as_emp_valid_forall] -instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP) +instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP) d io [hP : ∀ x, AsEmpValid d (Φ x) io PROP bi iprop(P x)] : AsEmpValid d (∀ x, Φ x) io PROP bi iprop(∀ x, P x) where as_emp_valid := ⟨λ hd h => forall_intro λ x => (hP x).1.1 hd (h x), @@ -51,7 +51,7 @@ instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 : -- FromWand @[rocq_alias from_wand_wand] -instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩ +instance fromWand_wand [BI PROP] (P1 P2 : PROP) io : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩ -- IntoWand #rocq_ignore into_wand_wand' "IntoWand' is not used in Lean" From b0d11a94163f37168fd3ede5cf8e090a49376bfe Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 22 Jul 2026 16:09:46 +0200 Subject: [PATCH 24/26] Revert "Replace `semiOutParamIPM` with `semiOutParam (inOutParam ...)`" This reverts commit f905106bdf58feb6c76d278dd2b110016b3c64ba. --- Iris/Iris/Algebra/IsOp.lean | 6 ++--- Iris/Iris/ProofMode/Classes.lean | 14 +++++------ Iris/Iris/ProofMode/SynthInstanceAttr.lean | 28 +++++++++++++++------- Iris/Iris/Tests/Instances.lean | 17 +++++++------ 4 files changed, 38 insertions(+), 27 deletions(-) diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 6985ec9d3..96de1ee34 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -35,9 +35,9 @@ end -/ @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR] class IsOp [CMRA α] - (d : IsOp.Direction) (a : semiOutParam <| inOutParam d.toInOut α) - (b1 : semiOutParam <| inOutParam d.toInOut.negate α) - (b2 : semiOutParam <| inOutParam d.toInOut.negate α) where + (d : IsOp.Direction) (a : semiOutParamIPM d.toInOut α) + (b1 : semiOutParamIPM d.toInOut.negate α) + (b2 : semiOutParamIPM d.toInOut.negate α) where is_op : a ≡ b1 • b2 set_option synthInstance.checkSynthOrder false in diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index f780abc78..2cc71a56c 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -37,8 +37,8 @@ end @[ipm_class, rocq_alias AsEmpValid] class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) io - (PROP : semiOutParam <| inOutParam io <| Type _) - (bi : semiOutParam <| inOutParam d.toInOut <| BI PROP) + (PROP : semiOutParamIPM io (Type _)) + (bi : semiOutParamIPM d.toInOut (BI PROP)) (P : outParam $ PROP) where as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ) @@ -73,7 +73,7 @@ export FromImp (from_imp) @[ipm_class, rocq_alias FromWand] class FromWand {PROP} [BI PROP] (P : PROP) (io : InOut) - (Q1 : semiOutParam <| inOutParam io PROP) (Q2 : outParam $ PROP) where + (Q1 : semiOutParamIPM io PROP) (Q2 : outParam $ PROP) where from_wand : (Q1 -∗ Q2) ⊢ P export FromWand (from_wand) @@ -81,8 +81,8 @@ export FromWand (from_wand) @[ipm_class, rocq_alias IntoWand] class IntoWand {PROP} [BI PROP] (p q : Bool) (R : PROP) - (ioP : InOut) (P : semiOutParam <| inOutParam ioP PROP) - (ioQ : InOut) (Q : semiOutParam <| inOutParam ioQ PROP) where + (ioP : InOut) (P : semiOutParamIPM ioP PROP) + (ioQ : InOut) (Q : semiOutParamIPM ioQ PROP) where into_wand : □?p R ⊢ □?q P -∗ Q export IntoWand (into_wand) @@ -158,7 +158,7 @@ export IntoAbsorbingly (into_absorbingly) @[ipm_class, rocq_alias FromAssumption, rocq_alias KnownLFromAssumption, rocq_alias KnownRFromAssumption] class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut) - (P : semiOutParam <| inOutParam ioP PROP) (Q : PROP) where + (P : semiOutParamIPM ioP PROP) (Q : PROP) where from_assumption : □?p P ⊢ Q export FromAssumption (from_assumption) @@ -171,7 +171,7 @@ export IntoPure (into_pure) @[ipm_class, rocq_alias FromPure, rocq_alias FromPureT] class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut) - (φ : semiOutParam <| inOutParam ioφ Prop) where + (φ : semiOutParamIPM ioφ Prop) where from_pure : ?a ⌜φ⌝ ⊢ P export FromPure (from_pure) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index 655feb94a..e02a90d46 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -126,12 +126,25 @@ private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Ar (ipmClassesExt.getState env).paramMap.find? declName @[reducible, expose] -def inOutParam (_io : InOut) (α : Sort u) : Sort u := α +def semiOutParamCore (_io : InOut) (α : Sort u) : Sort u := α + +/-- + The keyword `semiOutParamIPM` is analogous to `semiOutParam`, with + an `InOut` value as an explicit argument, which determines whether this is an + input parameter or an output paramter for the purpose of type class synthesis. + + One can use `InOut.negate` to negate the `InOut` value. + + This should be used instead of `semiOutParam` for any type class with + the annotation `[ipm_class]`. +-/ +macro "semiOutParamIPM" io:term:max α:term:max : term => + `(semiOutParam (semiOutParamCore $io $α)) private def parseInOutParam (d : Expr) : Option Expr := do if d.isAppOfArity ``semiOutParam 1 then let expr := d.getAppArgs[0]! - if expr.isAppOfArity ``inOutParam 2 then + if expr.isAppOfArity ``semiOutParamCore 2 then some expr.getAppArgs[0]! else none else none @@ -148,13 +161,12 @@ Except MessageData (Array ParamKind) := computeParamKinds (params.push .out) b else if let some expr := parseInOutParam d then computeParamKinds (params.push (.semiOut expr)) b - else if d.isAppOfArity ``inOutParam 2 then - Except.error m!"invalid ipm_class, `inOutParam` used in parameter \ - #{params.size + 1} but not within `semiOutParam`. \ - Use `semiOutParam (inOutParam …)` instead." + else if d.isAppOfArity ``semiOutParamCore 2 then + Except.error m!"invalid ipm_class, `semiOutParamCore` used directly \ + in parameter #{params.size + 1}. Use `semiOutParamIPM` instead" else if d.isSemiOutParam then - Except.error m!"invalid ipm_class, `semiOutParam` used without `inOutParam` \ - in parameter #{params.size + 1}. Use `semiOutParam (inOutParam …)` instead." + Except.error m!"invalid ipm_class, `semiOutParam` used directly \ + in parameter #{params.size + 1}. Use `semiOutParamIPM` instead" else computeParamKinds (params.push .in) b | _ => return params diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean index 3cb528802..882876713 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/Iris/Tests/Instances.lean @@ -304,8 +304,7 @@ section issue_456 -- test for https://github.com/leanprover-community/iris-lean/issues/456 @[ipm_class] -class C (io : InOut) (a : semiOutParam <| inOutParam io Nat) - (b : semiOutParam <| inOutParam io.negate Nat) : Prop where +class C (io : InOut) (a : semiOutParamIPM io Nat) (b : semiOutParamIPM io.negate Nat) : Prop where abbrev CMerge (a b : Nat) := C .out a b @@ -331,25 +330,25 @@ end issue_456 section semiOutParam -/-- error: invalid ipm_class, `semiOutParam` used without `inOutParam` in parameter #2. Use `semiOutParam (inOutParam …)` instead. -/ +/-- error: invalid ipm_class, `semiOutParam` used directly in parameter #2. Use `semiOutParamIPM` instead -/ #guard_msgs in @[ipm_class] class C1 (io : InOut) (a : semiOutParam Nat) : Prop where -/-- Tests `semiOutParam (inOutParam …)` where the `InOut` value depends on another argument by pattern matching. -/ +/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by pattern matching. -/ @[ipm_class] -class C2 (a : Bool) (a : semiOutParam <| inOutParam (match a with | false => .in | true => .out) Nat) : Prop where +class C2 (a : Bool) (a : semiOutParamIPM (match a with | false => .in | true => .out) Nat) : Prop where -/-- Tests `semiOutParam (inOutParam …)` where the `InOut` value depends on another argument by conditional branching. -/ +/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by conditional branching. -/ @[ipm_class] -class C3 (a : Bool) (a : semiOutParam <| inOutParam (if a then .in else .out) Nat) : Prop where +class C3 (a : Bool) (a : semiOutParamIPM (if a then .in else .out) Nat) : Prop where /- The attribute `semiOutParam` is still relevant for regular type classes -/ class C4 (io : InOut) (a : semiOutParam Nat) : Prop where -/-- error: invalid ipm_class, `inOutParam` used in parameter #2 but not within `semiOutParam`. Use `semiOutParam (inOutParam …)` instead. -/ +/-- error: invalid ipm_class, `semiOutParamCore` used directly in parameter #2. Use `semiOutParamIPM` instead -/ #guard_msgs in @[ipm_class] -class C5 (io : InOut) (a : inOutParam .in Nat) : Prop where +class C5 (io : InOut) (a : semiOutParamCore .in Nat) : Prop where end semiOutParam From d3401ec0c7c311e74be257aaa7c9e1e2e5645aa0 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 22 Jul 2026 16:10:19 +0200 Subject: [PATCH 25/26] Update `AsEmpValid0` --- Iris/Iris/ProofMode/Classes.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index 2cc71a56c..a6227a704 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -54,8 +54,8 @@ theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) {io} @[ipm_class, rocq_alias AsEmpValid0] class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (io : InOut := d.toInOut) - (PROP : semiOutParam $ inOutParam io <| Type _) - (bi : semiOutParam $ inOutParam d.toInOut <| BI PROP) (P : outParam PROP) where + (PROP : semiOutParamIPM io (Type _)) + (bi : semiOutParamIPM d.toInOut (BI PROP)) (P : outParam PROP) where as_emp_valid_0 : AsEmpValid d φ io PROP bi P attribute [ipm_backtrack,instance] AsEmpValid0.as_emp_valid_0 From 8a02501a4729596c21a706b5f4b0ebf0ac82ff8c Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Wed, 22 Jul 2026 16:23:24 +0200 Subject: [PATCH 26/26] update comments --- Iris/Iris/ProofMode/SynthInstanceAttr.lean | 34 +++++++++------------- 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean index e02a90d46..533e2bc71 100644 --- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean +++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean @@ -44,24 +44,21 @@ The parameters of a class declared with `ipm_class` are categorized into the fol 1. in: This is the default for a parameter when not annotated in another way. 2. out: These are parameters marked with `outParam`. These parameters must be mvars when starting typeclass search. -3. semiOut: These are parameters marked with `semiOutParam`. The preceding parameter must be of type `InOut`. - The value of the `InOut` parameter decides whether the `semiOut` parameter is treated as an input - or an output. +3. semiOut: These are parameters marked with `semiOutParamIPM`. The `InOut` argument of `semiOutParamIPM` + determines whether the semiOut parameter is treated as an input or an output. 4. uncheckedIn: These are parameters marked with `uncheckedInParam`. These behave like `in` parameters, but allow mvars to match terms (see below). The following constraints apply to the parameters: -(In the following, semiOut parameters are treated as inputs if the preceding `InOut` is `in` and as -outputs if the `InOut` is `out`.) -1. semiOut parameters must have a preceding `InOut` parameter. -2. For each synthesis problem, all output parameters must be mvars. -3. When an input parameter is a mvar, it is not considered to match an instance which does not have +(In the following, semiOut parameters are treated as inputs according to the value of their `InOut` argument.) +1. For each synthesis problem, all output parameters must be mvars. +2. When an input parameter is a mvar, it is not considered to match an instance which does not have an mvar at the top-level. This is to prevent accidentally instantiating mvars. Note that this only applies for mvars the top-level (matching the behavior of Hint Mode : ! in Rocq), since this is the simplest version to implement and catches most (all?) of the cases. -This check 3 is omitted for `uncheckedIn` parameters. +This check 2 is omitted for `uncheckedIn` parameters. -(We are reusing `outParam` and `semiOutParam` from the Lean TC infrastructure since this gives us +(We are reusing `outParam` from the Lean TC infrastructure since this gives us checking synthesis order checking, which is useful (though not perfect).) -/ inductive ParamKind @@ -133,8 +130,6 @@ def semiOutParamCore (_io : InOut) (α : Sort u) : Sort u := α an `InOut` value as an explicit argument, which determines whether this is an input parameter or an output paramter for the purpose of type class synthesis. - One can use `InOut.negate` to negate the `InOut` value. - This should be used instead of `semiOutParam` for any type class with the annotation `[ipm_class]`. -/ @@ -142,15 +137,12 @@ macro "semiOutParamIPM" io:term:max α:term:max : term => `(semiOutParam (semiOutParamCore $io $α)) private def parseInOutParam (d : Expr) : Option Expr := do - if d.isAppOfArity ``semiOutParam 1 then - let expr := d.getAppArgs[0]! - if expr.isAppOfArity ``semiOutParamCore 2 then - some expr.getAppArgs[0]! - else none - else none - -private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : -Except MessageData (Array ParamKind) := + if !d.isAppOfArity ``semiOutParam 1 then failure + let expr := d.getAppArgs[0]! + if !expr.isAppOfArity ``semiOutParamCore 2 then failure + some expr.getAppArgs[0]! + +private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : Except MessageData (Array ParamKind) := match type with | .forallE _ d b _ => -- we need to check this before outParam since `outParam (uncheckedInParam _)` should be