Tradeoff of defining types as subobjects #86
Conversation
|
|
||
| ## Typeclass search | ||
|
|
||
| In the Subobject design, all instances about `circle` are actually about `↥circle` where `↥` is [`CoeSort.coe`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=CoeSort.coe#doc). Eg `Foo circle` is secretly `Foo ↥circle`. This makes the head symbol be `CoeSort.coe`, meaning that typeclass search will try unifying *every* `Foo ↥someSubobject` instance with `Foo ↥circle`. In doing so, it will try unifying *every* subobject `someSubobject` with a `Foo` instance with `circle`. This is potentially really expensive. |
There was a problem hiding this comment.
Is this still the case in Lean 4? I thought discrimination trees avoided this...
There was a problem hiding this comment.
Very much so. Else why would leanprover-community/mathlib4#12386 have achieved anything perf-wise? The problem I believe is that the discr tree key is [CoeSort.coe, *]
There was a problem hiding this comment.
Can you prove this with an example that uses #discr_tree_key? My first attempt does not agree with you:
import Mathlib
#discr_tree_key Metric.unitSphere.coe_inv
-- @Eq _ (@Inv.inv (@Subtype _ (@Membership.mem _ (Set _) _ (@Metric.sphere _ _ 0 1))) _ _).1 (@Inv.inv _ _ _.1)There was a problem hiding this comment.
Nor does my second attempt:
import Mathlib
theorem foo (x y : Submonoid.unitSphere ℝ) : ↑(x * y : Submonoid.unitSphere ℝ) = (x * y : ℝ) := rfl
/--
info: @Eq
ℝ
(@HMul.hMul
(@Subtype ℝ (@Membership.mem ℝ (Submonoid ℝ _) _ (Submonoid.unitSphere ℝ _ _ _)))
(@Subtype ℝ (@Membership.mem ℝ (Submonoid ℝ _) _ (Submonoid.unitSphere ℝ _ _ _)))
(@Subtype ℝ (@Membership.mem ℝ (Submonoid ℝ _) _ (Submonoid.unitSphere ℝ _ _ _)))
_
_
_).1
(@HMul.hMul ℝ ℝ ℝ _ _.1 _.1)
-/
#guard_msgs in
#discr_tree_key foo
There was a problem hiding this comment.
In fact, https://loogle.lean-lang.org/?q=CoeSort.coe suggests that CoeSort.coe doesn't ever appear in any theorems (as it is inlined into Subtype)
Co-authored-by: damiano <[email protected]>
| @@ -0,0 +1,122 @@ | |||
| --- | |||
| author: 'Yaël Dillies' | |||
| category: 'Papers' | |||
There was a problem hiding this comment.
Not sure what to put here
Zulip