perf: preprocess tc instances to avoid nested tc#3042
Conversation
gebner
commented
Mar 22, 2023
|
!bench |
| This file defines a `[@Commutes C inst₁ inst₂]` type class meaning that the | ||
| instances `inst₁ : C` and `inst₂ : C` are defeq. This allows us to write instances like: |
There was a problem hiding this comment.
Presumably this is enforced socially and not by lean itself; it looks to me like the typeclass only enforces that they're propositionally equal?
There was a problem hiding this comment.
The only instance for Commutes witnesses definitional equality. It's not meant to be extended.
There was a problem hiding this comment.
Oh wow that's a neat trick! I totally missed that Commutes.mk was an instance.
|
I view this PR as a slightly experimental hack, both to see how well the approach works, as well as something that we could maybe ship today (and most likely allow us to enable eta). The same issue arises with simp, and in aesop, and really anything that tries to apply lemmas in any form. It would be great if we could fix this directly in unification, but even if had a perfect solution today, it would take a couple of weeks to get it in. |
| open Lean Elab Parser Command in | ||
| /-- | ||
| Similar to `instance`, but generalizes nonatomic instance terms in the | ||
| conclusion. Only use for `Prop`-valued classes. |
There was a problem hiding this comment.
Can you enforce this with an error message?
|
Here are the benchmark results for commit 066538b. |
|
!bench |
|
Here are the benchmark results for commit a7308f6. Benchmark Metric Change
==================================================================
- ~Mathlib.Algebra.CovariantAndContravariant instructions 33.8%
+ ~Mathlib.Algebra.GCDMonoid.Basic instructions -7.7%
+ ~Mathlib.Algebra.Module.Submodule.Lattice instructions -14.3%
+ ~Mathlib.Algebra.Order.AbsoluteValue instructions -6.0%
+ ~Mathlib.Algebra.Order.Group.Bounds instructions -11.3%
- ~Mathlib.Algebra.Order.Ring.WithTop instructions 5.2%
- ~Mathlib.Algebra.Ring.OrderSynonym instructions 7.2%
+ ~Mathlib.Algebra.Ring.Prod instructions -7.2%
+ ~Mathlib.Data.Polynomial.Identities instructions -21.5%
+ ~Mathlib.Data.Real.ENatENNReal instructions -5.4%
+ ~Mathlib.GroupTheory.GroupAction.ConjAct instructions -10.6%
+ ~Mathlib.LinearAlgebra.Ray instructions -11.6%
+ ~Mathlib.RingTheory.AlgebraTower instructions -21.4%
+ ~Mathlib.RingTheory.EuclideanDomain instructions -24.7%
+ ~Mathlib.RingTheory.Localization.Basic instructions -8.7%
+ ~Mathlib.RingTheory.Nilpotent instructions -9.9%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev instructions -9.3% |
|
That is a very specific improvement! Unfortunately it is not enough to enable eta, as it doesn't solve |
|
I am closing this PR since it seems it has fulfilled its purpose. Feel free to reopen it. |