feat: well-founded definitions irreducible by default #4061
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
we keep running into examples where working with well-founded recursion is slow becuase 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, and use `withAtLeastTransparency .all` when producing the equations. This fixes #3988
github-actions
bot
added
the
changes-stage0
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 3, 2024
nomeata
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
nomeata
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
nomeata
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
nomeata
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 3, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 3, 2024
nomeata
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 3, 2024
nomeata
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 3, 2024
github-merge-queue bot
pushed a commit
that referenced
this pull request
May 8, 2024
this is in preparation for #4061. Once that lands, `1 % 42 = 1` will no longer hold definitionally (at least not without an ungly `unseal Nat.modCore in` around). This affects mathlib in a few places, essentially every time a `1 : Fin (n+1)` literal is written. So this extends the existing special case for `0 % n = 0` to `1 % n`.
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 9, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 9, 2024
This was referenced May 13, 2024
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 13, 2024
In leanprover/lean4#4061, well-founded definitions become irreducible by default, and hence some `rfl` proofs stop working. This pre-emptively backports some of the adaptations from #12853.
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 14, 2024
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 14, 2024
leanprover/lean4#4061 results in well-founded definitions being irreducible by default. This PR robustifies some proofs. (Sometime over-robust: we're going to keep `minFacAux` as semireducible for now, so e.g. `Nat.Prime 5` will still be decidable.)
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 14, 2024
The main underlying change here is leanprover/lean4#4119, which fixed a number of typeclass search bugs. In particular, it fixed a caching bug (the `synthPendingDepth` was being ignored during caching, resulting in both false positive and false negatives). For the false positives (i.e. things that synthesis was finding that it really shouldn't have been!), we've had to introduce `set_option maxSynthPendingDepth 2 in` in places. These are all explained with `#adaptation_notes`. There's also leanprover/lean4#4061, which makes well-founded definitions irreducible by default. This helps avoid some horrible run-away unfoldings, and was surprisingly un-painful to Mathlib to (credit to @nomeata for discovering this!) There are some minor adaptations still required, however. --------- Co-authored-by: sgouezel <[email protected]>
callesonne
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 16, 2024
In leanprover/lean4#4061, well-founded definitions become irreducible by default, and hence some `rfl` proofs stop working. This pre-emptively backports some of the adaptations from #12853.
callesonne
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 16, 2024
leanprover/lean4#4061 results in well-founded definitions being irreducible by default. This PR robustifies some proofs. (Sometime over-robust: we're going to keep `minFacAux` as semireducible for now, so e.g. `Nat.Prime 5` will still be decidable.)
grunweg
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 17, 2024
In leanprover/lean4#4061, well-founded definitions become irreducible by default, and hence some `rfl` proofs stop working. This pre-emptively backports some of the adaptations from #12853.
grunweg
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 17, 2024
leanprover/lean4#4061 results in well-founded definitions being irreducible by default. This PR robustifies some proofs. (Sometime over-robust: we're going to keep `minFacAux` as semireducible for now, so e.g. `Nat.Prime 5` will still be decidable.)
github-merge-queue bot
pushed a commit
to opencompl/lean-mlir
that referenced
this pull request
Aug 27, 2024
Function `splitOn` is defined using `splitOnAux`, which is defined by well-founded recursion and marked @[irreducible] by default. As [advised](leanprover/lean4#4061), we set `splitOnAux` back to semireducible by using `unseal` to use it in `DCExample`. CC: @ymherklotz @alexkeizer --------- Co-authored-by: Tobias Grosser <[email protected]>
This was referenced Aug 28, 2024
AtticusKuhn
pushed a commit
to opencompl/lean-mlir
that referenced
this pull request
Sep 2, 2024
Function `splitOn` is defined using `splitOnAux`, which is defined by well-founded recursion and marked @[irreducible] by default. As [advised](leanprover/lean4#4061), we set `splitOnAux` back to semireducible by using `unseal` to use it in `DCExample`. CC: @ymherklotz @alexkeizer --------- Co-authored-by: Tobias Grosser <[email protected]>
3 tasks
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.
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 .allwhen producingthe 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 make1 % nreduce definitionally, so that1as aFin 2literalworks nicely. Theorems with larger
Finliterals tend to need aunseal Nat.modCorerefactor: make 1 % n reduce without well-founded recursion #4098
List.ofFnrewritten to be structurally recursive and not go viaArray.ofFn:refactor: structurally recursive List.ofFn leanprover-community/batteries#784
Alternative designs explored were
Making
WellFounded.fixirreducible.One benefit is that recursive functions with equal definitions (possibly after
instantiating fixed parameters) are defeq; this is used in mathlib to relate
OrdinalApprox.gfpApproxwith.lfpApprox.But the downside is that one cannot use
unsealin atargeted 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 goodreason.
Defining
WellFounded.fixto unroll defintionally once before hitting a irreducibleWellFounded.fixF. This was explored in feat: make fixF irreducible, but allow fix to unroll once #4002. It shares most of the ups and downswith 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 thatthe majority of existing
rflproofs 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.fixirreducible; this is good evidence thatthe present PR is the way to go.
This fixes #3988