Tests using `logInfo` were taking an additional two seconds on my
machine. This is a performance issue with the old code generator, where
we spend all this time specializing the logging functions for `GoalM`. I
have not checked whether the new code generator is also affected by this
performance issue.
Here is a small example that exposes the issue:
```lean
import Lean
set_option profiler true
open Lean Meta Grind in
def test (e : Expr): GoalM Unit := do
logInfo e
```
cc @zwarich
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 allows the dot ident notation to resolve to the current
definition, or to any of the other definitions in the same mutual block.
Existing code that uses dot ident notation may need to have `nonrec`
added if the ident has the same name as the definition.
Closes#6601
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.
Users have requested toolchain tags on `lean4-cli`, so let's add it to
the release checklist to make sure these get added regularly.
Previously, `lean4-cli` has used more complicated tags, but going
forward we're going to just use the simple `v4.16.0` style tags, with no
repository-specific versioning.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR adds a `toFin` and `msb` lemma for unsigned bitvector modulus.
Similar to #6402, we don't provide a general `toInt_umod` lemmas, but
instead choose to provide more specialized rewrites, with extra
side-conditions.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This PR adds a `toFin` and `msb` lemma for unsigned bitvector division.
We *don't* have `toInt_udiv`, since the only truly general statement we
can make does no better than unfolding the definition, and it's not
uncontroversially clear how to unfold `toInt` (see
`toInt_eq_msb_cond`/`toInt_eq_toNat_cond`/`toInt_eq_toNat_bmod` for a
few options currently provided). Instead, we do have `toInt_udiv_of_msb`
that's able to provide a more meaningful rewrite given an extra
side-condition (that `x.msb = false`).
This PR also upstreams a minor `Nat` theorem (`Nat.div_le_div_left`)
needed for the above from Mathlib.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
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>
