This PR adds theorems `BitVec.(toNat, toInt,
toFin)_shiftLeftZeroExtend`, completing the API for
`BitVec.shiftLeftZeroExtend`.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This PR allow structures to have non-bracketed binders, making it
consistent with `inductive`.
The change allows the following to be written instead of having to write
`S (n)`:
```lean
structure S n where
field : Fin n
```
This PR removes the auto-generated `binductionOn` and `ibelow`
implementations for inductive types in favor of the improved `brecOn`
implementation from #7639.
This PR defines the embedding of a `CommSemiring` into its `CommRing`
envelope, injective when the `CommSemiring` is cancellative. This will
be used by `grind` to prove results in `Nat`.
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 renames `BitVec.getLsb'` to `BitVec.getLsb`, now that older
deprecated definition occupying that name has been removed. (Similarly
for `BitVec.getMsb'`.)
This PR improves IR generation for constructors of inductive types that
are represented by scalars. Surprisingly, this isn't required for
correctness, because the boxing pass will fix it up. The extra `unbox`
operation it inserts shouldn't matter when compiling to native code,
because it's trivial for a C compiler to optimize, but it does matter
for the interpreter.
This PR adds a cache for constructor info in toIR. This is called for
all constructors, projections, and cases alternatives, so it makes sense
to cache.
This PR adds constant folding for Char.ofNat in LCNF simp. This
implicitly relies on the representation of `Char` as `UInt32` rather
than making a separate `.char` literal type, which seems reasonable as
`Char` is erased by the trivial structure optimization in `toMono`.
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 introduces the basic theory of ordered modules over Nat (i.e.
without subtraction), for `grind`. We'll solve problems here by
embedding them in the `IntModule` envelope.
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
```
