This PR fixes `grind` to support dot notation on declarations in the
lemma list.
When using `grind only [foo.le]` where `foo.le` is dot notation applying
`LT.lt.le` to a theorem `foo`, grind previously failed with "Unknown
constant `foo.le`" because it tried to look up `foo.le` as a constant
name rather than elaborating it as a term.
The fix adds a fallback in `processParam`: when constant lookup fails,
it now falls back to `processTermParam` which elaborates the identifier
as a term. This allows dot notation expressions like `log_two_lt_d9.le`
to work correctly.
Closes#11690🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds the new operation `MonadAttach.attach` that attaches a
proof that a postcondition holds to the return value of a monadic
operation. Most non-CPS monads in the standard library support this
operation in a nontrivial way. The PR also changes the `filterMapM`,
`mapM` and `flatMapM` combinators so that they attach postconditions to
the user-provided monadic functions passed to them. This makes it
possible to prove termination for some of these for which it wasn't
possible before. Additionally, the PR adds many missing lemmas about
`filterMap(M)` and `map(M)` that were needed in the course of this PR.
This PR improves `match` generalization such that it abstracts
metavariables in types of local variables and in the result type of the
match over the match discriminants. Previously, a metavariable in the
result type would silently default to the behavior of `generalizing :=
false`, and a metavariable in the type of a free variable would lead to
an error (#8099). Example of a `match` that elaborates now but
previously wouldn't:
```lean
example (a : Nat) (ha : a = 37) :=
(match a with | 42 => by contradiction | n => n) = 37
```
This is because the result type of the `match` is a metavariable that
was not abstracted over `a` and hence generalization failed; the result
is that `contradiction` cannot pick up the proof `ha : 42 = 37`.
The old behavior can be recovered by passing `(generalizing := false)`
to the `match`.
Furthermore, programs such as the following can now be elaborated:
```lean
example (n : Nat) : Id (Fin (n + 1)) :=
have jp : ?m := ?rhs
match n with
| 0 => ?jmp1
| n + 1 => ?jmp2
where finally
case m => exact Fin (n + 1) → Id (Fin (n + 1))
case jmp1 => exact jp ⟨0, by decide⟩
case jmp2 => exact jp ⟨n, by omega⟩
case rhs => exact pure
```
This is useful for the `do` elaborator.
Fixes#8099.
This PR fixes an inconsistency in the way Lake and Lean view the
transitivity of a `meta import`. Lake now works as Lean expects and
includes the meta segment of all transitive imports of a `meta import`
in its transitive trace.
This PR adds the `Context` type for cancellation with context
propagation. It works by storing a tree of forks of the main context,
providing a way to control cancellation.
This PR changes the "declaration uses 'sorry'" warning to use backticks
instead of single quotes, consistent with Lean's conventions for
formatting code identifiers in diagnostic messages.
This PR fixes the `grind` support for `Nat.ctorIdx`. Nat constructors
appear in `grind` as offsets or literals, and not as a node marked
`.constr`, so handle that case as well.
This PR moves many constants of the iterator API from `Std.Iterators` to
the `Std` namespace in order to make them more convenient to use. These
constants include, but are not limited to, `Iter`, `IterM` and
`IteratorLoop`. This is a breaking change. If something breaks, try
adding `open Std` in order to make these constants available again. If
some constants in the `Std.Iterators` namespace cannot be found, they
can be found directly in `Std` now.
This PR adds basic support for equality propagation in `grind linarith`
for the `IntModule` case. This covers only the basic case. See note in
the code.
We remark this feature is irrelevant for `CommRing` since `grind ring`
already has much better support for equality propagation.
This PR fixes an issue where a `by` in the public scope could create an
auxiliary theorem for the proof whose type does not match the expected
type in the public scope.
Fixes#11672
This PR adds support for `Nat.cast` in `grind linarith`. It now uses
`Grind.OrderedRing.natCast_nonneg`. Example:
```lean
open Lean Grind Std
attribute [instance] Semiring.natCast
variable [Lean.Grind.CommRing R] [LE R] [LT R] [LawfulOrderLT R] [IsLinearOrder R] [OrderedRing R]
example (a : Nat) : 0 ≤ (a : R) := by grind
example (a b : Nat) : 0 ≤ (a : R) + (b : R) := by grind
example (a : Nat) : 0 ≤ 2 * (a : R) := by grind
example (a : Nat) : 0 ≥ -3 * (a : R) := by grind
```
This PR fixes the `grind` pattern validator. It covers the case where an
instance is not tagged with the implicit instance binder. This happens
in declarations such as
```lean
ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
[self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
```
This PR adds support for `Int.sign`, `Int.fdiv`, `Int.tdiv`, `Int.fmod`,
`Int.tmod`, and `Int.bmod` to `grind`. These operations are just
preprocessed away. We assume that they are not very common in practice.
Examples:
```lean
example {x y : Int} : y = 0 → (x.fdiv y) = 0 := by grind
example {x y : Int} : y = 0 → (x.tdiv y) = 0 := by grind
example {x y : Int} : y = 0 → (x.fmod y) = x := by grind
example {x y : Int} : y = 1 → (x.fdiv (2 - y)) = x := by grind
example {x : Int} : x > 0 → x.sign = 1 := by grind
example {x : Int} : x < 0 → x.sign = -1 := by grind
example {x y : Int} : x.sign = 0 → x*y = 0 := by grind
```
See #11622
This PR adds propagation rules corresponding to the `Semiring`
normalization rules introduced in #11628. The new rules apply only to
non-commutative semirings, since support for them in `grind` is limited.
The normalization rules introduced unexpected behavior in Mathlib
because they neutralize parameters such as `one_mul`: any theorem
instance associated with such a parameter is reduced to `True` by the
normalizer.
This PR teaches `grind` how to reduce `.ctorIdx` applied to
constructors. It can also handle tasks like
```
xs ≍ Vec.cons x xs' → xs.ctorIdx = 1
```
thanks to a `.ctorIdx.hinj` theorem (generated on demand).
This PR fixes a SIGFPE crash on x86_64 when evaluating `INT_MIN / -1` or
`INT_MIN % -1` for signed integer types.
On x86_64, the `idiv` instruction traps when the quotient overflows the
destination register. For signed integers, `INT_MIN / -1` produces a
result that overflows (e.g., `-2147483648 / -1 = 2147483648` which
doesn't fit in Int32). ARM64's `sdiv` instruction wraps instead of
trapping.
The fix:
- For Int8/Int16/Int32: widen to the next larger type before
dividing/modding, then truncate back
- For Int64: explicitly check for the overflow case and return the
wrapped result
Fixes#11612🤖 Prepared with Claude Code
This PR adds support for `BitVec.ofNat` in `grind lia`. Example:
```lean
example (x y : BitVec 8) : y < 254#8 → x > 2#8 + y → x > 1#8 + y := by
grind
```
This PR implements a linter that warns when a deprecated coercion is
applied. It also warns when the `Option` coercion or the
`Subarray`-to-`Array` coercion is used in `Init` or `Std`. The linter is
currently limited to `Coe` instances; `CoeFun` instances etc. are not
considered.
The linter works by collecting the `Coe` instance declaration names that
are being expanded in `expandCoe?` and storing them in the info tree.
The linter itself then analyzes the info tree and checks for banned or
deprecated coercions.
This PR ensures the pattern normalizer used in `grind` does violate
assumptions made by the gadgets `Grind.genPattern` and
`Grind.getHEqPattern`.
Closes#11633
This PR causes Lean to search through `@[suggest_for]` annotations on
certain errors that look like unknown identifiers that got incorrectly
autobound. This will correctly identify that a declaration of type
`Maybe String` should be `Option String` instead.
## Example
```
example : Except String Unit := return .ok ()
```
```
Function expected at
Result
but this term has type
?m.1
Note: Expected a function because this term is being applied to the argument
String
Hint: The identifier `Result` 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.
Perhaps you meant `Except` in place of `Result`?
```
The last line is added by this PR.
This PR allows Lean to present suggestions based on `@[suggest_for]`
annotations for unknown identifiers without internal dots. (The
annotations in #11554 only gave suggestion for dotted identifiers like
`Array.every`->`Array.all` and not for bare identifiers like
`Result`->`Except` or `ℕ`->`Nat`.)
This PR makes argument-less tactic invokations of `Std.Do` tactics such
as `mintro` emit a proper error message "`mintro` expects at least one
pattern" instead of claiming that `Std.Tactic.Do` needs to be imported.
Closes#11509.
This PR ensures we apply the ring normalizer to equalities being
propagated from the `grind` core module to `grind lia`. It also ensures
we use the safe/managed polynomial functions when normalizing.
Closes#11539
This PR improves the case-split heuristics in `grind`. In this PR, we do
not increment the number of case splits in the first case. The idea is
to leverage non-chronological backtracking: if the first case is solved
using a proof that doesn't depend on the case hypothesis, we backtrack
and close the original goal directly. In this scenario, the case-split
was "free", it didn't contribute to the proof. By not counting it, we
allow deeper exploration when case-splits turn out to be irrelevant.
The new heuristic addresses the second example in #11545
