feat: bv_normalize rewrite shifts by BitVec const to shift by Nat con…

…st (#6851)

This PR makes `bv_normalize` rewrite shifts by `BitVec` constants to
shifts by `Nat` constants. This is part of the greater effort in
providing good support for constant shift simplification in
`bv_normalize`.

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -257,6 +257,11 @@ theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a :
 attribute [bv_normalize] BitVec.mul_zero
 attribute [bv_normalize] BitVec.zero_mul
 
+
+attribute [bv_normalize] BitVec.shiftLeft_ofNat_eq
+attribute [bv_normalize] BitVec.ushiftRight_ofNat_eq
+attribute [bv_normalize] BitVec.sshiftRight'_ofNat_eq_sshiftRight
+
 attribute [bv_normalize] BitVec.shiftLeft_zero
 attribute [bv_normalize] BitVec.zero_shiftLeft
 

tests/lean/run/bv_decide_rewriter.lean

@@ -52,6 +52,9 @@ example : BitVec.sshiftRight 0#16 n = 0#16 := by bv_normalize
 example {x : BitVec 16} : BitVec.sshiftRight x 0 = x := by bv_normalize
 example {x : BitVec 16} : 0#16 * x = 0 := by bv_normalize
 example {x : BitVec 16} : x * 0#16 = 0 := by bv_normalize
+example {x : BitVec 16} : x >>> (12 : Nat) = x >>> 12#16 := by bv_normalize
+example {x : BitVec 16} : x <<< (12 : Nat) = x <<< 12#16 := by bv_normalize
+example {x : BitVec 16} : x.sshiftRight (12 : Nat) = x.sshiftRight' 12#16 := by bv_normalize
 example {x : BitVec 16} : x <<< 0#16 = x := by bv_normalize
 example {x : BitVec 16} : x <<< 0 = x := by bv_normalize
 example : 0#16 <<< (n : Nat) = 0 := by bv_normalize