This PR reorganizes the monad hierarchy for symbolic computation in
Lean.
## Motivation
We want a clean layering where:
1. A foundational monad (`SymM`) provides maximally shared terms and
structural/syntactic `isDefEq`
2. `GrindM` builds on this foundation, adding E-graphs, congruence
closure, and decision procedures
3. Symbolic execution / VCGen uses `GrindM` directly without introducing
a third monad
## Changes
The core symbolic computation layer still lives in `Lean.Meta.Sym`. This
monad (`SymM`) provides:
- Maximally shared terms with pointer-based equality
- Structural/syntactic `isDefEq` and matching (no reduction, predictable
cost)
- Monotonic local contexts (no `revert` or `clear`), enabling O(1)
metavariable validation
- Efficient `intro`, `apply`, and `simp` implementations
The name "Sym" reflects that this is infrastructure for symbolic
computation: symbolic simulation, verification condition generation, and
decision procedures.
### Updated hierarchy
```
Lean.Meta.Sym -- SymM: shared terms, syntactic isDefEq, intro, apply, simp
Lean.Meta.Grind -- GrindM: E-graphs, congruence closure (extends SymM)
```
Symbolic execution is a usage pattern of `GrindM` operating on
`Grind.Goal`, not a separate monad. This keeps the API surface minimal:
users learn two monads, and VCGen is "how you use `GrindM`" (for users
that want to use `grind`) rather than a third abstraction to understand.
This PR fixes an issue where `grind` failed to prove `f ≠ 0` from `f * r
≠ 0` when using `Lean.Grind.CommSemiring`, but succeeded with
`Lean.Grind.Semiring`.
The `propagateMul` propagator handles `0 * a = 0` and `a * 0 = 0` rules
for semirings that don't have full ring support in grind. Previously,
`CommSemiring` was excluded because it uses a ring envelope for
normalization, but that approach doesn't propagate these equalities back
to the original terms. Now `CommSemiring` also uses `propagateMul`.
Reported as
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20failure.20for.20CommSemiring.2C.20not.20Semiring🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds a `done` flag to the result returned by `Simproc`s in
`Sym.simp`.
The `done` flag controls whether simplification should continue after
the result:
- `done = false` (default): Continue with subsequent simplification
steps
- `done = true`: Stop processing, return this result as final
## Use cases for `done = true`
### In `pre` simprocs
Skip simplification of certain subterms entirely:
```
def skipLambdas : Simproc := fun e =>
if e.isLambda then return .rfl (done := true)
else return .rfl
```
### In `post` simprocs
Perform single-pass normalization without recursive simplification:
```
def singlePassNormalize : Simproc := fun e =>
if let some (e', h) ← tryNormalize e then
return .step e' h (done := true)
else return .rfl
```
With `done = true`, the result `e'` won't be recursively simplified.
This PR adds support for simplifying lambda expressions in `Sym.simp`.
It is much more efficient than standard simp for very large lambda
expressions with many binders. The key idea is to generate a custom
function extensionality theorem for the type of the lambda being
simplified.
This technique is compatible with the standard `simp` tactic, and will
be ported in a separate PR.
<img width="581" height="455" alt="image"
src="https://github.com/user-attachments/assets/5911dc6c-03f0-48ed-843b-b8cb4f67ee61"
/>
### `lambda` benchmark summary
| Lambda size | MetaM (ms) | SymM (ms) | Speedup |
|-------------|------------|-----------|---------|
| 50 | 22.7 | 0.74 | ~31× |
| 100 | 120.5 | 1.75 | ~69× |
| 150 | 359.6 | 2.90 | ~124× |
| 200 | 809.5 | 4.51 | ~180× |
This PR ensures that `Sym.simp` checks thresholds for maximum recursion
depth and maximum number of steps. It also invokes `checkSystem`.
Additionally, this PR simplifies the main loop. Assigned metavariables
and `zetaDelta` reduction are now handled by installing `pre`/`post`
methods.
This PR adds `getMatch` and `getMatchWithExtra` for retrieving patterns
from
discrimination trees in the symbolic simulation framework.
The PR also adds uses `DiscrTree` to implement indexing in `Sym.simp`.
This PR adds discrimination tree support for the symbolic simulation
framework.
The new `DiscrTree.lean` module converts `Pattern` values into
discrimination
tree keys, treating proof/instance arguments and pattern variables as
wildcards
(`Key.star`). Motivation: efficient pattern retrieval during rewriting.
This PR adds a `with_unfolding_none` tactic that sets the transparency
mode to `.none`, in which no definitions are unfolded. This complements
the existing `with_unfolding_all` tactic and provides tactic-level
access to the `TransparencyMode.none` added in
https://github.com/leanprover/lean4/pull/11810.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR makes `mvcgen with tac` fail if `tac` fails on one of the VCs,
just as `induction ... with tac` fails if `tac` fails on one of the
goals. The old behavior can be recovered by writing `mvcgen with try
tac` instead.
This PR adds `CongrInfo` analysis for function applications in the
symbolic simulator framework. `CongrInfo` determines how to build
congruence proofs for rewriting subterms efficiently, categorizing
functions into:
- `none`: no arguments can be rewritten (e.g., proofs)
- `fixedPrefix`: common case where implicit/instance arguments form a
fixed prefix and explicit arguments can be rewritten (e.g., `HAdd.hAdd`,
`Eq`)
- `interlaced`: rewritable and non-rewritable arguments alternate (e.g.,
`HEq`)
- `congrTheorem`: uses auto-generated congruence theorems for functions
with dependent proof arguments (e.g., `Array.eraseIdx`)
This PR changes `bv_decide`'s heuristic for what kinds of structures to
split on to also allow
splitting on structures where the fields have dependently typed widths.
For example:
```lean
structure Byte (w : Nat) where
/-- A two's complement integer value of width `w`. -/
val : BitVec w
/-- A per-bit poison mask of width `w`. -/
poison : BitVec w
```
This is to allow handling situations such as `(x : Byte 8)` where the
width becomes concrete after
splitting is done.
This PR adds an incremental variant of `shareCommon` for expressions
constructed from already-shared subterms. We use this when an expression
`e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that does
not preserve maximal sharing, but the inputs to that API were already
maximally shared. Unlike `shareCommon`, this function does not use a
local `Std.HashMap ExprPtr Expr` to track visited nodes. This is more
efficient when the number of new (unshared) nodes is small, which is the
common case when wrapping API calls that build a few constructor nodes
around shared inputs.
This PR fixes a bug in the new pattern matching procedure for the Sym
framework. It was not correctly handling assigned metavariables during
pattern matching.
It also improves the support for free variables.
This PR adds performance comparison tests between the new `SymM` monad
and the standard `MetaM` for `intros`/`apply` operations.
The tests solve problems of the form:
```lean
let z := 0; ∀ x, ∃ y, x = z + y ∧ let z := z + x; ∀ x, ∃ y, x = z + y ∧ ... ∧ True
```
using repeated `intros` and `apply` with `Exists.intro`, `And.intro`,
`Eq.refl`, and `True.intro`.
**Results show 10-20x speedup:**
| Size | MetaM | SymM | Speedup |
|------|-------|------|---------|
| 1000 | 226ms | 21ms | 10.8x |
| 2000 | 582ms | 44ms | 13.2x |
| 3000 | 1.08s | 72ms | 15.0x |
| 4000 | 1.72s | 101ms | 17.0x |
| 5000 | 2.49s | 125ms | 19.9x |
| 6000 | 3.45s | 157ms | 22.0x |
This PR adds `BackwardRule` for efficient goal transformation via
backward chaining in `SymM`.
`BackwardRule` stores a theorem expression, precomputed pattern for
fast unification, and argument indices that become new subgoals. The
subgoal ordering lists non-dependent goals first to match the behavior
of `MetaM.apply`.
`BackwardRule.apply` unifies the goal type with the rule's pattern,
assigns the goal metavariable to the theorem application, and returns
new subgoals for unassigned arguments.
This PR adds `num?` parameter to `mkPatternFromTheorem` to control how
many leading quantifiers are stripped when creating a pattern. This
enables matching theorems where only some quantifiers should be
converted to pattern variables.
For example, to match `mk_forall_and : (∀ x, P x) → (∀ x, Q x) → (∀ x, P
x ∧ Q x)` against a goal `∀ x, q x 0 ∧ q (f (f x)) y`, we use
`mkPatternFromTheorem ``mk_forall_and (some 5)` to create the pattern `∀
x, ?P x ∧ ?Q x`, keeping the outermost `∀` in the pattern rather than
converting it to a pattern variable.
This PR completes the new pattern matching and unification procedures
for the symbolic simulation framework using a two-phase approach.
**Phase 1 (Syntactic Matching):**
- Patterns use de Bruijn indices for expression variables and renamed
level params for universe variables
- Purely structural matching after reducible definitions are unfolded
- Universe levels treat `max`/`imax` as uninterpreted functions
- Proof arguments skipped via proof irrelevance
- Instance and binder constraints deferred to Phase 2
**Phase 2 (Pending Constraints):**
- Level constraints: structural equality with mvar assignment
- Instance constraints: `isDefEqI` (full `isDefEq` for TC synthesis)
- Expression constraints: `isDefEqS` with Miller pattern support
- Unassigned instance pattern variables synthesized via
`trySynthInstance`
**`isDefEqS` (Structural DefEq):**
- Miller pattern detection and assignment (`?m x y z := rhs` → `?m :=
fun x y z => rhs`)
- Scope checking via `maxFVar` to prevent out-of-scope assignments
- Optional zeta-delta reduction for let-declarations
- Proof irrelevance and instance delegation to `isDefEqI`
**Key optimizations:**
- `abstractFVars` skips metavariables and uses `maxFVar` for early
cutoff
- Per-pattern `ProofInstInfo` cache for fast argument classification
- Maximal sharing.
This PR implements `isDefEqS`, a lightweight structural definitional
equality for the symbolic simulation framework. Unlike the full
`isDefEq`, it avoids expensive operations while still supporting Miller
pattern unification.
**Key features:**
- Structural matching with optional zeta-delta reduction for
let-declarations
- Miller pattern detection and assignment (`?m x y z := rhs` → `?m :=
fun x y z => rhs`)
- Scope checking via `maxFVar` to prevent out-of-scope assignments
- Proof arguments skipped via proof irrelevance
- Instance arguments delegated to full `isDefEq` (need TC machinery)
- Universe levels treated structurally (`max`/`imax` as uninterpreted)
This PR adds optimized `abstractFVars` and `abstractFVarsRange` for
converting free variables to de Bruijn indices during pattern
matching/unification.
**Optimizations:**
- Metavariables are skipped (their contexts must not include abstracted
fvars)
- Subterms whose `maxFVar` is below the minimal abstracted fvar are
skipped via early cutoff
- Results are maximally shared via `AlphaShareBuilderM`
These optimizations are sound for Miller pattern matching where
metavariables are created before entering binders.
This PR implements `instantiateRevBetaS`, which is similar to
`instantiateRevS` but beta-reduces nested applications whose function
becomes a lambda after substitution.
For example, if `e` contains a subterm `#0 a` and we apply the
substitution `#0 := fun x => x + 1`, then `instantiateRevBetaS` produces
`a + 1` instead of `(fun x => x + 1) a`.
This is useful when applying theorems. For example, when applying
`Exists.intro`:
```lean
Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
```
to a goal of the form `∃ x : Nat, p x ∧ q x`, we create metavariables
`?w` and `?h`. With `instantiateRevBetaS`, the type of `?h` becomes `p
?w ∧ q ?w` instead of `(fun x => p x ∧ q x) ?w`.
This PR introduces a fast pattern matching and unification module for
the symbolic simulation framework (`Sym`). The design prioritizes
performance by using a two-phase approach:
**Phase 1 (Syntactic Matching)**
- Patterns use de Bruijn indices for expression variables and renamed
level params (`_uvar.0`, `_uvar.1`, ...) for universe variables
- Matching is purely structural after reducible definitions are unfolded
during preprocessing
- Universe levels treat `max` and `imax` as uninterpreted functions (no
AC reasoning)
- Binders and term metavariables are deferred to Phase 2
**Phase 2 (Pending Constraints)** [WIP]
- Handles binders (Miller patterns) and metavariable unification
- Converts remaining de Bruijn variables to metavariables
- Falls back to `isDefEq` when necessary
**Key design decisions:**
- Preprocessing unfolds reducible definitions and performs beta/zeta
reduction
- Kernel projections are expected to be folded as projection
applications before matching
- Assignment conflicts are deferred to pending rather than invoking
`isDefEq` inline
- `instantiateRevS` ensures maximal sharing of result expressions
**TODO:**
- Skip instance arguments during matching, synthesize later
- Skip proof arguments (proof irrelevance)
- Implement `processPending` for Phase 2 constraints
This PR implements `intro` (and its variants) for `SymM`. These versions
do not use reduction or infer types, and ensure expressions are
maximally shared.
This PR adds the function `Sym.instantiateS` and its variants, which are
similar to `Expr.instantiate` but assumes the input is maximally shared
and ensures the output is also maximally shared.
This PR adds the function `Sym.replaceS`, which is similar to
`replace_fn` available in the kernel but assumes the input is maximally
shared and ensures the output is also maximally shared. The PR also
generalizes the `AlphaShareBuilder` API.
This PR adds functions for creating maximally shared terms from
maximally shared terms. It is more efficient than creating an expression
and then invoking `shareCommon`. We are going to use these functions for
implementing the symbolic simulation primitives.
This PR adds support for incrementally processing local declarations in
`grind`. Instead of processing all hypotheses at once during goal
initialization, `grind` now tracks which local declarations have been
processed via `Goal.nextDeclIdx` and provides APIs to process new
hypotheses incrementally.
This feature will be used by the new `SymM` monad for efficient symbolic
simulation.
This PR adds the attributes `[grind norm]` and `[grind unfold]` for
controlling the `grind` normalizer/preprocessor.
The `norm` modifier instructs `grind` to use a theorem as a
normalization rule. That is, the theorem is applied during the
preprocessing step. This feature is meant for advanced users who
understand how the preprocessor and `grind`'s search procedure interact
with each other.
New users can still benefit from this feature by restricting its use to
theorems that completely eliminate a symbol from the goal. Example:
```lean
theorem max_def : max n m = if n ≤ m then m else n
```
For a negative example, consider:
```lean
opaque f : Int → Int → Int → Int
theorem fax1 : f x 0 1 = 1 := sorry
theorem fax2 : f 1 x 1 = 1 := sorry
attribute [grind norm] fax1
attribute [grind =] fax2
example (h : c = 1) : f c 0 c = 1 := by
grind -- fails
```
In this example, `fax1` is a normalization rule, but it is not
applicable to the input goal since `f c 0 c` is not an instance of `f x
0 1`. However, `f c 0 c` matches the pattern `f 1 x 1` modulo the
equality `c = 1`. Thus, `grind` instantiates `fax2` with `x := 0`,
producing the equality `f 1 0 1 = 1`, which the normalizer simplifies to
`True`. As a result, nothing useful is learned. In the future, we plan
to include linters to automatically detect issues like these. Example:
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
@[grind norm] axiom fax : f x = x + 2
@[grind norm ←] axiom fg : f x = g x
example : f x ≥ 2 := by grind
example : f x ≥ g x := by grind
example : f x + g x ≥ 4 := by grind
```
The `unfold` modifier instructs `grind` to unfold the given definition
during the preprocessing step. Example:
```lean
@[grind unfold] def h (x : Nat) := 2 * x
example : 6 ∣ 3*h x := by grind
```
This PR fixes a mismatch between the behavior of `foldlM` and
`foldlMUnsafe` in the three array
types. This mismatch is only exposed when manually specifying a `stop`
value greater than the size
of the array and only exploitable through `native_decide`.
The mismatch was introduced as part of
4ba21ea10c which introduced
`foldlMUnsafe` and thus likely a mistake when building the `unsafe`
implementation instead of a
specification mistake.
Closes#11773
This PR implements support for user-defined attributes at
`grind_pattern`. Suppose we have declared the `grind` attribute
```lean
register_grind_attr my_grind
```
Then, we can now write
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
axiom fg : g (f x) = x
grind_pattern [my_grind] fg => g (f x)
```
This PR uses the new support for user-defined `grind` attributes to
implement the default `[grind]` attribute.
A manual update-stage0 is required because it affects the .olean files.
This PR implements user-defined `grind` attributes. They are useful for
users that want to implement tactics using the `grind` infrastructure
(e.g., `progress*` in Aeneas). New `grind` attributes are declared using
the command
```lean
register_grind_attr my_grind
```
The command is similar to `register_simp_attr`. After the new attribute
is declared. Recall that similar to `register_simp_attr`, the new
attribute cannot be used in the same file it is declared.
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
@[my_grind] theorem fax : f (f x) = f x := sorry
example theorem fax2 : f (f (f x)) = f x := by
fail_if_success grind
grind [my_grind]
```
TODO: remove leftovers after update stage0
This PR allows `grind` to use `List.eq_nil_of_length_eq_zero` (and
`Array.eq_empty_of_size_eq_zero`), but only when it has already proved
the length is zero.
