fix: modify projection instance binder info #5376
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
closes #5333 This PR tries to address issue #5333. My conjecture is that the binder annotations for `C.toB` and `Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations where the new command `set_synth_order` was used. Both classes, `C` and `Algebra`, are parametric over instances, and in both cases, the issue arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's focus on the binder annotations for `C.toB`. They are as follows: ``` C.toB [inst : A 20000] [self : @C inst] : @b ... ``` As a projection, it seems odd that `inst` is an instance-implicit argument instead of an implicit one, given that its value is fixed by `self`. We observe the same issue in `Algebra.toSMul`: ``` Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A] [self : @algebra R A inst1 inst2] : SMul R A ``` The PR changes the binder annotations as follows: ``` C.toB {inst : A 20000} [self : @C inst] : @b ... ``` and ``` Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A} [self : @algebra R A inst1 inst2] : SMul R A ``` In both cases, the `set_synth_order` is used to force `self` to be processed first. In the MWE, there is no instance for `C ...`, and `C.toB` is quickly discarded. I suspect a similar issue occurs when trying to use `Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean spends unnecessary time trying to synthesize `CommSemiring R` and `Semiring A` instances. I believe the new binder annotations make sense, as if there is a way to synthesize `Algebra R A ... ...`, it will tell us how to retrieve the instance-implicit arguments. Not sure what the impact will be on Mathlib.
github-actions
bot
temporarily deployed
to
lean-lang.org/lean4/doc
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 18, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 18, 2024
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
|
!bench |
|
Here are the benchmark results for commit 170166e. Benchmark Metric Change
================================================
- ilean roundtrip compress 1.0% (17.6 σ)
+ lake build no-op task-clock -2.1% (-23.4 σ) |
|
Mathlib CI status (docs):
|
github-actions
bot
temporarily deployed
to
lean-lang.org/lean4/doc
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 19, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 19, 2024
|
Mathlib CI status (docs):
|
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 19, 2024
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 19, 2024
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
builds-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-bot
removed
the
breaks-mathlib
leanprover-community-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
|
Yes, this is exactly my understanding of the problem in Mathlib and this fix is far more sensible. Thanks @leodemoura ! |
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
jcommelin
reviewed
Sep 19, 2024
Co-authored-by: Johan Commelin <[email protected]>
github-actions
bot
temporarily deployed
to
lean-lang.org/lean4/doc
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 20, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 20, 2024
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
This was referenced Oct 4, 2024
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 8, 2024
With the change to the construction of the synthesis order algorithm, we want to avoid searches with metavariables by specifying more `outParam`s.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
closes #5333
This PR tries to address issue #5333.
My conjecture is that the binder annotations for
C.toBandAlgebra.toSMulare not ideal.Algebra.toSMulis one of declarations where the new commandset_synth_orderwas used. Both classes,CandAlgebra, are parametric over instances, and in both cases, the issue arises due to projection instances:C.toBandAlgebra.toSMul. Let's focus on the binder annotations forC.toB. They are as follows:As a projection, it seems odd that
instis an instance-implicit argument instead of an implicit one, given that its value is fixed byself. We observe the same issue inAlgebra.toSMul:The PR changes the binder annotations as follows:
and
In both cases, the
set_synth_orderis used to forceselfto be processed first.In the MWE, there is no instance for
C ..., andC.toBis quickly discarded. I suspect a similar issue occurs when trying to useAlgebra.toSMul, where there is no@Algebra R A ... ..., but Lean spends unnecessary time trying to synthesizeCommSemiring RandSemiring Ainstances. I believe the new binder annotations make sense, as if there is a way to synthesizeAlgebra R A ... ..., it will tell us how to retrieve the instance-implicit arguments.TODO: