search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

feat: well-founded definitions irreducible by default #4061

Closed nomeata closed 1 week ago

nomeata commented 2 weeks ago

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:

Alternative designs explored were

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 https://github.com/leanprover/lean4/issues/3988

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

nomeata commented 1 week ago

Whoohoo, mathlib is green!

After having discussed this with Leo, I will move forward with this approach.

We can reduce the impact on mathlib (seen here) by rewriting some functions using structural recursion (I’m looking at you, Array.ofFn.go and Nat.modCore), but that can happen in separate PRs.

Another possible way to reduce the impact a bit is if the decides tactics reduces more aggressively by default.

digama0 commented 1 week ago

The PR says "by default". Is there a way to change the default for a given definition? Is slapping @[semireducible] on the definition sufficient?

nomeata commented 1 week ago

The latter, see https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4061#diff-fd2963a2e28f1375d7ef28b499c216ed5b86dceabd79c37154edf5f6bdb62295R82

semorrison commented 1 week ago

Perhaps rebase now that #4053 is in a nightly? Not essential.

nomeata commented 1 week ago

No need to rebase for that, the diff will simply disappear if there is no conflict.

nomeata commented 1 week ago

I plan to merge this once https://github.com/leanprover/lean4/pull/4098 and https://github.com/leanprover-community/batteries/pull/784 have landed.

I should trigger a stage0 update right afterwards, else it won’t have an effect on the released stdlib.