This PR adds a module `Lean.Util.CollectLooseBVars` with a function
`Expr.collectLooseBVars` that collects the set of loose bound variables
in an expression. That is, it computes the set of all `i` such that
`e.hasLooseBVar i` is true.
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 fixes a bug where the single-quote character `Char.ofNat 39`
would delaborate as `'''`, which causes a parse error if pasted back in
to the source code.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
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 changes the `show t` tactic to match its documentation.
Previously it was a synonym for `change t`, but now it finds the first
goal that unifies with the term `t` and moves it to the front of the
goal list.
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 handles constants with erased types in `toMonoType`. It is much
harder to write a test case for this than you would think, because most
references to such types get replaced with `lcErased` earlier.
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 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
```
This PR implements the main framework of the model search procedure for
the linarith component in grind. It currently handles only inequalities.
It can already solve simple goals such as
```lean
example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c : α)
: a < b → b < c → c < a → False := by
grind
example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c : α)
: a < b → b < c + d → a - d < c := by
grind
```
This PR implements the infrastructure for constructing proof terms in
the linarith procedure in `grind`. It also adds the `ToExpr` instances
for the reified objects.
This PR introduces an explicit `defeq` attribute to mark theorems that
can be used by `dsimp`. The benefit of an explicit attribute over the
prior logic of looking at the proof body is that we can reliably omit
theorem bodies across module boundaries. It also helps with intra-file
parallelism.
If a theorem is syntactically defined by `:= rfl`, then the attribute is
assumed and need not given explicitly. This is a purely syntactic check
and can be fooled, e.g. if in the current namespace, `rfl` is not
actually “the” `rfl` of `Eq`. In that case, some other syntax has be
used, such as `:= (rfl)`. This is also the way to go if a theorem can be
proved by `defeq`, but one does not actually want `dsimp` to use this
fact.
The `defeq` attribute will look at the *type* of the declaration, not
the body, to check if it really holds definitionally. Because of
different reduction settings, this can sometimes go wrong. Then one
should also write `:= (rfl)`, if one does not want this to be a defeq
theorem. (If one does then this is currently not possible, but it’s
probably a bad idea anyways).
The `set_option debug.tactic.simp.checkDefEqAttr true`, `dsimp` will
warn if could not apply a lemma due to a missing `defeq` attribute.
With `set_option backward.dsimp.useDefEqAttr.get false` one can revert
to the old behavior of inferring rfl-ness based on the theorem body.
Both options will go away eventually (too bad we can’t mark them as
deprecated right away, see #7969)
Meta programs that generate theorems (e.g. equational theorems) can use
`inferDefEqAttr` to set the attribute based on the theorem body of the
just created declaration.
This builds on #8501 to update Init to `@[expose]` a fair amount of
definitions that, if not exposed, would prevent some existing `:= rfl`
theorems from being `defeq` theorems. In the interest of starting
backwards compatible, I exposed these function. Hopefully many can be
un-exposed later again.
A mathlib adaption branch exists that includes both the meta programming
fixes and changes to the theorems (e.g. changing `:= by rfl` to `:=
rfl`).
With the module system there is now no special handling for `defeq`
theorem bodies, because we don’t look at the body anymore. The previous
hack is removed. The `defeq`-ness of the theorem needs to be checked in
the context of the theorem’s *type*; the error message contains a hint
if the defeq check fails because of the exported context.
This PR provides a special empty iterator type. Although its behavior
can be emulated with a list iterator (for example), having a special
type has the advantage of being easier to optimize for the compiler.
This PR makes the equational theorems of non-exposed defs private. If
the author of a module chose not to expose the body of their function,
then they likely don't want that implementation to leak through
equational theorems. Helps with #8419.
There is some amount of incidential complexity due to how `private`
works in lean, by mangling the name: lots of code paths that need now do
the right thing™ about private and non-private names, including the
whole reserved name machinery.
So this includes a number of refactorings:
* The logic for calculating an equational theorem name (or similar) is
now done by a single function, `mkEqLikeNameFor`, rather than all over
the place.
* Since the name of the equational theorem now depends on the current
context (in particular whether it’s a proper module, or a non-module
file), the forward map from declaration to equational theorem doesn’t
quite work anymore. This map is deleted; the list of equational theorems
are now always found by looking for declaration of the expected names
(`alreadyGenerated). If users define such theorems themselves (and make
it past the “do not allow reserved names to be declared”) they get to
keep both pieces.
* Because this map was deleted, mathlib’s `eqns` command can no longer
easily warn if equational lemmas have already been generated too early
(adaption branch exists). But in general I think lean could provide a
more principled way of supporting custom unfold lemmas, and ideally the
whole equational theorem machinery is just using that.
* The ReservedNamePredicate is used by `resolveExact`, so we need to
make sure that it returns the right name, including privateness. It is
not ok to just reserve both the private and non-private name but then
later in the ReservedNameAction produce just one of the two.
* We create `foo.def_eq` eagerly for well-founded recursion. This is
needed because we need feed in the proof of the rewriting done by
`wf_preprocess`. But if `foo.def_eq` is private in a module, then a
non-module importing it will still expect a non-private `foo.def_eq` to
exist. To patch that, we install a `copyPrivateUnfoldTheorem :
GetUnfoldEqnFn` that declares a theorem aliasing the private one. Seems
to work.
This PR removes the `NatCast (Fin n)` global instance (both the direct
instance, and the indirect one via `Lean.Grind.Semiring`), as that
instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
however that in Mathlib this happens anyway!
This PR adds a test case / use case example for `grind`, setting up the
very basics of `IndexMap`, modelled on Rust's
[`indexmap`](https://docs.rs/indexmap/latest/indexmap/). It is not
intended as a complete implementation: just enough to exercise `grind`.
(Thanks to @arthurpaulino for suggesting this as a test case.)
