This PR shifts the conversion from LCNF mono to lambda pure into the
LCNF impure phase. This is preparatory work for the upcoming refactor of
IR into LCNF impure.
The LCNF impure phase differs from the other LCNF phases in two crucial
ways:
1. I decided to have `Decl.type` be the result type as opposed to an
arrows from the parameter types to the result type. This is done because
impure does not have a notion of arrows anymore so keeping them around
for this one particular purpose would be slightly odd.
2. In order to avoid cluttering up the olean size LCNF impure saves only
the signature persistently to the disk. This is possible because we no
longer have inlining/specialization at this point of compilation so all
we need is typing information (and potentially other environment
extensions) to guide our analyses.
This PR implements RFC #12216: native computation (`native_decide`,
`bv_decide`) is represented in the logic as one axiom per computation,
asserting the equality that was obtained from the native computation.
`#print axiom` will no longer show `Lean.trustCompiler`, but rather the
auto-generated names of these axioms (with, for example,
`._native.bv_decide.` in the name). See the RFC for more information.
This PR introduces a common MetaM helper (`nativeEqTrue`) used by
`native_decide` and `bv_decide` alike that runs the computation and then
asserts the result using an axiom.
It also deprecated the `ofReduceBool` axioms etc.
Not included in this PR is infrastructure for enumerating these axioms,
prettier `#print axioms` (should we want his) and tactic concurrency.
Fixes#12216.
This PR refines upon #12106, by setting the `isRecursive` env extension
after adding the declaration, but before processing attributes like
`macro_inline` that want to look at the flag. Fixes#12268.
This PR fixes a unification issue that appeared in
`Lean.Meta.MkIffOfInductiveProp` machinery that was upstreamed from
Mathlib. Inside of `toInductive`, wrong free variables were passed,
which made it impossible to perform a unification in certain cases.
Closes#12215
This PR makes several small improvements to the list/array/vector API:
* It fixes typos in `Init.Core`.
* It adds `List.isSome_min_iff` and `List.isSome_max_iff`.
* It adds `grind` and `simp` annotations to various previously
unannotated lemmas.
* It adds lemmas for characterizing `∃ x ∈ xs, P x` using indices as `∃
(i : Nat), ∃ hi, P (xs[i])`, and similar universally quantified lemmas:
`exists_mem_iff_exists_getElem` and `forall_mem_iff_forall_getElem`.
* It adds `Vector.toList_zip`.
* It adds `map_ofFn` and `ofFn_getElem` for lists/arrays/vectors.
This PR adds the new transparency setting `@[instance_reducible]`. We
used to check whether a declaration had `instance` reducibility by using
the `isInstance` predicate. However, this was not a robust solution
because:
- We have scoped instances, and `isInstance` returns `true` only if the
scope is active.
- We have auxiliary declarations used to construct instances manually,
such as:
```lean
def lt_wfRel : WellFoundedRelation Nat
```
`isInstance` also returns `false` for this kind of declaration.
In both cases, the declaration may be (or may have been) used to
construct an instance, but `isInstance`
returns `false`. Thus, we claim it is a mistake to check the
reducibility status using `isInstance`.
`isInstance` indicates whether a declaration is available for the type
class resolution mechanism,
not its transparency status.
**We are decoupling whether a declaration is available for type class
resolution from its transparency status.**
**Remak**: We need a update stage0 to complete this feature.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes a bug on Windows with `IO.Process.spawn` where setting an
environment variable to the empty string would not set the environment
variable on the subprocess.
This PR fixes a bug where `grind?` suggestions would not include
parameters using local variable dot notation (e.g.,
`cs.getD_rightInvSeq` where `cs` is a local variable). These parameters
were incorrectly filtered out because the code assumed all ident params
resolve to global declarations. In fact, local variable dot notation
produces anchors that need the original term to be loaded during replay,
so they must be preserved in the suggestion.
Closes#12185🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
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 gives a simpler semantics to `noncomputable`, improving
predictability as well as preparing codegen to be moved into a separate
build step without breaking immediate generation of error messages.
Specifically, `noncomputable` is now needed whenever an axiom or another
`noncomputable` def is used by a def except for the following special
cases:
* uses inside proofs, types, type formers, and constructor arguments
corresponding to (fixed) inductive parameters are ignored
* uses of functions marked `@[extern]/@[implemented_by]/@[csimp]` are
ignored
* for applications of a function marked `@[macro_inline]`,
noncomputability of the inlining is instead inspected
# Breaking change
After this change, more `noncomputable` annotations than before may be
required in exchange for improved future stability.
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"
/>
This PR introduces a phase separation to the LCNF IR. This is a
preparation for the merge of
the old `Lean.Compiler.IR` and the new `Lean.Compiler.LCNF` framework.
The change parametrizes all relevant `LCNF` data structures over a
`Purity` parameter and
additionally carries around proofs that the `Purity` has certain values,
depending on what's
required. This is done as opposed to indexing the types over `Purity`
because we do (almost) never
have to store the `Purity` value for phase generic structures this way.
This PR reverts a lot of the changes done in #8308. We practically
encountered situations such as:
```
fun y (z) :=
let x := inst
mkInst x z
f y
```
Where the instance puller turns it into:
```
let x := inst
fun y (z) :=
mkInst x z
f y
```
The current heuristic now discovers `x` being in scope at the call site
of `f` and being used under a binder in `y` and thus blocks pulling in
`x` to the specialization, abstracting over an instance.
According to @zwarich this was done at the time either due to observed
stack overflows or pulling in computation into loops. With the current
configuration for abstraction in specialization it seems rather unlikely
that we pull in a non trivial computation into a loop with this. We also
practically didn't observe stack overflows in our tests or benchmarks.
Cameron speculates that the issues he observed might've been fixed
otherwise by now.
Crucial note: Deciding not to abstract over ground terms *might* cause
us to pull in computationally intensive ground terms into a loop. We
could decide to weaken this to just instance terms though of course even
computing instances might end up being non-trivial.
This PR updates docstrings and function signatures in order to complete
the transition from `Iter.Partial` to `Iter.Total` (extrinsically
terminating by default). It also deprecates `allowNontermination` and
adds `Iter.Total.atIdxSlow?`.
This PR ensures `dsimp` does not "simplify" instances by default. The
old behavior can be retrieved by using
```
set_option backward.dsimp.instances true
```
Applying `dsimp` to instances creates non-standard instances, and this
creates all sorts of problems in Mathlib.
This modification is similar to
```
set_option backward.dsimp.proofs true
```
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude <noreply@anthropic.com>
This PR fixes how we determine whether a function parameter is an
instance.
Previously, we relied on binder annotations (e.g., `[Ring A]` vs `{_ :
Ring A}`)
to make this determination. This is unreliable because users
legitimately use
`{..}` binders for class types when the instance is already available
from
context. For example:
```lean
structure OrdSet (α : Type) [Hashable α] [BEq α] where
...
def OrdSet.insert {_ : Hashable α} {_ : BEq α} (s : OrdSet α) (a : α) : OrdSet α :=
...
```
Here, `Hashable` and `BEq` are classes, but the `{..}` binder is
intentional, the
instances come from `OrdSet`'s parameters, so type class resolution is
unnecessary.
The fix checks the parameter's *type* using `isClass?` rather than its
syntax, and
caches this information in `FunInfo`. This affects several subsystems:
- **Discrimination trees**: instance parameters should not be indexed
even if marked with `{..}`
- **Congruence lemma generation**: instances require special treatment
- **`grind` canonicalizer**: must ensure canonical instances
**Potential regressions**: automation may now behave differently in
cases where it
previously misidentified instance parameters. For example, a rewrite
rule in `simp` that was
not firing due to incorrect indexing may now fire.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds the `introSubstEq` MetaM tactic, as an optimization over
`intro h; subst h` that avoids introducing `h : a = b` if it can be
avoided,
which is the case when `b` can be reverted without reverting anything
else. Speeds up the generation of `injEq` theorem.
This PR removes the LCNF testing framework. Unfortunately it never got
used much and porting it to
the extended LCNF structure now would be a bit of effort that would
ultimately be in vain.
This PR adds `mkBackwardRuleFromExpr` to create backward rules from
expressions, complementing the existing `mkBackwardRuleFromDecl` which
only works with declaration names.
The new function enables creating backward rules from partially applied
terms. For example, `mkBackwardRuleFromExpr (mkApp (mkConst
``Exists.intro [1]) Nat.mkType)` creates a rule for `Exists.intro` with
the type parameter fixed to `Nat`, leaving only the witness and proof as
subgoals.
The `levelParams` parameter supports universe polymorphism: when
creating a rule like `Prod.mk Nat` that should work at multiple universe
levels, the caller specifies which level parameters remain polymorphic.
The pattern's universe variables are then instantiated appropriately at
each application site.
Also refactors `Pattern.lean` to share code between declaration-based
and expression-based pattern creation, extracting `mkPatternFromType`
and `mkEqPatternFromType` as common helpers.
This PR activates `getElem?_pos` more aggressively, triggered by `c[i]`.
- [x] depends on: #12176🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR fixes a bug where delayed E-match theorem instances could cause
uniqueId collisions in the instance tracking map.
The `uniqueId` for theorem instances is generated using `numInstances`,
but this counter was only bumped for immediately activated instances
(`.ready` case), not for delayed instances (`.next` case). This caused
ID collisions:
1. Theorem A matches, becomes delayed, gets `uniqueId = N`
2. Counter isn't bumped (stays at N)
3. Theorem B matches next, gets `uniqueId = N` (same!)
4. B's entry overwrites A's entry in `instanceMap`
5. A's tracking is lost
This manifested as `grind?` and `finish?` producing `instantiate approx`
(meaning "we couldn't determine which theorems to use") instead of
proper `instantiate only [...]` with specific theorem lists.
The fix bumps `numInstances` for delayed instances too, ensuring each
theorem instance gets a truly unique ID.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds regression tests that catch issues where structures/classes
with class-typed fields produce HEq goals in `congr` instead of handling
Prop fields automatically.
Both tests pass on v4.28.0-rc1 (before isInstance detection changes).
## Test 1: Structure extending classes (mirrors Mathlib's GroupTopology)
```lean
structure MyGroupTopology (α : Type) extends MyTopology α, IsContinuousMul α
theorem MyGroupTopology.toMyTopology_injective {α : Type} :
Function.Injective (MyGroupTopology.toMyTopology : MyGroupTopology α → MyTopology α) := by
intro f g h
cases f
cases g
congr
```
**Failure mode:** `⊢ toIsContinuousMul✝¹ ≍ toIsContinuousMul✝`
## Test 2: Class with explicit class-typed field (mirrors Mathlib's
PseudoEMetricSpace)
```lean
class MyMetricSpace (α : Type) extends MyDist α where
dist_self : ∀ x : α, dist x x = 0
toMyUniformity : MyUniformity α -- explicit class-typed field (NOT from extends)
uniformity_dist : toMyUniformity.uniformity (fun x y => dist x y = 0)
protected theorem MyMetricSpace.ext {α : Type} {m m' : MyMetricSpace α}
(h : m.toMyDist = m'.toMyDist) (hU : m.toMyUniformity = m'.toMyUniformity) : m = m' := by
cases m
cases m'
congr 1 <;> assumption
```
**Failure mode:** `⊢ dist_self✝¹ ≍ dist_self✝` and `⊢ uniformity_dist✝¹
≍ uniformity_dist✝`
## Context
These tests are related to #12172, which changes instance parameter
detection from binder-based to `isClass?`-based. That change can affect
how structure fields are classified in congruence lemma generation.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds two benchmarks for mvcgen in the style of Leo's SymM
benchmarks.
While performance on add_sub_cancel_StateM.lean is in the same order of
magnitude as the corresponding MetaM benchmark, add_if_sub_StateM.lean
is far slower.
Measurements for add_sub_cancel:
```
goal_10: 245.576221 ms, kernel: 134.134182 ms
goal_20: 613.945320 ms, kernel: 115.453811 ms
goal_30: 1074.053596 ms, kernel: 179.076070 ms
goal_40: 1680.678302 ms, kernel: 252.066677 ms
goal_50: 2457.209584 ms, kernel: 293.974096 ms
goal_60: 3271.773330 ms, kernel: 368.394386 ms
goal_70: 3981.247921 ms, kernel: 434.297822 ms
goal_80: 5077.300540 ms, kernel: 507.047772 ms
goal_90: 6486.990060 ms, kernel: 556.952095 ms
goal_100: 7791.399986 ms, kernel: 623.605163 ms
```
Measurements for add_if_sub:
```
goal_2: 89.762349 ms, kernel: 43.320205 ms
goal_3: 190.655546 ms, kernel: 38.888499 ms
goal_4: 434.461936 ms, kernel: 75.234581 ms
goal_5: 1110.295284 ms, kernel: 161.698707 ms
goal_6: 3241.383031 ms, kernel: 326.137173 ms
goal_7: 11675.609970 ms, kernel: 684.907188 ms
```
Much room for improvement.
This PR makes the compiler produce C code that statically initializes
close terms when possible. This change reduces startup time as the terms
are directly stored in the binary instead of getting computed at
startup.
The set of terms currently supported by this mechanism are:
- string literals
- ctors called with other statically initializeable arguments
- `Name.mkStrX` and other `Name` ctors as they require special support
due to their computed field and occur frequently due to name literals.
In core there are currently 152,524 closed terms and of these 103,929
(68%) get initialized statically with this PR. The remaining 48585 ones
are not extracted because they use (potentially transitively) various
non trivial pieces of code like `stringToMessageData` etc. We might
decide to add special support for these in the future but for the moment
this feels like it's overfitting too much for core.
This PR adds `simpTelescope`, a simproc that simplifies telescope
binders (`have`-expression values and arrow hypotheses) but not the
final body. This is useful for simplifying targets before introducing
hypotheses.
This PR adds `simpArrowTelescope`, a simproc that simplifies telescopes
of non-dependent arrows (p₁ → p₂ → ... → q) while avoiding quadratic
proof growth.
When using `Expr.forallE` to represent nested implications, each nesting
level bumps de Bruijn indices in subterms, destroying sharing even with
hash-consing. For example, a free variable `x` gets different de Bruijn
representations at each depth, causing proof terms to grow.
`simpArrowTelescope` works by:
- Converting arrows to `Arrow p q` (a definitional wrapper)
- Simplifying each component
- Converting back to `→` form
Since `Arrow` arguments are not under binders, subterms remain identical
across nesting levels and can be shared.
The `simp_4` benchmark demonstrates the improvement:
With `forallE`: ~160ms, proof_size ≈ 173k
With `Arrow`: ~43ms, proof_size ≈ 16k
Tradeoff: `simpArrowTelescope` misses simplifications that depend on the
arrow structure (e.g., `p → p` to `True`), since post-methods aren't
applied to intermediate arrows. Thus, it is not used by default. to use
it, one has to set `simpArrowTelescope` as a `pre`-method.
This PR reverts #12000, which introduced a regression where `simp`
incorrectly rejects valid rewrites for perm lemmas.
The issue is that `NameGenerator.mkChild` creates names that don't
maintain the ordering assumption used by `acLt` for perm lemma
decisions. For example, after the change:
- Child generator creates names like `_uniq.102.2`
- Parent continues with `_uniq.7`
- But `Name.lt (.num (.num `_uniq 102) 2) (.num `_uniq 7)` is true
This causes fvars created later (in async tasks) to compare as smaller
than fvars created earlier, breaking the assumption that later fvars
compare greater according to `Name.lt`.
Fixes#12136.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds an API for building symbolic simulation engines and
verification
condition generators that leverage `grind`. The API wraps `Sym`
operations to
work with `grind`'s `Goal` type, enabling lightweight symbolic execution
while
carrying `grind` state for discharge steps.
New operations on `Goal`:
- `mkGoal`: create a `Goal` from an `MVarId`
- `introN`, `intros`: introduce binders
- `apply`: apply backward rules
- `simp`, `simpIgnoringNoProgress`: simplify using `Sym.Simp`
- `internalize`, `internalizeAll`: add hypotheses to the E-graph
- `grind`: attempt to close the goal using `grind`
- `assumption`: close by matching a hypothesis
A new test demonstrates the API on a stateful program with conditionals,
using `grind` to discharge arithmetic side conditions.
