feat: OFE step-indexing parametrisation using metaprogramming instead of an outParam step index type

[markusdemedeiros]

This PR fixes my concerns with PR #550.

Problem

#550 introduces the SIdx typeclass and adds it as a constraint to OFE. However, because the notation conerning OFE typically does not include explicit step indices, the elaborator cannot determine the type of indices.

In an attempt to fix this #550 makes the type of indices an outParam of OFE. Hierarchies of this type are not well-behaved. The documentation around outParam says this explicitly: outParams must be uniquely determined by the non-outParam types, because the type inference algorithm will pick outParam types arbitrarily.

With this kind of atypical hierarchy, type inference around the SIdx class must be tightly controlled via scoped instances. A single incorrectly scoped instance can violate the guarantee that the elaborator picks consistent SI types. This leads to errors in invisible code that are hard to identify and can require the same annotations that the original PR is trying to avoid. Unlike some more customized parts of Iris-Lean such as the proofmode (where the typeclasses are mainly used by a custom search), the Algebra/ folder is expected to behave like normal Lean code with a well-behaved system of typeclasses.

The proposed in the comments of #550 all have problems:
A) They lose generality (the parametric approach), or
B) They do not address the issue where an unrelated type is marked as an outParam, or
C) They introduce bundled layer at the bottom of the hierarchy, worsening automation and requiring explicit change or simp steps to modify step indices that are concrete types such as Nat or Ordinal.

These proposals all try to solve the notation problem by changing the algebraic hierarchy. The algebraic hierarchy of Iris-Lean is one of the primary ways where it is different from Iris-Rocq. Porting Iris in such a way that the algebraic hierarchy is stable is especially important to me in particular: while I don't think the problems introduced in #550 are the same as the ones which drove me from Iris-Rocq, some of the propsed solutions (unification hints, a mixed bundled/unbundled hierarchy....) have some similarities.

Solution

This PR fixes the notation issues with metaprogramming, as it ought to. In particular, I implemented a new enviornment extension for storing the current type of step indices, and an elab for returning it. With this, the SI fields can be specified using an autoParam or optParam that queries the enviornment.

The approach gives you the same programming idioms that were asked for in the comments of 550: you are able to declare the default type of step indices locally or per-scope. Many of the files here are fixed to Nat as in 550, but some set the default step index to be a section variable. Global defaults are intentionally disabled for stability. The setp index type type can be locally overridden within a definition by specifying (SI := ...) and extra notation is added for the cases where this is required. There is less notation than you would expect. Unlike 550, this PR retains the ability to write [OFE A].

However, the main advantage of this is that the algebraic hierarchy remains well-behaved. This fact alone would be worth annotating every single step index instance, because a stable hierarchy that does not introduce invisible problems or break between Lean versions is worth more than some annotation cost (that we're not even sure applies to anyone except Iris-Lean developers).

Limitations

Some annotations are not removed, however this approach also removes some annotations that #550 does not. OFunctors need to be annotated with their index type. autoParam has some limitations (eg. they cannot be implicit) so if we like keeping the [OFE A] syntax instead of [OFE SI A] then the step index type has to be the last parameter. I will highlight that #550 loses this abbreviated syntax.

Feedback is welcome!

AI Use

I used Claude to help with the metaprogramming and bulk edits of code. I was watching it closely while working on the PR but I have not examined the complete diff to the normal extent yet--I will self-review only to catch any problems. I will also work on eliminating the remaining SI annotations where possible. Claude reports a the ballpark of 130 explicit annotations across the repo.

[markusdemedeiros]

@alvinylt I can't request you as a reviewer but if you could look it over I think that would be great

[alvinylt]

Thanks for the suggested improvement! I will have a look into it.

[srghma]

No need to add here?

[MackieLoeffel]

Thanks for making a PR with what you have in mind. I had not considered this idea of using meta programming. However, I have to say that I am not fully sure what this solution achieves compared to the outParam version. It introduces quite a bit of complexity with the new meta programming commands that users maybe have to add to their definitions somewhere and they only seem to work in like 70% of the cases so some manual annotations are still necessary.

It seems like our difference are due to whether one thinks having a singleton typeclass is a problem or is fine. Your main worry seems to be:

A single incorrectly scoped instance can violate the guarantee that the elaborator picks consistent SI types.

Which is true, but this seems like a easy thing to avoid? We can probably even make it an error with meta programming if one accidentally imports multiple instances, so one would notice immediately.
Especially if all transfinite instances are in IrisMath, most users of Iris don't even have multiple instances available that they could import incorrectly. Maybe it would help to be more concrete about the situation you are worried about? How would an incorrectly scoped instance arise?

[markusdemedeiros]

It introduces quite a bit of complexity with the new meta programming commands that users maybe have to add to their definitions somewhere and they only seem to work in like 70% of the cases so some manual annotations are still necessary.

I adapted the repository to use the metaprogramming but it is not necessary to declare a stepindex. You can use OFE without declaring anything and it will behave just like a normal two-parameter typeclass. The metaprogramming is there strictly to appease your (correct) concerns about introducing an overwhelming amount of new notation.

As for the complexity: it is 22 lines of meta code that covers the vast majority of notation overhead, and re-establishes an important stability property about nearly every typeclass in our repository. Forgetting this PR: if this point is not convincing to you then I can't see us reaching consensus.

Which is true, but this seems like a easy thing to avoid?

If you wish to study any kind of closure construction you will require at least two instances in your context.

inductive TwoLevel (SI : Type _) where | L0 (SI : α) |  L1 (a : SI)
instance [SIdx SI] : SIdx (TwoLevel SI) := ...

This is not exercised by PR #550.

However my main justification is broader. Even if you claim that nobody would care about these kinds of examples, the rules of outParam explicitly mark #550's use as being out of spec. Neither you nor I know what implications that could have in the future and unlike your ProofMode we do not control regular typeclass inference. When I write Mathlib code I freely assume that unrelated class instances in the same context are safe. Under #550 that assumption stops being valid for Iris-Lean projects. This is a mistake.

I understand that we can do crazy things with typeclasses in ProofMode world, but for the core theory it is strongly preferable that we adhere to the same standard that all the other libraries do. We should do this even if that comes at a perceived cost when compared to Rocq: we shouldn't forget that we are in a different proof assistant and that might mean we need to adjust our expectations to match. In the Eileen project I tried a number of hierarchy alternatives and I came to the conclusion that following Mathlib's norms (which were essentially co-designed with Lean itself) is the right way forward. Mario's initial work on the hierarchy here, which I later expanded upon, has been consistently following that line of thought.

[MackieLoeffel]

From the discussion with @markusdemedeiros, @Kaptch, and @alvinylt (among other), the next steps of this PR would be to see if a term elab can be used to avoid all outParams and optParams and autoParams while also not introducing any new notation and reduce the manual annotations necessary. (see #550 (comment))

[markusdemedeiros]

I'm closing this in favour of #576