perf: avoid expensive instance re-synthesis in cbv#14009
Draft
wkrozowski wants to merge 1 commit into
Draft
Conversation
This PR speeds up the `cbv` and `decide_cbv` tactics by up to 2x on `Decidable` evaluation workloads and significantly reduces elaborator and kernel unfolding (visible in `diagnostics` counters). Previously, rewriting a proposition argument inside an instance term forced the congruence machinery to re-synthesize a `Decidable` instance for the entire remaining proposition at every step, making evaluation of bounded quantifier instances quadratic. The `cbv` pre-pass now evaluates class-valued applications whose congruence theorem carries instance arguments directly via equations (`handleClassApp`), instead of first rewriting their arguments via congruence. `Decidable`-transport wrappers (`decidable_of_decidable_of_eq`, `decidable_of_decidable_of_iff`, `decidable_of_iff`, `decidable_of_iff'`) are evaluated by dedicated simprocs that evaluate the wrapped instance and rewrite the wrapper to `isTrue`/`isFalse` directly, justified by `Subsingleton (Decidable p)`. Instances that cannot be evaluated structurally (e.g. dependent matches over functions defined by well-founded recursion, which neither congruence nor kernel reduction can evaluate) fall back to deciding the underlying proposition (`handleStuckDecidable`). The `ite`/`dite`/`decide` control-flow simprocs additionally try synthesizing an instance for the rewritten condition when the original instance is stuck, preserving the previous behavior for opaque instances. On `tests/elab_bench/cbv_decide.lean`, evaluation time drops by ~1.8x and kernel-checking time of the produced proofs by ~1.6x. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
|
!bench |
|
Benchmark results for ddbe36b against efbd4b8 are in. There are significant results. @wkrozowski
Large changes (3✅)
Medium changes (1🟥)
Small changes (2✅, 5🟥)
|
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
2 participants
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.
This PR is an experiment in using Fable in optimising
cbv.