refactor: structurally recursive List.ofFn #784
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
nomeata
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 7, 2024
This used to be defined via `Array.ofFn` but `Array.ofFn.go` is defined by well-founded recursion (slow to reduce) and used `Array.push` (quadratic complexity on lists). Since mathlib relies on reducing `List.ofFn`, use a structurally recursive definition here.
nomeata
force-pushed
the
joachim/List.ofFn-structural
branch
from
ec5e171
to
1c72ad6
Compare
nomeata
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 7, 2024
|
Mathlib adoption branch is green. Oddly, no perf benefit on mathlib. I guess unfolding wf recursive functions isn’t too bad after all. But in light of the upcoming leanprover/lean4#4061 probably still worth doing? |
semorrison
added
the
will-merge-soon
semorrison
reviewed
May 7, 2024
Co-authored-by: Kim Morrison <kim@tqft.net>
digama0
reviewed
May 8, 2024
Batteries/Data/List/Basic.lean
Outdated
| /-- Auxillary for `List.ofFn`. -/ | ||
| -- This used to be defined via `Array.ofFn` | ||
| -- but `Array.ofFn.go` is defined by well-founded recursion (slow to reduce) | ||
| -- and used `Array.push` (quadratic complexity on lists). Since mathlib relies on |
There was a problem hiding this comment.
I don't know what is meant by this: Array.push is not quadratic complexity on arrays, and it's an array function.
There was a problem hiding this comment.
I assumed that the original definition, List.ofFn = Array.ofFn would – in terms of definitional equality - use the logical definition of the Array functions, which work on Arrays as if they are structures with a fields .data which is a list, and thus Array.push is actually List.concat. Am I mistaken here?
|
Pushed a variation which uses a structural recursive version for the defeqs and a tail-rec version for performance. |
Thanks! I wager that the tail-recursive variant could even be the only definition and we’d still get the defeqs that we had with the Array variant, but didn’t test this. |
|
Can this be merged now? (I'd like to have this off my plate.) |
github-merge-queue bot
pushed a commit
to leanprover/lean4
that referenced
this pull request
May 10, 2024
we keep running into examples where working with well-founded recursion is slow because defeq checks (which are all over the place, including failing ones that are back-tracked) unfold well-founded definitions. The definition of a function defined by well-founded recursion should be an implementation detail that should only be peeked inside by the equation generator and the functional induction generator. We now mark the mutual recursive function as irreducible (if the user did not set a flag explicitly), and use `withAtLeastTransparency .all` when producing the equations. Proofs can be fixed by using rewriting, or – a bit blunt, but nice for adjusting existing proofs – using `unseal` (a.k.a. `attribute [local semireducible]`). Mathlib performance does not change a whole lot: http://speed.lean-fro.org/mathlib4/compare/08b82265-75db-4a28-b12b-08751b9ad04a/to/16f46d5e-28b1-41c4-a107-a6f6594841f8 Build instructions -0.126 %, four modules with significant instructions decrease. To reduce impact, these definitions were changed: * `Nat.mod`, to make `1 % n` reduce definitionally, so that `1` as a `Fin 2` literal works nicely. Theorems with larger `Fin` literals tend to need a `unseal Nat.modCore` #4098 * `List.ofFn` rewritten to be structurally recursive and not go via `Array.ofFn`: leanprover-community/batteries#784 Alternative designs explored were * Making `WellFounded.fix` irreducible. One benefit is that recursive functions with equal definitions (possibly after instantiating fixed parameters) are defeq; this is used in mathlib to relate [`OrdinalApprox.gfpApprox`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/FixedPointApproximants.html#OrdinalApprox.gfpApprox) with `.lfpApprox`. But the downside is that one cannot use `unseal` in a targeted way, being explicit in which recursive function needs to be reducible here. And in cases where Lean does unwanted unfolding, we’d still unfold the recursive definition once to expose `WellFounded.fix`, leading to large terms for often no good reason. * Defining `WellFounded.fix` to unroll defintionally once before hitting a irreducible `WellFounded.fixF`. This was explored in #4002. It shares most of the ups and downs with the previous variant, with the additional neat benefit that function calls that do not lead to recursive cases (e.g. a `[]` base case) reduce nicely. This means that the majority of existing `rfl` proofs continue to work. Issue #4051, which demonstrates how badly things can go if wf recursive functions can be unrolled, showed that making the recursive function irreducible there leads to noticeably faster elaboration than making `WellFounded.fix` irreducible; this is good evidence that the present PR is the way to go. This fixes #3988 --------- Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
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 used to be defined via
Array.ofFnbut
Array.ofFn.gois defined by well-founded recursion (slow to reduce)and used
Array.push(quadratic complexity on lists). Since mathlib relies onreducing
List.ofFn, use a structurally recursive definition here.