This PR replaces the previous tactic configuration system with a
significantly more efficient one that supports custom configuration
syntaxes and processing. On a simple benchmark, configuration evaluation
takes 6.2% of the time it used to. The `declare_config_elab` command
generates a configuration elaborator that now directly constructs
configuration objects; previously it relied on `Meta.evalExpr'`, which
involved running a configuration through the full term elaboration,
compilation, and evaluation processes. The generated configuration
elaborators now also have the capability to do direct `Syntax`
evaluation in common cases, skipping term elaboration. Furthermore, the
elaborator accepts configurations more liberally: any user-defined
syntax that has the form of an `optConfig`-style configuration or
configuration item (including, e.g., `namedArgument`s) is accepted.
Import `Lean.Elab.ConfigEval` to use the system; see this module for
some documentation in addition to the docstrings in
`Lean.Elab.ConfigEval.Commands`. Furthermore, the `simp` tactic now also
has `(user.optionName := ...)` user configuration options, which can be
declared using a global `tactic.simp.user.optionName` option; use
`getUserConfigOption` and `withUserConfig` to access and set these in
metaprograms.
Other features:
- `declare_config_elab` creates a function that exposes an `init`
parameter for the configuration that will be modified. It also now has a
`where` clause, enabling defining custom handlers for specific keys.
- Elaborators can be given additional binders, to make parameterized
elaborators. This is used by `simp` and `grind ` to support multiple
default configurations with the correct expected type for `(config :=
...)` elaboration.
- The `EvalTerm` class supports direct evaluation of `Syntax`, skipping
term elaboration. The system will attempt to automatically derive this
class when generating the elaborator.
- In case `EvalTerm` does not recognize the term, then the syntax is
elaborated to an expression and an `EvalExpr` instance is applied to
evaluate the expression. The system will similarly automatically derive
these instances if possible.
- Automatic derivation is *transitive*. It is able to seek instances
through other instances; e.g. if it needs an `EvalTerm (List T)`
instance it will be able to reduce this to seeking an `EvalTerm T`
instance.
- The system is designed to be flexible, and the various components can
be combined to construct a configuration elaborator. There are also now
`declare_core_config_elab` and `declare_term_config_elab` for
conveniently generating elaborators for `CoreM` and `TermElabM`. The
difference is that the first takes an explicit flag for whether to log
exceptions, and the second uses the current `errToSorry` state.
**Warning:** if you use the `TermElabM` one from `TacticM`, it will be
unaware of the current `recover` state. The only differences between
these macros are the ways error recovery is handled per monad.
Other changes:
- `#reduce` tactic configuration now makes use of this system and has
more options
- The module `Lean.Elab.Tactic.ConfigSetter` is removed; the
`declare_config_elab`-family macros subsume its functionality.
- The module `Lean.Elab.Tactic.Config` is deprecated and will be
removed; migration notes appear in the module docs there. Import
`Lean.Elab.ConfigEval` instead.
- One of the mvcgen benchmarks got significantly slower, but it turned
out to be caused by the new tactic configuration elaboration no longer
resetting the MetaM caches. Adding an explicit `resetCache` into the
test driver fixed the benchmark.
### Notes for metaprogram authors
If you are using the module system, you just need a `meta import
Lean.Elab.ConfigEval` to use the macros, and it should serve as a
drop-in replacement to the previous system so long as
1. your configuration type is a `structure` with no parameters, indices,
or universes (only `Type` is supported);
2. default values are self-contained and not dependent on other fields;
and
3. all fields have types that are composed from `Option`, `List`,
`Array`, `String`, `DataValue`, and inductive types in `Type` with no
parameters or indices, whose fields are similarly composed.
The macros synthesize a self-contained configuration elaboration
procedure, analyzing the `EvalTerm` and `EvalExpr` instances that are
currently available or can be automatically derived. These are the
components of the system:
- `EvalTerm` instances provide `Term → TermElabM α` functions for
evaluation of raw syntax; these handle the common cases where an option
value is a identifier, application, or other simple expression. They are
responsible for adding TermInfo when info is enabled, to support hovers.
One can invoke derivation of a `EvalTerm T` instance with the
`ensure_eval_term_instance T` command (after `open scoped
Lean.Elab.ConfigEval`).
- `EvalExpr` instances provide `Expr → TermElabM α` functions for
evaluation of elaborated expressions; these handle cases where an option
value may require reduction to evaluate. Similarly, one can invoke
derivation of an `EvalExpr T` instance with the
`ensure_eval_expr_instance T` command. If needed, there's also
`derive_eval_expr_instance_using_meta_eval T` for creating a
`Meta.evalExpr'`-based evaluator.
- Functions like `ConfigEval.evalExprWithElab` compose `EvalTerm` and
`EvalExpr` instances into a single procedure that first attempts
`EvalTerm`, and, if that fails, applies the standard term elaborator and
then attempts `EvalExpr`. This way term elaboration can be skipped in
all but uncommon cases.
- Configuration item interpretation is through `ConfigEval.foldConfigM`,
which is a procedure with a lax specification for what counts as a
configuration item, calling the provided function on each recognized
configuration item. The idea is:
- Null nodes are lists of configurations
- One-argument nodes are considered to be wrappers like `optConfig` or
`configItem`
- Two-argument nodes of the form `("+"<|>"-") (atom<|>ident)` are
considered to be boolean options
- Five-argument nodes of the form `"(" (atom<|>ident) ":=" syntax ")"`
are considered to be general configuration items. (It only checks for
the presence of `(` and that there are two-to-five arguments.)
- Bare atoms are considered to be positive boolean options
- Configuration evaluation then uses `EvalConfigItem.set` on each item
produced by the fold, for an `EvalConfigItem` structure defined for the
given configuration type. The `def_eval_config_item` command can be used
to generate this structure. It analyzes which `EvalTerm` and `EvalExpr`
instances exist and derives missing ones, then builds an efficient
procedure to process configuration items and apply evaluators.
- Lastly, there are the `declare_core_config_elab`,
`declare_term_config_elab`, `declare_config_elab`, and
`declare_command_config_elab` macros for conveniently running the
`def_eval_config_item` command and constructing a self-contained
elaboration function.
The derivation procedures analyze which `EvalTerm`/`EvalExpr` instances
already exist and only derive the "leaf" instances that are necessary to
construct `EvalTerm` and `EvalExpr` instances. The derived instances are
made `private local` — since configuration elaborators are meant to be
self-contained, we decided not to let the additional instances be a side
effect of the macros. The instances can be globally added by manually
using the `ensure_*` commands.
The macros support making parameterized elaborators with arbitrary
additional binders. See `make_elab_grind_config` and
`make_elab_simp_config` in core Lean for examples of generating a single
elaborator that's used with multiple default value configurations.
To see how to create a key handler that matches all configuration keys
with a given prefix, see `make_elab_simp_config`.
There is a todo item at `Lean.Elab.ConfigEval.ReflectConfigItems` for
reflecting configurations back to syntax, which is not yet supported.
### Performance evaluation
A legacy configuration parser was temporarily added to
`Lean.Elab.Tactic.Grind.Config` using `declare_term_config_elab_legacy
elabGrindConfigLegacy Grind.Config`, and then this file was used for
measuring elaboration time:
```lean
import Lean
open Lean Elab Meta Tactic Parser
def cfgs : Array Syntax := Unhygienic.run do
return #[
← `(Tactic.optConfig| ),
← `(Tactic.optConfig| +clean),
← `(Tactic.optConfig| +trace +markInstances -lookahead -useSorry),
← `(Tactic.optConfig| (trace := true) (markInstances := true) (lookahead := false) (useSorry := false)),
← `(Tactic.optConfig| -trace (splits := 20) +revert (maxSuggestions := some 3) (ematch := 2)),
← `(Tactic.optConfig| (gen := 5) -reducible +splitImp -funCC),
← `(Tactic.optConfig| (config := { trace := true, lookahead := false, maxSuggestions := some 3 })),
]
def testGrindElab (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do
profileitM Exception "test grind elab" (← getOptions) do
let mut ematch := 0
for _ in [0:n] do
for cfg in cfgs do
let c ← Tactic.elabGrindConfig cfg
ematch := ematch + c.ematch
logInfo m!"sum = {ematch}"
def testGrindElabLegacy (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do
profileitM Exception "test grind elab legacy" (← getOptions) do
let mut ematch := 0
for _ in [0:n] do
for cfg in cfgs do
let c ← Tactic.elabGrindConfigLegacy cfg
ematch := ematch + c.ematch
logInfo m!"sum = {ematch}"
def runTest (info : Bool) (test : TacticM Unit) : TermElabM Unit := do
withEnableInfoTree info do
let mvar ← mkFreshExprMVar none
discard <| Tactic.run mvar.mvarId! test
set_option maxHeartbeats 0
set_option profiler true
set_option profiler.threshold 1
def iters : Nat := 1000
#eval runTest false <| testGrindElab cfgs iters
#eval runTest true <| testGrindElab cfgs iters
#eval runTest false <| testGrindElabLegacy cfgs iters
#eval runTest true <| testGrindElabLegacy cfgs iters
```
A representative output is
```
test grind elab took 315ms
test grind elab took 333ms
test grind elab legacy took 5.22s
test grind elab legacy took 5.33s
```
Computing `(315.0 + 333.0) / (5220 + 5330)` and rounding up to the
nearest tenth gives the 6.2% figure.
---
The #13426 draft PR includes some LSP modifications to support
completions for `simp` user configuration options.
This PR adds an experimental tactic `mvcgen'` that will soon replace
`mvcgen`. It has been reimplemented from the ground up using the new
`SymM`-based framework for efficient symbolic evaluation and can
outperform `mvcgen` by a factor of >100x for some synthetic benchmarks.
`mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions
currently are join point sharing, introduction of local specs and
smaller bugs.
The implementation of `mvgen'` used to live in the benchmark suite for
rapid prototyping; this commit merely moves it into the Lean toolchain.
Doing so results in an build time instruction count increase in
seemingly unrelated tests such as `elab/delayed_assign//instructions`;
the reason is that the builtin elaborator attribute now pulls in
substantially more import code on startup.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR fixes the semantics of `mvcgen' with grind`: it now logs an
error per VC that `grind` cannot close and throws at the end, instead of
silently leaving the unsolved VC as a residual. The previous
silent-fallback behaviour is preserved as `mvcgen' with (try grind)`,
which `elabPreTac` recognises and routes to the same efficient `.grind`
path with a `silent` flag.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds a `+debug` config option to `mvcgen'` and a
`BackwardRule.applyChecked` wrapper around `BackwardRule.apply`. On
apply failure with `+debug` set, the wrapper retries on the
`unfoldReducible`-normalized goal type; if the retry succeeds, an
earlier step missed a normalization and `mvcgen'` raises a hard error
naming the rule (auto-derived from `rule.expr.getAppFn` when available)
and showing the original vs. normalized types.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR cleans up `tests/bench/mvcgen/sym/lib/VCGen/Util.lean`.
- Drops the four `mkApp{Rev,RevRange,Range,N}S` helpers that were
vendored locally; they are now public in `Lean.Meta.Sym.Internal`
(`Lean.Meta.Sym.AlphaShareBuilder`).
- Moves `Std.HashMap.getDM` out of the root `Std.HashMap` namespace into
`namespace VCGen` and relocates it to `RuleCache.lean`, where its only
call sites live.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR fixes an issue in the `mvcgen'` prototype where user-provided
invariant values were elaborated against a goal type containing
reducible abbreviations like `PostShape.args ps`, baking
`(PostShape.args PostShape.pure)` into the assignment instead of `[]`.
After `tryInlineInvariant` confirms the user tactic assigned the
invariant metavariable, reduce its assignment with `unfoldReducible`.
Fixes the `mvcgen'` migration path for several `tests/elab/*` proofs
that had been blocked on the entailment-phase apply failure.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR brings the Sym-based `mvcgen'` to feature parity with `mvcgen`;
the only remaining gap is `+jp` (join-point handling).
The slight benchmark regressions are due to simplifying VCs out of
`SPred` form, hitting hardest on cases with linearly many VCs like
`PurePreCond`. The ~10% vcgen slowdown is worth it for the cleaner
user-visible VCs.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR removes a FIXME in Sym-based mvcgen' concerning a hardcoded step
limit for grind simplification. I tested that this is no longer
necessary even at highest setting for the GetThrowSetGrind benchmark.
This PR replaces eager let-expression zeta-reduction in the sym-based
mvcgen with on-demand unfolding that mirrors the production mvcgen's
behavior.
Previously, all let-expressions in the program head were immediately
zeta-reduced. Now, let-expressions are hoisted to the top of the goal
target, and the value is only inlined if it is duplicable (literals,
fvars, consts, `OfNat.ofNat`). Complex values are introduced into the
local context via `introsSimp`, preserving SymM's maximal sharing
invariants, and unfolded on demand when the fvar later appears as the
program head.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR switches the mvcgen worklist from BFS (queue) to DFS (stack)
ordering for subgoal processing.
With the new do elaborator, `if`-without-`else` generates asymmetric
bind depth between branches (`pure () >>= cont` is optimized to just
`cont` in the else branch). This caused BFS-based VC numbering to depend
on elaborator internals, swapping vc10/vc11 in test cases. DFS ordering
follows the syntactic program structure more naturally and is robust to
such bind-depth asymmetries.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces the manual `simpForallDomains` / `implies_congr`
machinery in `introsSimp` with `Sym.Simp.simpTelescope` as the
pre-combinator, which already handles simplifying forall telescope
domains.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `simplifying_assumptions` clause to the `mvcgen'` tactic
that allows users to specify Sym.simp rewrite theorems for simplifying
hypotheses during VC generation. The syntax is `mvcgen'
simplifying_assumptions [thm₁, thm₂, ...]`. This replaces the previous
approach of hardcoding `reassocNatAdd` in `mvcgen' with grind` mode,
making hypothesis simplification user-extensible and independent of
grind.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR refactors the sym-based VCGen (`tests/bench/mvcgen/sym`) to
separate concerns between
goal decomposition and VC discharge, following the architecture of
loom2's `mvcgen'`.
- `solve` now operates on plain `MVarId` with no knowledge of grind,
returning `List MVarId`
in `SolveResult.goals`.
- `work` handles grind E-graph internalization: after `solve` returns
multiple subgoals, it
calls `processHypotheses` on the parent goal to share context before
forking.
- `emitVC` dispatches on a new `PreTac` enum (`.none`, `.grind`,
`.tactic`) to try solving
each VC, replacing the previous inline grind logic and post-hoc tactic
loop in the elaborator.
- The redundant `WorkItem` wrapper (which duplicated `Grind.Goal`'s
`mvarId`) is removed; the
worklist operates directly on `Grind.Goal`.
- `GrindContext` is replaced by `PreTac` + `hypSimpMethods` fields in
`VCGen.Context`, cleanly
separating hypothesis simplification from the discharge strategy.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds iota reduction to the sym-based `mvcgen'` tactic by calling
`reduceRecMatcher?` before falling back to the match split backward
rule.
When a matcher/recursor has a concrete discriminant, it is reduced
directly
instead of constructing and applying a splitting backward rule, which is
significantly faster for benchmarks like `MatchIota` (previously
`MatchSplit`)
where `loop n` unrolls into `n` nested matches with known `Nat`
discriminants.
The old `MatchSplit` test case (concrete discriminants) is renamed to
`MatchIota`
and a new `MatchSplit` test case with symbolic discriminants (matching
on state)
is added to keep exercising the split backward rule code path.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extends the sym-based `mvcgen'` tactic with two new modes:
1. `mvcgen' with <tac>`: run VCGen, then apply `<tac>` to each remaining
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,
avoiding O(n) re-internalization per VC.
The grind mode accepts the full grind configuration syntax (`mvcgen'
with grind (config := { ... }) [params]`).
A persistent `Sym.Simp` cache with a `reassocNatAdd` simproc 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`):
- n=100: 400ms total, 180ms kernel
- n=250: 855ms total, 1.8s kernel
- n=500: 1.9s total, 11.8s kernel
Kernel checking time grows superlinearly and is the dominant cost at
larger sizes. This is a separate issue from VCGen performance.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR generalizes the sym MVCGen's match splitting from `ite`-only to
`ite`, `dite`, and arbitrary matchers. Previously, only `ite` was
supported; `dite` and match expressions were rejected with an error.
`mkBackwardRuleForSplit` uses `SplitInfo.splitWith` to build the
splitting proof. Hypothesis types are discovered via `rwIfOrMatcher`
inside the splitter telescope, and `TransformAltFVars.all` provides the
proper fvars for `mkForallFVars`. Subgoal type metavariables use
`mkFreshExprSyntheticOpaqueMVar` so that `rwIfOrMatcher`'s internal
`assumption` tactic cannot assign them.
Adds `DiteSplit`, `MatchSplit`, and `MatchSplitState` test cases and a
`vcgen_match_split` benchmark.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds support for simp/equational spec theorems in the SymM-based
`mvcgen'` tactic,
catching up with a feature that the original `mvcgen` has supported for
a long time.
Users can write `@[spec] theorem : get (m := StateT σ m) = fun s => pure
(s, s) := rfl`
instead of manually specifying equivalent Hoare triples. The equational
form is more
concise and natural for specs that simply unfold definitions.
The universe level normalization (`normalizeLevelsExpr`) applied in
`work` and the backward
rule constructors is a workaround; ideally this should be integrated
into
`preprocessMVar`/`preprocessExpr` in the SymM framework so all users
benefit.
Changes:
- Add `SpecTheoremKind` to distinguish triple vs simp specs in
`SpecTheoremNew`
- Add `mkSpecTheoremNewFromSimpDecl?` to create spec entries from
equational lemmas, filtering no-op equations
- Add `mkBackwardRuleFromSimpSpec` to build backward rules via
`Eq.mpr`/`congrArg`, with instance synthesis, projection reduction, and
`unfoldReducible` on the RHS
- Migrate simp theorems from `SimpTheorems` database during
`migrateSpecTheoremsDatabase`
- Normalize universe levels so structural matching in
`BackwardRule.apply` succeeds when `max u v` vs `max v u` arise from
different code paths
- Simplify `mkSpecContext` by removing the mock `simp` context
construction
- Use `mkBackwardRuleFromExpr` instead of `mkAuxLemma` for triple specs,
since the proof may contain free variables from the goal context
- Add `AddSubCancelSimp` benchmark case and test exercising the simp
spec code path
- Change `AddSubCancel` spec proofs from `mvcgen` to `mvcgen'`
(dogfooding)
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extracts the example programs from the sym mvcgen benchmarks
into
shared `Cases.*` modules so that both benchmarks and a new fast test
suite
can reuse them. It also renames `vcgen_deep_add_sub_cancel` to
`vcgen_add_sub_cancel_deep` for consistency.
The test suite (`test_vcgen.lean`) runs all cases at n=10, completing in
~2s vs minutes for the full benchmarks. It is wired up as a `lake test`
driver and integrated with the lean4 test/bench infrastructure via
`run_test`/`run_bench` scripts registered in `CMakeLists.txt`.
Benchmark output now uses aligned `CaseName(n):` labels. The `run_bench`
script extracts per-case vcgen and kernel timings into
`measurements.jsonl`.
Benchmarks run single-threaded (`LEAN_NUM_THREADS=1`) for
reproducibility.
`vcgen_get_throw_set` is excluded from benchmarks due to pathological
`instantiateMVars` behavior.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR changes the spec lookup procedure in Sym-based mvcgen so that
1. Spec candidates are sorted first before being filtered
2. Instead of filtering the whole set of candidates using
`spec.pattern.match?`, we take the first match with the highest
priority.
The second point means we will do a lot fewer matches when the highest
priority spec matches immediately. In this case, the one match is still
partially redundant with the final application of the backward rule
application. It would be great if could somehow specialize the backward
rule after it has been created. Still, this yields some welcome
speedups. Before and after for each.
```
vcgen_add_sub_cancel:
goal_1000: 865 ms, 1 VCs by grind: 228 ms, kernel: 435 ms
goal_1000: 540 ms, 1 VCs by grind: 229 ms, kernel: 426 ms
vcgen_ping_pong:
goal_1000: 458 ms, 0 VCs, kernel: 431 ms
goal_1000: 454 ms, 0 VCs, kernel: 443 ms (unchanged, because there is only ever one candidate spec)
vcgen_deep_add_sub_cancel:
goal_1000: 986 ms, 1 VCs by grind: 234 ms, kernel: 735 ms
goal_1000: 728 ms, 1 VCs by grind: 231 ms, kernel: 708 ms
vcgen_reader_state:
goal_1000: 746 ms, 1 VCs by sorry: 1 ms, kernel: 803 ms
goal_1000: 525 ms, 1 VCs by sorry: 1 ms, kernel: 840 ms
```
This PR adds support for generating and discharging postcondition VCs in
Sym-based `mvcgen`. It also adds a new benchmark case
`vcgen_ping_pong.lean` that tests this functionality. This benchmark
required a more diligent approach to maintain maximal sharing in goal
preprocessing. Goal preprocessing was subsequently merged into the main
VC generation function.
This PR improves the Sym VCGen such that we can use Sym.simp to unfold
definitions in the benchmark driver. To do so, it adds support for
zeta-reduction in the VCGen and ensures that proof terms are maximally
shared before being sent to the kernel.
This PR removes the unnecessary and potentially broken handling of
`let`s by zeta-reduction in Sym-based `mvcgen`.
It turns out to be unnecessary for the benchmarks so far, so there is a
lack of motivation to publicize `betaRevS` which would be needed to fix
it.
This PR shares the driver code from the Sym-based mvcgen benchmarks. It
also moves the `simp only [loop, step]` call out of the measured
section, so that we measure purely the overhead of VC generation.
The new benchmark results are as follows. All measurements for n=1000:
```
baseline_add_sub_cancel: 719.318425 ms, kernel: 382.708178 ms
vcgen_add_sub_cancel: 306.883079 ms, kernel: 455.050825 ms
vcgen_deep_add_sub_cancel: 543.350543 ms, kernel: 896.926298 ms
vcgen_get_throw_set: 669.566541 ms, kernel: 60754.202714 ms
```
Note that `vcgen_add_sub_cancel` sped up by 100% because we no longer
measure unfolding `loop` and `step`. The baseline didn't speed up as
much because it unfolded in the same `Sym.simp` call that also does
other rewrites, so there was no `simp` pass that could be eliminated.
This PR adds two more benchmarks for the Sym-based mvcgen prototype in
the style of `add_sub_cancel`.
The first is `deep_add_sub_cancel`, which is like `add_sub_cancel` but
with a much deeper monad stack:
```lean
abbrev M := ExceptT String <| ReaderT String <| ExceptT Nat <| StateT Nat <| ExceptT Unit <| StateM Unit
```
By specializing the specs for `get` and `set`, we get competitive
performance:
```
goal_100: 180.365086 ms, kernel: 79.634989 ms
goal_200: 313.465611 ms, kernel: 187.808631 ms
goal_300: 478.278585 ms, kernel: 270.210634 ms
goal_400: 638.884320 ms, kernel: 380.381127 ms
goal_500: 759.802772 ms, kernel: 472.662882 ms
goal_600: 933.575180 ms, kernel: 649.040746 ms
goal_700: 1174.367200 ms, kernel: 759.470010 ms
goal_800: 1298.866482 ms, kernel: 864.420171 ms
goal_900: 1475.315552 ms, kernel: 1008.662783 ms
goal_1000: 1627.957444 ms, kernel: 1078.627830 ms
```
Recall that `add_sub_cancel` had `goal_1000: 824.476962 ms, kernel:
477.069045 ms`, but that doesn't need to repeatedly unwrap 3 layers of
the monad.
The second benchmark is `get_throw_set`. Its kernel is
```lean
def step (lim : Nat) : ExceptT String (StateM Nat) Unit := do
let s ← get
if s > lim then
throw "s is too large"
set (s + 1)
def loop (n : Nat) : ExceptT String (StateM Nat) Unit := do
match n with
| 0 => pure ()
| n+1 => loop n; step n
def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄
```
It will generate `n+1` VCs. We get `n` VCs of the form
```
s✝ : Nat
_ : ¬0 < s✝
...
_ : n < s✝ + 1 ...<n times>... + 1
⊢ ⌜s✝ = 0⌝ ⊢ₛ ⌜False⌝ (s✝ + ...<n times>...)
```
and one VC of the form
```
⌜s✝ = 0⌝ ⊢ₛ ⌜s✝ + 1 + <n times> ... + 1 = n⌝
```
which can be discharged by `grind`, but presently are discharged with
`sorry`.
Statistics:
```
goal_100: 209.435869 ms, kernel: 128.768919 ms
goal_200: 386.639441 ms, kernel: 482.244717 ms
goal_300: 559.795137 ms, kernel: 1251.777405 ms
goal_400: 753.243978 ms, kernel: 3020.878177 ms
goal_500: 1014.939522 ms, kernel: 5182.120327 ms
goal_600: 1229.173622 ms, kernel: 9296.551442 ms
goal_700: 1410.024180 ms, kernel: 16655.954682 ms
goal_800: 1684.059305 ms, kernel: 32065.951705 ms
goal_900: 1905.602401 ms, kernel: 55299.942894 ms
goal_1000: 2172.823244 ms, kernel: 84082.492485 ms
```
Need to look at kernel times here, but tactic time looks about alright.
Using `grind` to discharge just `n=100` goals took 8s.
This PR improves and simplifies the SymM-based mvcgen prototype by
creating `BackwardRule.apply`-ready auxiliary theorems for spec
theorems. These auxiliary theorems have types that have reducible
definitions unfolded and shared, just like the rest of the SymM world
assumes. Furthermore, in order to aid kernel checking times,
definitional reductions leave behind expected type hints. With #12290,
we get the following numbers:
```
goal_100: 100.671964 ms, kernel: 34.104676 ms
goal_200: 152.650808 ms, kernel: 70.653251 ms
goal_300: 222.973242 ms, kernel: 105.874266 ms
goal_400: 294.032333 ms, kernel: 150.025106 ms
goal_500: 366.748098 ms, kernel: 193.483843 ms
goal_600: 442.509542 ms, kernel: 236.845115 ms
goal_700: 517.527685 ms, kernel: 268.804230 ms
goal_800: 601.657910 ms, kernel: 310.765606 ms
goal_900: 681.020759 ms, kernel: 357.428032 ms
goal_1000: 762.212989 ms, kernel: 403.789517 ms
```
The baseline is `shallow_add_sub_cancel`:
```
goal_100: 62.721757 ms, kernel: 22.109237 ms
goal_200: 140.118652 ms, kernel: 45.219512 ms
goal_300: 241.077690 ms, kernel: 78.779379 ms
goal_400: 363.274462 ms, kernel: 128.951250 ms
goal_500: 517.350791 ms, kernel: 155.498217 ms
goal_600: 678.291416 ms, kernel: 212.325487 ms
goal_700: 881.479043 ms, kernel: 258.690695 ms
goal_800: 1092.357375 ms, kernel: 351.996079 ms
goal_900: 1247.759480 ms, kernel: 319.197608 ms
goal_1000: 1497.203628 ms, kernel: 364.532560 ms
```
The latter is with the main solving loop in interpreter mode, but the
kernel checking times are still representative.
Earlier experiments suggest that the precompiled baseline performs at
roughly 650ms for `goal_1000`, so the new mvcgen is getting close.
This PR recognizes certain kinds of composite proof terms of the form
`hpre.trans hspec |> (wp prog).mono _ _ hpost` and abstracts them into
bespoke theorems. This should yield smaller proof terms. Sadly, kernel
checking time is unaffected, even regressing a bit. The number of shared
terms stays almost the same (+- a constant). Hence I deactivate the code
path in this patch. We keep the code, though, because it might be useful
in the future, also there are a few other improvements.
This PR adds a clone of the `mvcgen` tactic based on `SymM` and
evaluates it based on a ported `add_sub_cancel` benchmark. Notably, it
can reuse all the existing `@[spec]`-annotated theorems to generate VCs.
(It doesn't do control-flow splitting, simp rules on the program
expression or handling of lets; we'll get there.)
It is quite fast already, with the kernel being the bottle-neck:
```
goal_50: 69.524305 ms, kernel: 155.327778 ms
goal_100: 93.834221 ms, kernel: 407.370786 ms
goal_150: 131.364098 ms, kernel: 762.936720 ms
goal_200: 169.577172 ms, kernel: 1181.199093 ms
goal_250: 206.421738 ms, kernel: 1707.539380 ms
```
```
goal_200: 169.458637 ms, kernel: 1186.221085 ms
goal_400: 322.819718 ms, kernel: 3791.613854 ms
goal_600: 474.929013 ms, kernel: 7763.373757 ms
goal_800: 634.379422 ms, kernel: 13107.810430 ms
```
It is best compared to the `solveUsingSym <n> false true` measurements
of the SymM `add_sub_cancel` benchmark (`false`: without intermediate
eager simplification). For `n=200`, it reports
```
goal_200: 779.482300 ms, kernel: 742.097404 ms
```
suggesting that the generated proof term could be improved for kernel
reduction. (TODO.)
I'm unsure whether `solveUsingSym` is run in interpreted mode, so take
the >400% speedup with a grain of salt.
We can definitely conclude that VC generation time is currently not a
bottleneck compared to kernel checking time.
Plot for discharging goals of sizes 100..800:
<img width="1000" height="600" alt="Code_Generated_Image(1)"
src="https://github.com/user-attachments/assets/90e76a45-fa46-4d02-912a-c3355e2aa094"
/>
Plot comparing Kernel and Goal time:
<img width="1000" height="600" alt="Code_Generated_Image(2)"
src="https://github.com/user-attachments/assets/5849ba0f-1d83-4f2d-98dd-fa65b840bb4e"
/>
