Skip to content
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

[Merged by Bors] - perf(FunLike.Basic): beta reduce CoeFun.coe #7905

Closed
wants to merge 28 commits into from

Conversation

FR-vdash-bot
Copy link
Collaborator

@FR-vdash-bot FR-vdash-bot commented Oct 24, 2023

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


Open in Gitpod

Zulip

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

Not sure about the name.
@FR-vdash-bot FR-vdash-bot added the WIP Work in progress label Oct 24, 2023
FR-vdash-bot added a commit that referenced this pull request Oct 24, 2023
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.
@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

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%

@FR-vdash-bot
Copy link
Collaborator Author

!bench

@FR-vdash-bot FR-vdash-bot added awaiting-review and removed WIP Work in progress labels Oct 26, 2023
@leanprover-bot
Copy link
Collaborator

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%

@Vierkantor Vierkantor self-assigned this Oct 26, 2023
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@[simp]
-- @[simp] -- LHS doesn't simplify after #7905
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one is rather worrying

@@ -225,7 +225,7 @@ def stalkIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ≅ Y) (x : X) :
set_option linter.uppercaseLean3 false in
#align algebraic_geometry.PresheafedSpace.stalk_map.stalk_iso AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso

@[simp, reassoc, elementwise]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@FR-vdash-bot FR-vdash-bot Oct 26, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@FR-vdash-bot
Copy link
Collaborator Author

!bench

Comment on lines 121 to 126
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)

Copy link
Member

@eric-wieser eric-wieser Nov 15, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've gone ahead and done that

simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]
simp_rw [fundSystem, QuotientGroup.out_eq']; rfl
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -486,7 +486,6 @@ protected noncomputable def image {α β} (f : α → β) (s : Set α) (H : Inje
#align equiv.set.image Equiv.Set.image
#align equiv.set.image_apply Equiv.Set.image_apply

@[simp]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Collaborator

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
Copy link
Member

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
Copy link
Member

bors merge

@github-actions 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 pushed a commit that referenced this pull request Nov 15, 2023
This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`.




Co-authored-by: Matthew Ballard <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Nov 15, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors 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 mathlib-bors bot closed this Nov 15, 2023
@mathlib-bors mathlib-bors bot deleted the FR_funlike_shortcut branch November 15, 2023 22:36
alexkeizer pushed a commit that referenced this pull request Nov 17, 2023
This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`.




Co-authored-by: Matthew Ballard <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
mathlib-bors bot pushed a commit that referenced this pull request Nov 19, 2023
…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
This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`.




Co-authored-by: Matthew Ballard <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
alexkeizer pushed a commit that referenced this pull request Nov 21, 2023
…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
This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`.




Co-authored-by: Matthew Ballard <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
grunweg pushed a commit that referenced this pull request Dec 15, 2023
…s now (#8496)

According to `git bisect`, #7905 is what made the single `linarith` call work here.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants