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>
Every usage of `carry` followed the pattern: `carry _ x.toNat y.toNat`,
so we've refactorod `carry` to take the `BitVec`s as arguments, and made
the `toNat` part of its definition.
This is a follow up to 'https://github.com/leanprover/std4/pull/645',
where the simp lemmas were requested:
https://github.com/leanprover/std4/pull/645#issuecomment-1944862251
---
Note that @semorrison asked to use `(Fin.last _)` to index. Now that we
use a `Nat` to index `msb` , the pattern `(Fin.last _)` would not have
the width be automatically inferred. Therefore, I've changed the
definitions to use `Nat` for indexing.
---------
Co-authored-by: Siddharth Bhat Mala <sb2743@cl.cam.ac.uk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This PR is an effort to improve reasoning at the Nat level about
bitvectors and reduce of Fin and Nat.
It slightly tightens some proofs, but is generally aimed at reducing
inconsistencies between definitions at the Nat and Fin types in favor of
more consistently using Nat operations.
This ports leanprover/std4#664 to Lean core.
Here was the rational I provided in the discussion for
leanprover/std4#664:
It's mostly about consistency. If we use the same types and style in
definitions and proofs, there is less surprise when unfolding or
otherwise using definitions. We use some Nat based operations that
haven't been extended to Fin such as the bitwise operations, and I don't
want to pay the overhead of introducing a Fin version of every Bitvector
operation.
So this basically means Nat is preferred.
One argument potentially in favor of Fin is that we could reuse results
proven there, but that doesn't really seem to be the case so far.
A second argument is that we want to simplify expression to use more
canonical forms and we currently can pretty-print those operations
better using ofNat than ofFin. We could define the notations using ofFin
of course though, but that's additional operators that will show up in
expressions.
