Offer relevant earlier theorems to the simp closer on request - #5
Merged
Merged
Conversation
Proofs in a development often cite a lemma proved earlier in the same file, and waterfall's simplifier cannot use such a lemma unless it is registered or supplied. With `premises := n`, the tactic selects up to `n` theorems of the current module by the constants their statements share with the goals, weighting rare constants more and ignoring logical connectives, instances, generated lemmas and theorems proved with `sorry`. At each node the `simp` closer runs its ordinary simplifier first and, only if that fails, retries with at most 16 selected theorems relevant to that node. The option adds no moves and no attempts; `grind` is unchanged. It is off by default. Evaluation on the lean-waterfall case studies (Lean 4.30.0, Luddy cluster). Every existing proof is left as written and nothing is admitted. Existing proofs. A clean build of all case studies passes with the default, as with main. A default of 4 instead makes 24 waterfall calls in 13 modules fail (LF IndProp, Rel, Imp; PLF Equiv, Smallstep, Records, Sub; VFA Multiset, SearchTree, Queue, Redblack, Color; ProofAgentsDemo SmallStep). Giving 64 theorems to both leaf solvers broke many more and tripled build time, and the per-node simp fallback with a default of 64 broke 18 modules. Manual proofs. Before each theorem whose proof does not call waterfall, the probe inserts `example <same statement> := by waterfall ...`, so the example sees exactly the original proof's context and has its own heartbeat budget. | Corpus | Manual proofs | `waterfall` | `waterfall (premises := 64)` | | --- | ---: | ---: | ---: | | SF LF | 97 | 1 | 11 | | SF PLF | 279 | 0 | 2 | | SF VFA | 64 | 1 | 1 | | ACL2 case studies | 60 | 26 | 27 | | DVH compiler | 57 | 18 | 23 | | Proof agents demo | 27 | 4 | 4 | | Total | 584 | 50 | 68 | The option gains 19 goals and loses 1. The inserted examples took 11,655 s against 8,590 s, mostly in searches that fail either way. Two files are not counted: VFA Queue (3 manual proofs) crashes creating threads under the cluster's limits, and ProofAgentsDemo Reduction (48) crashed that way in the option's run. Why it is off by default. Two effects make any nonzero default lose proofs. First, every node where the ordinary simplifier fails pays for a second call. The lost goal, Redblack2006 `nonempty_ins`, is proved by `waterfall` in 547 attempts and 143.7M heartbeats; with the option it used 199.96M heartbeats by attempt 372 and reached the 200M limit. Second, a closure the extra lemmas find sends the search down a branch it did not take before; when that branch fails, its attempts are spent, and several calls exhaust 1000 attempts without any heartbeat problem.
samth
changed the title
samth
force-pushed
the
feat/relevant-premises
branch
from
September 28, 2026 17:32
9218b22 to
8086fd2
Compare
The premise selector dropped every private theorem, because Lean treats private names as internal details, and it let generated matcher congruence equations take slots. Judge a private theorem by the name its user wrote, and skip matcher lemmas. Candidates now also include the public theorems of imported modules whose names share the current module's root, computed once per module. Only the leading candidates are checked for sorry, since that check walks the whole proof.
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.
Waterfall can now retrieve earlier rewrite lemmas without listing each one explicitly.
premises := nselects up tonrelevant earlier theorems and offers them to a fallbacksimp_allcloser after ordinary simplification fails. Selection uses shared vocabulary, weighted by rarity. The option remains off by default.The scope includes the current module and public imported theorems sharing its module root.
premiseModulesadds imported module prefixes when a development spans several roots:This includes already imported
LFhelpers when working in aTSchapter. It does not import modules. Private current-module lemmas are eligible; imported private lemmas, generated declarations and directly admitted proofs are excluded. Scope is included in the import-cache key.The selected pool is filtered for each residual goal, preserving its original ranking. There is no second, hidden sixteen-lemma cap: increasing
premisesincreases the number the closer can actually use. The fallback adds no proof-search moves; grind and ordinary rule application are unchanged. Generated proposition recursors such asHasType.brecOnno longer occupy premise slots.Focused Penn SF validation
Penn source
dcf44331b94b0918ec9655c06a459390e3924177, Lean 4.33.1, CPU nodekj, one thread per proof, effort 1000, enclosing limit 200 million raw heartbeats. Timings are internal single-run measurements.NatList.reverse_appendNatList.reverse_involutiveThe failure was concrete:
nil_appendranked twentieth and was never offered despite a pool of 64. Both revised proofs use onlywaterfall (premises := 64). They were checked together in the intact upstream chapter; neither transitive axiom set containssorryAx. No source-specific theorem names or rules were added to the implementation.Tests cover cross-root imported helpers, alternating scopes in one file, private and generated declarations, and a proof requiring lemmas beyond the former cap. Focused build and intact-source verification pass. The full package test suite and the Lean 4.30.0 / 4.33.1 CI matrix validate the final revision separately.
Earlier corpus evaluation
Before the follow-up changes, a probe of 584 manual goals found 50 proofs without premises and 68 with premises: 19 gains and one loss. Increasing retrieval recall did not produce further successes. Nonzero defaults also regressed existing case-study proofs through extra solver cost and changed finite-budget search paths. Those results explain the default of zero; the 584-goal probe has not been rerun for this follow-up, and is not a score for the revised filter or larger effective pools.
Larger pools can still slow or lose finite-budget proofs. Reranking at every node traded successes on the Penn examples and was not retained. Giving all retrieved names to every solver exhausted the weakening heartbeat budget and was not retained. Cross-root retrieval makes the weakening helper available but does not by itself solve the remaining induction-ordering problem. Search-ordering and substitution investigations are separate experiments, not changes to this PR.