This PR adapts the lambda lifter in LCNF to eta contract instead of
lambda lift if possible. This prevents the creation of a few hundred
unnecessary lambdas across the code base.
This PR fixes a panic in `getEqnsFor?` when called on matchers generated
from match expressions in theorem types.
When a theorem's type contains a match expression (e.g., `theorem bar :
(match ... with ...) = 0`), the compiler generates a matcher like
`bar.match_1`. Calling `getEqnsFor?` on this matcher would panic with:
```
PANIC: duplicate normalized declaration name bar.match_1.eq_1 vs. _private...bar.match_1.eq_1
```
This also affected the `try?` tactic, which internally uses
`getEqnsFor?`.
We make `shouldGenerateEqnThms` return `false` for matchers, since their
equations are already generated separately by
`Lean.Meta.Match.MatchEqs`. This prevents the equation generation
machinery from attempting to create duplicate equation theorems.
Closes#11461Closes#10390🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds `+suggestions` support to `solve_by_elim`, following the
pattern established by `grind +suggestions` and `simp_all +suggestions`.
Gracefully handles invalid/nonexistent suggestions by filtering them out
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds `solve_by_elim` as a fallback in the `try?` tactic's simple
tactics. When `rfl` and `assumption` both fail but `solve_by_elim`
succeeds (e.g., for goals requiring hypothesis chaining or
backtracking), `try?` will now suggest `solve_by_elim`.
The structure is `first | (attempt_all | rfl | assumption) |
solve_by_elim`, so `solve_by_elim` only runs when the faster tactics
fail.
This is a prerequisite for removing the "first pass" `solve_by_elim`
from `apply?`. Currently `apply?` calls `solve_by_elim` twice: once
before library search, and once after each lemma application. The first
pass can be removed once `try?` includes `solve_by_elim`.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR removes the "first pass" behavior where `exact?` and `apply?`
would try `solve_by_elim` on the original goal before doing library
search. This simplifies the `librarySearch` API and focuses these
tactics on their primary purpose: finding library lemmas.
Users who want to find proofs using local hypotheses should use `try?`
instead, which now includes `solve_by_elim` in its pipeline (see
https://github.com/leanprover/lean4/pull/11462).
Changes:
- Removed first pass from `librarySearch`
- Simplified `tactic` parameter from `Bool → List MVarId → MetaM (List
MVarId)` to `List MVarId → MetaM (List MVarId)`
- Updated test expectations
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR improves the error message when no library suggestions engine is
registered to recommend importing `Lean.LibrarySuggestions.Default` for
the built-in engine.
**Before:**
```
No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
```
**After:**
```
No library suggestions engine registered. (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, or use `set_library_suggestions` to configure a custom one.)
```
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds recording functionality such that `shake` can more
precisely track whether an import should be preserved solely for its
`attribute` commands.
This PR slightly improves the types involved in creating boxed
declarations. Previously the type of
the vdecl used for the return was always `tobj` when returning a boxed
scalar. This is not the most
precise annotation we can give.
This PR modifies the error message for type synthesis failure for the
case where the type class in question is potentially derivable using a
`deriving` command. Also changes the error explanation for type class
instance synthesis failure with an illustration of this pattern.
## Example
```lean4
inductive MyColor where
| chartreuse | sienna | thistle
def forceColor (oc : Option MyColor) :=
oc.get!
```
Before this PR, this gives the potentially confusing impression that
Lean may have decided that `MyColor` is _not_ inhabited — people used to
Rust may be especially inclined towards this confusion.
```
failed to synthesize instance of type class
Inhabited MyColor
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
```
After this PR, a targeted hint suggests precisely the command that will
fix the issue:
```
error: failed to synthesize instance of type class
Inhabited MyColor
Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.
```
This PR lets recursive functions defined by well-founded recursion use a
different `fix` function when the termination measure is of type `Nat`.
This fix-point operator use structural recursion on “fuel”, initialized
by the given measure, and is thus reasonable to reduce, e.g. in `by
decide` proofs.
Extra provisions are in place that the fixpoint operator only starts
reducing when the fuel is fully known, to prevent “accidential” defeqs
when the remaining fuel for the recursive calls match the initial fuel
for that recursive argument.
To opt-out, the idiom `termination_by (n,0)` can be used.
We still use `@[irreducible]` as the default for such recursive
definitions, to avoid unexpected `defeq` lemmas. Making these functions
`@[semireducible]` by default showed performance regressions in lean.
When the measure is of type `Nat`, the system will accept an explicit
`@[semireducible]` without the usual warning.
Fixes#5234. Fixes: #11181.
This PR performs minor maintenance on the String API
- Rename `String.Pos.toCopy` to `String.Pos.copy` to adhere to the
naming convention
- Rename `String.Pos.extract` to `String.extract` to get sane dot
notation again
- Add `String.Slice.Pos.extract`
This PR implements support for **guards** in `grind_pattern`. The new
feature provides additional control over theorem instantiation. For
example, consider the following monotonicity theorem:
```lean
opaque f : Nat → Nat
theorem fMono : x ≤ y → f x ≤ f y := ...
```
We can use `grind_pattern` to instruct `grind` to instantiate the
theorem for every pair `f x` and `f y` occurring in the goal:
```lean
grind_pattern fMono => f x, f y
```
Then we can automatically prove the following simple example using
`grind`:
```lean
/--
trace: [grind.ematch.instance] fMono: f a ≤ b → f (f a) ≤ f b
[grind.ematch.instance] fMono: f a ≤ c → f (f a) ≤ f c
[grind.ematch.instance] fMono: f a ≤ a → f (f a) ≤ f a
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
[grind.ematch.instance] fMono: f a ≤ f a → f (f a) ≤ f (f a)
[grind.ematch.instance] fMono: f (f a) ≤ b → f (f (f a)) ≤ f b
[grind.ematch.instance] fMono: f (f a) ≤ c → f (f (f a)) ≤ f c
[grind.ematch.instance] fMono: f (f a) ≤ a → f (f (f a)) ≤ f a
[grind.ematch.instance] fMono: f (f a) ≤ f (f a) → f (f (f a)) ≤ f (f (f a))
[grind.ematch.instance] fMono: f (f a) ≤ f a → f (f (f a)) ≤ f (f a)
[grind.ematch.instance] fMono: a ≤ b → f a ≤ f b
[grind.ematch.instance] fMono: a ≤ c → f a ≤ f c
[grind.ematch.instance] fMono: a ≤ a → f a ≤ f a
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
[grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
[grind.ematch.instance] fMono: c ≤ b → f c ≤ f b
[grind.ematch.instance] fMono: c ≤ c → f c ≤ f c
[grind.ematch.instance] fMono: c ≤ a → f c ≤ f a
[grind.ematch.instance] fMono: c ≤ f (f a) → f c ≤ f (f (f a))
[grind.ematch.instance] fMono: c ≤ f a → f c ≤ f (f a)
[grind.ematch.instance] fMono: b ≤ b → f b ≤ f b
[grind.ematch.instance] fMono: b ≤ c → f b ≤ f c
[grind.ematch.instance] fMono: b ≤ a → f b ≤ f a
[grind.ematch.instance] fMono: b ≤ f (f a) → f b ≤ f (f (f a))
[grind.ematch.instance] fMono: b ≤ f a → f b ≤ f (f a)
-/
#guard_msgs in
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
set_option trace.grind.ematch.instance true in
grind
```
However, many unnecessary theorem instantiations are generated.
With the new `guard` feature, we can instruct `grind` to instantiate the
theorem **only if** `x ≤ y` is already known to be true in the current
`grind` state:
```lean
grind_pattern fMono => f x, f y where
guard x ≤ y
x =/= y
```
If we run the example again, only three instances are generated:
```lean
/--
trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
-/
#guard_msgs in
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
set_option trace.grind.ematch.instance true in
grind
```
Note that `guard` does **not** check whether the expression is
*implied*. It only checks whether the expression is *already known* to
be true in the current `grind` state. If this fact is eventually
learned, the theorem will be instantiated.
If you want `grind` to check whether the expression is implied, you
should use:
```lean
grind_pattern fMono => f x, f y where
check x ≤ y
x =/= y
```
Remark: we can use multiple `guard`/`check`s in a `grind_pattern`
command.
This PR reverts https://github.com/leanprover/lean4/pull/11396, which
changed `set_library_suggestions` to create an auxiliary definition
marked with `@[library_suggestions]`, rather than storing `Syntax`
directly in the environment extension.
It wasn't tested properly.
Co-authored-by: Claude <noreply@anthropic.com>
This PR fixes a kernel type mismatch error in grind's denominator
cleanup feature. When generating proofs involving inverse numerals (like
`2⁻¹`), the proof context is compacted to only include variables
actually used. This involves renaming variable indices - e.g., if
original indices were `{0: r, 1: 2⁻¹}` and only `2⁻¹` is used, it gets
renamed to index 0.
The bug was that polynomials were correctly renamed via `varRename`, but
the variable index `x` stored in `cancelDen` constraints was passed
directly to the proof without renaming, causing a mismatch between the
polynomial's variable references and the theorem's variable argument.
Added `ringVarDecls` to track ring variable indices that need renaming,
similar to how `ringPolyDecls` tracks polynomials. The `mkRingContext`
function now also renames these variable indices.
See zulip discussion at [#nightly-testing > Mathlib status updates @
💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20status.20updates/near/560575295).
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR changes `set_library_suggestions` to create an auxiliary
definition marked with `@[library_suggestions]`, rather than storing
`Syntax` directly in the environment extension. This enables better
persistence and consistency of library suggestions across modules.
The change requires a stage0 update before tests can be restored. After
CI updates stage0, a follow-up PR will restore the test cases.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
This PR fixes an issue where `grind` would fail after multiple
`norm_cast`
calls with the error "unexpected metadata found during internalization".
The `norm_cast` tactic adds mdata nodes to expressions, and when called
multiple times it creates nested mdata. The `eraseIrrelevantMData`
preprocessing function was using `.continue e` when stripping mdata,
which causes `Core.transform` to reconstruct the mdata node around the
visited children. By changing to `.visit e`, the inner expression is
passed back to `pre` for another round of processing, allowing all
nested mdata layers to be stripped.
Closes#11411🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR implements the following `grind_pattern` constraints:
```lean
grind_pattern fax => f x where
depth x < 2
grind_pattern fax => f x where
is_ground x
grind_pattern fax => f x where
size x < 5
grind_pattern fax => f x where
gen < 2
grind_pattern fax => f x where
max_insts < 4
grind_pattern gax => g as where
as =?= _ :: _
```
This PR is a followup of #11381 and enforces the invariants on ordering
of closed terms and constants required by the EmitC pass properly by
toposorting before saving the declarations into the Environment.
This PR fixes a bug where the closed term extraction does not respect
the implicit invariant of the
c emitter to have closed term decls first, other decls second, within an
SCC. This bug has not yet
been triggered in the wild but was unearthed during work on upcoming
modifications of the
specializer.
This PR makes the library suggestions extension state available when
importing from `module` files.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds support for cleaning up denominators in `grind linarith`
when the type is a `Field`.
Examples:
```lean
open Std Lean.Grind
section
variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α]
example (a b : α) (h : a < b / 2) : 2 * a < b := by grind
example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind
example (a b : α) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind
example (a b : α) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind
example (a b : α) (h : a < b / (2^2 - 3/2 + -1 + 1/2)) : 2 * a < b := by grind
end
example (a b : Rat) (h : a < b / 2) : a + a < b := by grind
example (a b : Rat) (h : a < b / 2) : a + a ≤ b := by grind
example (a b : Rat) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind
example (a b : Rat) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind
```
This PR makes the `Std.Time.Format` import in
`Lean.Elab.Tactic.Grind.Annotated` private rather than public,
preventing the entire `Std.Time` infrastructure (including timezone
databases) from being re-exported through `import Lean`.
The `grindAnnotatedExt` extension is kept private, with a new public
accessor function `isGrindAnnotatedModule` exposed for use by
`LibrarySuggestions.Basic`.
This should address the +2.5% instruction increase on `import Lean`
observed after merging #11332.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR enables parallelism in `try?`. Currently, we replace the
`attempt_all` stages (there are two, one for builtin tactics including
`grind` and `simp_all`, and a second one for all user extensions) with
parallel versions. We do not (yet?) change the behaviour of `first`
based stages.
This PR implements a helper simproc for `grind`. It is part of the
infrastructure used to cleanup denominators in `grind linarith`.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR changes the interface of the `ForIn`, `ForIn'`, and `ForM`
typeclasses to not take a `Monad m` parameter. This is a breaking change
for most downstream `instance`s, which will will now need to assume
`[Monad m]`.
The rationale is that if the provider of an instance requires `m` to be
a Monad, they should assume this up front. This makes it possible for
the instanve to assume `LawfulMonad m` or some other stronger
requirement, and also to provided a concrete instance for a particular
`m` without assuming a non-canonical `Monad` structure on it.
Zulip: [#lean4 > Monad assumptions in fields of other typeclasses @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Monad.20assumptions.20in.20fields.20of.20other.20typeclasses/near/537102158)
This PR activates the `grind_annotated` command in
`Init.Data.List.Lemmas` by removing the TODO comment and uncommenting
the command.
This PR depends on #11346 (implement `grind_annotated` command) and
should be merged after that PR (and after CI has done an
`update-stage0`.
This PR enables the syntax `use [ns Foo]` and `instantiate only [ns
Foo]` inside a `grind` tactic block, and has the effect of activating
all grind patterns scoped to that namespace. We can use this to
implement specialized tactics using `grind`, but only controlled subsets
of theorems.
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR upstreams the `with_weak_namespace` command from Mathlib:
`with_weak_namespace <id> <cmd>` changes the current namespace to `<id>`
for the duration of executing command `<cmd>`, without causing scoped
things to go out of scope. This is in preparation for upstreaming the
`scoped[Foo.Bar]` syntax from Mathlib, which will be useful now that we
are adding `grind` annotations in scopes.
This PR adds a `grind_annotated "YYYY-MM-DD"` command that marks files
as manually annotated for grind.
When LibrarySuggestions is called with `caller := "grind"` (as happens
with `grind +suggestions`), theorems from grind-annotated files are
filtered out from premise selection. The date argument validates using
Std.Time and is informational only for now, but could be used later to
detect files that need re-review.
There's no need for the library suggestions tools to suggest `grind`
theorems from files that have already been carefully annotated by hand.
This PR adds infrastructure for parallel execution across Lean's tactic
monads.
- Add IO.waitAny' to Init/System/IO.lean for waiting on task completion
- Add `Lean.Elab.Task` with `asTask` utilities for `CoreM`, `MetaM`,
`TermElabM`, `TacticM`
- Add `Lean.Elab.Parallel` with parallel execution strategies:
* `par`/`par'` - collect results in original order
* `parIter`/`parIterGreedy` - iterate over results (original or
completion order) (also variants with a cancellation token)
* `parFirst` - return first successful result
This does *not* attempt to be a monad-polymorphic framework for
parallelism. It's intentionally hard-coded to the Lean tactic monads
which I need to work with. If there's desire to make this polymorphic,
hopefully that can be done separately.
This PR renames `String.bytes` to `String.toByteArray`.
This is for two reasons: first, `toByteArray` is a better name, and
second, we have something else that wants to use the name `bytes`,
namely the function that returns in iterator over the string's bytes.
This PR renames `String.ValidPos` to `String.Pos`, `String.endValidPos`
to `String.endPos` and `String.startValidPos` to `String.startPos`.
Accordingly, the deprecations of `String.Pos` to `String.Pos.Raw` and
`String.endPos` to `String.rawEndPos` are removed early, after an
abbreviated deprecation cycle of two releases.
This PR adds an explicit normalization layer for ring constraints in the
`grind linarith` module. For example, it will be used to clean up
denominators when the ring is a field.
This PR renames the `cutsat` tactic to `lia` for better alignment with
standard terminology in the theorem proving community.
`cutsat` still works but now emits a deprecation warning and suggests
using `lia` instead via "Try this:". Both tactics have identical
behavior.
Co-authored-by: Claude <noreply@anthropic.com>
This PR ensures that users can provide `grind` proof parameters whose
types are not `forall`-quantified. Examples:
```lean
opaque f : Nat → Nat
axiom le_f (a : Nat) : a ≤ f a
example (a : Nat) : a ≤ f a := by
grind [le_f a]
example (a b : α) (h : ∀ x y : α, x = y) : a = b := by
grind [h a b]
```
This PR introduces a new `grind` option, `funCC` (enabled by default),
which extends congruence closure to *function-valued* equalities. When
`funCC` is enabled, `grind` tracks equalities of **partially applied
functions**, allowing reasoning steps such as:
```lean
a : Nat → Nat
f : (Nat → Nat) → (Nat → Nat)
h : f a = a
⊢ (f a) m = a m
g : Nat → Nat
f : Nat → Nat → Nat
h : f a = g
⊢ f a b = g b
```
Given an application `f a₁ a₂ … aₙ`, when `funCC := true` and function
equality is enabled for `f`, `grind` generates and tracks equalities for
all partial applications:
* `f a₁`
* `f a₁ a₂`
* …
* `f a₁ a₂ … aₙ`
This allows equalities such as `f a₁ = g` to propagate through further
applications.
**When is function equality enabled for a symbol?**
Function equality is enabled for `f` in the following cases:
1. `f` is **not a constant** (e.g., a lambda, a local function, or a
function parameter).
2. `f` is a **structure field projection**, provided the structure is
**not a `class`**.
3. `f` is a constant marked with `@[grind funCC]`
Users can also enable function equality for specific constants in a
single call using:
```lean
grind [funCC f, funCC g]
```
**Examples:**
```lean
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
f a m = a m := by
grind
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
f a m = a m := by
fail_if_success grind -funCC -- fails if `funCC` is disabled
grind
```
```lean
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
f a b = g b := by
grind
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
f a b = g b := by
fail_if_success grind -funCC
grind
```
**Enabling per-symbol with parameters or attributes**
```lean
opaque f : Nat → Nat → Nat
opaque g : Nat → Nat
example (a b c : Nat) : f a = g → b = c → f a b = g c := by
grind [funCC f, funCC g]
attribute [grind funCC] f g
example (a b c : Nat) : f a = g → b = c → f a b = g c := by
grind
```
This feature substantially improves `grind`’s support for higher-order
and partially-applied function equalities, while preserving
compatibility with first-order SMT behavior when `funCC` is disabled.
Closes#11309
This PR improves the support for `Fin n` in `grind` when `n` is not a
numeral.
- `toInt (0 : Fin n) = 0` in `grind lia`.
- `Fin.mk`-applications are treated as interpreted terms in `grind lia`.
- `Fin.val` applications are suppressed from `grind lia`
counterexamples.
This PR fixes an issue affecting `grind -revert`. In this mode, assigned
metavariables in hypotheses were not being instantiated. This issue was
affecting two files in Mathlib.
