diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean index bc120154e110..8b24cd627849 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean @@ -78,6 +78,16 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate let some i ← Nat.fromExpr? e.appArg! | return .continue return .done <| toExpr (op v.value i) +/-- +Helper function for reducing `x <<< i` and `x >>> i` where `i` is a bitvector literal, +into one that is a natural number literal. +-/ +@[inline] def reduceShiftWithBitVecLit (declName : Name) (e : Expr) : SimpM DStep := do + unless e.isAppOfArity declName 6 do return .continue + let v := e.appFn!.appArg! + let some i ← fromExpr? e.appArg! | return .continue + return .visit (← mkAppM declName #[v, toExpr i.value.toNat]) + /-- Helper function for reducing bitvector predicates. -/ @@ -158,9 +168,15 @@ builtin_dsimproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) := /-- Simplification procedure for shift left on `BitVec`. -/ builtin_dsimproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) := reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·) +/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/ +builtin_dsimproc [simp, seval] reduceHShiftLeft' ((_ <<< (_ : BitVec _) : BitVec _)) := + reduceShiftWithBitVecLit ``HShiftLeft.hShiftLeft /-- Simplification procedure for shift right on `BitVec`. -/ builtin_dsimproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) := reduceShift ``HShiftRight.hShiftRight 6 (· >>> ·) +/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/ +builtin_dsimproc [simp, seval] reduceHShiftRight' ((_ >>> (_ : BitVec _) : BitVec _)) := + reduceShiftWithBitVecLit ``HShiftRight.hShiftRight /-- Simplification procedure for rotate left on `BitVec`. -/ builtin_dsimproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) := reduceShift ``BitVec.rotateLeft 3 BitVec.rotateLeft diff --git a/tests/lean/run/bitvec_simproc.lean b/tests/lean/run/bitvec_simproc.lean index cd18c5a3b066..997095fb0703 100644 --- a/tests/lean/run/bitvec_simproc.lean +++ b/tests/lean/run/bitvec_simproc.lean @@ -113,3 +113,11 @@ example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by simp; guard_target =ₛ1019#10 = x; assumption example (h : 5#10 = x) : -signExtend 10 (-5#8) = x := by simp; guard_target =ₛ5#10 = x; assumption +example (h : 40#32 = b) : 10#32 <<< 2#32 = b := by + simp; guard_target =ₛ 40#32 = b; assumption +example (h : 3#32 = b) : 12#32 >>> 2#32 = b := by + simp; guard_target =ₛ 3#32 = b; assumption +example (a : BitVec 32) (h : a >>> 2 = b) : a >>> 2#32 = b := by + simp; guard_target =ₛ a >>> 2 = b; assumption +example (a : BitVec 32) (h : a <<< 2 = b) : a <<< 2#32 = b := by + simp; guard_target =ₛ a <<< 2 = b; assumption