feat: optimized simp routine for let telescopes #8968
Conversation
Did you mean ”so zeta reducing only dependent lets” in the last sentence, referring to the behavior with |
kmill
force-pushed
the
kmill_simp_letToHave
branch
from
f8d88ed to
8945bb6
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
This PR adds the following features to `simp`: - A routine for simplifying `let` telescopes, like what leanprover#6220 did for `letFun` telescopes. Furthermore, simp converts `letFun`s into `have`s (nondependent lets), and we remove the leanprover#6220 routine. - A `+letToHave` configuration option (enabled by default) that converts lets into haves when possible, when `-zeta` is set. Previosuly Lean would need to do a full typecheck the bodies of `let`s, but the `letToHave` procedure can be faster, and it modifies the `let`s in an entire expression at once. - A `+zetaHave` configuration option, to turn off zeta reduction of `have`s specifically. The motivation is that dependent `let`s can only be dsimped by let, so zeta reducing just nondependent lets is a reasonable way to make progress.
kmill
force-pushed
the
kmill_simp_letToHave
branch
from
3c15843 to
af87540
Compare
leanprover-community-bot
added
the
builds-mathlib
| and then after that we have the versions that `simpHaveTelescope` actually uses, | ||
| which avoid this issue. | ||
| -/ | ||
| /- |
There was a problem hiding this comment.
@kmill I will add this issue to my todo list for next quarter. Could you please send me examples that expose the quadratic behavior? Have you checked whether the external checker written in Rust also has this performance issue?
There was a problem hiding this comment.
The deep telescopes at the ends of simpHave.lean and simpLetFunIssue.lean illustrate the issue. They also have a separate issue arising from using simp to unfold a recursive function that introduces a have to the telescope. (This is what the id id hack is addressing.)
I'll make some more examples for you next quarter.
I haven't had a chance to compare this with external checkers yet. I would be surprised if they did not have a similar issue.
|
|
||
| theorem have_body_congr' {α : Sort u} {β : Sort v} (a : α) {f f' : α → β} | ||
| (h : ∀ x, f x = f' x) : f a = f' a := | ||
| h a |
There was a problem hiding this comment.
@kmill As far as I understood, the theorems above are a workaround for the performance issue, and are not stated as you wanted to state them. If I understood it correctly, could you please include in the comment the desired version you wanted to have?
There was a problem hiding this comment.
The desired ones are in the comment. (I added the desired ones in a previous PR, and in this PR I commented them out to make sure I didn't accidentally use them.)
I haven't confirmed it yet, but I think there's a similar performance issue still with these ∀ x, f x = f' x hypotheses causing beta reductions. We can talk about it next week.
| deps.insert idx | ||
| else | ||
| deps | ||
| return { info with bodyDeps, bodyTypeDeps, body, bodyType, level } |
There was a problem hiding this comment.
We didn't have time to run a full SMT-LIB run on this yet but testing some of the files that have long let chains and are solved only in rewriting I can already see significant improvements yes.
Baseline:
λ time lake env .lake/build/bin/leanwuzla --disableEmbeddedConstraintSubst --timeout=1200 --maxSteps=100000000 --disableKernel --maxRecDepth=1048576 --maxHeartbeats=20000000000 /home/henrik/smtlib/non-incremental/QF_BV/sage/app7/bench_4994.smt2 <<<
Normalizing
unsat
lake env .lake/build/bin/leanwuzla --disableEmbeddedConstraintSubst 51.34s user 0.23s system 99% cpu 51.691 total
With this PR
λ time lake env .lake/build/bin/leanwuzla --disableEmbeddedConstraintSubst --timeout=1200 --maxSteps=100000000 --disableKernel --maxRecDepth=1048576 --maxHeartbeats=20000000000 /home/henrik/smtlib/non-incremental/QF_BV/sage/app7/bench_4994.smt2
Normalizing
unsat
lake env .lake/build/bin/leanwuzla --disableEmbeddedConstraintSubst 14.85s user 0.11s system 99% cpu 14.961 total
The fresh profile also looks quite sane to me (apart from the already known check assignment quick that's not as quick), none of the previous deep whnf calls during discrimination tree lookups and stuff like that is around anymore.
| by detecting a `simpHaveTelescope` proofs and removing the type hint. | ||
| -/ | ||
| def simpHaveTelescope (e : Expr) : SimpM Result := do | ||
| Prod.fst <$> withTraceNode `Debug.Meta.Tactic.simp (fun |
There was a problem hiding this comment.
@kmill Have you observed a positive impact on performance?
There was a problem hiding this comment.
Yes, and in particular
- for the
letEencoding ofhavethis is a huge win - it appears to be about as fast as (maybe marginally faster than) the
letFuntelescope code, while handling dependent types.
Though as we've discussed the kernel checking is slower (about 2x time), but that should be addressable eventually.
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
5 participants
This PR adds the following features to
simp:havetelescopes in a way that avoids quadratic complexity arising from locally nameless expression representations, like what feat: properlet_funsupport insimp#6220 did forletFuntelescopes. Furthermore, simp convertsletFuns intohaves (nondependent lets), and we remove the feat: properlet_funsupport insimp#6220 routine since we are moving away fromletFunencodings of nondependent lets.+letToHaveconfiguration option (enabled by default) that converts lets into haves when possible, when-zetais set. Previously Lean would need to do a full typecheck of the bodies oflets, but theletToHaveprocedure can skip checking some subexpressions, and it modifies thelets in an entire expression at once rather than one at a time.+zetaHaveconfiguration option, to turn off zeta reduction ofhaves specifically. The motivation is that dependentlets can only be dsimped by let, so zeta reducing just the dependent lets is a reasonable way to make progress. The+zetaHaveoption is also added to the meta configuration.simpis zeta reducing, it now uses an algorithm that avoids complexity quadratic in the depth of the let telescope.simp,whnf, andisDefEqnow all are consistent with how they apply thezeta,zetaHave, andzetaUnusedconfigurations.The
letToFunoption is addressing a TODO ingetSimpLetCase("handle a block of nested let decls in a single pass if this becomes a performance problem").Performance should be compared to before #8804, which temporarily disabled the #6220 optimizations for
letFuntelescopes.Good kernel performance depends on carefully handling the
haveencoding. Due to the way the kernel instantiates bvars (it does not beta reduce when instantiating), we cannot use congruence theorems of the form(have x := v; f x) = (have x ;= v'; f' x), since the bodies of thehaves will not be syntactically equal, which triggers zeta reduction in the kernel inis_def_eq. Instead, we work withf v = f' v', wherefandf'are lambda expressions. There is still zeta reduction, but only when converting between these two forms at the outset of the generated proof.