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

feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) (#6795)

Browse source 
This PR adds theorems `BitVec.(getElem_umod_of_lt, getElem_umod,
getLsbD_umod, getMsbD_umod)`. For the defiition of these theorems we
rely on `divRec`, excluding the case where `d=0#w`, which is treated
separately because there is no infrastructure to reason about this case
within `divRec`. In particular, our implementation follows the mathlib
standard [where division by 0 yields
0](c7c1e091c9/src/Init/Data/BitVec/Basic.lean (L217)),
while in [SMTLIB this yields
`allOnes`](c7c1e091c9/src/Init/Data/BitVec/Basic.lean (L237)).

Co-authored by @bollu.

---------

Co-authored-by: Siddharth <siddu.druid@gmail.com>
This commit is contained in:
Luisa Cicolini 2025-02-04 16:07:29 +00:00 • committed by GitHub
parent da2b91558e
commit 3b41e43264
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Init/Data/BitVec/Bitblast.lean
View file

@ -1230,4 +1230,33 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
· simp [of_length_zero]
· simp [ushiftRightRec_eq]
/- ### umod -/
theorem getElem_umod {n d : BitVec w} (hi : i < w) :
(n % d)[i]
= if d = 0#w then n[i]
else (divRec w { n := n, d := d } (DivModState.init w)).r[i] := by
by_cases hd : d = 0#w
· simp [hd]
· have := (BitVec.not_le (x := d) (y := 0#w)).mp
rw [← BitVec.umod_eq_divRec (by simp [hd, this])]
simp [hd]
theorem getLsbD_umod {n d : BitVec w}:
(n % d).getLsbD i
= if d = 0#w then n.getLsbD i
else (divRec w { n := n, d := d } (DivModState.init w)).r.getLsbD i := by
by_cases hi : i < w
· simp only [BitVec.getLsbD_eq_getElem hi, getElem_umod]
· simp [show w ≤ i by omega]
theorem getMsbD_umod {n d : BitVec w}:
(n % d).getMsbD i
= if d = 0#w then n.getMsbD i
else (divRec w { n := n, d := d } (DivModState.init w)).r.getMsbD i := by
by_cases hi : i < w
· rw [BitVec.getMsbD_eq_getLsbD, getLsbD_umod]
simp [BitVec.getMsbD_eq_getLsbD, hi]
· simp [show w ≤ i by omega]
end BitVec