max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add BitVec.toNat_[abs|sdiv|smod] (#5491)

Browse source 
Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
This commit is contained in:
Tobias Grosser 2024-09-27 11:35:41 +01:00 • committed by GitHub
parent 2221296d3c
commit 0733273a78
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 39 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/Init/Data/BitVec/Lemmas.lean
View file

@ -1335,6 +1335,16 @@ theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
rw [BitVec.sdiv]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
match x.msb, y.msb with
| false, false => (udiv x y).toNat
| false, true => (- (x.udiv (- y))).toNat
| true, false => (- ((- x).udiv y)).toNat
| true, true => ((- x).udiv (- y)).toNat := by
simp only [sdiv_eq, toNat_udiv]
by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
have hx : x = 0#1 ∨ x = 1#1 := by bv_omega
have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
@ -1358,6 +1368,24 @@ theorem smod_eq (x y : BitVec w) : x.smod y =
rw [BitVec.smod]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
match x.msb, y.msb with
| false, false => (x.umod y).toNat
| false, true =>
let u := x.umod (- y)
(if u = 0#w then u.toNat else (u + y).toNat)
| true, false =>
let u := (-x).umod y
(if u = 0#w then u.toNat else (y - u).toNat)
| true, true => (- ((- x).umod (- y))).toNat := by
simp only [smod_eq, toNat_umod]
by_cases h : x.msb <;> by_cases h' : y.msb
<;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w
<;> simp only [h, h', h'', h''']
<;> simp only [umod, toNat_eq, toNat_ofNatLt, toNat_ofNat, Nat.zero_mod] at h'' h'''
<;> simp [h'', h''']
/-! ### signExtend -/
/-- Equation theorem for `Int.sub` when both arguments are `Int.ofNat` -/
@ -1961,6 +1989,17 @@ theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
subst h'
simp at h
/-! ### abs -/
@[simp, bv_toNat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
simp only [BitVec.abs, neg_eq]
by_cases h : x.msb = true
· simp only [h, ↓reduceIte, toNat_neg]
have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
rw [Nat.mod_eq_of_lt (by omega)]
· simp [h]
/-! ### mul -/
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl