refactor: pot -> twoPow

src/Init/Data/BitVec/Lemmas.lean

@@ -1220,27 +1220,27 @@ theorem BitVec.mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
-/-- The Bitvector that is equal to `2^i % 2^w`, the power of 2 (`pot`). -/
-def pot {w : Nat} (i : Nat) : BitVec w := (1#w) <<< i
+/-- `twoPow i` is the bitvector `2^i` if `i < w`, and `0` otherwise. That is, the power of 2. -/
+def twoPow {w : Nat} (i : Nat) : BitVec w := (1#w) <<< i
 
 @[simp]
-theorem toNat_pot (w : Nat) (i : Nat) : (pot i : BitVec w).toNat = 2^i % 2^w := by
+theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow i : BitVec w).toNat = 2^i % 2^w := by
   rcases w with rfl | w
   · simp [Nat.mod_one]
-  · simp [pot, toNat_shiftLeft]
+  · simp [twoPow, toNat_shiftLeft]
     have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega)
     rw [Nat.mod_eq_of_lt h1]
     rw [Nat.shiftLeft_eq, Nat.one_mul]
 
 
 
 @[simp]
-theorem getLsb_pot (i j : Nat) : (pot i : BitVec w).getLsb j = ((i < w) && (i = j)) := by
+theorem getLsb_twoPow (i j : Nat) : (twoPow i : BitVec w).getLsb j = ((i < w) && (i = j)) := by
   rcases w with rfl | w
-  · simp only [pot, BitVec.reduceOfNat, Nat.zero_le, getLsb_ge, Bool.false_eq,
+  · simp only [twoPow, BitVec.reduceOfNat, Nat.zero_le, getLsb_ge, Bool.false_eq,
     Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
     omega
-  · simp only [pot, getLsb_shiftLeft, getLsb_ofNat]
+  · simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
     by_cases hj : j < i
     · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
       Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
@@ -1254,17 +1254,17 @@ theorem getLsb_pot (i j : Nat) : (pot i : BitVec w).getLsb j = ((i < w) && (i =
           simp at hi
         simp_all
 
-theorem and_pot_eq_getLsb (x : BitVec w) (i : Nat) :
-    x &&& (pot i : BitVec w) = if x.getLsb i then pot i else 0#w := by
+theorem and_twoPow_eq_getLsb (x : BitVec w) (i : Nat) :
+    x &&& (twoPow i : BitVec w) = if x.getLsb i then twoPow i else 0#w := by
   ext j
-  simp only [getLsb_and, getLsb_pot]
+  simp only [getLsb_and, getLsb_twoPow]
   by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
 
 @[simp]
-theorem mul_pot_eq_shiftLeft (x : BitVec w) (i : Nat) :
-    x * (pot i : BitVec w) = x <<< i := by
+theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
+    x * (twoPow i : BitVec w) = x <<< i := by
   apply eq_of_toNat_eq
-  simp only [toNat_mul, toNat_pot, toNat_shiftLeft, Nat.shiftLeft_eq]
+  simp only [toNat_mul, toNat_twoPow, toNat_shiftLeft, Nat.shiftLeft_eq]
   by_cases hi : i < w
   · have hpow : 2^i < 2^w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
     rw [Nat.mod_eq_of_lt hpow]
@@ -1277,18 +1277,18 @@ theorem mul_pot_eq_shiftLeft (x : BitVec w) (i : Nat) :
 /-- This is proven in BitBlast.lean, but it's a dependency that needs an import cycle to be broken. -/
 theorem add_eq_or_of_and_eq_zero (x y : BitVec w) (h : x &&& y = 0#w) : x + y = x ||| y := by sorry
 
-theorem BitVec.toNat_pot (w : Nat) (i : Nat) : (pot i : BitVec w).toNat = 2^i % 2^w := by
+theorem BitVec.toNat_twoPow (w : Nat) (i : Nat) : (twoPow i : BitVec w).toNat = 2^i % 2^w := by
   rcases w with rfl | w
   · simp [Nat.mod_one]
-  · simp [pot, toNat_shiftLeft]
+  · simp [twoPow, toNat_shiftLeft]
     have hone : 1 < 2 ^ (w + 1) := by
       rw [show 1 = 2^0 by simp[Nat.pow_zero]]
       exact Nat.pow_lt_pow_of_lt (by omega) (by omega)
     simp [Nat.mod_eq_of_lt hone, Nat.shiftLeft_eq]
 
-theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_pot (x : BitVec w) (i : Nat) :
+theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w) (i : Nat) :
     zeroExtend w (x.truncate (i + 1)) =
-      zeroExtend w (x.truncate i) + (x &&& (BitVec.pot i)) := by
+      zeroExtend w (x.truncate i) + (x &&& (BitVec.twoPow i)) := by
   rw [add_eq_or_of_and_eq_zero]
   · ext k
     simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
@@ -1327,11 +1327,11 @@ theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) :
       rw [hs];
       have heq :
         (if r.getLsb (s' + 1) = true then l <<< (s' + 1) else 0) =
-          (l * (r &&& (BitVec.pot (s' + 1)))) := by
-        simp only [ofNat_eq_ofNat, and_pot_eq_getLsb]
+          (l * (r &&& (BitVec.twoPow (s' + 1)))) := by
+        simp only [ofNat_eq_ofNat, and_twoPow_eq_getLsb]
         by_cases hr : r.getLsb (s' + 1) <;> simp [hr]
       rw [heq, ← BitVec.mul_add]
-      rw [← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_pot]
+      rw [← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
 
 /-- Zero extending by number of bits larger than the bitwidth has no effect. -/
 theorem zeroExtend_of_ge {x : BitVec w} {i j : Nat} (hi : i ≥ w) :