This PR implements a cache for the positions of class universe level
parameters that only appear in output parameter types.
During type class resolution, the cache key for a query like
`HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of
the specific metavariable IDs in output parameter positions. To achieve
this, output parameter arguments are erased from the cache key. However,
universe levels that only appear in output parameter types (e.g., `?u`
corresponding to the result type's universe) must also be erased to
avoid cache misses when the same query is issued with different universe
metavariable IDs.
This function identifies which universe level parameter positions are
"output-only" by collecting all level param names that appear in
non-output parameter domains, then returning the positions of any level
params not in that set.
**Remark**: This PR requires a manual update stage0 because it changes
the structure of our .olean files.
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 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 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 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 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 fixes a bug in `System.Uri.fileUriToPath?` where it wouldn't use
the default Windows path separator in the path it produces.
It also adjusts the URI patching in the interactive test runner to be
more robust.
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 fixes a comment that said "implicit arguments" when the code
actually checks `isInstImplicit`, which is specifically for instance
implicit arguments (`[...]` binders), not all implicit arguments.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
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 extracts a `postCallback` helper so that only the actual callback
is inlined.
Part of the motivation here is to exclude these tracing frames from
flame graph profiles.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
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.
This PR fixes the verso hint that appears when using `sorry` in an
example block. It previously said: `` The `+error` flag indicates that
warnings are expected: +warning `` This PR replaces `error` with
`warning`. Fixes#12064
