perf: use NatPow Int instead of HPow Int Nat Int
#4903
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
This modification improves the performance of the example in issue #4861. It no longer times out but is still expensive. Here is the analysis of the performance issue: Given `(x : Int)`, to elaborate `x ^ 1`, a few default instances have to be tried. First, the homogeneous instance is tried and fails since `Int` does not implement `Pow Int`. Then, the `NatPow` instance is tried, and it also fails. The same process is performed for each term of the form `p ^ 1`. There are seveal of them at #4861. After all of these fail, the lower priority default instance for numerals is tried, and `x ^ 1` becomes `x ^ (1 : Nat)`. Then, `HPow Int Nat Int` can be applied, and the elaboration succeeds. However, this process has to be repeated for every single term of the form `p ^ 1`. The elaborator tries all homogeneous `HPow` and `NatPow` instances for all `p ^ 1` terms before trying the lower priority default instance `OfNat`. This commit ensures `Int` has a `NatPow` instance instead of `HPow Int Nat Int`. This change shortcuts the process, but it still first tries the homogeneous `HPow` instance, fails, and then tries `NatPow`. The elaboration can be made much more efficient by writing `p ^ (1 : Nat)`.
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 2, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 2, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 2, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 2, 2024
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
This seems to have been an oversight in #2778, and it should have become a Mathlib adds a default |
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.
This modification improves the performance of the example in issue #4861. It no longer times out but is still expensive.
Here is the analysis of the performance issue: Given
(x : Int), to elaboratex ^ 1, a few default instances have to be tried.First, the homogeneous instance is tried and fails since
Intdoes not implementPow Int. Then, theNatPowinstance is tried, and it also fails. The same process is performed for each term of the formp ^ 1. There are seveal of them at #4861. After all of these fail, the lower priority default instance for numerals is tried, andx ^ 1becomesx ^ (1 : Nat). Then,HPow Int Nat Intcan be applied, and the elaboration succeeds. However, this process has to be repeated for every single term of the formp ^ 1. The elaborator tries all homogeneousHPowandNatPowinstances for allp ^ 1terms before trying the lower priority default instanceOfNat.This commit ensures
Inthas aNatPowinstance instead ofHPow Int Nat Int. This change shortcuts the process, but it still first tries the homogeneousHPowinstance, fails, and then triesNatPow. The elaboration can be made much more efficient by writingp ^ (1 : Nat).