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 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 avoids a potential deadlock on shutdown of a Lean program when
the number of pooled threads has temporarily been pushed above the
limit.
There's a potential race between the finalizer "waking up everyone"
after setting `m_shutting_down = true` and a worker that is about to be
throttled because of concurrency limits.
- `m_max_std_workers = 1`, `m_std_workers.size() = 2`, and the queue
still has tasks.
- Finalizer sets `m_shutting_down = true` and calls `notify_all()` while
a worker is running a task (outside of the mutex).
- Worker finishes a task, re-enters the loop, sees work, and "should
wait" because `active >= max`.
- Worker then calls `wait()` after the notify and never wakes, so
`join()` in the finalizer hangs.
This PR avoids the worker being blocked by not `wait()`ing if we are
already shutting down. The code is restructured a bit for readability,
where the first section is "there's no work in the queue" and the next
section is "there is some work in the queue"
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 provides more lemmas about sums of lists/arrays/vectors,
especially sums of `Nat` or `Int` lists/arrays/vectors.
This change has been motivated by my experience solving
`human-eval-lean` problems. Sums, minima and maxima are frequently
required and the improvements provided in this PR make it easier to
verify such programming tasks.
Changes:
* Added lemmas that `sum` equals `foldl`/`foldr`.
* Generalized `sum_append_nat` and `sum_reverse_nat` lemmas so that they
are polymorphic, requiring only some type class instances about the list
elements' type. The polymorphic lemmas aren't simp- or grind-annotated
because I fear the instance synthesis overhead. However, the `Nat` and
`Int` specializations are annotated (see below). Note that as
`{Array,Vector}.min` do not exist, some lemmas can't be stated and were
omitted.
* Added `List.min_singleton` and `List.max_singleton` lemmas as they
were needed for some proofs.
* `Nat`-related:
* Moved all `{List,Array,Vector}.sum` lemmas that are specific for `Nat`
into their own module: `Init.Data.List.Nat.Sum`, `Init.Data.Array.Nat`
and `Int.Data.Vector.Nat`.
* Notably, moved `Nat.sum_pos_iff_exists_pos` and renamed it to
`List.sum_pos_iff_exists_pos_nat`. This is more consistent and made it
possible to add `Array` and `Vector` variants of this lemma.
* Added lemmas proving that `l.sum / l.length` lies between the minimum
and the maximum of a list.
* Added analogous lemmas for `Int` lists/arrays/vectors to parallel
modules: `Init.Data.List.Int.Sum`, `Init.Data.Array.Int` and
`Int.Data.Vector.Int`.
* Renamed `sum_eq_sum_toList` to `sum_toList`, which better represents
the theorem's content.
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 adds the function `Std.Iter.isEmpty` and proves the
specification lemmas `Std.Iter.isEmpty_eq_match_step` and
`Std.Iter.isEmpty_toList` if the iterator is productive.
The monadic variant on `Std.IterM` is also provided.
This PR introduces projected minima and maxima, also known as
"argmin/argmax", for lists under the names `List.minOn` and
`List.maxOn`. It also introduces `List.minIdxOn` and `List.maxIdxOn`,
which return the index of the minimal or maximal element. Moreover,
there are variants with `?` suffix that return an `Option`. The change
further introduces new instances for opposite orders, such as
`LE.opposite`, `IsLinearOrder.opposite` etc. The change also adds the
missing `Std.lt_irrefl` lemma.
This PR ensures we cache the result of `unfold_definition` definition in
the kernel type checker. We used to cache this information in a thread
local storage, but it was deleted during the Lean 3 to Lean 4
transition.
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 adds a "Stabilizing output" section to the `#guard_msgs`
docstring, explaining how to use `pp.mvars.anonymous` and `pp.mvars`
options to stabilize output containing autogenerated metavariable names
like `?m.47`.
This was prompted by discussion on Zulip about improving #mwe
documentation:
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/JacobiZariski.20is.20slow.2E/near/570739745🤖 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 the defining equality `Triple.iff` and uses that in
proofs instead of relying on definitional equality. It also introduces
`Triple.iff_conseq` that is useful for backward reasoning and introduces
verification conditions. Similarly, `Triple.entails_wp_*` theorems are
introduced for backward reasoning where the target is an stateful
entailment rather than a triple.
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 provides `Array` operations analogous to `List.min(?)` and
`List.max(?)`.
I had to prove a few auxiliary lemmas. Downstream in Batteries, which
already had `List.min` and `List.max`, I renamed their variants to
`List.rangeMin` and `List.rangeMax` in the PR testing branch. Their
version is more general in the sense that it has `start` and `stop`
autoParams, like `Array.foldl` has, but I think the futore belongs to
`Subarray.min` instead (which I haven't implemented yet).
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 `Init.Data.Dyadic.Instances` and `Init.Data.Dyadic.Inv`.
Previously, all declarations defined in boths file were private and not
exposed.
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>
Due to the way variable expansion and if interact in cmake, unquoted
variable expansions should essentially never be used inside if and may
lead to unexpected behavior. Also, quoted variable expansions can
usually be replaced by the unquoted variable name.
For more details, see this section in the cmake docs:
https://cmake.org/cmake/help/latest/command/if.html#variable-expansion
As one example of the kinds of issues that can occur with unquoted
variable expansions, consider this check from
`src/shell/CMakeLists.txt`, which tries to ensure that a test is only
run in non-WASM builds.
```cmake
if(NOT ${EMSCRIPTEN})
```
If the variable `EMSCRIPTEN` is empty or not defined (as is the case in
a non-WASM build), `${EMSCRIPTEN}` expands to 0 arguments, meaning the
check becomes
```cmake
if(NOT)
```
Since the `NOT` is unquoted, the if now tries to resolve it as a
variable. Since the variable `NOT` does not exist, the condition is
false and the test is never executed, even in non-WASM builds.
This PR provides the `Nat`/`Int` lemmas `x ≤ y * z ↔ (x + z - 1) / z ≤
y`, `x ≤ y * z ↔ (x + y - 1) / y ≤ z` and `x / z + y / z ≤ (x + y) / z`.
The PR is inspired by a `human-eval-lean` problem, the solution of which
required these lemmas.
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 adds theorems showing the consistency between `find?` and the
various index-finding functions. The theorems establish bidirectional
relationships between finding elements and finding their indices.
**Forward direction** (find? in terms of index):
- `find?_eq_map_findFinIdx?_getElem`: `xs.find? p = (xs.findFinIdx?
p).map (xs[·])`
- `find?_eq_bind_findIdx?_getElem?`: `xs.find? p = (xs.findIdx? p).bind
(xs[·]?)`
- `find?_eq_getElem?_findIdx`: `xs.find? p = xs[xs.findIdx p]?`
**Reverse direction** (index in terms of find?):
- `findIdx?_eq_bind_find?_idxOf?`: `xs.findIdx? p = (xs.find? p).bind
(xs.idxOf?)`
- `findFinIdx?_eq_bind_find?_finIdxOf?`: `xs.findFinIdx? p = (xs.find?
p).bind (xs.finIdxOf?)`
- `findIdx_eq_getD_bind_find?_idxOf?`: `xs.findIdx p = ((xs.find?
p).bind (xs.idxOf?)).getD xs.length`
All theorems are provided for `List`, `Array`, and `Vector` (where
applicable).
Requested at
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/show.20that.20Array.2Efind.3F.20and.20Array.2EfindFinIdx.3F.20consistent/near/567340199🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
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>
