This PR improves the theorems used to justify the steps performed by the
inequality offset module. See new test for examples of how they are
going to be used.
This PR implements `Std.Net.Addr` which contains structures around IP
and socket addresses.
While we could implement our own parser instead of going through the
`addr_in`/`addr_in6` route we will need to implement these conversions
to make proper system calls anyway. Hence this is likely the approach
with the least amount of non trivial code overall. The only thing I am
uncertain about is whether `ofString` should return `Option` or
`Except`, unfortunately `libuv` doesn't hand out error messages on IP
parsing.
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 fixes the location of the error emitted when the `rintro` and
`intro` tactics cannot introduce the requested number of binders.
This patch adds a few `withRef` wrappers to invocations of
`MVarId.intro` to fix error locations. Perhaps `MVarId.intro` should
take a syntax object to set the location itself in the future; however
there are a couple other call sites which would need non-trivial fixup.
Closes #5659.
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 modifies the `induction`/`cases` syntax so that the `with`
clause does not need to be followed by any alternatives. This improves
friendliness of these tactics, since this lets them surface the names of
the missing alternatives:
```lean
example (n : Nat) : True := by
induction n with
/- ~~~~
alternative 'zero' has not been provided
alternative 'succ' has not been provided
-/
```
Related to issue #3555
This PR adds additional tests for `grind`, demonstrating that we can
automate some manual proofs from Mathlib's basic category theory
library, with less reliance on Mathlib's `@[reassoc]` trick.
In several places I've added bidirectional patterns for equational
lemmas.
I've updated some other files to use the new `@[grind_eq]` attribute
(but left as is all cases where we are inspecting the info messages from
`grind_pattern`).
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
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.
This PR introduces support for user-defined fallback code in the `grind`
tactic. The fallback code can be utilized to inspect the state of
failing `grind` subgoals and/or invoke user-defined automation. Users
can now write `grind on_failure <code>`, where `<code>` should have the
type `GoalM Unit`. See the modified tests in this PR for examples.
This PR adds a custom congruence rule for equality in `grind`. The new
rule takes into account that `Eq` is a symmetric relation. In the
future, we will add support for arbitrary symmetric relations. The
current rule is important for propagating disequalities effectively in
`grind`.
This PR fixes a bug in the congruence closure data structure used in the
`grind` tactic. The new test includes an example that previously caused
a panic. A similar panic was also occurring in the test
`grind_nested_proofs.lean`.
This PR adds a simple strategy to the (WIP) `grind` tactic. It just
keeps internalizing new theorem instances found by E-matching. The
simple strategy can solve examples such as:
```lean
grind_pattern Array.size_set => Array.set a i v h
grind_pattern Array.get_set_eq => a.set i v h
grind_pattern Array.get_set_ne => (a.set i v hi)[j]
example (as bs : Array α) (v : α)
(i : Nat)
(h₁ : i < as.size)
(h₂ : bs = as.set i v)
: as.size = bs.size := by
grind
example (as bs cs : Array α) (v : α)
(i : Nat)
(h₁ : i < as.size)
(h₂ : bs = as.set i v)
(h₃ : cs = bs)
(h₄ : i ≠ j)
(h₅ : j < cs.size)
(h₆ : j < as.size)
: cs[j] = as[j] := by
grind
opaque R : Nat → Nat → Prop
theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry
grind_pattern Rtrans => R a b, R b c
example : R a b → R b c → R c d → R d e → R a d := by
grind
```
This PR fixes a bug in the theorem instantiation procedure in the (WIP)
`grind` tactic. For example, it was missing the following instance in
one of the tests:
```lean
[grind.ematch.instance] Array.get_set_ne: ∀ (hj : i < bs.size), j ≠ i → (bs.set j w ⋯)[i] = bs[i]
```
This PR also renames the `grind` base monad to `GrindCoreM`.
This PR adds a deriving handler for the `ToExpr` class. It can handle
mutual and nested inductive types, however it falls back to creating
`partial` instances in such cases. This is upstreamed from the Mathlib
deriving handler written by @kmill, but has fixes to handle autoimplicit
universe level variables.
This is a followup to #6285 (adding the `ToLevel` class). This PR
supersedes #5906.
Co-authored-by: Alex Keizer <alex@keizer.dev>
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
This PR adds support for activating relevant theorems for the (WIP)
`grind` tactic. We say a theorem is relevant to a `grind` goal if the
symbols occurring in its patterns also occur in the goal.
This PR adds pattern validation to the `grind_pattern` command. The new
`checkCoverage` function will also be used to implement the attributes
`@[grind_eq]`, `@[grind_fwd]`, and `@[grind_bwd]`.
This PR implements the command `grind_pattern`. The new command allows
users to associate patterns with theorems. These patterns are used for
performing heuristic instantiation with e-matching. In the future, we
will add the attributes `@[grind_eq]`, `@[grind_fwd]`, and
`@[grind_bwd]` to compute the patterns automatically for theorems.
This PR completes the implementation of `addCongrTable` in the (WIP)
`grind` tactic. It also adds a new test to demonstrate why the extra
check is needed. It also updates the field `cgRoot` (congruence root).
