perf: optimize simp calls across proof modules (~54s saved)#1646
Merged
Th0rgal merged 3 commits intofollowup/optimization-pr1639-no-codefrom Mar 19, 2026
Merged
perf: optimize simp calls across proof modules (~54s saved)#1646Th0rgal merged 3 commits intofollowup/optimization-pr1639-no-codefrom
Th0rgal merged 3 commits intofollowup/optimization-pr1639-no-codefrom
Conversation
Replace bare `simp` with `simp only` using explicit lemma lists to reduce elaboration overhead. StatementEquivalence: 19s→10s (47% faster). SupportedSpec: 71s→61s (14% faster). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Convert 119 bare simp [...] to simp only [...] and 4 simpa to simpa only, restricting lemma search to explicit arguments for faster elaboration. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Convert ~70 additional bare simp [...] to simp only [...] in the hot path (lines 1333-2077). Bool-returning proofs need Bool.or_false/Bool.false_or, List-returning proofs need List.nil_append/List.append_nil. Combined with previous optimization (71s→61s), total speedup is 90s→60s. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Th0rgal
merged commit 6d0b051
into
followup/optimization-pr1639-no-code
6 of 8 checks passed
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.
Summary
simp [...]tosimp only [...]across 3 proof modules, eliminating unnecessary default lemma database searchesBool.or_false/Bool.false_orandList.nil_append/List.append_nilsimpa→simpa onlysimp_all→simp_all only, 20simpa→simpa onlyTest plan
lake buildsorryoraxiomintroduced🤖 Generated with Claude Code
Note
Low Risk
Low risk: changes are proof-script refinements (
simp/simpa/simp_allto… only) intended to reduce simp search; they should not alter definitions or executable semantics, but could make proofs more brittle to future lemma changes.Overview
Speeds up proof compilation by systematically replacing broad
simp/simpa/simp_allinvocations withsimp only/simpa only/simp_all onlyinIRInterpreter.lean,SupportedSpec.lean, andStatementEquivalence.lean.Updates many termination/decreasing proofs and boolean/list normalization steps by explicitly listing the simp lemmas needed (e.g.,
Bool.or_false,List.nil_append), reducing simp’s default lemma-database search without changing the underlying theorems or interpreter behavior.Written by Cursor Bugbot for commit cb11130. This will update automatically on new commits. Configure here.