Continuation from #5429: eliminates uses of these two functions that
care about something other than reducible defs/theorems, then restricts
the function definition to these cases to be more true to its name.
This PR splits the environment used by the kernel from that used by the
elaborator, providing the foundation for tracking of asynchronously
elaborated declarations, which will exist as a concept only in the
latter.
Minor changes:
* kernel diagnostics are moved from an environment extension to a direct
environment as they are the only extension used directly by the kernel
* `initQuot` is moved from an environment header field to a direct
environment as it is the only header field used by the kernel; this also
makes the remaining header immutable after import
This PR adds support for extensionality theorems (using the `[ext]`
attribute) to the `grind` tactic. Users can disable this functionality
using `grind -ext` . Below are examples that demonstrate problems now
solvable by `grind`.
```lean
open List in
example : (replicate n a).map f = replicate n (f a) := by
grind only [Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
```
```lean
@[ext] structure S where
a : Nat
b : Bool
example (x y : S) : x.a = y.a → y.b = x.b → x = y := by
grind
```
This PR improves the canonicalizer used in the `grind` tactic and the
diagnostics it produces. It also adds a new configuration option,
`canonHeartbeats`, to address (some of) the issues. Here is an example
illustrating the new diagnostics, where we intentionally create a
problem by using a very small number of heartbeats.
<img width="1173" alt="image"
src="https://github.com/user-attachments/assets/484005c8-dcaa-4164-8fbf-617864ed7350"
/>
This PR fixes a bug in the `grind` term preprocessor. It was abstracting
nested proofs **before** reducible constants were unfolded.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR improves the diagnostic information provided in `grind` failure
states. We now include the list of issues found during the search, and
all search thresholds that have been reached. This PR also improves its
formatting.
This PR adds support for numerals, lower & upper bounds to the offset
constraint module in the `grind` tactic. `grind` can now solve examples
such as:
```
example (f : Nat → Nat) :
f 2 = a →
b ≤ 1 → b ≥ 1 →
c = b + 1 →
f c = a := by
grind
```
In the example above, the literal `2` and the lower&upper bounds, `b ≤
1` and `b ≥ 1`, are now processed by offset constraint module.
This PR completes aligning `List`/`Array`/`Vector` lemmas about
`flatten`. `Vector.flatten` was previously missing, and has been added
(for rectangular sizes only). A small number of missing `Option` lemmas
were also need to get the proofs to go through.
This PR implements support for offset equality constraints in the
`grind` tactic and exhaustive equality propagation for them. The `grind`
tactic can now solve problems such as the following:
```lean
example (f : Nat → Nat) (a b c d e : Nat) :
f (a + 3) = b →
f (c + 1) = d →
c ≤ a + 2 →
a + 1 ≤ e →
e < c →
b = d := by
grind
```
This PR improves the failure message produced by the `grind` tactic. We
now include information about asserted facts, propositions that are
known to be true and false, and equivalence classes.
This PR implements exhaustive offset constraint propagation in the
`grind` tactic. This enhancement minimizes the number of case splits
performed by `grind`. For instance, it can solve the following example
without performing any case splits:
```lean
example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by
grind (splits := 0)
```
TODO: support for equational offset constraints.
This PR implements support for offset constraints in the `grind` tactic.
Several features are still missing, such as constraint propagation and
support for offset equalities, but `grind` can already solve examples
like the following:
```lean
example (a b c : Nat) : a ≤ b → b + 2 ≤ c → a + 1 ≤ c := by
grind
example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 2 ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 1 ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
grind
example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
grind
```
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
This PR improves the usability of the `[grind =]` attribute by
automatically handling
forbidden pattern symbols. For example, consider the following theorem
tagged with this attribute:
```
getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]
```
Here, the selected pattern is `xs.getLast? = some a`, but `Eq` is a
forbidden pattern symbol.
Instead of producing an error, this function converts the pattern into a
multi-pattern,
allowing the attribute to be used conveniently.
This PR adds support for creating local E-matching theorems for
universal propositions known to be true. It allows `grind` to
automatically solve examples such as:
```lean
example (b : List α) (p : α → Prop) (h₁ : ∀ a ∈ b, p a) (h₂ : ∃ a ∈ b, ¬p a) : False := by
grind
```
This PR adds support for case splitting on `match`-expressions in
`grind`.
We still need to add support for resolving the antecedents of
`match`-conditional equations.
This PR introduces the parametric attribute `[grind]` for annotating
theorems and definitions. It also replaces `[grind_eq]` with `[grind
=]`. For definitions, `[grind]` is equivalent to `[grind =]`.
The new attribute supports the following variants:
- **`[grind =]`**: Uses the left-hand side of the theorem's conclusion
as the pattern for E-matching.
- **`[grind =_]`**: Uses the right-hand side of the theorem's conclusion
as the pattern for E-matching.
- **`[grind _=_]`**: Creates two patterns. One for the left-hand side
and one for the right-hand side.
- **`[grind →]`**: Searches for (multi-)patterns in the theorem's
antecedents, stopping once a usable multi-pattern is found.
- **`[grind ←]`**: Searches for (multi-)patterns in the theorem's
conclusion, stopping once a usable multi-pattern is found.
- **`[grind]`**: Searches for (multi-)patterns in both the theorem's
conclusion and antecedents. It starts with the conclusion and stops once
a usable multi-pattern is found.
The `grind_pattern` command remains available for cases where these
attributes do not yield the desired result.
This PR introduces the `[grind_eq]` attribute, designed to annotate
equational theorems and functions for heuristic instantiations in the
`grind` tactic.
When applied to an equational theorem, the `[grind_eq]` attribute
instructs the `grind` tactic to automatically use the annotated theorem
to instantiate patterns during proof search. If applied to a function,
it marks all equational theorems associated with that function.
```lean
@[grind_eq]
theorem foo_idempotent : foo (foo x) = foo x := ...
@[grind_eq] def f (a : Nat) :=
match a with
| 0 => 10
| x+1 => g (f x)
```
In the example above, the `grind` tactic will add instances of the
theorem `foo_idempotent` to the local context whenever it encounters the
pattern `foo (foo x)`. Similarly, functions annotated with `[grind_eq]`
will propagate this annotation to their associated equational theorems.
