[Merged by Bors] - perf(FunLike.Basic): beta reduce `CoeFun.coe` by astrainfinita · Pull Request #7905 · leanprover-community/mathlib4

astrainfinita · 2023-10-24T20:09:26Z

This eliminates (fun a ↦ β) α in the type when applying a FunLike.

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Not sure about the name.

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Not sure about the name. I'd like to see if it's much better than #7905.

astrainfinita · 2023-10-26T05:19:17Z

!bench

leanprover-bot · 2023-10-26T06:04:30Z

Here are the benchmark results for commit 4d6319b.
There were significant changes against commit bf077b1:

  Benchmark                                                    Metric             Change
  ======================================================================================
+ build                                                        linting             -6.2%
+ build                                                        tactic execution    -5.1%
+ lint                                                         instructions        -6.1%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings            instructions        -8.5%
+ ~Mathlib.Algebra.Category.Ring.Constructions                 instructions       -38.4%
+ ~Mathlib.Algebra.DirectLimit                                 instructions       -19.6%
+ ~Mathlib.Algebra.Homology.ModuleCat                          instructions       -32.2%
+ ~Mathlib.Algebra.Jordan.Basic                                instructions        -5.9%
+ ~Mathlib.Algebra.Lie.Weights.Basic                           instructions       -12.6%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point               instructions        -4.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated          instructions       -19.6%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties       instructions        -7.1%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme         instructions        -7.1%
+ ~Mathlib.AlgebraicGeometry.Properties                        instructions        -9.2%
+ ~Mathlib.AlgebraicGeometry.Spec                              instructions       -11.5%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                    instructions        -1.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                   instructions        -2.0%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution          instructions        -1.6%
+ ~Mathlib.CategoryTheory.LiftingProperties.Adjunction         instructions       -22.3%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module             instructions        -6.8%
+ ~Mathlib.Combinatorics.HalesJewett                           instructions       -83.1%
+ ~Mathlib.FieldTheory.AbelRuffini                             instructions        -6.1%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation   instructions        -4.2%
- ~Mathlib.Geometry.Manifold.VectorBundle.SmoothSection        instructions       153.3%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing         instructions        -3.5%
+ ~Mathlib.GroupTheory.HNNExtension                            instructions        -7.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction           instructions        -8.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                  instructions       -13.6%
+ ~Mathlib.LinearAlgebra.DFinsupp                              instructions       -12.2%
+ ~Mathlib.LinearAlgebra.Dual                                  instructions        -4.0%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                        instructions       -50.9%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic                     instructions        -9.9%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                      instructions        -5.0%
+ ~Mathlib.NumberTheory.NumberField.Units                      instructions        -3.6%
+ ~Mathlib.RepresentationTheory.Character                      instructions       -28.9%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution     instructions       -56.1%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation             instructions       -24.1%
+ ~Mathlib.RingTheory.IsTensorProduct                          instructions        -9.3%
+ ~Mathlib.RingTheory.Kaehler                                  instructions        -2.9%
+ ~Mathlib.RingTheory.PowerSeries.Basic                        instructions       -12.4%
+ ~Mathlib.RingTheory.RootsOfUnity.Basic                       instructions        -6.1%
+ ~Mathlib.RingTheory.Trace                                    instructions        -6.5%

astrainfinita · 2023-10-26T08:14:36Z

!bench

leanprover-bot · 2023-10-26T08:47:44Z

Here are the benchmark results for commit 18d65c8.
There were significant changes against commit bf077b1:

  Benchmark                                                    Metric             Change
  ======================================================================================
+ build                                                        linting             -6.7%
+ build                                                        tactic execution    -5.4%
+ lint                                                         instructions        -6.1%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings            instructions        -8.5%
+ ~Mathlib.Algebra.Category.Ring.Constructions                 instructions       -38.4%
+ ~Mathlib.Algebra.DirectLimit                                 instructions       -19.6%
+ ~Mathlib.Algebra.Homology.ModuleCat                          instructions       -32.1%
+ ~Mathlib.Algebra.Jordan.Basic                                instructions        -5.8%
+ ~Mathlib.Algebra.Lie.Weights.Basic                           instructions       -12.6%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point               instructions        -4.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated          instructions       -19.6%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties       instructions        -7.1%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme         instructions        -7.1%
+ ~Mathlib.AlgebraicGeometry.Properties                        instructions        -9.2%
+ ~Mathlib.AlgebraicGeometry.Spec                              instructions       -11.5%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                   instructions        -2.0%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution          instructions        -1.6%
+ ~Mathlib.CategoryTheory.LiftingProperties.Adjunction         instructions       -22.3%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module             instructions        -6.8%
+ ~Mathlib.Combinatorics.HalesJewett                           instructions       -83.1%
+ ~Mathlib.FieldTheory.AbelRuffini                             instructions        -6.1%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation   instructions        -4.2%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing         instructions        -3.4%
+ ~Mathlib.GroupTheory.HNNExtension                            instructions        -7.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction           instructions        -8.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                  instructions       -13.6%
+ ~Mathlib.LinearAlgebra.DFinsupp                              instructions       -12.3%
+ ~Mathlib.LinearAlgebra.Dual                                  instructions        -4.0%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                        instructions       -50.9%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic                     instructions        -9.9%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                      instructions        -4.9%
+ ~Mathlib.NumberTheory.NumberField.Units                      instructions        -3.6%
+ ~Mathlib.RepresentationTheory.Character                      instructions       -28.9%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution     instructions       -56.0%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation             instructions       -24.2%
+ ~Mathlib.RingTheory.IsTensorProduct                          instructions        -9.3%
+ ~Mathlib.RingTheory.Kaehler                                  instructions        -2.9%
+ ~Mathlib.RingTheory.PowerSeries.Basic                        instructions       -12.4%
+ ~Mathlib.RingTheory.RootsOfUnity.Basic                       instructions        -6.1%
+ ~Mathlib.RingTheory.Trace                                    instructions        -6.5%

Mathlib/Data/FunLike/Basic.lean

eric-wieser

Can you add a file in test/ that demonstrates that the inferred type of non-dependent funlikes is improved?

Mathlib/Data/FunLike/Basic.lean

eric-wieser · 2023-10-26T10:35:12Z

Mathlib/Algebra/Lie/DirectSum.lean

 #align direct_sum.lie_of_of_eq DirectSum.lie_of_of_eq

-@[simp]
+-- @[simp] -- LHS doesn't simplify after #7905


This one is rather worrying

Mathlib/Data/Finsupp/Pointwise.lean

eric-wieser · 2023-10-26T10:36:43Z

Mathlib/Geometry/RingedSpace/Stalks.lean

 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.stalk_map.stalk_iso AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso

-@[simp, reassoc, elementwise]


Why was this de-simped? Does the same comment apply as elsewhere about simpNF getting confused?

Is a lemma with proof parameters that do not appear directly on the LHS (but in LHS there's a proof that uses it) appropriate as a simp lemma? If it should be, then I'll add a note.

Yes, I think this is still fine as a simp lemma, since simp creates x ⤳ y as a side-goal. Did the linter complain?

Yes, simpNF linter complains. I think this is because x ⤳ y doesn't appear directly on the LHS.

Is x ⤳ y a proof as you said it was, or is it data?

It's a proof https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Inseparable.html#Specializes

astrainfinita · 2023-11-15T13:34:10Z

!bench

Mathlib/Data/Finsupp/Pointwise.lean

eric-wieser · 2023-11-15T13:41:07Z

Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

+theorem mk_reindex_cast' {n m : ℕ} (h : Fin n = Fin m) (x : (⨂[R]^n) M) :
+    GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m
+    (PiTensorProduct.reindex R M (Equiv.cast h) x) =
+    GradedMonoid.mk n x :=
+  Eq.symm (PiTensorProduct.gradedMonoid_eq_of_reindex_cast (fin_injective h) rfl)
+


I think we should get rid of this, since type equalities are evil. Does the proof below break without it?

(if not, then it doesn't belong in this PR anyway)

For the same reason as above, the version with h : n = m is no longer a simp lemma. But removing it won't break things.

I think all of the removed simp attributes should come with a comment referring to 7905; as far as I can tell, all of them look a bit iffy.

This looks like a bug to me, leanprover-community/batteries#365.

I suggest you replace all of these with simpNF, and add a comment referencing std4#365.

I've gone ahead and done that

Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

eric-wieser · 2023-11-15T13:46:30Z

Mathlib/NumberTheory/NumberField/Units.lean

                        QuotientGroup.mk_prod, ofMul_prod]; rfl
                    _ = ∑ i, (f i) • (basisModTorsion K i) := by
-                      simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]
+                      simp_rw [fundSystem, QuotientGroup.out_eq']; rfl


This one is a bit weird; I'll take a look once a cache is ready.

eric-wieser · 2023-11-15T13:47:08Z

Mathlib/Logic/Equiv/Set.lean

 #align equiv.set.image Equiv.Set.image
 #align equiv.set.image_apply Equiv.Set.image_apply

-@[simp]


Was this rejected by simpNF? If so, in favor of what lemma?

⟨x, ⟨h, rfl⟩⟩ : f x ∈ f '' s is a proof.

That's not supposed to matter... Either way, I'm happy with the comments for now, this PR is clearly a big improvement in general.

leanprover-bot · 2023-11-15T14:29:03Z

Here are the benchmark results for commit 6267d0a.
There were significant changes against commit 91e2d02:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ build                                                        linting         -8.9%
+ lint                                                         instructions    -7.7%
+ lint                                                         wall-clock      -7.7%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings            instructions    -7.8%
+ ~Mathlib.Algebra.Category.Ring.Constructions                 instructions   -39.0%
+ ~Mathlib.Algebra.DirectLimit                                 instructions   -19.7%
+ ~Mathlib.Algebra.Homology.ModuleCat                          instructions   -32.0%
+ ~Mathlib.Algebra.Jordan.Basic                                instructions    -5.9%
+ ~Mathlib.Algebra.Lie.Weights.Basic                           instructions   -10.0%
+ ~Mathlib.Algebra.Module.PID                                  instructions    -5.1%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point               instructions    -4.6%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme         instructions    -7.3%
+ ~Mathlib.AlgebraicGeometry.Properties                        instructions    -9.9%
+ ~Mathlib.AlgebraicGeometry.Spec                              instructions   -11.7%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                    instructions    -3.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                   instructions    -2.1%
+ ~Mathlib.CategoryTheory.LiftingProperties.Adjunction         instructions   -23.0%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module             instructions    -6.7%
+ ~Mathlib.Combinatorics.HalesJewett                           instructions   -82.2%
+ ~Mathlib.Data.Sum.Lattice                                    instructions   -40.8%
+ ~Mathlib.FieldTheory.AbelRuffini                             instructions    -6.2%
+ ~Mathlib.FieldTheory.Adjoin                                  instructions    -4.2%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation   instructions    -4.3%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing         instructions    -2.2%
+ ~Mathlib.GroupTheory.HNNExtension                            instructions    -7.5%
+ ~Mathlib.GroupTheory.PushoutI                                instructions   -10.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction           instructions    -8.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                  instructions   -13.7%
+ ~Mathlib.LinearAlgebra.DFinsupp                              instructions   -13.9%
+ ~Mathlib.LinearAlgebra.Dual                                  instructions    -4.4%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace                    instructions    11.0%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                        instructions   -45.5%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic                     instructions    -8.7%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                      instructions    -4.9%
+ ~Mathlib.NumberTheory.NumberField.Units                      instructions    -4.1%
+ ~Mathlib.RepresentationTheory.Action                         instructions    -1.6%
+ ~Mathlib.RepresentationTheory.Character                      instructions   -28.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution     instructions   -66.7%
+ ~Mathlib.RepresentationTheory.Rep                            instructions    -4.9%
+ ~Mathlib.RingTheory.AdjoinRoot                               instructions    -3.5%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation             instructions   -25.0%
+ ~Mathlib.RingTheory.IsTensorProduct                          instructions   -10.0%
+ ~Mathlib.RingTheory.Kaehler                                  instructions    -4.4%
+ ~Mathlib.RingTheory.PowerSeries.Basic                        instructions   -12.7%
+ ~Mathlib.RingTheory.RootsOfUnity.Basic                       instructions    -7.4%
+ ~Mathlib.RingTheory.Trace                                    instructions    -6.6%
+ ~Mathlib.Topology.Sheaves.Stalks                             instructions    -5.1%

eric-wieser · 2023-11-15T14:33:57Z

I'm happy with this now, thanks! I'd like to jump into an editor once the cache is ready and fiddle with a couple proofs; please ping me if this PR is green and I haven't already done so. If I don't respond, I'm fine with it being merged in 8 hours.

eric-wieser · 2023-11-15T21:18:53Z

bors merge

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2023-11-15T22:36:10Z

Pull request successfully merged into master.

Build succeeded:

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…s now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here.

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…s now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here.

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…s now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here.

chore: short cut instance for non-dependent FunLike

67a8504

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Not sure about the name.

astrainfinita added the WIP Work in progress label Oct 24, 2023

astrainfinita added a commit that referenced this pull request Oct 24, 2023

chore: typeclass for non-dependent FunLike

233fb89

This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Not sure about the name. I'd like to see if it's much better than #7905.

astrainfinita mentioned this pull request Oct 24, 2023

chore: typeclass for non-dependent FunLike #7906

Closed

astrainfinita added 10 commits October 25, 2023 05:01

fix

ec8fbfe

fix

1db1016

fix

1d7a1cf

fix

d45d7ab

fix

2170722

fix

d9b0cee

fix

2e8d234

fix

f4a4e79

lint

1dc6a94

fix

4d6319b

local high priority

18d65c8

astrainfinita added awaiting-review and removed WIP Work in progress labels Oct 26, 2023

astrainfinita added 2 commits October 26, 2023 17:47

this is faster

3414e9b

docs

1018451

Vierkantor self-assigned this Oct 26, 2023

eric-wieser reviewed Oct 26, 2023

View reviewed changes

Mathlib/Data/FunLike/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Oct 26, 2023

View reviewed changes

Mathlib/Data/FunLike/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Oct 26, 2023

View reviewed changes

Mathlib/Data/Finsupp/Pointwise.lean Show resolved Hide resolved

eric-wieser reviewed Oct 26, 2023

View reviewed changes

astrainfinita added 3 commits November 15, 2023 21:01

fix

4752f1c

reduce diffs

40912e7

keep both versions

6267d0a

eric-wieser reviewed Nov 15, 2023

View reviewed changes

Mathlib/Data/Finsupp/Pointwise.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 15, 2023

View reviewed changes

Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 15, 2023

View reviewed changes

astrainfinita added 2 commits November 15, 2023 22:23

suggestions

b1bebb1

more notes

bd9dd94

eric-wieser added 2 commits November 15, 2023 15:51

fix a weird rfl failure

2b7a1d5

add comments

73fdc27

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 15, 2023

mathlib-bors bot changed the title ~~perf(FunLike.Basic): beta reduce CoeFun.coe~~ [Merged by Bors] - perf(FunLike.Basic): beta reduce CoeFun.coe Nov 15, 2023

mathlib-bors bot closed this Nov 15, 2023

mathlib-bors bot deleted the FR_funlike_shortcut branch November 15, 2023 22:36

dwrensha mentioned this pull request Nov 18, 2023

[Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now #8496

Closed

mathlib-bors bot pushed a commit that referenced this pull request Nov 19, 2023

chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith work…

55ad9df

…s now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here.

alexkeizer pushed a commit that referenced this pull request Nov 21, 2023

chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith work…

97f34d8

…s now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here.

grunweg pushed a commit that referenced this pull request Dec 15, 2023

chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith work…

6dcf66b

…s now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here.

Conversation

astrainfinita commented Oct 24, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

astrainfinita commented Oct 26, 2023

Uh oh!

leanprover-bot commented Oct 26, 2023

Uh oh!

astrainfinita commented Oct 26, 2023

Uh oh!

leanprover-bot commented Oct 26, 2023

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

astrainfinita Oct 26, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

astrainfinita commented Nov 15, 2023

Uh oh!

Uh oh!

eric-wieser Nov 15, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leanprover-bot commented Nov 15, 2023

Uh oh!

eric-wieser commented Nov 15, 2023

Uh oh!

eric-wieser commented Nov 15, 2023

Uh oh!

mathlib-bors bot commented Nov 15, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

astrainfinita commented Oct 24, 2023 •

edited

Loading

astrainfinita Oct 26, 2023 •

edited

Loading

eric-wieser Nov 15, 2023 •

edited

Loading