This PR fixes how theorems without parameters are handled in `grind`.
This is a better fix than #11579
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR implements the option `revert`, which is set to `false` by
default. To recover the old `grind` behavior, you should use `grind
+revert`. Previously, `grind` used the `RevSimpIntro` idiom, i.e., it
would revert all hypotheses and then re-introduce them while simplifying
and applying eager `cases`. This idiom created several problems:
* Users reported that `grind` would include unnecessary parameters. See
[here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20aggressively.20includes.20local.20hypotheses.2E/near/554887715).
* Unnecessary section variables were also being introduced. See the new
test contributed by Sebastian Graf.
* Finally, it prevented us from supporting arbitrary parameters as we do
in `simp`. In `simp`, I implemented a mechanism that simulates local
universe-polymorphic theorems, but this approach could not be used in
`grind` because there is no mechanism for reverting (and re-introducing)
local universe-polymorphic theorems. Adding such a mechanism would
require substantial work: I would need to modify the local context
object. I considered maintaining a substitution from the original
variables to the new ones, but this is also tricky, because the mapping
would have to be stored in the `grind` goal objects, and it is not just
a simple mapping. After reverting everything, I would need to keep a
sequence of original variables that must be added to the mapping as we
re-introduce them, but eager case splits complicate this quite a bit.
The whole approach felt overly messy.
The new behavior `grind -revert` addresses all these issues. None of the
`grind` proofs in our test suite broke after we fixed the bugs exposed
by the new feature. That said, the traces and counterexamples produced
by `grind` are different. The new proof terms are also different.
This PR optimizes support for `Decidable` instances in `grind`. Because
`Decidable` is a subsingleton, the canonicalizer no longer wastes time
normalizing such instances, a significant performance bottleneck in
benchmarks like `grind_bitvec2.lean`. In addition, the
congruence-closure module now handles `Decidable` instances, and can
solve examples such as:
```lean
example (p q : Prop) (h₁ : Decidable p) (h₂ : Decidable (p ∧ q)) : (p ↔ q) → h₁ ≍ h₂ := by
grind
```
Although `HEq` was abbreviated as `≍` in #8503, many instances of the
form `HEq x y` still remain.
Therefore, I searched for occurrences of `HEq x y` using the regular
expression `(?<![A-Za-z/@]|``)HEq(?![A-Za-z.])` and replaced as many as
possible with the form `x ≍ y`.
This PR adds the attribute `[grind?]`. It is like `[grind]` but displays
inferred E-matching patterns. It is a more convinient than writing.
Thanks @kim-em for suggesting this feature.
```lean
set_option trace.grind.ematch.pattern true
```
This PR also improves some tests, and adds helper function
`ENode.isRoot`.
This PR makes `#guard_msgs` to treat `trace` messages separate from
`info`, `warning` and `error`. It also introduce the ability to say
`#guard_msgs (pass info`, like `(drop info)` so far, and also adds
`(check info)` as the explicit form of `(info)`, for completeness.
Fixes#8266
This PR improves support for `Nat` in the `cutsat` procedure used in
`grind`:
- `cutsat` no longer *pollutes* the local context with facts of the form
`-1 * NatCast.natCast x <= 0` for each `x : Nat`. These facts are now
stored internally in the `cutsat` state.
- A single context is now used for all `Nat` terms.
The PR also introduces a mapping mechanism for all "foreign" types that
can be converted to `Int`. Currently, only `Nat` is supported, but
additional types will be added in the future.
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.
