[Merged by Bors] - feat: deprecate Expr.isConstantApplication

[JovanGerb]

The function Expr.isConstantApplication does its de bruijn index managenent incorrectly, so this PR deprecates it. It was added in #1861. It should have used de bruijn index 0, but it actually used de bruijn index n - 2. This means that it would works correctly for the number of arguments being at most 2.

This PR removes the call to Expr.isConstantApplication used by to_additive, which is not needed anymore. It turns out that the check is simply not necessary.

---

[github-actions]

PR summary 37d2101b79

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## 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 scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

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

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joneugster]

LGTM, thanks!

How do we see that

[...] we don't treat (fun x => α) (n + 1) as a type that depends on Nat

?

Is there an test/example/anything which illustrates this is working as intended without the check?

maintainer merge

[github-actions]

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

[grunweg]

Can you fix the test failures, please? Thanks!

[JovanGerb]

(I've added some more details to the PR description. The function was working as intended for the most common cases, but as can be seen from this PR, the check is not necessary. I can't tell whether it was never necessary, or if some improvements have been made to Lean in the meantime that have made it unnecessary. I'll fix the test tomorrow)

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for e08549f against 37d2101 are in! @JovanGerb

• ✅ build//instructions: -20.8G (-0.01%)

No significant changes detected.

[Vierkantor]

I agree with @joneugster that it's not obvious why this check is no longer needed, and I'd like to see a test case.

[JovanGerb]

What sort of test case would you like? I claim that this is simply not relevant, because it doesn't come up in practice.

[JovanGerb]

The relevant history is that this particular test was added at some point early in the port, in order to fix a basic use case. However, since CI is green on this PR, the check isn't necessary anymore.

[Vierkantor]

Okay, looking at the history in detail, commit f0a4e27e added the test case myFin.foo alongside the isConstantFun check. So that answers my question: myFin.foo is this test case.

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-CI job