This PR fixes a bug in `floatLetIn` where if one decl (e.g. a join
point) is floated into a case arm and it uses another decl (e.g. another
join point) that does not have any other existing uses in that arm, then
the second decl does not get floated in despite this being perfectly
legal. This was causing artificial array linearity issues in
`Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis`.
This PR adds the following instance
```
instance [Field α] [LinearOrder α] [Ring.IsOrdered α] : IsCharP α 0
```
The goal is to ensure we do not perform unnecessary case-splits in our
test suite.
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 makes Lean code generation respect the module name provided
through `lean --setup`.
This is accomplished by porting to Lean the portion of `shell.cpp` that
spans running the frontend to exiting the process. This makes it easier
to load the module setup and control how its name is passed to the code
generation functions. This port attempts to minimize the changes made to
Lean. It marks the new Lean functions `private` and tries to preserve as
faithfully as possible the behavior of the original C++ code. Exposing
the new Lean interface publicly and/or further improving the code now
that is written in Lean is left for the future.
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 modifies the `structure` elaborator to add local terminfo for
structure fields and explicit parent projections, enabling "go to
definition" when there are dependent fields.
Terminfo for inherited fields is still missing.
This PR adds `have` forms of simp lemmas that will be used in a future
`have` simplifier. This depends on #8751 and future elaboration changes,
since these are meant to elaborate using `Expr.letE (nondep := true) ..`
expressions; for now they are duplicates of the `letFun_*` lemmas.
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>
glibc adds `__attribute__((nothrow))` to its declarations, at least for
those related to malloc. glibc has yet to introduce `free_sized`, but
when it does it would cause compilation errors. This is due to the fact
that if a function declarations has `__attribute__((nothrow))` and it is
re-declared or implemented in C++ it must also have
`__attribute__((nothrow))` or `noexcept`, otherwise the compilation will
fail.
This is a follow up to https://github.com/leanprover/lean4/pull/6598.
Signed-off-by: Justin King <jcking@google.com>
This PR changes the LCNF pass pipeline so checks are no longer run by
default after every pass, only after `init`, `saveBase`, `toMono` and
`saveMono`. This is a compile time improvement, and the utility of these
checks is decreased a bit after the decision to no longer attempt to
preserve types throughout compilation. They have not been a significant
way to discover issues during development of the new compiler.
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 adds caching for the `hasTrivialStructure?` function for LCNF
types. This is one of the hottest small functions in the new compiler,
so adding a cache makes a lot of sense.
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.
