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.)

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.)

* 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 PR removes a rather ugly hack in the module system, exposing the
bodies of theorems whose type mention `WellFounded`.

The original motivation was that reducing well-founded definitions (e.g.
in `by rfl`) requires reducing proofs, so they need to be available.

But reducing proofs is generally fraught with peril, and we have been
nudging our users away from using it for a while, e.g. in #5182. Since
the module system is opt-in and users will gradually migrate to it, it
may be reasonable to expect them to avoid reducing well-founded
recursion in the process

This way we don't need hacks like this (which, without evidence, I
believe would be incomplete anyways) and we get the nice guarantee that
within the module system, theorems bodies are always private.

This PR makes theorems opaque in almost all ways, including in the
kernel.

Already now, because of proof irrelevance, theorems are almost never
unfolded. Furthermore, the import handling allows conflicting theorem
declaration with same type and different values. This is sound, but
would be confusing if the value, and thus the import order, matters for
completeness.

So with this change, a `theorem` becomes more like an `opaque`: It has a
value (for soundness), but it is never unfolded during reduction or type
checking. There are still some places in meta code that have to peek
into theorems (e.g. `FunInd`, wfrec processing), but these are code
transformations, not reduction.

One place where reducing proofs is necessary is reducing `Acc.rec`
eliminating into Type. With this change, all proofs that need to be
reducable that way have to be `def`, not `theorem`. This is already the
case due to the module system. This does not affect uses of `Acc` via
well-founded recursion, because that has already been made opaque in
#5182. This moves the reduction behavior of `Acc.rec` further into the
“supported by the theory but not relied upon by regular Lean“ corner.

Fixes #12804

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>