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

feat: add BitVec.[getMsbD_mul, getElem_udiv, getLsbD_udiv, getMsbD_udiv] (#6674)

Browse source 
This PR adds theorems `BitVec.[getMsbD_mul, getElem_udiv, getLsbD_udiv,
getMsbD_udiv]`

---------

Co-authored-by: Siddharth <siddu.druid@gmail.com>
This commit is contained in:
Luisa Cicolini 2025-01-21 03:59:27 +00:00 • committed by GitHub
parent 8375d00d8c
commit f9e904af50
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -631,6 +631,13 @@ theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
· simp
· omega
theorem getMsbD_mul (x y : BitVec w) (i : Nat) :
(x * y).getMsbD i = (mulRec x y w).getMsbD i := by
simp only [mulRec_eq_mul_signExtend_setWidth]
rw [setWidth_setWidth_of_le]
· simp
· omega
theorem getElem_mul {x y : BitVec w} {i : Nat} (h : i < w) :
(x * y)[i] = (mulRec x y w)[i] := by
simp [mulRec_eq_mul_signExtend_setWidth]
@ -1084,6 +1091,21 @@ theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
divRec m args input := by
simp [divRec_succ, divSubtractShift]
theorem getElem_udiv (n d : BitVec w) (hy : 0#w < d) (i : Nat) (hi : i < w) :
(n / d)[i] = (divRec w {n, d} (DivModState.init w)).q[i] := by
rw [udiv_eq_divRec (by assumption)]
theorem getLsbD_udiv (n d : BitVec w) (hy : 0#w < d) (i : Nat) :
(n / d).getLsbD i = (decide (i < w) && (divRec w {n, d} (DivModState.init w)).q.getLsbD i) := by
by_cases hi : i < w
· simp [udiv_eq_divRec (by assumption)]
omega
· simp_all
theorem getMsbD_udiv (n d : BitVec w) (hd : 0#w < d) (i : Nat) :
(n / d).getMsbD i = (decide (i < w) && (divRec w {n, d} (DivModState.init w)).q.getMsbD i) := by
simp [getMsbD_eq_getLsbD, getLsbD_udiv, udiv_eq_divRec (by assumption)]
/- ### Arithmetic shift right (sshiftRight) recurrence -/
/--