This PR adds a linter (`linter.unusedSimpArgs`) that complains when a
simp argument (`simp [foo]`) is unused. It should do the right thing if
the `simp` invocation is run multiple times, e.g. inside `all_goals`. It
does not trigger when the `simp` call is inside a macro. The linter
message contains a clickable hint to remove the simp argument.
I chose to display a separate warning for each unused argument. This
means that the user has to click multiple times to remove all of them
(and wait for re-elaboration in between). But this just means multiple
endorphine kicks, and the main benefit over a single warning that would
have to span the whole argument list is that already the squigglies tell
the users about unused arguments.
This closes#4483.
Making Init and Std clean wrt to this linter revealed close to 1000
unused simp args, a pleasant experience for anyone enjoying tidying
things: #8905
This PR modifies `let` and `have` term syntaxes to be consistent with
each other. Adds configuration options; for example, `have` is
equivalent to `let +nondep`, for *nondependent* lets. Other options
include `+usedOnly` (for `let_tmp`), `+zeta` (for `letI`/`haveI`), and
`+postponeValue` (for `let_delayed)`. There is also `let (eq := h) x :=
v; b` for introducing `h : x = v` when elaborating `b`. The `eq` option
works for pattern matching as well, for example `let (eq := h) (x, y) :=
p; b`.
Future PRs will add these options to tactic syntax, once a stage0 update
has been done.
This PR implements support for (commutative) semirings in `grind`. It
uses the Grothendieck completion to construct a (commutative) ring
`Lean.Grind.Ring.OfSemiring.Q α` from a (commutative) semiring `α`. This
construction is mostly useful for semirings that implement
`AddRightCancel α`. Otherwise, the function `toQ` is not injective.
Examples:
```lean
example (x y : Nat) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
grind
example [CommSemiring α] [AddRightCancel α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
grind
example (a b : Nat) : 3 * a * b = a * b * 3 := by grind
example (k z : Nat) : k * (z * 2 * (z * 2 + 1)) = z * (k * (2 * (z * 2 + 1))) := by grind
example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α)
: x^2*y = 1 → x*y^2 = y → x + y = 1 → False := by
grind
```
This PR makes `simp` consult its own cache more often, to avoid
replicating work.
Before, the simp cache was checked upon entry of `simpImpl` only, which
then calls `simpLoop`, which recursively iterates the `pre`-lemmas,
without checking the cache again.
Now, `simpLoop` itself checks the cache. This seems more principled,
given that `simpLoop` is actually putting entries into the cache for
each of its calls, so it’s more uniform if it checks the cache itself.
This avoids repeated rewrites. For example given
```
theorem ab : a = b := testSorry
theorem bc : b = c := testSorry
example (h : P c) : P b ∧ P a := by simp [ab, bc, h]
```
simp would rewrite `b ==> c` twice (once as part of `b ==> c` and then
again as part of `a ==> b ==> c`). And it’d be order dependent: With
```
example (h : P c) : P a ∧ P b := by simp [ab, bc, h]
```
the `a ==> b ==> c` chain would insert `b ==> c` into the cache, and
picked up by `simpImpl` when rewriting `P b`.
With this change, `b ==> c` is performed only once in both examples.
Instruction counts on stdlib and mathlib both show a mild improvement
across the board (0.5%), with individual modules improving by up to 4%
in stdlib and even more in mathlib.
(This does not check the cache before applying `post`, which explains
where there are still some repeated rewrites in the trace logs. But I’m
less sure about inserting a cache check here and so I am treading
carefully here. It’s also going to be at most one `post` application
that’s duplicated, because if `post` returns `.visit`, we go back to
`pre` and thus a cache check.)
This PR refactors the way simp arguments are elaborated: Instead of
changing the `SimpTheorems` structure as we go, this elaborates each
argument to a more declarative description of what it does, and then
apply those. This enables more interesting checks of simp arguments that
need to happen in the context of the eventually constructed simp context
(the checks in #8688), or after simp has run (unused argument linter
#8901).
The new data structure describing an elaborated simp argument isn’t the
most elegant, but follows from the code.
While I am at it, move handling of `[*]` into `elabSimpArgs`. Downstream
adaption branches exist (but may not be fully up to date because of the
permission changes).
While I am at it, I cleaned up `SimpTheorems.lean` file a bit (sorting
declarations, mild renaming) and added documentation.
This PR make sure that the local instance cache calculation applies more
reductions. In #2199 there was an issue where metavariables could
prevent local variables from being considered as local instances. We use
a slightly different approach that ensures that, for example, `let`s at
the ends of telescopes do not cause similar problems. These reductions
were already being calculated, so this does not require any additional
work to be done.
Metaprogramming interface addition: the various forall telescope
functions that do reduction now have a `whnfType` flag (default false).
If it's true, then the callback `k` is given the WHNF of the type. This
is a free operation, since the telescope function already computes it.
This PR refactors `Lean.Grind.NatModule/IntModule/Ring.IsOrdered`.
We ensure the the diamond from `Ring` to `NatModule` via either
`Semiring` or `IntModule` is defeq, which was not previously the case.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This PR corrects the pretty printing of `grind` modifiers. Previously
`@[grind →]` was being pretty printed as `@[grind→ ]` (Space on the
right of the symbol, rather than left.) This fixes the pretty printing
of attributes, and preserves the presence of spaces after the symbol in
the output of `grind?`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
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 a new `BitVec.clz` operation and a corresponding `clz`
circuit to `bv_decide`, allowing to bitblast the count leading zeroes
operation. The AIG circuit is linear in the number of bits of the
original expression, making the bitblasting convenient wrt. rewriting.
`clz` is common in numerous compiler intrinsics (see
[here](https://clang.llvm.org/docs/LanguageExtensions.html#intrinsics-support-within-constant-expressions))
and architectures (see
[here](https://en.wikipedia.org/wiki/Find_first_set)).
Co-authored by @bollu.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR makes the `clear_value` tactic preserve the order of variables
in the local context. This is done by adding
`Lean.MVarId.withRevertedFrom`, which reverts all local variables
starting from a given variable, rather than only the ones that depend on
it.
Note: an alternative implementation might convert the ldecl to a cdecl
and then reset the meta cache. This assumes that there are no other
caches that might still remember the value of the ldecl.
This PR removes the auto-generated `binductionOn` and `ibelow`
implementations for inductive types in favor of the improved `brecOn`
implementation from #7639.
This PR avoids importing all of `BitVec.Lemmas` and `BitVec.BitBlast`
into `UInt.Lemmas`. (They are still imported into `SInt.Lemmas`; this
seems much harder to avoid.)
This PR implements equality elimination in `grind linarith`. The current
implementation supports only `IntModule` and `IntModule` +
`NoNatZeroDivisors`
This PR filters out all declarations from `Lean.*`, `*.Tactic.*`, and
`*.Linter.*` from the results of `exact?` and `rw?`.
---------
Co-authored-by: damiano <adomani@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR ensures the `grind linarith` module is activated for any type
that implements only `IntModule`. That is, the type does not need to be
a preorder anymore.
This PR adds the `nondep` field of `Expr.letE` to the C++ data model.
Previously this field has been unused, and in followup PRs the
elaborator will use it to encode `have` expressions (non-dependent
`let`s). The kernel does not verify that `nondep` is correctly applied
during typechecking. The `letE` delaborator now prints `have`s when
`nondep` is true, though `have` still elaborates as `letFun` for now.
Breaking change: `Expr.updateLet!` is renamed to `Expr.updateLetE!`.
This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?`
when the body is not a lambda. In any case, these functions will be
removed once the `Expr.letE (nondep := true)` encoding of `have`
expressions is complete.
This PR implements the Rabinowitsch transformation for `Field`
disequalities in `grind`. For example, this transformation is necessary
for solving:
```lean
example [Field α] (a : α) : a^2 = 0 → a = 0 := by
grind
```
This PR improves the support for fields in `grind`. New supported
examples:
```lean
example [Field α] [IsCharP α 0] (x : α) : x ≠ 0 → (4 / x)⁻¹ * ((3 * x^3) / x)^2 * ((1 / (2 * x))⁻¹)^3 = 18 * x^8 := by grind
example [Field α] (a : α) : 2 * a ≠ 0 → 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
example [Field α] [IsCharP α 0] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
example [Field α] [IsCharP α 0] (a b : α) : 2*b - a = a + b → 1 / a + 1 / (2 * a) = 3 / b := by grind
example [Field α] [NoNatZeroDivisors α] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
example [Field α] {x y z w : α} : x / y = z / w → y ≠ 0 → w ≠ 0 → x * w = z * y := by grind
example [Field α] (a : α) : a = 0 → a ≠ 1 := by grind
example [Field α] (a : α) : a = 0 → a ≠ 1 - a := by grind
```
This PR implements basic `Field` support in the commutative ring module
in `grind`. It is just division by numerals for now. Examples:
```lean
open Lean Grind
example [Field α] [IsCharP α 0] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c := by
grind
example [Field α] (a b : α) : b = 0 → (a + a) / 0 = b := by
grind
example [Field α] [IsCharP α 3] (a b : α) : a/3 = b → b = 0 := by
grind
example [Field α] [IsCharP α 7] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c + 7 := by
grind
example [Field R] [IsCharP R 0] (x : R) (cos : R → R) :
(cos x ^ 2 + (2 * cos x ^ 2 - 1) ^ 2 + (4 * cos x ^ 3 - 3 * cos x) ^ 2 - 1) / 4 =
cos x * (cos x ^ 2 - 1 / 2) * (4 * cos x ^ 3 - 3 * cos x) := by
grind
```
This PR changes the generated `below` and `brecOn` implementations for
reflexive inductive types to support motives in `Sort u` rather than
`Type u`.
Closes#7638
This PR adds an option for disabling the cutsat procedure in `grind`.
The linarith module takes over linear integer/nat constraints. Example:
```lean
set_option trace.grind.cutsat.assert true in -- cutsat should **not** process the following constraints
example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12*y - 4* z < 0 := by
grind -cutsat -- `linarith` module solves it
```
This PR implements support for the heterogeneous `(k : Nat) * (a : R)`
in ordered modules. Example:
```lean
variable (R : Type u) [IntModule R] [LinearOrder R] [IntModule.IsOrdered R]
example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
grind
example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
grind
```
This PR implements model-based theory combination for grind linarith.
Example:
```lean
example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (f : α → α → α) (x y z : α)
: z ≤ x → x ≤ 1 → z = 1 → f x y = 2 → f 1 y = 2 := by
grind
```
This PR fixes a bug in `simp` where it was not resetting the set of
zeta-delta reduced let definitions between `simp` calls. It also fixes a
bug where `simp` would report zeta-delta reduced let definitions that
weren't given as simp arguments (these extraneous let definitions appear
due to certain processes temporarily setting `zetaDelta := true`). This
PR also modifies the metaprogramming interface for the zeta-delta
tracking functions to be re-entrant and to prevent this kind of no-reset
bug from occurring again. Closes#6655.
Re-entrance of this metaprogramming interface is not needed to fix
#6655, but it is needed for some future PRs.
The `tests/lean/run/6655.lean` file has an example of a deficiency of
`simp?`, where `simp?` still over-reports unfolded let declarations.
This is likely due to `withInferTypeConfig` setting `zetaDelta := true`
from within `isDefEq`, but I did not verify this.
This PR supersedes #7539. The difference is that this PR has
`withResetZetaDeltaFVarIds` save and restore `zetaDeltaFVarIds`, but
that PR saves and then extends `zetaDeltaFVarIds` to persist unfolded
fvars. The behavior in this PR lets metaprograms control whether they
want to persist any of the unfolded fvars in this context themselves. In
practice, metaprograms that use `withResetZetaDeltaFVarIds` are creating
many temporary fvars and are doing dependence computations. These
temporary fvars shouldn't be persisted, and also dependence shouldn't be
inferred from the fact that a dependence calculation was done. (Concrete
example: the let-to-have transformation in an upcoming PR can be run
from within simp. Just because let-to-have unfolds an fvar while
calculating dependencies of lets doesn't mean that this fvar should be
included by `simp?`.)
This PR implements counterexamples for grind linarith. Example:
```lean
example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
: b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d → False := by
grind
```
produces the counterexample
```
a := 7/2
b := 1
c := 2
d := 3
```
```lean
example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
: a ≤ b → a - c ≥ 0 + d → d ≤ 0 → b = c → a ≠ b → False := by
grind
```
generates the counterexample
```
a := 0
b := 1
c := 1
d := -1
```
This PR implements disequality splitting and non-chronological
backtracking for the `grind` linarith procedure.
```lean
example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
: a ≤ b → a - c ≥ 0 + d → d ≤ 0 → d ≥ 0 → b = c → a ≠ b → False := by
grind
```
This PR adds the pre-stage0-update infrastructure for named error
messages. It adds macro syntax for registering and throwing named errors
(without elaborators), mechanisms for displaying error names in the
Infoview and at the command line, and the ability to link to error
explanations in the manual (once they are added).
This PR adds documentation to builtin attributes like `@[refl]` or
`@[implemented_by]`.
Closes#8432
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
This PR fixes an internalization bug in the interface between linarith
and ring modules in `grind`. The `CommRing` module may create new terms
during normalization.
This PR turns off the default warning when using `grind`, in preparation
for v4.22. I'll removing all the `set_option grind.warning false` in our
codebase in a second PR, after an update-stage0.
This PR implements support for inequalities in the `grind` linear
arithmetic procedure and simplifies its design. Some examples that can
already be solved:
```lean
open Lean.Grind
example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c d : α)
: a + d < c → b = a + (2:Int)*d → b - d > c → False := by
grind
example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
: a = 0 → b = 1 → a + b ≤ 2 := by
grind
example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c d e : α) :
2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0
→ a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0
→ a + b + 3*c + d + 2*e < 0 → False := by
grind
```
