This PR implements `grind` propagators for `Nat` operators that have a
simproc associated with them, but do not have any theory solver support.
Examples:
```lean
example (a b : Nat) : a = 3 → b = 6 → a &&& b = 2 := by grind
example (a b : Nat) : a = 3 → b = 6 → a ||| b = 7 := by grind
example (a b : Nat) : a = 3 → b = 6 → a ^^^ b = 5 := by grind
example (a b : Nat) : a = 3 → b = 6 → a <<< b = 192 := by grind
example (a b : Nat) : a = 1135 → b = 6 → a >>> b = 17 := by grind
```
Closes#11498
This PR marks `Nat` power and divisibility theorems for `grind`. We use
the new `grind_pattern` constraints to control theorem instantiation.
Examples:
```lean
example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
grind
example (a m n o p : Nat) : a ∣ n → a ∣ m * n * o * p := by
grind
example {a b x m n : Nat}
: n > 0 → x = b * 4^m * a → a = 9^n → m > 0 → x % 6 = 0 := by
grind
example {a n : Nat}
: m > 4 → a = 2^(m^n) → a % 2 = 0 := by
grind
```
Closes#11515
Remark: We are adding support for installing extra theorems to `lia`
(aka `cutsat`). The example at #11515 can already be solved by `grind`
with this PR, but we still need to add the new theorems to the set for
`lia`.
cc @kim-em
This PR provides an additional hint when the type of an autobound
implicit is required to have function type or equality type — this
fails, and the existing error message does not address the fact that the
source of the error is an unknown identifier that was automatically
bound.
## Example
```
import Lean
example : MetaM String := pure ""
```
Current error message:
```
Function expected at
MetaM
but this term has type
?m
Note: Expected a function because this term is being applied to the argument
String
```
Additional error message provided by this PR:
```
Hint: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option
causes an unknown identifier to be treated as an implicitly bound variable
with an unknown type. However, the unknown type cannot be a function, and a
function is what Lean expects here. This is often the result of a typo or a
missing `import` or `open` statement.
```
This PR re-enables star-indexed lemmas as a fallback for `exact?` and
`apply?`.
Star-indexed lemmas (those with overly-general discrimination tree keys
like `[*]`)
were previously dropped entirely for performance reasons. This caused
useful lemmas
like `Empty.elim`, `And.left`, `not_not.mp`, `Sum.elim`, and
`Function.mtr` to be
unfindable by library search.
The implementation adds a two-pass search strategy:
1. First, search using concrete discrimination keys (the current
behavior)
2. If no results are found, fall back to trying star-indexed lemmas
The star-indexed lemmas are extracted during tree initialization and
cached in an
environment extension, avoiding repeated computation.
Users can disable the fallback with `-star`:
```lean
example {α : Sort u} (h : Empty) : α := by apply? -star -- error: no lemmas found
example {α : Sort u} (h : Empty) : α := by apply? -- finds Empty.elim
```
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds support for the difference operation for
`ExtDHashMap`/`ExtHashMap`/`ExtHashSet` and proves several lemmas about
it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR changes how match splitters are generated: Rather than rewriting
the match statement, the match compilation pipeline is used again.
The benefits are:
* Re-doing the match compilation means we can do more intelligent book
keeping, e.g. prove overlap assumptions only once and re-use the proof,
or prune the context of the MVar to speed up `contradiction`. This may
have allowed a different solution than #11200.
* It would unblock #11105, as the existing splitter implementation would
have trouble dealing with the matchers produced that way.
* It provides the necessary machinery also for source-exposed “none of
the above” bindings, a feature that we probably want at some point (and
we mostly need to find good syntax for, see #3136, although maybe I
should open a dedicated RFC).
* It allows us to skip costly things during matcher creation that would
only be useful for the splitter, and thus allows performance
improvements like #11508.
* We can drop the existing implementation.
It’s not entirely free:
* We have to run `simpH` twice, once for the match equations and once
for the splitter.
This PR introduces a new annotation that allows definitions to describe
plausible-but-wrong name variants for the purpose of improving error
messages.
This PR just adds the notation and extra functionality; a stage0 update
will allow standard Lean functions to have suggestion annotations.
(Hence the changelog-no tag: this should go in the changelog when some
preliminary annotations are actually added.)
## Example
```lean4
inductive MyBool where | tt | ff
attribute [suggest_for MyBool.true] MyBool.tt
attribute [suggest_for MyBool.false] MyBool.ff
@[suggest_for MyBool.not]
def MyBool.swap : MyBool → MyBool
| tt => ff
| ff => tt
/--
error: Unknown constant `MyBool.true`
Hint: Perhaps you meant `MyBool.tt` in place of `MyBool.true`:
M̵y̵B̵o̵o̵l̵.̵t̵r̵u̵e̵M̲y̲B̲o̲o̲l̲.̲t̲t̲
-/
#guard_msgs in
example := MyBool.true
/--
error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
MyBool.tt
of type `MyBool`
Hint: Perhaps you meant one of these in place of `MyBool.not`:
[apply] `MyBool.swap`: MyBool.tt.swap
-/
#guard_msgs in
example := MyBool.tt.not
```
This PR marks `Char -> Bool` patterns as default instances for string
search. This means that things like `" ".find (·.isWhitespace)` can now
be elaborated without error.
Previously, it was necessary to write `" ".find Char.isWhitespace`.
Thank you to David Christiansen for the idea of using a default
instance.
This PR gives suggestions based on the currently-available constants
when projecting from an unknown type.
## Example: single suggestion in namespace
This was the originally motivating example, as the string refactor led
to a number of anonymous-lambda-expressions with `Char` functions that
were no longer recognized as such.
```lean4
example := (·.isWhitespace)
```
Before:
```
Invalid field notation: Type of
x✝
is not known; cannot resolve field `isWhitespace`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.
```
## Example: single suggestion in namespace
```lean4
example := fun n => n.succ
```
Before:
```
Invalid field notation: Type of
n
is not known; cannot resolve field `succ`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection with a call to one of the following:
• `Fin.succ`
• `Nat.succ`
• `Std.PRange.succ`
```
This PR adds a heterogeneous version of the constructor injectivity
theorems. These theorems are useful for indexed families, and will be
used in `grind`.
This PR adds a module resolution procedure to Lake to disambiguate
modules that are defined in multiple packages.
On an `import`, Lake will now check if multiple packages within the
workspace define the module. If so, it will verify that modules have
sufficiently similar definitions (i.e., artifacts with the same content
hashes). If not, Lake will report an error.
This verification is currently only done for direct imports. Transitive
imports are not checked for consistency. An overhaul of transitive
imports will come later.
This PR fixes a bug in `grind?`. The suggestion using the `grind`
interactive mode was dropping the configuration options provided by the
user. In the following account, the third suggestion was dropping the
`-reducible` option.
```lean
/--
info: Try these:
[apply] grind -reducible only [Equiv.congr_fun, #5103]
[apply] grind -reducible only [Equiv.congr_fun]
[apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
-/
example :
(Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
= (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
grind? -reducible [Equiv.congr_fun]
```
This PR adds the `grind` option `reducible` (default: `true`). When
enabled, definitional equality tests expand only declarations marked as
`@[reducible]`.
Use `grind -reducible` to allow expansion of non-reducible declarations
during definitional equality tests.
This option affects only definitional equality; the canonicalizer and
theorem pattern internalization always unfold reducible declarations
regardless of this setting.
This PR refines several error error messages, mostly involving invalid
use of field notation, generalized field notation, and numeric
projection. Provides a new error explanation for field notation.
## Error message changes
In general:
- Uses a slightly different convention for expression-type pairs, where
the expression is always given `indentExpr` and the type is given
`inlineExpr` treatment. This is something of a workaround for the fact
that the `Format` type is awkward for embedding possibly-linebreaking
expressions in not-linebreaking text, which may be a separate issue
worth addressing.
- Tries to give slightly more "why" reasoning — the environment does not
contain `String.parse`, and _therefore you can't project `.parse` from a
`String`_.
Some specific examples:
### No such projection function
```lean4
#check "".parse
```
before:
```
error: Invalid field `parse`: The environment does not contain `String.parse`
""
has type
String
```
after:
```
error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
""
of type `String`
```
### Type does not have the correct form
```lean4
example (x : α) := (foo x).foo
```
before:
```
error: Invalid field notation: Type is not of the form `C ...` where C is a constant
foo x
has type
α
```
after:
```
error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
foo x
has type `α` which does not have the necessary form.
```
## Refactoring
Includes some refactoring changes as well:
- factors out multiple uses of number (1, 2, 3, 212, 222) to ordinal
("first", "second", "third", "212th", "222nd") conversion into
Lean.Elab.ErrorUtils
- significant refactoring of `resolveLValAux` in `Lean.Elab.App` — in
place of five helper functions, a special-case function case analysis,
and a case analysis on the projection type and structure, there's now a
single case analysis on the projection type and structure. This allows
several error messages to be more explicit (there were a number of cases
where index projection was being described as field projection in an
error messages) and gave the opportunity to slightly improve positining
for several errors: field *notation* errors should appear on `foo.bar`,
but field *projection* errors should appear only on the `bar` part of
`foo.bar`.
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).
(Redo of #11345 to fix Windows issue.)
This PR generalizes the `noConfusion` constructions to heterogeneous
equalities (assuming propositional equalities between the indices). This
lays ground work for better support for applying injection to
heterogeneous equalities in grind.
The `Meta.mkNoConfusion` app builder shields most of the code from these
changes.
Since the per-constructor noConfusion principles are now more
expressive, `Meta.mkNoConfusion` no longer uses the general one.
In `Init.Prelude` some proofs are more pedestrian because `injection`
now needs a bit more machinery.
This is a breaking change for whoever uses the `noConfusion` principle
manually and explicitly for a type with indices.
Fixes#11450.
This PR adds lemmas stating that if a get operation returns a value,
then the queried key must be contained in the collection. These lemmas
are added for HashMap and TreeMap-based collections, with a similar
lemma also added for `Init.getElem`.
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 moves the `Inhabited` instances in constant `DTreeMap` (and
related) queries, such as `Const.get!`, where the `Inhabited` instance
can be provided before proving a key.
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 fixes various typos across the codebase in documentation and
comments.
- `infered` → `inferred` (ParserCompiler.lean)
- `declartation` → `declaration` (Cleanup.lean)
- `certian` → `certain` (CasesInfo.lean)
- `wil` → `will` (Cache.lean)
- `the the` → `the` (multiple files - PrefixTree.lean, Sum/Basic.lean,
List/Nat/Perm.lean, Time.lean, Bounded.lean, Lake files)
- `to to` → `to` (MutualInductive.lean, simp_bubblesort_256.lean)
- Grammar improvements in Bounded.lean and Time.lean
All changes are to comments and documentation only - no functional
changes.
🤖 Generated with [Claude Code](https://claude.com/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 adds the difference operation on `DTreeMap`/`TreeMap`/`TreeSet`
and proves several lemmas about it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
