feat: add contextDependent to Sym.simp Result with two-tier cache#12996
Merged
leodemoura merged 5 commits intomasterfrom Mar 20, 2026
Merged
feat: add contextDependent to Sym.simp Result with two-tier cache#12996leodemoura merged 5 commits intomasterfrom
contextDependent to Sym.simp Result with two-tier cache#12996leodemoura merged 5 commits intomasterfrom
Conversation
Replace the coarse `wellBehavedMethods` flag with per-result `contextDependent : Bool` tracking. Split the simp cache into `persistentCache` (context-independent results, survives binder entry) and `transientCache` (context-dependent results, cleared on binder entry). Propagate `contextDependent` through all combinators (congruence, transitivity, control flow, arrows, rewriting). The invariant: when combining sub-results, `cd` is the disjunction of all sub-results' flags — including `.rfl` results, since `simp` might take a completely different code path in another local context. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Tests cover: 1. Ground evaluation → persistent cache hit 2. Conditional rewrite with dischargeAssumption → transient only 3. Congruence with mixed cd/non-cd sub-results → cd propagates 4. Arrow/implication → cd propagates through domain simplification 5. Lambda/funext → cd propagates through body under binder 6. Control flow (ite) → cd propagates through condition
When fails (no matching hypothesis), it returns `.failed true`. This cd propagates through the rewrite result, so `n + 2` lands in the transient cache even though no rewrite occurred.
Exercises `simpForall'` with `withFreshTransientCache` — the body `n + 2 = 2 + n` is simplified context-dependently inside the binder. The binder type `Nat` hits persistent cache on second traversal.
isRfl was using `matches .rfl` which only matched when ALL fields have default values. With the new contextDependent field, .rfl false true (cd=true) no longer matched, causing Theorems.rewrite to incorrectly return cd .rfl results instead of continuing to the next theorem. Fix: match `.rfl false _` (done=false, ignore cd). Add unit tests for mkEqTransResult, andThen, orElse cd propagation.
leodemoura
added
changelog-language
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
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 adds per-result
contextDependenttracking toSym.Simp.Resultand splits the simplifier cache into persistent (context-independent) and transient (context-dependent, cleared on binder entry). This replaces the coarsewellBehavedMethodsflag.Key changes:
contextDependent : Bool := falsetoResult.rflandResult.stepState.cacheintopersistentCacheandtransientCachewellBehavedMethodsfromMethodswithoutModifyingCacheIfNotWellBehavedwithwithFreshTransientCacheDischargeResultto an inductive (.failed/.solved)dischargeAssumption(context-dependent discharger for testing)sym.simp.debug.cachetrace classcontextDependentthrough all combinators (congruence, transitivity, control flow, arrows, rewriting)mkRflResult/mkRflResultCDto avoid dynamic allocation of rfl resultsisRflto ignorecontextDependent(was silently broken by the extra field)Propagation invariant: when combining sub-results,
cdis the disjunction of ALL sub-results' flags — including.rflresults. Ifsimpreturned.rfl (contextDependent := true), it meanssimpmight take a completely different code path in another local context, so all downstream results must be marked context-dependent.