[Merged by Bors] - refactor: do not allow `nsmul` and `zsmul` to default automatically #6262

eric-wieser · 2023-07-31T08:54:29Z

This PR removes the default values for nsmul and zsmul, forcing the user to populate them manually.
The previous behavior can be obtained by writing nsmul := nsmulRec and zsmul := zsmulRec, which is now in the docstring for these fields.

The motivation here is to make it more obvious when module diamonds are being introduced, or at least where they might be hiding; you can now simply search for nsmulRec in the source code.

Arguably we should do the same thing for intCast, natCast, pow, and zpow too, but diamonds are less common in those fields, so I'll leave them to a subsequent PR.

depends on: [Merged by Bors] - chore(Algebra/Category/*/Colimits): golf #6265

This was particularly bad in light of leanprover/lean4#2387, which encouraged us (in order to avoid a performance issue) to write { nsmul := foo.nsmul, toY := foo.toY, z := z } instead of { foo with z := z }; if nsmul := is forgotten in this case, a new diamond is created.

…l-default

…to eric-wieser/no-nsmul-default

kbuzzard · 2023-07-31T14:27:39Z

Could this be related to why Algebra.Category.ModuleCat.Limits compiles more slowly after #6144 ? Or are your changes colimit-only?

sgouezel · 2023-07-31T15:53:21Z

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -161,6 +161,7 @@ instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M)
  zero_add _ := bot_sup_eq
  add_zero _ := sup_bot_eq
  add_comm _ _ := sup_comm
+  nsmul := letI : Zero (Submodule R M) := ⟨⊥⟩; letI : Add (Submodule R M) := ⟨Sup.sup⟩; nsmulRec


Doesn't this indicate that it would be better to declare the Zero and Add instances separately?

Does it matter if we're using letI, because this just inlines everything.

I think my patch behaves exactly the same as what we currently do, though I haven't checked. (Yours generates a smaller term.)

I've pulled this out as requested.

sgouezel · 2023-07-31T15:54:04Z

Mathlib/Algebra/Ring/BooleanRing.lean

+  nsmul := letI : Zero α := ⟨⊥⟩; letI : Add α := ⟨(· ∆ ·)⟩; nsmulRec
+  zsmul := letI : Zero α := ⟨⊥⟩; letI : Add α := ⟨(· ∆ ·)⟩; letI : Neg α := ⟨id⟩; zsmulRec


This is a def, so pulling these out is impractical.

Mathlib/Algebra/Ring/BooleanRing.lean

leanprover-community-mathlib4-bot · 2023-08-02T14:46:49Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra/Category/*/Colimits): golf #6265~~
By Dependent Issues (🤖). Happy coding!

…l-default

eric-wieser · 2024-03-08T21:54:50Z

Ah, you were technically correct; the conflict marked was in Counterexamples, as was the build failure. Now fixed.

eric-wieser · 2024-03-08T21:55:49Z

!bench

leanprover-bot · 2024-03-08T22:23:16Z

Here are the benchmark results for commit c85d804.
There were significant changes against commit cb921c1:

  Benchmark                                                  Metric         Change
  ================================================================================
+ ~Mathlib.Algebra.Module.PID                                instructions    -5.5%
+ ~Mathlib.CategoryTheory.Preadditive.FunctorCategory        instructions   -47.5%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                        instructions   -22.6%
+ ~Mathlib.RepresentationTheory.Action.Limits                instructions   -47.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic        instructions   -20.5%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions    -7.2%

eric-wieser · 2024-03-09T09:16:17Z

Well that's a nice bonus

bors merge

…6262) This PR removes the default values for `nsmul` and `zsmul`, forcing the user to populate them manually. The previous behavior can be obtained by writing `nsmul := nsmulRec` and `zsmul := zsmulRec`, which is now in the docstring for these fields. The motivation here is to make it more obvious when module diamonds are being introduced, or at least where they might be hiding; you can now simply search for `nsmulRec` in the source code. Arguably we should do the same thing for `intCast`, `natCast`, `pow`, and `zpow` too, but diamonds are less common in those fields, so I'll leave them to a subsequent PR. Co-authored-by: Matthew Ballard <matt@mrb.email>

mathlib-bors · 2024-03-09T10:41:41Z

Pull request successfully merged into master.

Build succeeded:

mattrobball · 2024-03-09T14:18:55Z

I didn't compare the profiles before and after but I guess unification is not unfolding + now in some checks?