Merge remote-tracking branch 'origin/master' into BitVec.pow

src/Init/Data/BitVec/Basic.lean

@@ -227,6 +227,20 @@ SMT-LIB name: `bvmul`.
 protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)
 instance : Mul (BitVec n) := ⟨.mul⟩
 
+/--
+Raises a bitvector to a natural number power. Usually accessed via the `^` operator.
+
+Note that this is currently an inefficient implementation,
+and should be replaced via an `@[extern]` with a native implementation.
+See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def pow (x : BitVec n) (y : Nat) : BitVec n :=
+  match y with
+  | 0 => 1
+  | y + 1 => x.pow y * x
+instance : Pow (BitVec n) Nat where
+  pow x y := x.pow y
+
 /--
 Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
 Usually accessed via the `/` operator.

src/Init/Data/BitVec/Lemmas.lean

@@ -3653,6 +3653,13 @@ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := b
 @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
 @[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
 
+theorem ofNat_mul {n} (x y : Nat) : BitVec.ofNat n (x * y) = BitVec.ofNat n x * BitVec.ofNat n y := by
+  apply eq_of_toNat_eq
+  simp [BitVec.ofNat, Fin.ofNat'_mul]
+
+theorem ofNat_mul_ofNat {n} (x y : Nat) : BitVec.ofNat n x * BitVec.ofNat n y = BitVec.ofNat n (x * y) :=
+  (ofNat_mul x y).symm
+
 protected theorem mul_comm (x y : BitVec w) : x * y = y * x := by
   apply eq_of_toFin_eq; simpa using Fin.mul_comm ..
 instance : Std.Commutative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_comm⟩
@@ -3746,6 +3753,22 @@ theorem setWidth_mul (x y : BitVec w) (h : i ≤ w) :
   have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h
   simp [bitvec_to_nat, h, Nat.mod_mod_of_dvd _ dvd]
 
+/-! ### pow -/
+
+@[simp]
+protected theorem pow_zero {x : BitVec w} : x ^ 0 = 1#w := rfl
+
+protected theorem pow_succ {x : BitVec w} : x ^ (n + 1) = x ^ n * x := rfl
+
+@[simp]
+protected theorem pow_one {x : BitVec w} : x ^ 1 = x := by simp [BitVec.pow_succ]
+
+protected theorem pow_add {x : BitVec w} {n m : Nat}: x ^ (n + m) = (x ^ n) * (x ^ m):= by
+  induction m with
+  | zero => simp
+  | succ m ih =>
+    rw [← Nat.add_assoc, BitVec.pow_succ, ih, BitVec.mul_assoc, BitVec.pow_succ]
+
 /-! ### le and lt -/
 
 @[bitvec_to_nat] theorem le_def {x y : BitVec n} :