fix: redefine semiring instance on tensor product#6134
fix: redefine semiring instance on tensor product#6134
Conversation
kbuzzard
commented
Jul 25, 2023
|
!bench |
| } | ||
|
|
||
| instance instSemiring : Semiring (A ⊗[R] B) := | ||
| { (by infer_instance : AddMonoidWithOne (A ⊗[R] B)), |
There was a problem hiding this comment.
I worry that this discarded the natCast field, though I have no idea whether it actually does.
There was a problem hiding this comment.
Do you still worry given that it compiles and the benchmark results?
There was a problem hiding this comment.
Yes, because neither of those steps necessarily checks for diamonds problems, and previously we relied on the source code making it obvious that they didn't exist. I'll add an example to verify that it's fine.
There was a problem hiding this comment.
Thanks. I don't understand the issue that you're concerned about so please feel free to check this out (or explain the issue to me, either will do).
There was a problem hiding this comment.
The issue is
example : (algebraNat : Algebra ℕ (ℕ ⊗[ℕ] ℕ)) = leftAlgebra := rfl -- failsbut this already failed on master so you're off the hook!
|
Here are the benchmark results for commit 9448a00. Benchmark Metric Change
================================================================================
- build maxrss 8.1%
+ ~Mathlib.Algebra.Category.Ring.Constructions instructions -12.7%
+ ~Mathlib.Data.Matrix.Kronecker instructions -22.6%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions 5.2%
- ~Mathlib.RingTheory.ClassGroup instructions 8.8%
+ ~Mathlib.RingTheory.Etale instructions -9.6%
+ ~Mathlib.RingTheory.IntegralClosure instructions -8.4%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -24.3%
+ ~Mathlib.RingTheory.Kaehler instructions -44.9%
+ ~Mathlib.RingTheory.RingHom.Finite instructions -32.4%
+ ~Mathlib.RingTheory.RingHom.Integral instructions -47.7%
+ ~Mathlib.RingTheory.RingHom.Surjective instructions -7.4%
+ ~Mathlib.RingTheory.RingHomProperties instructions -20.9%
+ ~Mathlib.RingTheory.TensorProduct instructions -14.8% |
|
|
|
The six remaining |
|
I'm a bit concerned that github is currently broken, and that there is no guarantee that bors will merge what we expect it to: so I think we should leave this until the commit I mention above appears! |
| #align kaehler_differential.total_surjective KaehlerDifferential.total_surjective | ||
|
|
||
| set_option maxHeartbeats 3200000 in -- 2569452 | ||
| set_option maxHeartbeats 400000 in -- 2569452 |
There was a problem hiding this comment.
| set_option maxHeartbeats 400000 in -- 2569452 | |
| set_option maxHeartbeats 400000 in |
I guess this is not relevant anymore.