feat: Generalize type of step indices with metaprogramming and typeclasses - #576
feat: Generalize type of step indices with metaprogramming and typeclasses #576markusdemedeiros wants to merge 42 commits into
Conversation
… for `Nat` in `StepIndexFinite.lean`
…stances not yet complete
Replace all proofs in section `Fixpoint`, all requires rewrite
…and `Contractive.succ`
Parametrisation of `CMRA` to be done in a future PR
…nt with `SI = Nat`
|
Not for nothing: a similar design might be capable of removing the |
MackieLoeffel
left a comment
MackieLoeffel
left a comment
There was a problem hiding this comment.
Thank you for working on this! I think this design looks great and solves all the problems. I like the idea of the DefaultSIdx typeclass with the default instance. We can indeed explore if we want to use a similar design for other cases. I left some small comments (partly also for @alvinylt, who wrote the original version). I also hope to have a look that is a bit deeper later to see if we can clean up things a bit more, but overall this looks great.
Thanks again for all your work on this! It took a bit of time, but in the end we now have a great solution that addresses all problems, which I think is very nice.
|
Nice! I've taken a look, and for me it was a matter of just rebasing and fixing a few annotations on top of this PR. |
|
|
||
| namespace DFracAgree | ||
|
|
||
| local stepindex Nat |
There was a problem hiding this comment.
It is a bit unclear for me where to put these local stepindex Nat commands in a file. It seems the clearest version for me would be to put the local stepindex Nat command at the top of the file directly after the imports. Then it is clear that it applies to the whole file and not just some namespace or so. What do you think about this?
There was a problem hiding this comment.
The stepindex command follows the scoping rules (in the literal sense: the local translates to a local instance of the DefaultSIdx typeclass). So, as written here it does just apply until end DFracAgree, but it also works to move it right after the imports and it will apply to the whole file.
Which would you prefer? The only hard constraint is that for generic SI, the stepindex annotation has to come after the section variable.
| compl c := by | ||
| refine ⟨fun k => compl ⟨fun i => c.1 i k, fun h => c.cauchy h k⟩, ?_⟩ | ||
| refine OFE.eq_dist.mpr (fun n => ?_) | ||
| refine (OFE.eq_dist (SI := Nat)).mpr (fun n => ?_) |
There was a problem hiding this comment.
I was not able to figure out, why eq_dist needs a type annotation, but basically nothing else needs it. Does anyone have an idea why?
There was a problem hiding this comment.
It seems to be because SIdx is not an instance parameter for eq_distandDist`. Not sure how to fix this. Maybe something like the following helps?
@[rocq_alias ofe]
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
/-- Thin abbreviation for `OFE (SI := SI) α`. -/
class abbrev IOFE (SI : Type _) [SIdx SI] (α : Type _) := OFE (SI := SI) α
abbrev OFE.Dist {SI} [SIdx SI] {α} [self : IOFE SI α] : SI → α → α → Prop :=
OFE.Dist'
abbrev OFE.eq_dist {SI} [SIdx SI] {α} [self : IOFE SI α] {x y : α} :
x = y ↔ ∀ n, OFE.Dist (SI:=SI) n x y := OFE.eq_dist'
Not sure if there is another way to change the status of implicit parameters.
There was a problem hiding this comment.
This looks to be promising! I will propagate it throughout the rest of the PR and remove those annotations :)
There was a problem hiding this comment.
Hm. It doesn't work in all cases, sadly. I can get the annotation to be OFE.eq_dist _ using an autoParam (this version at least doesn't have to change when the local stepindex type gets generalized) but the underscore can't be removed without implicit autoparams, which are not planned.
I'll commit this work once my agent finishes propagating the changes but I could take it or leave it.
/-- Ordered family of equivalences -/
@[rocq_alias ofe]
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
/-- Thin abbreviation for `OFE (SI := SI) α`. -/
class abbrev IOFE (SI : Type _) [SIdx SI] (α : Type _) := OFE (SI := SI) α
open OFE
scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist n x y (SI := stepindex%)
abbrev OFE.eq_dist (SI := by infer_stepindex) [SIdx SI] {α} [self : IOFE SI α] {x y : α} :
x = y ↔ ∀ n, OFE.Dist (SI:=SI) n x y := OFE.eq_dist'
There was a problem hiding this comment.
Even this does't get rid of all annotations, sadly. Latest commit still fixes a couple of them to Nat.
This version is still less characters (it is clear form the type that you must supply the step index type somehow, as it is not marked implicit) but if we wanted to disable the autoparam altogether for consistency I think that would be fine too.
|
!bench |
|
Benchmark results for f68356e against 69dee49 are in. There are significant results. @MackieLoeffel
Large changes (5🟥)
Medium changes (17🟥)
Small changes (2✅, 32🟥)
|
|
Seems like there is some performance hit from this change. This was expected since Rocq had a similar performance hit (if not worse) for the corresponding PR. Not sure if there is something we can do about this. |
|
My best guess as to any unnecessary negative perf would be the additional typeclasses not being private to the modules. Let me try making them |
|
Ah right, that prevents |
|
@MackieLoeffel Do you think the performance should be a blocker for this? |
|
No, I don't think the performance should be a blocker for this. If there is some easy win, we can go for it, but otherwise I think the performance regression is fine. We don't focus much on performance at the moment and if someone has a more efficient implementation of this in the future, we can still improve it. |
5 participants
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:
outParambehaviors around local class inference.OFE.eq_dist: see limitations below).SIdxclasses 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
SIdximplementations, and let that provide the default instance forSIdx. Concretely, we start with the normal implicit index version of OFE (similar for COFE, OFunctor, etc)however, we add a second class for declaring default step index instances with an
outParamindex, and let it be the default instance for the step index typeInitially 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
stepindexcommand puts an instance of theDefaultSIclass in scope and does some sanity checks to ensure that it is the only one at elab time:scoped stepindex NatOrdinal 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
SIdxconstraint on the type obeys normal typeclass synthesis rules:Hierarchy
Once a
stepindexis declared, aDefaultSIinstance is put in scope, so plain typeclass synthesis will handle filling in theSItype and the[SIdx SI]instances almost exactly like it would have in theoutParamapproach. However there are big improvements related to how stable this is. Synthesis of this arbitrary instance happens once, at the time thelocal stepindexcommand 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 forSIin 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
DefaultSIinstances 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 anopenstatement that includes a scope you didn't realize had aSIdxinstance 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
SIdxtypeclass instance to break unrelatedOFEsynthesis. Thestepindexcommand 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 theoutParamappraoches, the default step indices are fully opt-in. I can useOFE/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.OFEdoes not need to specify itsSIparameter, and step indices (even0) do not need to specify their type. I also reused thestepindex%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 oddoptParamstuff: it's used a total of three times so that we can have reuse the old notation and make it fill in theSItype at its elab site: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
SIbecause 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 anoptParamcan be used to fill the type. Admittedly, theoutParamversion (nondetermistically) fills this in at every call site where mind doesn't.In this PR I explicitly fixed each
SIinstance beNatorSIas at each call site so that the Lean code looks normal. I could have also definedeq_dist'to beeq_distfixing(SI := stepindex%)with anoptParamand 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