From 8f98fee41497aa81657432cb51d4f85e8516f541 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Tue, 21 Jan 2025 03:59:27 +0000 Subject: [PATCH] feat: add `BitVec.[getMsbD_mul, getElem_udiv, getLsbD_udiv, getMsbD_udiv]` (#6674) This PR adds theorems `BitVec.[getMsbD_mul, getElem_udiv, getLsbD_udiv, getMsbD_udiv]` --------- Co-authored-by: Siddharth --- src/Init/Data/BitVec/Bitblast.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 1f086933f7ce..003d35aa2ca3 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -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 -/ /--