-
Notifications
You must be signed in to change notification settings - Fork 93
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: upstream @[simps] attribute #347
base: main
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't have bandwidth for a full review this week, but I added a couple notes.
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Std/Tactic/Simps/Basic.lean
Outdated
def updateName (nm : Name) (s : String) (isPrefix : Bool) : Name := | ||
nm.updateLast fun s' => if isPrefix then s ++ "_" ++ s' else s' ++ "_" ++ s | ||
|
||
-- move |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What should be moved?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've made updateName
private, as it is idiosyncratic to simps
, and moved the mkSimpContext
material to Std/Lean/Meta/Simp.lean
, and made a note there about the duplication occurring.
/-- Find the indices of the projections that need to be applied to elaborate `$e.$projName`. | ||
Example: If `e : α ≃+ β` and ``projName = `invFun`` then this returns `[0, 1]`, because the first | ||
projection of `MulEquiv` is `toEquiv` and the second projection of `Equiv` is `invFun`. -/ | ||
def findProjectionIndices (strName projName : Name) : MetaM (List Nat) := do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Comment example is from Mathlib and uses e
instead of strName
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've clarified the comment to explain the use of e
. It's still in terms of Mathlib. (This is a bigger overhaul: there are lots of Mathlib specific examples in this file --- Equiv
isn't even defined in Std.)
let allProjs := pathToField ++ [fullProjName] | ||
return allProjs.map (env.getProjectionFnInfo? · |>.get!.i) | ||
|
||
/-- Auxiliary function of `getCompositeOfProjections`. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could more detail be added either here to body of code?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@fpvandoorn, could I perhaps interest you in this? :-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added a few comments in the code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, I don't have push access to this repo. Can I get access, or shall I make a PR into this PR?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@fpvandoorn, for now, would you mind a PR to the PR? Really I should have made this PR from a fork so I could have given you access myself.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
|
||
This is very similar to `expr.substs`, but this also reduces head let-expressions. -/ | ||
partial def _root_.Lean.Expr.instantiateLambdasOrApps (es : Array Expr) (e : Expr) : Expr := | ||
e.betaRev es.reverse true -- check if this is what I want |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Comment seems fishy and this should either be moved to Std/Lean/Expr.lean
or renamed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I never tested whether this function satisfies the docstring exactly, and it doesn't do the second half of Also reduces head let-expressions in `e`, including those after instantiating all lambdas.
In leanprover-community/mathlib4@master...simps_upstream_tests I tried to see if doing that breaks anything in Mathlib. I expect not, given the low number of let
expressions in definitions.
We can also keep the current functionality. It would be nice if Lean.Expr.beta
supports the optional flags of Lean.Expr.betaRev
, then this function doesn't need to exist.
""}even if the definition is a constructor application. For example, if you give a { | ||
""}`MulEquiv` by giving the corresponding `Equiv` and the proof that it respects { | ||
""}multiplication, then you need to mark it as `@[simps!]`, since the attribute needs to { | ||
""}unfold the corresponding `Equiv` to get to the `toFun` field." |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd love to see this function and the one above broken up into smaller entities with comments about what they do.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, this code is not pretty, since I wrote it in Lean 3, and then ported it to Lean 4 keeping the Lean 3 structure. I think the proper way to make this code better is to make use of monad extensions with a state and context, instead of these functions that take ~10 arguments. That makes it also much easier to split off small sub-functions.
I don't have time for that refactor at the moment.
It is a bit tricky to break up this function in the current state, since there are recursive calls in multiple places.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks.
While it would be really nice to get @[simps]
into Std, it is not essential: users can always write the boilerplate by hand!
I propose that we shop this project around a bit, and see if anyone on zulip might be interested in taking on a refactor?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds good to me
No description provided.