feat: Nat.{div,mod} to use fuel, not fix#7558
Merged
Conversation
This PR changes the definition of `Nat.div` and `Nat.mod` to use a structurally recursive, fuel-based implementation rather than well-founded recursion. This leads to more predicable reduction behavior in the kernel. `Nat.div` and `Nat.mod` are somewhat special because the kernel has native reduction for them when applied to literals. But sometimes this does not kick in, and the kernel has to unfold `Nat.div`/`Nat.mod` (e.g. in `lazy_delta_reduction` when there are open terms around). In these cases we want a well-behaved definition. We really do not want to reduce proofs in the kernel, which we want to prevent anyways well-founded recursion (to be prevented by #5182). Hence we avoid well-founded recursion here, and use a (somewhat standard) translation to a fuel-based definition. (If this idiom is needed more often we could even support it in Lean with `termination_by +fuel <measure>` rather easily.)
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 18, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 18, 2025
|
Mathlib CI status (docs):
|
github-merge-queue bot
pushed a commit
that referenced
this pull request
Mar 21, 2025
This PR marks `Nat.div` and `Nat.modCore` as `irreducible`, to recover the behavior from from before #7558. Fixes #7612. H't to @tobiasgrosser for the good bug report.
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 31, 2025
* fix * fix again * chore: bump to nightly-2025-03-15 * fix * harden script * chore: bump to nightly-2025-03-16 * Update lean-toolchain for testing leanprover/lean4#7516 * lake update * fixes for leanprover/lean4#7516 * fixes for leanprover/lean4#7516 * partial test fixes * fix stacks * "fix" eqns test * Remove neg instance, there is one upstream now * chore: bump to nightly-2025-03-17 * lake update * lake update * lint * Update lean-toolchain for testing leanprover/lean4#7522 * Update lean-toolchain for testing leanprover/lean4#5182 * Bump batteries for leanprover/lean4#5182 * simp works * Fewer unseal * Trigger CI for leanprover/lean4#5182 * max heartbeats * update test * Update lean-toolchain for testing leanprover/lean4#7519 * Update lean-toolchain for testing leanprover/lean4#7302 * Fix * fixes * Trigger CI for leanprover/lean4#5182 * chore: bump to nightly-2025-03-18 * Less rfl abuse * fix `compile_inductive%` regression * Trigger CI for leanprover/lean4#5182 * Trigger CI for leanprover/lean4#5182 * Trigger CI for leanprover/lean4#5182 * Adapt * process deprecations * Update lean-toolchain for testing leanprover/lean4#7558 * Adapt * deprecations * chore: bump to nightly-2025-03-19 * chore: fixes for leanprover/lean4#7519 * Update lean-toolchain for testing leanprover/lean4#7544 * lake update * fixes for leanprover/lean4#7544 * fixes for leanprover/lean4#7544 * fixes for leanprover/lean4#7544 * fixes for leanprover/lean4#7544 * Trigger CI for leanprover/lean4#7544 * . * cleaning up * chore: bump to nightly-2025-03-20 * update * deprecation/note about upstreamed version * fix * Update lean-toolchain for testing leanprover/lean4#7614 * chore: bump to nightly-2025-03-21 * Adapt back * fix test output * chore: bump to nightly-2025-03-22 * Merge master into nightly-testing * chore: adaptations for nightly-2025-03-22 * fix * Merge master into nightly-testing * protected * chore: bump to nightly-2025-03-24 * update batteries and aesop * fixes for count_cons_of_ne * fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context) * bump heartbeats in MathlibTest/observe * fix, deprecated * fix merge * Update lean-toolchain for testing leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes * chore: bump to nightly-2025-03-25 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * Trigger CI for leanprover/lean4#7672 * one fix * fixes * maxheartbeats * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * cleanups * . * chore: bump to nightly-2025-03-26 * update aesop * Update lean-toolchain for testing leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * maxHeartbeats * max heartbeats * invalidate cache * another heartbeats * bump batteries * deprecation * Update lean-toolchain for testing leanprover/lean4#7692 * Delete * chore: bump to nightly-2025-03-27 * update batteries * bump batteries * many more maxHeartbeats * chore: bump leantar v0.1.15 * invalidate cache * cache flush, take 2 * feat(Cache): root hash generation counter * 1-line fix * chore: bump to nightly-2025-03-28 * update deps * remove upstreamed * remove all adaptation notes, hooray * merge lean-pr-testing-7692 * fixes from Kevin's review --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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 PR changes the definition of
Nat.divandNat.modto use a structurally recursive, fuel-based implementation rather than well-founded recursion. This leads to more predicable reduction behavior in the kernel.Nat.divandNat.modare somewhat special because the kernel has native reduction for them when applied to literals. But sometimes this does not kick in, and the kernel has to unfoldNat.div/Nat.mod(e.g. inlazy_delta_reductionwhen there are open terms around). In these cases we want a well-behaved definition.We really do not want to reduce proofs in the kernel, which we want to prevent anyways well-founded recursion (to be prevented by #5182).
Hence we avoid well-founded recursion here, and use a (somewhat standard) translation to a fuel-based definition.
(If this idiom is needed more often we could even support it in Lean with
termination_by +fuel <measure>rather easily.)