refactor: simplify grind canonicalizer and fix preprocessing issues#13149
Merged
leodemoura merged 7 commits intomasterfrom Mar 27, 2026
Merged
refactor: simplify grind canonicalizer and fix preprocessing issues#13149leodemoura merged 7 commits intomasterfrom
leodemoura merged 7 commits intomasterfrom
Conversation
The `Canon.State.canon : PHashMap Expr Expr` field was written to but never read. The canonicalizer uses a transient `HashMap` local to each `canonImpl` invocation for its expression cache, making the persistent field pure dead state. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
`proofCanon` deduplicated `Grind.nestedProof p _` terms by mapping canonicalized propositions to a single representative. This prevented cache sharing across goals because different proofs may reference different hypotheses, making the result context-dependent. Without `proofCanon`, structurally identical propositions with different proof terms become distinct in congruence closure. This adds a small number of extra terms but enables a simpler, shareable cache. The cost shrinks further once `GetElemV` eliminates most `nestedProof` terms. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
`propagateCtorHomo` constructs injectivity proofs via `mkAppOptM`, which
unifies implicit arguments at the current transparency. For indexed
inductive types like `Vector`, the implicit size argument may require
default transparency to unify (e.g., `({ toList := [] }.mapFinIdx f).size`
with `0`). Without this, `mkAppOptM` throws `throwAppTypeMismatch`.
Previously, `isDefEqBounded` in the canonicalizer masked this by eagerly
unifying such arguments during canonicalization. This fix addresses the
root cause, enabling the removal of `isDefEqBounded`.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
`abstractGroundMismatches?` constructs terms of the form `(fun x => body) arg` for congruence closure. Beta reduction in `preprocessLight` was collapsing these back to `body[arg/x]`, undoing the abstraction. Wrap the lambda with `Grind.abstractFn` (a non-reducible identity) so that no preprocessing pass can reduce the application. Congruence closure still detects the equality via congruence on the shared `abstractFn f`. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
`isDefEqBounded` was a fallback in `canonElemCore` that retried `isDefEq` at default transparency with a heartbeat budget. The only test that depended on it (`grind_lint_misc`) was fixed by using default transparency in `propagateCtorHomo` (commit b26706b). This also removes the `useIsDefEqBounded` and `parent` parameters from `canonElemCore`, simplifying the canonicalizer interface. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
`etaReduceAll` only performs structural eta reduction without any `MetaM` operations. Lower it to `CoreM` using `Core.transform`. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…cit cache `etaReduceWithCache` takes and returns a `HashMap ExprPtr Expr` cache explicitly, enabling the canonicalizer to thread a single cache across multiple expressions. The traversal eta-reduces lambdas eagerly: if a lambda is eta-reducible, it visits the reduced form directly instead of descending into the binder types. `etaReduceAll` is now a thin wrapper around `etaReduceWithCache`. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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 simplifies the
grindcanonicalizer by removing dead state and unnecessarycomplexity, and fixes two bugs discovered during the cleanup.
Changes
Canonicalizer cleanup:
Canon.State.canonfield — values were inserted but never read.The canonicalizer uses a transient
HashMaplocal to eachcanonImplinvocation.proofCanon— it deduplicatedGrind.nestedProofterms by mappingcanonicalized propositions to a single representative, but different proofs may
reference different hypotheses, making the result context-dependent and preventing
cache sharing across goals.
isDefEqBounded— a fallback that retriedisDefEqat default transparencywith a heartbeat budget. The one test that depended on it was actually masking a
transparency bug in
propagateCtorHomo.Bug fixes:
withDefaultformkAppOptMinpropagateCtorHomo(Ctor.lean) — theinjectivity proof construction needs default transparency to unify implicit
arguments of indexed inductive types like
Vector.Grind.abstractFngadget to protect lambda abstractions created byabstractGroundMismatches?from beta reduction during preprocessing. Withoutthis,
Core.betaReduceinpreprocessLightcollapses(fun x => body) argback to
body[arg/x], undoing the abstraction that congruence closure needs.Eta reduction infrastructure:
etaReduceAllfromMetaMtoCoreM— it only performs structuraloperations, no
MetaMneeded.etaReduceWithCachethat takes and returns an explicitHashMapcache,enabling callers to thread a single cache across multiple expressions.
The net effect on
Canon.Stateis removing 3 fields (canon,proofCanon)and the
isDefEqBoundedfunction, along with theuseIsDefEqBoundedandparentparameters fromcanonElemCore.