This implements the recurrence theorems `getLsb_mul`, `mulRec_zero_eq`,
`mulRec_succ_eq` to allow bitblasting multiplication.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This example, reported from LNSym, started failing when we changed the
definition of `Fin.sub` in
https://github.com/leanprover/lean4/pull/4421.
When we use the new definition, `omega` produces a proof term that the
kernel is very slow on.
To work around this for now, I've removed `BitVec.toNat_sub` from the
`bv_toNat` simp set,
and replaced it with `BitVec.toNat_sub'` which uses the old definition
for subtraction.
This is only a workaround, and I would like to understand why the term
chokes the kernel.
```
example
(n : Nat)
(addr2 addr1 : BitVec 64)
(h0 : n ≤ 18446744073709551616)
(h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
(h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
n = 18446744073709551616 := by
bv_omega
```
We add a new definition `BitVec.twoPow w i` to represent `(1#w <<< i)`.
This expression is used to test bits when building the multiplication
bitblaster.
Patch 1/?, being peeled from https://github.com/opencompl/lean4/pull/6.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
The linters in Batteries can be used to spot mistakes in Lean. See the
message on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Go-to-def.20on.20typeclass.20fields.20and.20type-dependent.20notation/near/442613564).
These are the different linters with errors:
- unusedArguments:
There are many unused instance arguments, especially a redundant `[Monad
m]` is very common
- checkUnivs:
There was a problem with universes in a definition in
`Init.Control.StateCps`. I fixed it by adding a `variable` statement for
the implicit arguments in the file.
- defLemma:
many proofs are written as `def` instead of `theorem`, most notably
`rfl`. Because `rfl` is used as a match pattern, it must be a def. Is
this desirable?
The keyword `abbrev` is sometimes used for an alias of a theorem, which
also results in a def. I would want to replace it with the `alias`
keyword to fix this, but it isn't available.
- dupNamespace:
I fixed some of these, but left `Tactic.Tactic` and `Parser.Parser` as
they are as these seem intended.
- unusedHaveSuffices:
I cleaned up a few proofs with unused `have` or `suffices`
- explicitVarsOfIff:
I didn't fix any of these, because that would be a breaking change.
- simpNF:
I didn't fix any of these, because I think that requires knowing the
intended simplification order.
The performance issue at #4413 is due to our `Fin.sub` definition.
```
def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
```
Thus, the following runs out of stack space
```
example (a : UInt64) : a - 1 = a :=
rfl
```
at the `isDefEq` test
```
(a.val.val + 18446744073709551615) % 18446744073709551616 =?= a.val.val
```
From the user's perspective, this timeout is unexpected since they are
using small numerals, and none of the other `Fin` basic operations (such
as `Fin.add` and `Fin.mul`) suffer from this problem.
This PR implements an inelegant solution for the performance issue. It
redefines `Fin.sub` as
```
def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩
```
This approach is unattractive because it relies on the fact that
`Nat.add` is defined using recursion on the second argument.
The impact on this repo was small, but we want to evaluate the impact on
Mathlib.
closes#4413
The key idea is to notice that `signExtend` behavior is controlled by
the `msb`. When `msb = false`, `sext` behaves the same as `trunc`. When
`msb = true`, `sext` behaves like `trunc` but adds high 1-bits. This is
expressed using the negate-truncate-negate pattern. Lemma statements
below:
```lean
theorem signExtend_eq_neg_truncate_neg_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
(x.signExtend v) = x.truncate v := by
theorem signExtend_eq_neg_truncate_neg_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
(x.signExtend v) = ~~~((~~~x).truncate v) := by
```
These give the final theorem statement:
```lean
theorem getLsb_signExtend {x : BitVec w} {v i : Nat} :
(x.signExtend v).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb) := by
```
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <scott@tqft.net>
Remark: when splitting an `if-then-else` term, the subgoals now have
tags `isTrue` and `isFalse` instead of `inl` and `inr`.
closes#4313
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
In the course of the development, I grabbed facts about right shifting
over integers [from
`mathlib4`](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Int/Bitwise.lean).
The core proof strategy is to perform a case analysis of the msb:
- If `msb = false`, then `sshiftRight = ushiftRight`.
- If `msb = true`. then `x >>>s i = ~~~(~~~(x >>>u i))`. The double
negation introduces the high `1` bits that one expects of the arithmetic
shift.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
These will be used by LeanSAT for bitblasting rotations by constant
distances.
We first reduce the case when the rotation amount is larger than the
width to the case where the rotation amount is less than the width
(`x.rotateLeft/Right r = x.rotateLeft/Right (r%w)`).
Then, we case analyze on the low bits versus the high bits of the
rotation, where we prove equality by extensionality.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <github@grosser.es>
These lemmas are morally equivalent to Mathlib lemmas which are proposed
to be deleted from Mathlib in
[#13286](https://github.com/leanprover-community/mathlib4/pull/13286).
It is only morally equivalent, because the Mathlib lemmas are stated in
terms of Mathlib-defined things: `toFin_natCast` uses a coercion from
`Nat` to `Fin (2^w)` which relies on `NeZero` machinery available only
in Mathlib. Thus, I've rephrased the rhs in terms of the def-eq
`Fin.ofNat'` with an explicit proof that `2^w` is non-zero.
Similarly, the RHS of `toFin_neg` was phrased in terms of negation on
`Fin`s, which is only defined in Mathlib, so I've unfolded the
definition.
This PR extracts `msb_eq_false_iff_two_mul_lt` and
`msb_eq_true_iff_two_mul_ge` from #4179, and uses them to prove a
theorem that characterizes `BitVec.toInt` in terms of `BitVec.msb`. This
lemma will be useful to prove a bit-blasting theorem for `BitVec.slt`
and `BitVec.sle`.
Also cleans up an existing proof (`toInt_eq_toNat_cond `), which turns
out to be provable by `rfl`.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This ensures that rotateLeft/Right behave correctly even when the
rotation amount is larger than the bitwidth.
This shall be followed up with `getLsb` theorems for rotations for
LeanSAT.
We choose to write `aux` definitions since it is cleaner to reason about
the `aux` theorems with the assumption that `rotation-amount <
bit-width`, followed by auxiliary lemmas that link the behavior of
rotation to the canonical case when `rotation-amount < bit-width`.
Proof strategy we will execute based on these definitions: [Link to
proof of
`getLsb_rotateLeft`](a0b18ec0f4/src/Init/Data/BitVec/Lemmas.lean (L1129-L1204))
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR adds theorems that relate unsigned bitvector comparisons
`BitVec.ult` and `BitVec.ule` to `BitVec.carry`. These lemmas are a
prerequisite to bit-blasting these comparisons in LeanSAT.
Fixes#3270 by moving the deprecation check from
`Lean.Elab.Term.mkConsts` to `Lean.Elab.Term.mkConst`, so
`Lean.Elab.Term.mkBaseProjections`, `.elabAppLValsAux`, `.elabAppFn`,
and `.elabForIn` also hit the check. Not all of these really need to hit
the check, so I'll run `!bench` to see if it's a problem.
Previously the `ac_rfl` tactic was only really usable when depending on
mathlib. With these instances, `ac_rfl` can deal with the various
operations defined in Lean.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This adds some basic lemmas to support commuting ofInt/toInt and
add/mul.
It also removes the simp annotation on `ofNat_add_ofNat` as in some
contexts the other direction or conversion to Int may be desired.
This removes simp attributes from `Nat.succ.injEq` and
`Nat.succ_sub_succ_eq_sub` to replace them with simprocs. This is
because any reductions involving `Nat.succ` has a high risk of leading
proof performance problems when dealing with even moderately large
numbers.
Here are a couple examples that will both report a maximum recursion
depth error currently. These examples are fixed by this PR.
```
example : (123456: Nat) = 12345667 := by
simp
example (x : Nat) (p : x = 0) : 1000 - (x + 1000) = 0 := by
simp
```
Make `x.toNat * 2 + b.toNat` the simp normal form of `(concat x
b).toNat`.
The choice for multiplication and addition was inspired by `Nat.bit_val`
from Mathlib.
Also, because we have considerably more lemmas about multiplication and
`_ + 1` than about shifts and `_ ||| 1`.
First (baby)-step to a `concat`-based `bitblast`: a characterization of
`concat` in terms of `getLsb`.
The proof might benefit slightly from a `toNat_concat` lemma, but I
wasn't sure what the normal form there should be, so I avoided it.
---------
Co-authored-by: Scott Morrison <scott@tqft.net>
