test: add mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen#12893
Merged
test: add mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen#12893
mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen#12893Conversation
…VCGen
This PR extends the sym-based `mvcgen'` tactic with two new modes:
1. `mvcgen' with <tac>`: run VCGen, then apply `<tac>` to each VC.
2. `mvcgen' with grind`: integrate grind into the VCGen loop for
incremental context internalization. Each VC inherits the parent's
E-graph state, so hypothesis processing is shared across sibling
VCs. This avoids O(n) re-internalization per VC.
The grind mode accepts the full grind configuration syntax
(`mvcgen' with grind (config := { ... }) [params]`).
Key implementation details:
- `WorkItem` carries `MVarId × Option Grind.Goal` through the worklist
- `VCGenM` wraps `GrindM` (which wraps `SymM`), so all existing
operations lift automatically
- `emitVC` uses `withNewMCtxDepth` + `resolveDelayedAssignments` to
isolate grind's internal mvars and produce clean proofs
- `internalizePending` shares hypothesis internalization before forking,
with rollback on inconsistency so children can construct their own
proofs
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This removes the reimplemented `resolveDelayedAssignments` and the manual `withNewMCtxDepth` + `mkFreshExprSyntheticOpaqueMVar` pattern in `emitVC`, replacing them with a call to `Grind.withProtectedMCtx`. On exception, `withProtectedMCtx` admits the goal, so we save/restore the `MetavarContext` to undo the admit and fall back to emitting an unsolved VC. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
# Conflicts: # tests/bench/mvcgen/sym/lakefile.lean # tests/bench/mvcgen/sym/lib/VCGen.lean
…gen' with grind` This PR adds a persistent `Sym.Simp.State` cache to VCGen and a `reassocNatAdd` simproc that rewrites `(a + m) + n → a + (m + n)` for Nat literals. Hypotheses and targets are simplified via `replaceLocalDeclDefEq` and `replaceTargetDefEq` (O(1)) before grind internalization, avoiding O(n) re-internalization of unsimplified `s + 1 + 1 + ...` chains. The persistent cache gives O(1) amortized simplification per VC since pointer-based cache hits on shared subexpressions avoid redundant work. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Mar 14, 2026
leanprover-bot
added
the
builds-manual
…impTarget` from sym VCGen This PR refactors `mvcgen' with grind` for clarity and correctness: - Replace `grindMode : Bool` with `Option GrindContext` in `VCGen.Context`, storing `hypSimpMethods` for configurable hypothesis simplification - Remove `normalizeLevelsExpr` in `work` (superseded by #12923) - Remove `simpTarget` — let grind simplify targets as it sees fit - Remove `tryCatchRuntimeEx` around `withProtectedMCtx` — let exceptions propagate - Extract `mkGrindParamsFromSyntax` helper - Revert unrelated `AddSubCancel` spec change from 8fc4ea8 - Use `fail` instead of `sorry` in `mvcgen' with grind` test cases Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
`getOptional?` requires exactly 1 child but `(&" with " tactic)?` produces 2 (keyword + tactic), so use `getNumArgs` instead. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
sgraf812
changed the title
mvcgen' with <tac> and mvcgen' with grind to sym-based VCGenmvcgen' with <tac> and mvcgen' with grind to sym-based VCGen
sgraf812
changed the title
mvcgen' with <tac> and mvcgen' with grind to sym-based VCGenmvcgen' with <tac> and mvcgen' with grind to sym-based VCGen
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 extends the sym-based
mvcgen'tactic with two new modes:mvcgen' with <tac>: run VCGen, then apply<tac>to each remaining VC.mvcgen' with grind: integrate grind into the VCGen loop for incremental context internalization. Each VC inherits the parent's E-graph state, so hypothesis processing is shared across sibling VCs, avoiding O(n) re-internalization per VC.The grind mode accepts the full grind configuration syntax (
mvcgen' with grind (config := { ... }) [params]).A persistent
Sym.Simpcache with areassocNatAddsimproc normalizes hypothesis types (e.g.,s + 1 + 1 + 1→s + 3) before grind internalization, achieving O(1) amortized simplification per VC.Benchmark results for GetThrowSet (
mvcgen' with grind):Kernel checking time grows superlinearly and is the dominant cost at larger sizes. This is a separate issue from VCGen performance.