[Merged by Bors] - refactor: don't use lambdas in `CoeFun` instances by YaelDillies · Pull Request #21405 · leanprover-community/mathlib4

YaelDillies · 2025-02-04T07:38:53Z

Hiding the lambdas behind a non-reducible toFun or changing the CoeFun instance to FunLike prevents many lemmas (some simp) to have a lambda as their head symbol.

Arguably, those were misports because Lean 3's has_coe_to_fun was not reducible. Whether or not those should have become FunLike or CoeFun := ⟨semireducibleDef⟩ back then is unclear.

Zulip

github-actions · 2025-02-04T07:39:51Z

PR summary cc3c6e85a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ apply_def
+ apply_ne_top
+ instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (adicCompletion K)
+ instance : FunLike (Content G) (Compacts G) ℝ≥0∞
+ mk_apply
+ opensHom.instFunLike
+ opensNhds.instFunLike
+ toFun_eq_toNNReal_apply
++ apply_mk
++ coe_id
++ comp_apply
++ id_apply
++ val_apply
- instance : CoeFun (Content G) fun _ => Compacts G → ℝ≥0∞
- instance : CoeFun (FiniteAdeleRing R K)
- opensHomHasCoeToFun
- opensNhdsHomHasCoeToFun

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 script/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).

adomani · 2025-02-04T07:49:56Z

!bench

adomani · 2025-02-04T07:58:32Z

Oops, I did not realise that this was still in progress!

adomani · 2025-02-04T08:13:58Z

I wish we had a bench-after-CI automation!

YaelDillies · 2025-02-04T08:15:12Z

Be the automation you want to see 😇

YaelDillies · 2025-02-04T08:21:17Z

I think I got them all!

leanprover-bot · 2025-02-04T08:31:51Z

Here are the benchmark results for commit c62aed9.
There were no significant changes against commit e13a712.

github-actions · 2025-02-04T08:32:25Z

File	Instructions	%
`lint`	-18.118⬝10⁹	(-0.23%)
CI run

adomani · 2025-02-04T19:14:45Z

!bench

leanprover-bot · 2025-02-04T19:45:43Z

Here are the benchmark results for commit f0e206e.
There were no significant changes against commit e13a712.

github-actions · 2025-02-04T19:46:06Z

File	Instructions	%
`build`	-4.808⬝10⁹	(+0.00%)
`lint`	-92.666⬝10⁹	(-1.21%)
`Mathlib.AlgebraicGeometry.Modules.Tilde`	+3.281⬝10⁹	(+2.47%)

2 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Category.TopCat.Opens`	+2.964⬝10⁹	(+5.60%)
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf`	+2.432⬝10⁹	(+3.15%)

File	Instructions	%
`Mathlib.MeasureTheory.Measure.Content`	+1.208⬝10⁹	(+6.32%)
`Mathlib.Topology.Sheaves.Sheafify`	-1.408⬝10⁹	(-18.21%)
`Mathlib.Analysis.InnerProductSpace.l2Space`	-5.57⬝10⁹	(-5.27%)
`Mathlib.AlgebraicGeometry.StructureSheaf`	-9.798⬝10⁹	(-5.98%)
CI run

YaelDillies · 2025-02-04T19:54:41Z

Wow! -1.21% on linting

eric-wieser · 2025-02-05T00:05:32Z

Mathlib/Analysis/InnerProductSpace/l2Space.lean

 /-- `b i` is the `i`th basis vector. -/
-instance instCoeFun : CoeFun (HilbertBasis ι 𝕜 E) fun _ => ι → E where
-  coe b i := b.repr.symm (lp.single 2 i (1 : 𝕜))
+@[coe] def toFun (b : HilbertBasis ι 𝕜 E) (i : ι) : E := b.repr.symm <| lp.single 2 i (1 : 𝕜)


Just to not lose it from the other PR; this one should be adjusted to use FunLike, which needs the proofs in #21440 and probably the API in #21444

I've reverted this. Changes were in commit 712d7f6

Sorry, which "other PR" does this refer to?

"other PR" refers to comments in #21395 on lines that were moved to this PR.

Vierkantor · 2025-02-11T12:05:02Z

It looks like this was misported.

This refers to the original PR, which has grown a bit. Could you make sure it is still up to date?

Vierkantor

bors d+

mathlib-bors · 2025-02-11T12:05:11Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

YaelDillies · 2025-02-11T12:44:08Z

bors merge

Hiding the lambdas behind a non-reducible `toFun` or changing the `CoeFun` instance to `FunLike` prevents many lemmas (some simp) to have a lambda as their head symbol. Arguably, those were misports because Lean 3's `has_coe_to_fun` was not reducible. Whether or not those should have become `FunLike` or `CoeFun := ⟨semireducibleDef⟩` back then is unclear. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bad.20simp.20discrimination.20tree.20keys)

mathlib-bors · 2025-02-11T13:04:06Z

Build failed (retrying...):

Build

Hiding the lambdas behind a non-reducible `toFun` or changing the `CoeFun` instance to `FunLike` prevents many lemmas (some simp) to have a lambda as their head symbol. Arguably, those were misports because Lean 3's `has_coe_to_fun` was not reducible. Whether or not those should have become `FunLike` or `CoeFun := ⟨semireducibleDef⟩` back then is unclear. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bad.20simp.20discrimination.20tree.20keys)

mathlib-bors · 2025-02-11T13:23:52Z

Build failed (retrying...):

Build

Hiding the lambdas behind a non-reducible `toFun` or changing the `CoeFun` instance to `FunLike` prevents many lemmas (some simp) to have a lambda as their head symbol. Arguably, those were misports because Lean 3's `has_coe_to_fun` was not reducible. Whether or not those should have become `FunLike` or `CoeFun := ⟨semireducibleDef⟩` back then is unclear. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bad.20simp.20discrimination.20tree.20keys)

mathlib-bors · 2025-02-11T13:31:33Z

Build failed:

Build

sgouezel · 2025-02-11T13:45:00Z

bors r-
Can you merge master and fix the build?
bors d+

mathlib-bors · 2025-02-11T13:45:03Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

It looks like this was misported.

ghost · 2025-02-11T14:19:15Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

Hiding the lambdas behind a non-reducible `toFun` or changing the `CoeFun` instance to `FunLike` prevents many lemmas (some simp) to have a lambda as their head symbol. Arguably, those were misports because Lean 3's `has_coe_to_fun` was not reducible. Whether or not those should have become `FunLike` or `CoeFun := ⟨semireducibleDef⟩` back then is unclear. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bad.20simp.20discrimination.20tree.20keys)

mathlib-bors · 2025-02-11T14:48:42Z

This PR was included in a batch that was canceled, it will be automatically retried

Hiding the lambdas behind a non-reducible `toFun` or changing the `CoeFun` instance to `FunLike` prevents many lemmas (some simp) to have a lambda as their head symbol. Arguably, those were misports because Lean 3's `has_coe_to_fun` was not reducible. Whether or not those should have become `FunLike` or `CoeFun := ⟨semireducibleDef⟩` back then is unclear. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bad.20simp.20discrimination.20tree.20keys)

mathlib-bors · 2025-02-11T16:19:56Z

Pull request successfully merged into master.

Build succeeded:

github-actions bot added the t-combinatorics Combinatorics label Feb 4, 2025

YaelDillies mentioned this pull request Feb 4, 2025

[Merged by Bors] - chore: remove @[simp] when the discr_key is a lambda #21395

Closed

YaelDillies changed the title ~~refactor: use Line.toFun in the CoeFun instance~~ refactor: don't use lambdas in CoeFun instances Feb 4, 2025

eric-wieser reviewed Feb 5, 2025

View reviewed changes

YaelDillies force-pushed the hales_jewett_no_head_lambda branch from f0e206e to e3b2d1f Compare February 5, 2025 08:58

YaelDillies removed the t-combinatorics Combinatorics label Feb 11, 2025

YaelDillies requested a review from Vierkantor February 11, 2025 11:41

Vierkantor approved these changes Feb 11, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 11, 2025

ghost removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 11, 2025

YaelDillies added 5 commits February 11, 2025 13:46

refactor: use Line.toFun in the CoeFun instance

09ec2ef

It looks like this was misported.

content

0a9578a

finite adele ring

2c21c51

open nhds

e8f4ae7

fix

cc3c6e8

YaelDillies force-pushed the hales_jewett_no_head_lambda branch from e3b2d1f to cc3c6e8 Compare February 11, 2025 14:05

YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Feb 11, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Feb 11, 2025

mathlib-bors bot changed the title ~~refactor: don't use lambdas in CoeFun instances~~ [Merged by Bors] - refactor: don't use lambdas in CoeFun instances Feb 11, 2025

mathlib-bors bot closed this Feb 11, 2025

mathlib-bors bot deleted the hales_jewett_no_head_lambda branch February 11, 2025 16:20

Conversation

YaelDillies commented Feb 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cc3c6e85a0

Import changes for modified files

Declarations diff

Uh oh!

adomani commented Feb 4, 2025

Uh oh!

adomani commented Feb 4, 2025

Uh oh!

adomani commented Feb 4, 2025

Uh oh!

YaelDillies commented Feb 4, 2025

Uh oh!

YaelDillies commented Feb 4, 2025

Uh oh!

leanprover-bot commented Feb 4, 2025

Uh oh!

github-actions bot commented Feb 4, 2025

Uh oh!

adomani commented Feb 4, 2025

Uh oh!

leanprover-bot commented Feb 4, 2025

Uh oh!

github-actions bot commented Feb 4, 2025

Uh oh!

YaelDillies commented Feb 4, 2025

Uh oh!

eric-wieser Feb 5, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 5, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Feb 11, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Feb 11, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor commented Feb 11, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

YaelDillies commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

sgouezel commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

ghost commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

YaelDillies commented Feb 4, 2025 •

edited

Loading

github-actions bot commented Feb 4, 2025 •

edited

Loading