feat: OFE step-indexing parametrisation, port algebra/stepindex_finite.v

[alvinylt]

Description

Ports algebra/stepindex_finite.v, which involves an instance of SIdx with natural numbers (Nat), and generalises definitions in Algebra/OFE.lean. Everything dependent on Algebra/OFE.lean shall be updated accordingly.

Addresses #29 and #230 in part.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[alvinylt]

At the moment, only the definitions within Algebra/OFE.lean have been changed. The main changes are:

• OFE, IsCOFE and COFE: adds SI as an explicit parameter and [SIdx SI] as a premise. We have SI as an output parameter (outParam (Type _)) so that, given α, Lean finds the instance OFE SI α and infers SI automatically.
  • Before refactor: retire setoids #533 was merged, I tried having SI as a regular parameter (Type _). But that meant, for every occurrence of x ≡ y, x ≡{0}≡ y, α -n> β or α -c> β, we have to specify SI := SI explicitly. (See the now discarded commit for that attempt.) This was not an issue in Rocq with ofe as a structure fixed to {SI : sidx} declared in the beginning, rather than as a type class.
• The instances OFE SI Unit (previously OFE Unit) and @COFE SI _ Unit (previously COFE Unit) are now reducible defs instead of instances.
  • A consequence of having SI as an outParam. We already concretely have SI, so Lean would complain about the synthesis order if they were defined using instance.
  • Some proofs may now require local haveI to use these instances.

The proofs are not yet updated, so the code on the branch does not compile. @Kaptch Could you check if these changes are in the direction that we want before we proceed with updating the rest of the code?

[Kaptch]

Thanks! Looks nice by me!

Before #533 was merged, I tried having SI as a regular parameter (Type _). But that meant, for every occurrence of x ≡ y, x ≡{0}≡ y, α -n> β or α -c> β, we have to specify SI := SI explicitly. (See the now discarded commit for that attempt.) This was not an issue in Rocq with ofe as a structure fixed to {SI : sidx} declared in the beginning, rather than as a type class.

Yeah, I also had the same problem before, I'm not sure if there's a good way to avoid explicit SI in the current setup. Probably, it feature we could experiment with some attribute/flag, but for now explicit parameter should be fine.

[alvinylt]

Up to commit f59dcf0 (see diff), OFE, IsCOFE, COFE and some related type classes in Algebra/OFE.lean have been parametrised over SI, along with some relatively simple changes to the proofs throughout the file. The section Fixpoint is where things get more involved, as bounded chains have not been ported.

So here's the plan: until the latest commit (see diff), definitions in relation to BChain, BFChain, etc. have been ported, and at the point everything should build without error except for some warning about sorrys. The next step is to fill in those proofs. Meanwhile, we now have CMRA α extending OFE Nat α. Likewise, all other files under the Algebra directory are expressed in terms of OFE Nat .../COFE Nat .../OFunctorPre Nat/..., which we can gradually parametrise. This will hopefully make the changes easier to review.

[Kaptch]

Sounds good! I think finishing OFE parametrization in this PR (including fixpoints, but limited to OFE.lean file) is a good goal, because CMRA parametrization will also require changing BI (and probably some parts of proof mode), so it would be nice to do it separately. Just ping me, when you think it is ready, and i can review and merge it.

[MackieLoeffel]

Sorry, I might have missed it in the discussion, but what do you think about following what Rocq does and use the following (proposed by Alvin above)?

class SIdx : Type _ where
  I : Type u
  ... -- existing fields here
    
class OFE [SI : SIdx] (α : Type _) where
  Dist : SI.I → α → α → Prop
  dist_eqv : Equivalence (Dist n)
  eq_dist : x = y ↔ ∀ n, Dist n x y
  dist_lt : Dist n x y → m < n → Dist m x y

edited in response to Markus' comment below

This indeed assumes that there is only SIdx structure in the context at any point, but this is quite easy to achieve: files that are generic over the SIdx use variable [SI : SIdx], files that want natural numbers do something like import Algebra.NatSIdx and files that want ordinals use something like import IrisMath.Algebra.OrdinalSIdx . The benefit of this is that the porting effort is really minimal. This is how it works in Rocq and it seems to work fine there. Also this solution requires the least amount of porting work and if we later run into issues and want to use a different solution, we can still change it (and maybe also talk with the Iris Rocq maintainers since they might run into similar issues as well).

[markusdemedeiros]

Before I reply, is this a typo? I assumed Alvin was bringing this up just an an analogy to how this is done in Rocq, not a suggestion for doing it this way in Lean. What you suggested here is actually an extremely invasive change: it would mean going from an unbundled typeclass hierarchy to a bundled hierarchy, and if you use typeclass inference for that you can only have one OFE in scope at once. I assume you meant something different but I'm not sure what.

[MackieLoeffel]

You are of course right, the version from my previous message did not make sense. I've edited it to the version I actually had in mind (hopefully at least).

[markusdemedeiros]

Positing that it is actually easy to manage these scopes (I'm not sure I actually believe this) there are other challenges. For one, projecting out of the SIdx type requires a dependent cast, which are generally poorly behaved in Lean and should be avoided. We use them in the construction of BundledGFunctors because they are unavoidable and can be contained behind an API. Neither is not the case here.

Here is an example of the kind of mess you can get yourself into with this approach: live.lean-lang.org. Maybe you can find a fix for this specific example but I'm more partial to staying in the happy path of Lean's typeclass synthesis algorithm if at all possible.

[MackieLoeffel]

I was able to fix all issues in your example with type annotations, see here.
Alternatively, you can fix all the problems with

instance : OfNat instNatSIdx.I n where
  ofNat := n

see here.

I have not worked enough with Lean to know exactly what the pitfalls of dependent casts are. I guess we could try the (fixed) approach from my previous message in a branch and see what kind of problems appear?

[markusdemedeiros]

Off the top of my head I'll also note the following:

• Any operation you do to a step index now involves dependent cases, which is known to be limited in Lean.
• Step indices are no longer defeq to their underlying type (we are ignoring an explicit compiler warning against this in the example) so all automation including typeclasses and rewriting is suspect. Alvin's work uses omega, this will need to be rewritten. I have no idea what happens to Sergei's work.
• It adds a universe bump to OFE. Might not be a problem, though I am not confident about this.

Zooming back out: the question is whether this is worth complicating our core theory like this just to avoid having extra notation. To me the answer to this still seems to be an obvious no!! But if you guys think this is worth it, I guess we might as well try...

In fact, why don't we have a general notation for the general case, and then scoped notation for each instance that makes it look like the existing code? The general library code will need to use the slightly more verbose notation but clients with a fixed index type would not.

[MackieLoeffel]

About your points:

Any operation you do to a step index now involves dependent cases, which is known to be limited in Lean.

This point is very vague to me. Do you have concrete pointers that describe the limitations of dependent cases in Lean? (I am not even fully sure what you mean with dependent cases.) I think this point would also be best demonstrated by trying the bundled version of SIdx and seeing what problems arise. I think this will be interesting in any case.

Step indices are no longer defeq to their underlying type (we are ignoring an explicit compiler warning against this in the example) so all automation including typeclasses and rewriting is suspect. Alvin's work uses omega, this will need to be rewritten. I have no idea what happens to Sergei's work.

Nat is still defeq to instNatSIdx.I in the examples above, at least at default reducibility. It might be not defeq for lower reducibility settings. Maybe unification hints can help there. I am not sure how this interacts with omega, but in the worst case it seems like one would need to call a tactic that unfolds all instNatSIdx.I to Nat before calling omega.

It adds a universe bump to OFE. Might not be a problem, though I am not confident about this.

I don't think this is true. OFE can still live in Type, see here.

I also want to be clear that at this point I don't know what the better approach is. I think this encoding of stepindices is a quite fundamental decision and we should make this decision carefully. This is why I think we should try out both approaches such that we can get some actual data on what the advantages and disadvantages of each approach are such that we can make an informed decision and don't need to speculate.

@alvinylt Would it be possible to create a new branch based on this sketch of the approach? (Note the use of SIdxMixin to move out the data.)

[MackieLoeffel]

There is actually another version that comes to mind (based on the discussion above): We can use the non-bundled version, but make the stepindex type an outParam. This should avoid all the dependent cases problems that @markusdemedeiros is worried about, while still ensuring that we don't need to add the type of stepindices to all notations and so on since it can be inferred automatically. (This still requires there to be a single instance in scope, like in Rocq.)
The sketch of it is here. What do you think about this?

[alvinylt]

We can use the non-bundled version, but make the stepindex type an outParam.

Do you mean the following?

class SIdx (I : outParam <| Type u) extends LT I, LE I, Zero I where
  succ : I → I
  lt_trans : ∀ {n m p : I}, n < m → m < p → n < p
  ... -- other fields here

class OFE {SI : Type _} [SIdx SI] (α : Type _) where
  Dist : SI → α → α → Prop
  dist_eqv : Equivalence (Dist n)
  eq_dist : x = y ↔ ∀ n, Dist n x y
  dist_lt : Dist n x y → m < n → Dist m x y

...

open OFE

scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist n x y

namespace OFE

variable [instSI : SIdx SI]

theorem Dist.of_eq [OFE α] {x y : α} : x = y → x ≡{n}≡ y := (· ▸ .rfl)

In this case, Lean gives an error about OFE α having metavariables. This can be easily solved by making the type of n explicit:

theorem Dist.of_eq [OFE α] {n : SI} {x y : α} : x = y → x ≡{n}≡ y := (· ▸ .rfl)

Not that this solution is difficult, but the error message that the "type class instance problem is stuck with OFE α" does not make the cause immediately obvious, so it is worth noting if we adopt this approach.

[MackieLoeffel]

Does making SI an outParam in OFE solve this? I.e.

class OFE {SI : outParam <| Type _} [SIdx SI] (α : Type _) where

[alvinylt]

Does making SI an outParam in OFE solve this?

Yes, I have managed to have OFE.lean, StepIndex.lean and StepIndexFinite.lean successfully built with this new definition in a branch (see diff). Currently the SIdx instance for natural numbers exists in the global scope. For modules that depend on both OFE.lean and StepIndexFinite.lean, whenever [OFE α] is a premise of a class/theorem, it defaults to the instance natSIdx : SIdx Nat.

Would it be possible to create a new branch based on this sketch of the approach? (Note the use of SIdxMixin to move out the data.)

Here is another branch: see diff. The proofs in relation to SIdx and things beyond the first section in OFE.lean will have to be updated accordingly, but other than that, it seems that there is no problem with type class inference when the OFE relations are used.

[markusdemedeiros]

I don't think this is true. OFE can still live in Type

You are right about this, my mistake. The universe bump in SIdx does not translate to OFE.

I am not sure how this interacts with omega, but in the worst case it seems like one would need to call a tactic that unfolds all instNatSIdx.I to Nat before calling omega.

I would like to see this--you're probably better at dependent-type-fu than I am:

-- What automation breaks? 
open NatIndices in 
example {m n : instNatSIdx.I} (h' : m ≤ n) (h : m ≠ n) : m < n := by 
  -- omega  -- fails
  -- exact?  -- fails
  -- grind -- fails
  unfold instNatSIdx at m 
  unfold instNatSIdx at n 
  -- omega -- fails
  -- exact? -- fails
  -- grind -- fails
  have H : instNatSIdx.I = Nat := by exact optParam_eq SIdx.I m
  -- rw [H] in m --  Tactic `rewrite` failed: motive is not type correct ... 
  cases h' 
  · grind
  · simp only [Nat.succ_eq_add_one, gt_iff_lt]
    /-
    T : Type ?u.2
    U : Type ?u.4
    m : SIdx.I
    H : SIdx.I = Nat
    m✝ : Nat
    a✝ : Nat.le m m✝
    h : m ≠ m✝.succ
    ⊢ m < m✝ + 1
    -- There is a new m in the context, because of the dependent cases, but at least it's a Nat now?
    -/
    -- Maybe cases on m too?
    cases m -- Well, at least everything is a Nat now
    · -- apply? -- Doesn't work??
      -- Oh, is SIdx.I still present in the invisible LT instance? 
      -- This should be defeq to the instance for Nat but of course
      -- Maybe I need to transport the instance as well?
      sorry
    · sorry

-- Of course, supplying the answer directly works, even though exact? can't find it. 
open NatIndices in 
example {m n : SIdx.I} (h' : m ≤ n) (h : m ≠ n) : m < n := Nat.lt_of_le_of_ne h' h

Does making SI an outParam in OFE solve this?

This is more or less where the PR started.

Anyways, I feel like I'm missing something, because intentionally breaking the assumptions of Lean's typeclass system just to solve a metaprogramming problem seems like a total self-own for no reason. I'm probably just overfit to this because a poor hierarchy is the reason I stopped using Iris-Rocq, and I was hoping the hierarchy in Iris-Lean could be as stable as possible. I'm will prepare a new PR with my proposal so I understand your guy's problem with it better.

[MackieLoeffel]

I would like to see this--you're probably better at dependent-type-fu than I am:
The following works, see here:

example {m n : instNatSIdx.I} (h' : m ≤ n) (h : m ≠ n) : m < n := by 
  simp [SIdx.I] at h h' m n |- 
  grind 

This is more or less where the PR started.

Well, there is a crucial difference: This PR in its current form has a 1000-line diff since it needs to add an explicit parameter to all uses of OFE. My hope would be that uses outParam significantly reduces this diff.

Thanks for preparing the different versions @alvinylt ! It seems like the outParam version avoids the problems of the bundled type while still providing the benefits of automatic inference. (In particular, compare the changes to e.g. CofeSolver.lean with outParam and without outParam.) This seems quite nice. @markusdemedeiros What do you think about the version in this diff?

Anyways, I feel like I'm missing something, because intentionally breaking the assumptions of Lean's typeclass system just to solve a metaprogramming problem seems like a total self-own for no reason. I'm probably just overfit to this because a poor hierarchy is the reason I stopped using Iris-Rocq, and I was hoping the hierarchy in Iris-Lean could be as stable as possible. I'm will prepare a new PR with my proposal so I understand your guy's problem with it better.

To be clear, I don't have any emotional attachment to any of these versions. I just want to discuss the different possibilities to make sure that we make an informed decision about this.
I am not sure what metaprogramming problem you are referring to. The problem I am worried about is that a lot of things get polluted with step-index type annotations.
I also lost track of what your proposal is and how it relates to the other options, so it would be great if you could describe it or implement it.

[Kaptch]

Just to provide more data, I've ported my thing to use this PR instead of using a home-brewed version of (C)OFEs parameterized by ordinals, and it worked well. It doesn't use concrete instances of SI though, just an arbitrary SI parameter. So purely from api completeness perspective it works nice!

Just to discuss possibilities: is there a way to produce an error/warning if there are two instances of SI in the context? I'm still not 100% sure what would be the problem, because the way I thought about it is: eventually we will have iProp/iPropTransfinite (or iProp (SI : Type _)), they bring different instances of SI into context and have different reasoning rules, but ultimately, the end-user never imports SI themself (unless they want to define yet another version of iProp).

[MackieLoeffel]

eventually we will have iProp/iPropTransfinite (or iProp (SI : Type _)), they bring different instances of SI into context

iProp/iPropTransfinite bring different instances in the context, but if they are never used in the same context, we still only ever have one instance in each context.
I think the crucial question is: Will we ever need a theorem that contains both iProp and iPropTransfinite? I don't know a reason why we would need this. Also the Iris Rocq maintainers think the answer is no (at least, the Iris Rocq setup assumes that there is at most one step index instance in the context). Can anyone think of a usecase that requires combining finite and transfinite step indexing in the same theorem?

[Kaptch]

iProp/iPropTransfinite bring different instances in the context, but if they are never used in the same context, we still only ever have one instance in each context.

Yes, sorry, I probably phrased in ambiguously. My point was that if we design it in a way that bringing SI instance can happen only by deliberate choice, then the current PR should be fine. Morally, right now SI should be fixed when importing CMRA (so probably SI instances and the interface should be split into different modules). Eventually, as more modules get parameterized, the pinning is going to happen when importing iProp/sProp.

Will we ever need a theorem that contains both iProp and iPropTransfinite?

I was thinking about one potential application, but haven't attempted it yet. For iPropTransfinite (over ordinal \gamma) one can define a family of modalities j_\alpha (for \alpha < \gamma) with j_\alpha(P)(n)(w) = n < \alpha \and P(n)(w). If cf(\alpha) < cf(\gamma) (e.g., \alpha = \omega, \gamma = \omega_1), then one can restore some missing logical rules in the transfinite setting, when working under the modality. But given that it's just a rough idea, and we still have a lot to do before it's even expressible, it's probably not an issue for now.

[MackieLoeffel]

From the discussion with @markusdemedeiros, @Kaptch, and @alvinylt (among other), the next steps of this PR would be to switch to the outParam version and see if we can get a linter that warns the user if there is ever more than one instance of the step index typeclass in scope.

It seem like Mathlib has an overlapping instance linter, which sounds like the linter we want: leanprover-community/mathlib4#38126 , implementation here

[markusdemedeiros]

I might misunderstand but the instances in the outParam version are not overlapping though, right? But we could also probably adapt that code to look for our specific case.

Not mentioned here I will be also exploring if my other PR if a term elab can be used to avoid all outParams and optParams and autoParams while also not introducing any new notation.

[MackieLoeffel]

I might misunderstand but the instances in the outParam version are not overlapping though, right?

I am not fully sure what counts as an overlapping instance in Lean. In any case, this linter might be a good starting point as you say.

Not mentioned here I will be also exploring if my other PR if a term elab can be used to avoid all outParams and optParams and autoParams while also not introducing any new notation.

Indeed, I've added a comment about this to the other PR.

[digama0]

I have an alternative proposal which I'm still working on a demo for, but the short version is to remove the outparam from SI and just use a combination of notation overloading and abbrev, plus a default_instance for the SIdx Nat instance, to avoid needing too much annotations when not working in general.

[digama0]

Here's the proposal. (analysis written by claude)

I spent some time building this out to see what the outParam question actually costs, and ended up with a branch that drops outParam entirely and gets the whole library building.

Branch: sidx-clean (df0eabe, diff vs master). It keeps Alvin's StepIndex/StepIndexFinite/bounded-chain port, reverts this PR's downstream churn to master, and then fixes what actually breaks. Iris builds in 272 jobs and IrisMath in 2134, both with 0 errors.

Numbers

	files	+/-
this PR, vs its base	58	+1176 −753
— excluding OFE/StepIndex*/COFESolver	55	+372 −348
sidx-clean, vs master	26	+1152 −543
— excluding OFE/StepIndex*/COFESolver	23	+76 −44

The downstream half of the diff fits on one screen. Line-length discipline is comparable to master: OFE.lean has 18 lines over 100 columns, master has 19, this PR has 37.

The proposal

OFE, IsCOFE, COFE and OFunctorPre take SI as an ordinary implicit input:

class OFE {SI : Type _} [SIdx SI] (α : Type _) where

The polymorphic core spells SI out; ω-indexed clients get it back from a block at the end of OFE.lean:

attribute [default_instance] natSIdx
scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist (SI := Nat) n x y
@[inherit_doc] infixr:25 " -n> " => OFE.Hom
theorem OFE.eq_dist [OFE α] {x y : α} : x = y ↔ ∀ n : Nat, x ≡{n}≡ y := OFE.eq_dist'

The position is load-bearing: the file itself elaborates without these, using local notation that carries SI, and every importer gets the ω-fixed versions. Clients keep writing [OFE α], α -n> β, x ≡{n}≡ y, OFE.eq_dist unchanged.

Why drop outParam: leaf instances

The reason isn't the #synth order-dependence, it's this. outParam promises the parameter is functionally determined by the inputs, and SI is not determined by α. So no leaf OFE can be an instance:

cannot find synthesization order for instance @natOFE with type
  {SI : Type u_1} → [inst : SIdx SI] → OFE SI Nat
all remaining arguments have metavariables:
  SIdx ?SI

Option α, α × β, α -n> β are fine — SI falls out of the argument's OFE instance. But anything whose OFE structure doesn't consume another OFE has nothing to determine SI, and must become a reducible def + a letI at each use site. That's why this PR has def unitOFE, def unitCOFE, def DiscreteO.instCOFE, theorem DiscreteO.OFE where master had plain instances, plus Nat-specific duplicates in StepIndexFinite.lean.

On the branch they are ordinary instances again. Restoring just those four fixed 129 downstream errors. That is the concrete cost of the workaround today, and it grows as more of the hierarchy is parametrised.

(For a pragmatic middle path: this only bites polymorphic leaves. instance : OFE Unit at SI := Nat passes checkSynthOrder fine, so even keeping outParam, the def + letI pattern could be dropped in favour of Nat instances plus polymorphic defs.)

Where default_instance reaches, and where it doesn't

@[default_instance] natSIdx does more than I expected — it fires for instance binders and for type constructors:

theorem t0 {α : Type} [OFE α] : True := trivial      -- ✓ SI defaults
theorem t2 {α : Type} [OFE α] (f : Hom α α) : True   -- ✓

It does not fire for OFE.Dist n x y with an untyped n, because a binder's type is settled before the default-instance pass runs. The Nat-fixed ≡{n}≡ closes that by unification instead, so the library's ~1000 untyped {n} binders keep inferring Nat:

@CMRA.pcore_ne : ∀ {α : Type} [self : CMRA α] {n : Nat} {x y cx : α}, …

CMRA.lean went from 102 errors to 0 with the file unchanged.

One more name needed the same treatment. eq_dist's statement mentions SI only under a binder, so as a term it can't infer it — and it is a class field, so OFE.eq_dist was taken. Renaming the field to eq_dist' frees the name for the ω-fixed statement above, which means all 114 client uses of OFE.eq_dist are untouched. Only the 27 sites that define an OFE instance change (eq_dist := … → eq_dist' := …), and those are being touched anyway. Without this, all 114 would need (SI := Nat).

What it costs

• The polymorphic core pays. OFE.lean carries ~790 (SI := SI) annotations and 35 local notation lines. No notation trick removes this: local notation "NonExpansive" f => … breaks NonExpansive.comp, because the name becomes a parser token.
• One (SI := Nat) pin left downstream, plus: two @Hom.id α _ applications that skipped implicits positionally, one Discrete that became ambiguous between CMRA.Discrete and OFE.Discrete, and five rw chains that no longer close Dist n x x by their trailing rfl.
• One ≡{n}≡ per file. A file can't use both the polymorphic and the ω notation — they overload, and a postponed instance failure doesn't disambiguate. The polymorphic/ω split respects this naturally, but anyone extending the core needs to know.
• I also tried semiOutParam. It does fix leaf instances, but produced the identical 21 errors, because those sites have α undetermined too, not just SI.

Verification

IrisMath has a SIdx Ordinal instance, so the two-indices-in-scope case can be checked for real rather than with a toy:

example : SIdx Nat := inferInstance                                -- ✓
example : SIdx Ordinal := inferInstance                            -- ✓
example : COFE (SI := Ordinal) (DiscreteO Nat) := inferInstance     -- ✓
#check fun {α : Type} [OFE α] {n} {x y : α} (h : x ≡{n}≡ y) => h.symm
--  ⊢ ∀ {α : Type} [inst : OFE α] {n : ℕ} {x y : α}, Dist n x y → Dist n y x

{n : ℕ} with SIdx Ordinal in scope — and deterministically, not by instance-declaration order: the notation pins it by unification and the default instance is a declared default rather than a search outcome. That is the property outParam cannot offer.

Churn that's essential either way

Part of this PR's downstream diff is unavoidable and unrelated to how SI is threaded: LimitPreserving becomes a class (f99f9ae) and IsCOFE gains lbcompl/conv_lbcompl/lbcompl_ne. Every instance provider must be updated regardless. At SI := Nat the new fields are vacuous — hn.elim via SIdx.Limit.elim — which is worth adopting as the standard idiom.

Pieces that are separable

This is one proposal among several, and most of it can be taken piecemeal — none of the following depends on the outParam decision:

• Leaf instances. instance : OFE Unit at SI := Nat passes checkSynthOrder even with outParam, so the reducible def + letI pattern can be dropped now in favour of Nat instances plus polymorphic defs.
• The vacuous limit fields. lbcompl hn _ := hn.elim via SIdx.Limit.elim is worth adopting as the standard idiom for SI := Nat instances of IsCOFE/LimitPreserving, however SI ends up being threaded.
• eq_dist' + an ω-fixed OFE.eq_dist. Any design in which SI is not guessed will hit this, since the statement mentions SI only under a binder. Renaming the field and republishing the familiar name at Nat costs 27 sites and saves 114.
• Publishing ω-fixed notation at the end of OFE.lean. Independent of how the class itself is parameterised; it is what keeps untyped {n} binders working.

Where this leaves the discussion

@markusdemedeiros's objection stands, and the leaf-instance breakage is a stronger form of it than the #synth example. But the prescription is not "a couple of duplicate notations": it is ~790 annotations in OFE.lean, because outParam on OFE is load-bearing for the whole derived hierarchy (NonExpansive, Contractive, Discrete, …), not just for notation. Making those classes' SI an outParam instead doesn't help — their [OFE SI α] premise is then stuck. If there is a way to keep the short positional spelling in polymorphic code while still refusing to guess, that would beat what I have here on the axis that costs the most.

@Kaptch's requirement is met: ω users write exactly what they write today, with no new notation and no annotations. The generalisation is invisible to them.

[markusdemedeiros]

@digama0 Did you want to make a PR out of this so there's somewhere to comment on it, or are you holding off for some reason?

[MackieLoeffel]

Thanks for trying this out. But it seems like the https://github.com/leanprover-community/iris-lean/tree/sidx-clean branch does not solve the problem that writing generic code requires a lot of adaptation, as the description says itself. Also I don't think hard coding Nat in the notations is a good idea. We want to use these notations for generic step indices, not just for Nat.

I do not understand the point about leaf instances. They seem to work fine with outParam, as far as I can tell. See the instance here, which is part of the outParam branch.

[markusdemedeiros]

@MackieLoeffel @Kaptch How much code outside of Iris-Lean would you expect to be generic in terms of the type of step indices? I didn't think about default_instance but it seems like scoped default instances would help out here (open a scope to update all of the notation and the default instance, no scope keeps the normal typeclass behavior). The fact that we can't do this seems like a bug leanprover/lean4#6604

[markusdemedeiros]

The other thing which would be nice (in theory) would be if a scoped default instance could refer to section variables. Together, these two features would solve all of our problems, because we could just open a GenericSI scope to make everything generic, and the hierarchy would remain stable because at any point the default instance resolution would be self-consistent.

[Kaptch]

How much code outside of Iris-Lean would you expect to be generic in terms of the type of step indices?

Could you please elaborate? I'm not sure I understood correctly. E.g., the stuff that I work on is generic in SI.

[markusdemedeiros]

How much code outside of Iris-Lean would you expect to be generic in terms of the type of step indices?

Could you please elaborate? I'm not sure I understood correctly. E.g., the stuff that I work on is generic in SI.

I was not sure if what you were working on required the core theory to be generic in terms of SI so you could fix it to something (omega or whatnot) or if your work was also generic. This answers my question, thanks

[digama0]

@digama0 Did you want to make a PR out of this so there's somewhere to comment on it, or are you holding off for some reason?

I'm just providing it as a point of reference and a possible design. I trust you to make good use of it; I do not intend to force my opinion on this matter.