From 997ae402dab2fb671a201098b4459cb254f70a1a Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 22 Feb 2024 02:28:14 +0000
Subject: [PATCH] feat: show basic properties of BitVec multiplication (#3445)

Show that multiplication of bitvectors is associative and commutative,
and show that it has 1#w as identity (both on the left and right).
---
 src/Init/Data/BitVec/Lemmas.lean | 19 +++++++++++++++++++
 src/Init/Data/Fin/Lemmas.lean    |  6 ++++++
 2 files changed, 25 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 81d3c3ee29..b27c29db57 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -505,6 +505,25 @@ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := b
 @[simp, bv_toNat] 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
 
+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⟩
+
+protected theorem mul_assoc (x y z : BitVec w) : x * y * z = x * (y * z) := by
+  apply eq_of_toFin_eq; simpa using Fin.mul_assoc ..
+instance : Std.Associative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_assoc⟩
+
+@[simp] protected theorem mul_one (x : BitVec w) : x * 1#w = x := by
+  cases w
+  · apply Subsingleton.elim
+  · apply eq_of_toNat_eq; simp [Nat.mod_eq_of_lt]
+
+@[simp] protected theorem one_mul (x : BitVec w) : 1#w * x = x := by
+  rw [BitVec.mul_comm, BitVec.mul_one]
+
+instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
+  right_id := BitVec.mul_one
+
 /-! ### le and lt -/
 
 @[bv_toNat] theorem le_def (x y : BitVec n) :
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index c21b6c2184..df3b4646ac 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -793,6 +793,12 @@ protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   ext <| by rw [mul_def, mul_def, Nat.mul_comm]
 
+protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
+  apply eq_of_val_eq
+  simp only [val_mul]
+  rw [← Nat.mod_eq_of_lt a.isLt, ← Nat.mod_eq_of_lt b.isLt, ← Nat.mod_eq_of_lt c.isLt]
+  simp only [← Nat.mul_mod, Nat.mul_assoc]
+
 protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]