feat: Generalize type of step indices with metaprogramming and typeclasses

[markusdemedeiros]

This PR builds off of Alvin's work in #550, as well as Mario's work and my own attempt. I believe it solves every single problem reported with the prior attempts at this feature. The text here is long because I will try to explain how.

TL;DR:

• A strictly isolated typeclass restores the old outParam behaviors around local class inference.
• It does not violate the global typeclass rules for our unbundled algebraic hierarchy.
• A lightweight command elab guards against common errors.
• No duplicate or scoped notation needed and essentially no step index type annotations (the single exception is OFE.eq_dist: see limitations below).
• No bundling, automation is unchanged.
• Fully opt-in, hierarchy behaves normally when turned off. Working without default indices enabled allows multiple (non-overlapping) SIdx classes even in the same theorem.

In PR #550 I mentioned that having local scoped instances that could depend on section variables would solve all of our problems. This PR started by trying to emulate that, and morphed into something I think might make everybody 99%-100% happy.

Technique

The trick is to have a special typeclasss for default SIdx implementations, and let that provide the default instance for SIdx. Concretely, we start with the normal implicit index version of OFE (similar for COFE, OFunctor, etc)

@[rocq_alias ofe]
class OFE {SI : Type _} [SIdx SI] (α : Type _) where
  Dist : SI → α → α → Prop
  -- ... 

however, we add a second class for declaring default step index instances with an outParam index, and let it be the default instance for the step index type

class DefaultSI (SI : outParam (Type u)) where
  private mk ::
  sidx : SIdx SI

@[default_instance, reducible]
def dfltSIdx {SI : Type u} [d : DefaultSI SI] : SIdx SI := d.sidx

Initially I did this to put different defaults in different scopes (so we could emulate scoped default instances) but I ended up deciding that an elab was a better way to control it. To that end, the stepindex command puts an instance of the DefaultSI class in scope and does some sanity checks to ensure that it is the only one at elab time:

scoped stepindex Nat

Ordinal works in IrisMath too. Unlike hypothetical scoped default instances, the default index type can depend on section variables, so your type of step indices can be defined from any other Lean machinery. Here is how to generalize a section to use a generic type of step indices, such that the SIdx constraint on the type obeys normal typeclass synthesis rules:

variable {SI : Type _} [SIdx SI]
local stepindex SI

Hierarchy

Once a stepindex is declared, a DefaultSI instance is put in scope, so plain typeclass synthesis will handle filling in the SI type and the [SIdx SI] instances almost exactly like it would have in the outParam approach. However there are big improvements related to how stable this is. Synthesis of this arbitrary instance happens once, at the time the local stepindex command is elab'd, and in the happy path this instance will be synthesized using normal synthesis rules (ie. it will pick the [SIdx SI] instance for SI in the snippet above, not an arbitrary instance at every call site). Even if you get it wrong, and break the hierarchy in some other way, because synthesis happens only once this choice is guaranteed to be self-consistent for the rest of the section.

I've also used the module system to make declaring DefaultSI instances out of band difficult. It's not impossible, I don't think, but I think it is very hard to do by accident. Compare this to accidentally copy-pasting an open statement that includes a scope you didn't realize had a SIdx instance in it: the latter is much easier to get wrong. Setting a global step index type is also disabled.

Basic hierarchy discipline like avoiding non-definitional diamonds still applies of course, but it is no longer possible for an unrelated SIdx typeclass instance to break unrelated OFE synthesis. The stepindex command also has an option to provide an explicit instance name: I suspect this is unnecessary, but it gives you to turn off even the command elab-time nondeterminism if such a need arises. The final hierarchy thing I'll mention is that, unlike the outParam appraoches, the default step indices are fully opt-in. I can use OFE/COFE/OFunctor/... without interacting setting default step indices at all, and it behaves like any other two-parameter Lean typeclass. You can use multiple index types in the same theorem if you want. The stability of our algebraic hierarchy is preserved with or without default step indices set.

Notations

Because of the outParam, you get nearly every nicety of Alvin's original approaches, and adapting old code is nearly zero work. OFE does not need to specify its SI parameter, and step indices (even 0) do not need to specify their type. I also reused the stepindex% term elab from my other attempt: this elaborates to the current default step index type or a hole if none is set. However, unlike my prior approach, this is not used for any odd optParam stuff: it's used a total of three times so that we can have reuse the old notation and make it fill in the SI type at its elab site:

scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist n x y (SI := stepindex%)

Doing it this way avoids the need for the duplicate scoped notations as in Mario's version. I didn't even define notation for adding in the type SI because I think at this point it is not necessary.

Limitation

The only edge case I could not resolve was for eq_dist (and a few one-offs like it): this is an annoying combination of both not being a notation, and not referencing the step index type, so neither typeclass inference nor an optParam can be used to fill the type. Admittedly, the outParam version (nondetermistically) fills this in at every call site where mind doesn't.

In this PR I explicitly fixed each SI instance be Nat or SI as at each call site so that the Lean code looks normal. I could have also defined eq_dist' to be eq_dist fixing (SI := stepindex%) with an optParam and it would be uniform across the repo. I'm open to any solutions to this problem.

Conclusion

I hope this version meets everybody's requirements! I think this solution is more than the sum of its parts, and cards on the table, I'm very pleased with it. To me it feels quite inline with other Lean features. I look forward to your feedback :)

cc: @alvinylt @MackieLoeffel @Kaptch @digama0

[markusdemedeiros]

Not for nothing: a similar design might be capable of removing the \vdash@{IProp GF} annotations as well. Happy to prototype this if people find the idea acceptable.