[Merged by Bors] - feat: support and improve notation_class in simps #2883
Conversation
fpvandoorn
added
awaiting-review
fpvandoorn
added
awaiting-author
fpvandoorn
added
awaiting-review
| an applicable name. (e.g. `Iso.inv`) | ||
|
|
||
| Implementation note: getting rid of TermElabM is tricky, since `Expr.mkAppOptM` doesn't allow to | ||
| keep metavariables around, which are necessary for `OutParam`. -/ |
There was a problem hiding this comment.
I won't suggest that you change this, but since we last talked about it I realized that it's possible to do a pattern where you create new FVars rather than metavariables, use mkAppOptM and friends, and then at the end substitute those FVars for metavariables. You could probably set up a nice combinator for this, a variant of withLocalDecl.
By the way, I'm using elabAppArgs in apply_fun (see this block). It's much more powerful than using mkAppOptM since it is the function application elaborator.
| catch ex => | ||
| trace[simps.debug] "Projection doesn't have the right type for the automatic projection:\n{ | ||
| ex.toMessageData}" | ||
| return none |
There was a problem hiding this comment.
Might there be any instances that need solving in eInstType before synthInstance? You might insert Lean.Elab.Term.synthesizeSyntheticMVars here.
There was a problem hiding this comment.
It seems incredibly unlikely, since the classes that will be used here are notation classes like Mul and HasSubset, and those shouldn't have other type-class arguments. And if there are, I probably need to change more, because I made all meta variables using mkFreshExprMVar, and I probably need to make some of them synthetic, if I wanted to support this case (which I probably don't want to).
|
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
semorrison
added
delegated
and removed
awaiting-review
|
bors merge |
* If you write `@[simps]` for the definition of an `AddGroup`, it will now generate the correct lemmas for `0`, `+`, `nsmul` and `zsmul` using `OfNat` and heterogenous operations. This is needed for #2609. * This is a lot more flexible than the Lean 3 implementation, in order to handle `nsmul`, `zsmul` and numerals. * It doesn't handle the `zpow` and `npow` projections, since their argument order is different than that of `HPow.pow` (that was likely done for the sake of `to_additive`, but we can consider to revisit that choice). * Also fixes the `nvMonoid` bug encountered in #2609 * There was an issue where the wrong projection was chosen, since `toDiv` is a prefix of `toDivInvMonoid` * Before we were checking if `_toDiv` is a prefix of your projection with `_` prepended (e.g. `_toDivInvMonoid`), now we are checking whether `toDiv_` is a prefix of your projection with `_` appended (which doesn't match `toDivInvMonoid_`).
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
- [x] depends on: #2883 Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@[simps]for the definition of anAddGroup, it will now generate the correct lemmas for0,+,nsmulandzsmulusingOfNatand heterogenous operations. This is needed for [Merged by Bors] - feat: port CategoryTheory.Groupoid.VertexGroup #2609.nsmul,zsmuland numerals.zpowandnpowprojections, since their argument order is different than that ofHPow.pow(that was likely done for the sake ofto_additive, but we can consider to revisit that choice).nvMonoidbug encountered in [Merged by Bors] - feat: port CategoryTheory.Groupoid.VertexGroup #2609toDivis a prefix oftoDivInvMonoid_toDivis a prefix of your projection with_prepended (e.g._toDivInvMonoid), now we are checking whethertoDiv_is a prefix of your projection with_appended (which doesn't matchtoDivInvMonoid_).A potential better implementation to this is to have a custom simp-set that simplifies standard projections to the desired custom projections (suggested by Kyle).