PR summary 13a1b47278

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ totalSpaceMk

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

./scripts/technical-debt-metrics.sh pr_summary

Thanks for the comments! I'm aware it's a bit hard to judge if these changes are useful.

This question ("should T% beta-reduce") came up in direct conversation with Floris (fpvandoorn). An instance where I might have hit this is in #30357 in SmoothSection.lean: if I want to use the T% elaborator in ContMDiffWithinAt.sum_section_of_locallyFinite, for example (and I do, because it's much easier to read), the lemma statement changes slightly.

Running dsimp at the start of the proof makes it work again: otherwise, the subsequent rw fails.

I tested this after this PR; I remember seeing these kind of error a lot of times when trying this without #30879. I can re-test (tomorrow perhaps) in SmoothSection on top of just #30413, to see if this PR actually makes a difference.

The general theme is: I have a function fun x \map TotalSpace.mk' F x (some slightly more complicated expression using x), and want to write this using T%. If I wrote T% (fun x \maps <complicated expression>), this sometimes yields a defeq, but not syntactically equal expression.
was e.g. sum finsum, sum or infinite sum; SmoothSection has examples.

Ah, okay, I think I see...does this mean we want to head-beta-reduce e.app x instead of just e?

This PR/issue depends on:

• [Merged by Bors] - feat: further extensions of the differential geometry elaborators #30413
  By Dependent Issues (🤖). Happy coding!

I just tested with the current state of this PR: all the need for dsimp is gone; it seems head-beta reducing e.app x was exactly the right call 🎉

Thanks for the careful review, yet again. I've revamped the PR title and PR description - this is ready for another look.

Awesome! Looks ready to me! :)

maintainer merge

🚀 Pull request has been placed on the maintainer queue by thorimur.

This PR currently makes the change that T% σ x is not elaborated as an element of the total space anymore. This is undesirable. L66-68 of the test file should be:

/-- info: TotalSpace.mk' F x (σ x) : TotalSpace F V -/
#guard_msgs in
#check T% σ x

Changes needed:

• T% should try to read 2 arguments ahead, if they exist (probably at precedence arg)
• Then, after elaborating T% σ, we should apply it to x, and head-beta-reduce once more.

This PR currently makes the change that T% σ x is not elaborated as an element of the total space anymore. This is undesirable. L66-68 of the test file should be:

/-- info: TotalSpace.mk' F x (σ x) : TotalSpace F V -/
#guard_msgs in
#check T% σ x

Changes needed:

* `T%` should try to read 2 arguments ahead, if they exist (probably at precedence `arg`)

* Then, after elaborating `T% σ`, we should apply it to `x`, and head-beta-reduce once more.

The only change this PR actually makes to this example is a parsing change: T% σ x is now parsed as T% (σ x) instead of (T% σ) x. On master, T% (σ x) becomes σ x : V x and (T% σ) x becomes (fun x ↦ TotalSpace.mk' F x (σ x)) x : TotalSpace F V. This PR doesn't actually affect beta reduction in either of these cases, only parsing for the unparenthesized T% σ x.

I don't think it's been the case (yet!) that T% elaborates points to points in the corresponding total space, but I think this would be neat! It would be a separate feature and thus separate PR, though. I believe we're better set up to handle that case if we handle things at the term level instead of parsing multiple args: then we can destructure into σ and x at the expression level.

There could be a separate point here about enforcing parentheses—maybe we expect T% σ x to parse as (T% σ) x always, and parsing a whole term is unexpected? We could still make points into elements of the total space in the way you'd like when parsing a single arg with T% (σ x), and maybe that would be clearer? Haven't thought about this. (This is a (somewhat) separate question, though.)

If you think this explanation is reasonable, I'd still recommend merging as-is, but I'll refrain from over-eagerly modifying labels here while still in conversation. 😁

I have reverted the precendence change from this PR: indeed, this should arguably be a separate PR. This PR is only about applying head-beta reduction. I have also updated the tests accordingly. I believe this addresses all your comments, Floris.

Ok, this change seems fine by itself, so let's merge it. The reason I asked for head-beta reducing the whole application, is because that is how I interpret this sentence of the PR description:

Whenever the T% elaborator succeeds, head beta reduce the resulting application.

But sure, let's do that in a later PR if desired.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build