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 moves the processing of options passed to the CLI from
`shell.cpp` to `Shell.lean`.
As with previous ports, this attempts to mirror as much of the original
behavior as possible, Benefits to be gained from the ported code can
come in later PRs. There should be no significant behavioral changes
from this port. Nonetheless, error reporting has changed some, hopefully
for the better. For instance, errors for improper argument
configurations has been made more consistent (e.g., Lean will now error
if numeric arguments fall outside the expected range for an option).
This PR accelerates termination of the ElimDeadBranches compiler pass.
The implementation addresses situations such as `choice [none, some
top]` which can be summarized to
`top` because `Option` has only two constructors and all constructor
arguments are `top`.
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 adds a focused error explanation aimed at the case where someone
tries to use Natural-Numbers-Game-style `induction` proofs directly in
Lean, where such proofs are not syntactically valid.
## Discussion
The natural numbers game uses a syntax that overlaps with Lean's
`induction` syntax despite having more structural similarity to
`induction'`. This means that fully correct proofs in the natural
numbers game, like this...
```lean4
import Mathlib
theorem zero_mul (m : ℕ) : 0 * m = 0 := by
induction m with n n_ih
rw [mul_zero]
rfl
rw [mul_succ]
rw [add_zero]
rw [n_ih]
rfl
```
...have completely baffling error messages from a newcomers'
perspective:
```
notNaturalNumbersGame.lean:3:20: error: unknown tactic
notNaturalNumbersGame.lean:3:2: error: Alternative `zero` has not been provided
notNaturalNumbersGame.lean:3:2: error: Alternative `succ` has not been provided
```
(the Mathlib import here only provides the `ℕ` syntax here; equivalently
`ℕ` could be renamed to `Nat` and the import could be removed, [like
this](https://live.lean-lang.org/#codez=C4Cwpg9gTmC2AEAvMUIH1YFcA28AUCAXPAHICGwAlPMQAzwBU8CAvPPYWwEYCeAUPHgBLAHYATTAGNgQiCObwA7kNDx5ItEJAD4URfADaWbGmSoAujqgAzbFf1GcaAM5TJlwXsNkxY0yggPXQcNLSCbbCA))
There are many problems with this proof from the perspective of "stock"
Lean, but the error messages in the `induction` case are particularly
unfriendly and provide no guidance from a NNG learner's perspective.
This PR provides more information about what is wrong:
```
notNaturalNumbersGame.lean:3:20: error: unknown tactic
notNaturalNumbersGame.lean:3:14: error(lean.inductionWithNoAlts): Invalid syntax for induction tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
```
The error explanation it links to explicitly flags the transition of
NNG-style proofs to Lean as the likely culprit, and gives an example of
an effective translation.
This PR updates the `foldr`, `all`, `any` and `contains` functions on
`String` to be defined in terms of their `String.Slice` counterparts.
This is the last one in a long series of PRs. After this, all `String`
operations are polymorphic in the pattern, and no `String` operation
falls back to `String.Pos.Raw` internally (except those in the
`String.Pos.Raw` and `String.Substring.Raw` namespaces of course, which
still play a role in metaprogramming and will stay for the foreseeable
future).
This PR adds a new [radar]-based [temci]-less bench suite that replaces
the `stdlib` benchmarks from the old suite and also measures per-module
instruction counts. All other benchmarks from the old suite are
unaffected.
The readme at `tests/bench-radar/README.md` explains in more detail how
the bench suite is structured and how it works. The readmes in the
benchmark subdirectories explain what each benchmark does and which
metrics it collects.
All metrics except `stdlib//max dynamic symbols` were ported to the new
suite, though most have been renamed.
[radar]: https://github.com/leanprover/radar
[temci]: https://github.com/parttimenerd/temci
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 documents that `backward.*` options are only temporary
migration aids and may disappear without further notice after 6 months
after their introduction. Users are kindly asked to report if they rely
on these options.
This PR adds a coercion from `String` to `String.Slice`.
In our envisioned future, most functions operating on strings will
accept `String.Slice` parameters by default (like `str` in Rust), and
this enables calling such functions with arguments of type `String`.
Closes#11298.
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 removes the `group` field from option descriptions. It is
unused, does not have a clear meaning and often matches the first
component of the option name.
Given its run time of >2hrs, the job is added as a secondary job for
nightly releases and a primary job for full releases. A new check level
for differentiating between nightlies and full releases is added for
this.
(Trying to) reactivate lsan will happen in a follow-up PR.
This PR fixes freeing memory accidentally retained for each document
version in the language server on certain elaboration workloads. The
issue must have existed since 4.18.0.
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 cleans up the API around `String.find` and moves it uniformly to
the new position types `String.ValidPos` and `String.Slice.Pos`
Overview:
- To search for a character, character predicate, string or slice in a
string or slice `s`, use `s.find?` or `s.find`.
- To do the same, but starting at a position `p` of a string or slice,
use `p.find?` or `p.find`.
- To do the same but between two positions `p` and `q`, construct the
slice from `p` to `q` and then use `find?` or `find` on that.
- To search backwards, all of the above applies, except that the
function is called `revFind?`, there is no non-question-mark version
(use `getD` if there is a sane default return value in your specific
application), and that you can only search for characters and character
predicates, not strings or slices.
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 redefines `front` and `back` on `String` to go through
`String.Slice` and adds the new `String` functions `front?`, `back?`,
`positions`, `chars`, `revPositions`, `revChars`, `byteIterator`,
`revBytes`, `lines`.
This PR adds `CoreM.toIO'`, the analogue of `CoreM.toIO` dropping the
state from the return type, and similarly for `TermElabM.toIO'` and
`MetaM.toIO'`.
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 significantly changes the signature of the `ToIterator` type
class. The obtained iterators' state is no longer dependently typed and
is an `outParam` instead of being bundled inside the class. Among other
benefits, `simp` can now rewrite inside of `Slice.toList` and
`Slice.toArray`. The downside is that we lose flexibility. For example,
the former combinator-based implementation of `Subarray`'s iterators is
no longer feasible because the states are dependently typed. Therefore,
this PR provides a hand-written iterator for `Subarray`, which does not
require a dependently typed state and is faster than the previous one.
Converting a family of dependently typed iterators into a simply typed
one using a `Sigma`-state iterator generates forbiddingly bad code, so
that we do provide such a combinator. This PR adds a benchmark for this
problem.
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 a breakage in Lake's TOML test caused by String API
changes. It also removes a JSON parser workaround that has since been
fixed, and it more generally polishes up the code.
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.
This PR fixes a local declaration internalization in `grind` that was
exposed when using `grind -revert`. This bug was affecting a `grind`
proof in Mathlib.
