This adds a simplification lemma for `(x - y).toNat` when the
subtraction is known to not overflow (i.e., `y ≤ x`).
We make a new section for this for two reasons:
1. Definitions of subtraction occur before the definition of
`BitVec.le_def`, so we cannot directly place this lemma at `sub`.
2. There are other theorems of this kind, for addition and
multiplication, which can morally live in the same section.
The theorem
```lean
namespace Int
theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
match a, b with
| ofNat a, b =>
match Int.le_antisymm Ha (ofNat_zero_le a) with
| h1 =>
rw [h1, zero_ediv,]
exact Int.le_refl 0
| a, ofNat b =>
match Int.le_antisymm Hb (ofNat_zero_le b) with
| h1 =>
rw [h1, Int.ediv_zero]
exact Int.le_refl 0
| negSucc a, negSucc b =>
rw [Int.div_def, ediv]
have le_succ {a: Int} : a ≤ a+1 := (le_add_one (Int.le_refl a))
have h2: 0 ≤ ((↑b:Int) + 1) := Int.le_trans (ofNat_zero_le b) le_succ
have h3: (0:Int) ≤ ↑a / (↑b + 1) := (ediv_nonneg (ofNat_zero_le a) h2)
exact Int.le_trans h3 le_succ
```
is nontrivial to prove from existing theorems and would be nice to add
as standard theorem in DivModLemmas.
See the zullip conversation
[here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Adding.20theorem.20theorem.20ediv_nonneg'.20for.20negative.20a.20and.20b)
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
From the new doc-string:
```quote
In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, Mathlib,
and often mathematical reasoning is easier with these conventions.
At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
In September 2024, we decided to do this rename (with deprecations in place),
and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
ever need to use these functions and their associated lemmas.
```
Proves that `<` and `<=` on `BitVec` are (strict) (total) partial
orders. This is required for the `UInt` as `BitVec` refactor.
This does open the question how to state these theorems "correctly" for
`BitVec`, we have both `<` living in `Prop` and `BitVec.ult` living in
`Bool`. We might of course say to always use `<` but: Once we start
adding `IntX` we need to prove the same results for `BitVec.slt` to
provide an equivalent API. So it would appear that it is unavoidable to
have a `= true` variant of these theorems there?
Question answered: Use `<` and `slt`.
This is "upstreaming" mathlib's `unfold_let` tactic by incorporating its
functionality into `unfold`. Now `unfold` can, in addition to unfolding
global definitions, unfold local definitions. The PR also updates the
`conv` version of the tactic.
An improvement over `unfold_let` is that it beta reduces unfolded local
functions.
Two features not present in `unfold` are that (1) `unfold_let` with no
arguments does zeta delta reduction of *all* local definitions, and also
(2) `unfold_let` can interleave unfoldings (in contrast, `unfold a b c`
is exactly the same as `unfold a; unfold b; unfold c`).
Closes RFC #4090
I don't think we gain anything from having them as `abbrev` here, and
the simpNF linter complains:
```
-- Init.Data.BitVec.Lemmas
#check @BitVec.toNat_intMin /- simp can prove this:
by simp only [BitVec.toNat_twoPow]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
-/
#check @BitVec.toNat_intMax /- Left-hand side simplifies from
(BitVec.intMax w).toNat
to
(2 ^ w - 1 % 2 ^ w + 2 ^ (w - 1)) % 2 ^ w
using
simp only [@BitVec.toNat_sub, @BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat, BitVec.toNat_twoPow, Nat.add_mod_mod]
Try to change the left-hand side to the simplified term!
-/
```
```
#lint only simpNF in all
```
reports (amongst others):
```
-- Init.Data.Int.Order
#check @Int.toNat_of_nonneg /- Left-hand side simplifies from
↑a.toNat
to
max a 0
using
simp only [Int.ofNat_toNat]
Try to change the left-hand side to the simplified term!
-/
#check Int.toNat_sub_toNat_neg /- Left-hand side simplifies from
↑n.toNat - ↑(-n).toNat
to
max n 0 - max (-n) 0
using
simp only [Int.ofNat_toNat]
Try to change the left-hand side to the simplified term!
-/
```
