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 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 implements iteration over ranges for `Fin` and `Char`.
To this end, we introduce machinery for pulling back lawfulness of
`UpwardEnumerable` along an injective map and study the function
`Char.ordinal : Char -> Fin Char.numCodePoints`.
This PR fixes the procedure for finding the mangled symbol name of boxed
variants of native functions. Previously, the wrong symbol name has been
used for names ending in `_`: For example `test_` mangles to `l_test__`
but `test_._boxed` mangles to `l_test___00__boxed`, not
`l_test_____boxed` which the compiler would previously wrongly use.
This probably didn't affect anybody though since the failure condition
is pretty rare: the name of a native function that the interpreter tries
to execute would've had to end in `_`.
This PR makes the automatic first token detection in tactic docs much
more robust, in addition to making it work in modules and other contexts
where builtin tactics are not in the environment. It also adds the
ability to override the tactic's first token as the user-visible name.
Previously, first token detection would look up the parser descriptor in
the environment and process its syntax. This would be incorrect for
builtin parsers, as well as for modules in which the definition is not
loaded. Now, it instead consults the Pratt parsing table for the
`tactic` syntax category. Tests are added that ensure this keeps working
in modules, and also that the first token of all tactics that ship with
Lean are either detected unambiguously or annotated to remove ambiguity.
Closes#12038.
This PR fixes a bug where the unknown identifier code actions were
broken in NeoVim due to the language server not properly setting the
`data?` field for all code action items that it yields.
This PR adds support for offset terms in `SymM`. This is essential for
handling equational theorems for functions that pattern match on natural
numbers in `Sym.simp`. Without this, it cannot handle simple examples
such as
```lean
def pw (n : Nat) : Nat :=
match n with
| 0 => 1
| n+1 => 2 * pw n
example : pw 4 = 16 := by
sym_simp [pw.eq_1, pw.eq_2]
example : pw (a + 2) = 2 * (2 * pw a) := by
sym_simp [pw.eq_2]
```
This PR adds `simpControl`, a simproc that handles control-flow
expressions such as `if-then-else`. It simplifies conditions while
avoiding unnecessary work on branches that won't be taken.
The key behavior of `simpControl`:
- Simplifies the condition of `if-then-else` expressions
- If the condition reduces to `True` or `False`, returns the appropriate
branch, and continue simplifying.
- If the condition simplifies to a new expression, rebuilds the
`if-then-else` with the simplified condition (synthesizing a new
`Decidable` instance), and mark it as "done". That is, simplifier main
loop will not visit branches.
- Does **not** visit branches unless the condition becomes `True` or
`False`
This is useful for symbolic simplification where we want to avoid
wasting effort
simplifying branches that may be eliminated after the condition is
resolved.
This PR also fixes a bug in `Sym/Simp/EvalGround.lean`, and adds some
helper functions.
This PR adds `Sym.Simp.evalGround`, a simplification procedure for
evaluating ground terms of builtin numeric types. It is designed for
`Sym.simp`.
Key design differences from `Meta.Simp` simprocs:
- Pure value extraction: `getValue?` functions are `OptionT Id` rather
than
`MetaM`, avoiding `whnf` overhead since `Sym` maintains canonical forms
- Specialized predicate lemmas: comparisons use pre-proved lemmas like
`Int.lt_eq_true` applied with `rfl`, avoiding `Decidable` instance
reconstruction at each call site
- Type dispatch via `match_expr`: assumes standard instances, no
synthesis
Supported types: `Nat`, `Int`, `Rat`, `Fin n`, `BitVec n`,
`UInt8/16/32/64`,
`Int8/16/32/64`.
Supported operations: arithmetic (`+`, `-`, `*`, `/`, `%`, `^`), bitwise
(`&&&`, `|||`, `^^^`, `~~~`), shifts (`<<<`, `>>>`), comparisons (`<`,
`≤`,
`>`, `≥`, `=`, `≠`, `∣`), and boolean predicates (`==`, `!=`).
This PR fixes an issue where attributes like `@[irreducible]` would not
be allowed under the module system unless combined with `@[exposed]`,
but the former may be helpful without the latter to ensure downstream
non-`module`s are also affected.
Fixes#12025
Drastically speeds up `isTracingEnabledFor` in the common case, which
has evolved from "no options set" to "`Elab.async` and probably some
linter options set but no `trace`".
## Breaking changes
`Lean.Options` is now an opaque type. The basic but not all of the
`KVMap` API has been redefined on top of it.
This PR allows 'Go to Definition' to look through reducible definition
when looking for typeclass instance projections.
Specifically, this means that using 'Go to Definition' on uses of
`GT.gt` will now yield the corresponding `LT` instance as well.
This PR splits up the SCC that the compiler manages into (potentially)
multiple ones after
performing lambda lifting. This aids both the closed term extractor and
the elimDeadBranches pass as
they are both negatively influenced when more declarations than required
are within one SCC.
This PR fixes an issue where go-to-definition would jump to the wrong
location in presence of async theorems.
While the elaborator does not explicitly depend on `FVar`s not being
reused between declarations, the language server turned out to do so. As
we would have to split the name generator in any case as soon as we add
any parallelism within proofs, we now do so for any async code in order
to uphold this invariant again.
---------
Co-authored-by: mhuisi <mhuisi@protonmail.com>
This PR adds support for simplifying the arguments of over-applied and
under-applied function application terms in `Sym.simp`, completing the
implementation for all three congruence strategies (fixed prefix,
interlaced, and congruence theorems).
This PR implements support for auto-generated congruence theorems in
`Sym.simp`, enabling simplification of functions with complex argument
dependencies such as proof arguments and `Decidable` instances.
Previously, `Sym.simp` used basic congruence lemmas (`congrArg`,
`congrFun`, `congrFun'`, `congr`) to construct proofs when simplifying
function arguments. This approach is efficient for simple cases but
cannot handle functions with dependent proof arguments or `Decidable`
instances that depend on earlier arguments.
The new `congrThm` function applies pre-generated congruence theorems
(similar to the main simplifier) to handle these complex cases.
This PR fixes the `floatLetIn` pass to not move variables in case it
could break linearity (owned variables being passed with RC 1). This
mostly improves the situation in the parser which previously had many
functions that were supposed to be linear in terms of `ParserState` but
the compiler made them non-linear. For an example of how this affected
parsers:
```lean-4
def optionalFn (p : ParserFn) : ParserFn := fun c s =>
let iniSz := s.stackSize
let iniPos := s.pos
let s := p c s
let s := if s.hasError && s.pos == iniPos then s.restore iniSz iniPos else s
s.mkNode nullKind iniSz
```
previously moved the `let iniSz := ...` declaration into the `hasError`
branch. However, this means that at the point of calling the inner
parser (`p c s`), the original state `s` needs to have RC>1 because it
is used later in the `hasError` branch, breaking linearity. This fix
prevents such moves, keeping `iniSz` before the `p c s` call.
This PR adds missing type checking for pattern variables during pattern
matching/unification to prevent incorrect matches.
Previously, the pattern matcher could incorrectly match expressions even
when pattern variable types were incompatible with the matched subterm
types. For example, a pattern like `x` where `x : BitVec 0` could match
any term, ignoring the specific type constraint on `x`.
This PR introduces a two-phase type checking approach:
1. **Static analysis** (`mkCheckTypeMask`): Identifies which pattern
variables require type checking based on their syntactic position.
Variables that appear only as arguments to function applications skip
checking (the application structure already constrains their types),
while variables in function position, binder contexts, or standalone
positions must be checked.
2. **Runtime validation**: During matching, when a pattern variable is
assigned, its type is checked against the matched subterm's type if
flagged by the mask. Checking uses `withReducible` to balance soundness
and performance.
The PR also adds helper functions for debugging (`Sym.mkMethods`,
`Sym.simpWith`, `Sym.simpGoal`) and fixes a minor issue where
`Theorem.rewrite` could return `.step` with identical expressions
instead of `.rfl`.Body:
This PR fixes a panic that occurred when a theorem had a docstring on an
auxiliary definition within a `where` clause.
Reproducer:
```lean
theorem foo : True := aux where /-- -/ aux := True.intro
```
The issue was that `asyncMayModify` used `.any` to check if a nested
declaration could have its extension state modified, which returned
`false` when the declaration wasn't yet in `asyncConsts`. Using `.all`
instead returns `true` for `none` (vacuously true), allowing
modification
of extension state for nested declarations that haven't been added to
`asyncConsts` yet.
Closes#11799🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR fixes library suggestions to include private proof-valued
structure fields.
Private proof-valued structure fields (like `private size_keys' :
keys.size = values.size`) generate projections with `_private.*` mangled
names. These were being filtered out by `isDeniedPremise` because
`isInternalDetail` returns true for names starting with `_`.
The fix allows private names through by checking `!isPrivateName name`,
following the pattern from #11946. This enables `grind +suggestions` to
discover and use private proof-valued structure fields from the current
module.
Soon I would like to fix the semantics of `isInternalDetail`, as the
current behaviour is clearly wrong, but as there are many call sites, I
would like to get the behaviour of tactics correct first.
Also switches `currentFile` to use `wasOriginallyTheorem` instead of
matching on `.thmInfo`, which correctly identifies both theorems and
proof-valued projections.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds a new `first_par` tactic combinator that runs multiple
tactics in parallel and returns the first successful result (cancelling
the others).
The `try?` tactic's `atomicSuggestions` step now uses `first_par` to try
three grind variants in parallel:
- `grind? +suggestions` - uses library suggestion engine
- `grind? +locals` - unfolds local definitions from current file
- `grind? +locals +suggestions` - combines both
This leverages `TacticM.parFirst` which already provides the "first
success wins" parallel execution with cancellation.
### Depends on
- [x] depends on: #11946🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds a `+locals` configuration option to the `simp`, `simp_all`,
and `dsimp` tactics that automatically adds all definitions from the
current file to unfold.
Example usage:
```lean
def foo (n : Nat) : Nat := n + 1
-- Without +locals, simp doesn't know about foo
example (n : Nat) : foo n = n + 1 := by simp -- fails
-- With +locals, simp can unfold foo
example (n : Nat) : foo n = n + 1 := by simp +locals -- succeeds
```
The implementation iterates over `env.constants.map₂` (which contains
constants defined in the current module) and adds definitions to unfold.
Instance definitions and internal details are filtered out.
**Note:** For local theorems, use `+suggestions` instead, which will
include relevant local theorems via the library suggestion engine.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
