From 7584a93b5fd0a9b4a60165a7ef267fce8f98612b Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 11 Nov 2024 07:32:01 +0000
Subject: [PATCH] theorems

---
 src/Init/Data/BitVec/Lemmas.lean | 83 ++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 139d07705068..a3041c46e219 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2638,6 +2638,53 @@ theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
       if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by
   simp [← BitVec.getLsbD_eq_getElem, h]
 
+theorem add_mod_eq_add_sub {w : Nat} {a b : Nat} (hab_ge : a + b ≥ w) (hab_lt : a + b < 2 * w) :
+    (a + b) % w = a + b -  w := by
+  rw [Nat.mod_eq_sub_mod, Nat.mod_eq_of_lt (by omega)]
+  omega
+
+theorem getMsbD_rotateLeft {m n w : Nat} {x : BitVec w} :
+    (x.rotateLeft m).getMsbD n = (decide (n < w) && x.getMsbD ((m + n) % w)) := by
+  rw [getMsbD_eq_getLsbD, getMsbD_eq_getLsbD]
+  rcases w with rfl | w
+  · simp
+  · by_cases h₀ : n < (w + 1)
+    · simp only [h₀, decide_True, Nat.add_one_sub_one, Bool.true_and]
+      rw [← rotateLeft_mod_eq_rotateLeft]
+      have : m % (w + 1) < w + 1 := by apply Nat.mod_lt; omega
+      rw [rotateLeft_eq_rotateLeftAux_of_lt (by assumption)]
+      by_cases w - n ≥ m % (w + 1)
+      · rw [getLsbD_rotateLeftAux_of_geq (by omega)]
+        congr 1
+        · simp only [show w - n < w + 1 by omega, decide_True, Bool.true_and,
+          show (m + n) % (w + 1) < w + 1 by apply Nat.mod_lt; omega]
+        · simp only [Nat.sub_sub,
+          show (m + n) % (w + 1) = (m % (w + 1)) + n by
+            rw [Nat.add_mod, Nat.mod_eq_of_lt (a := n) (by omega), Nat.mod_eq_of_lt]; omega,
+          Nat.add_comm]
+      · rw [getLsbD_rotateLeftAux_of_le (by omega)]
+        simp_all only [ge_iff_le, Nat.not_le,
+          show ((m + n) % (w + 1) < w + 1) by apply Nat.mod_lt; omega, decide_True, Bool.true_and]
+        rw [Nat.add_mod]
+        generalize h₃ : m % (w + 1) = m'
+        rw [Nat.mod_eq_of_lt (a := n) (by omega)]
+        simp only [show w + 1 - m' + (w - n) = w - m' + (w + 1 - n) by omega,
+          show w - m' + (w + 1 - n) = w - (m' - (w + 1 - n)) by omega,
+          show w - (m' - (w + 1 - n)) = w - (m' + n - (w + 1)) by omega]
+        have : m' + n < 2 * (w + 1) := by omega
+        have : m' + n ≥ (w + 1) := by omega
+        rw [add_mod_eq_add_sub (by omega) (by omega)]
+    · simp [h₀]
+
+@[simp]
+theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
+    (x.rotateLeft m).msb = x.getMsbD (m % w) := by
+  simp only [BitVec.msb, getMsbD_rotateLeft, Nat.add_zero, Bool.and_iff_right_iff_imp,
+    decide_eq_true_eq]
+  by_cases h₀ : 0 < w
+  · simp [h₀]
+  · simp [show w = 0 by omega]
+
 /-! ## Rotate Right -/
 
 /--
@@ -2725,6 +2772,42 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
   simp only [← BitVec.getLsbD_eq_getElem]
   simp [getLsbD_rotateRight, h]
 
+@[simp]
+theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} :
+    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w) then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
+  rw [getMsbD_eq_getLsbD, getMsbD_eq_getLsbD, getMsbD_eq_getLsbD]
+  rcases w with rfl | w
+  · simp
+  · by_cases h₀ : n < w + 1
+    · have : m % (w + 1) < w + 1 := by apply Nat.mod_lt; omega
+      rw [← rotateRight_mod_eq_rotateRight, rotateRight_eq_rotateRightAux_of_lt (by assumption)]
+      simp only [h₀, decide_True, Nat.add_one_sub_one, Bool.true_and,
+        show (w + 1 + n - m % (w + 1)) % (w + 1) < w + 1 by apply Nat.mod_lt; omega]
+      generalize hm' : m % (w + 1) = m'
+      by_cases h₁ : w - n ≥ w + 1 - m'
+      · rw [getLsbD_rotateRightAux_of_geq (by omega)]
+        simp only [show w - n < w + 1 by omega, decide_True, Bool.true_and,
+          show w + 1 + n - m' < w + 1 by omega, Nat.mod_eq_of_lt]
+        by_cases h₂ : n < m'
+        <;> simp only [h₂, ↓reduceIte]; congr 1; omega
+        omega
+      · rw [getLsbD_rotateRightAux_of_le (by omega)]
+        by_cases h₂ : n < m'
+        <;> simp only [h₂, ↓reduceIte, show n - m' < w + 1 by omega, decide_True, Bool.true_and]; omega
+        congr 1; omega
+    · simp [h₀]
+
+@[simp]
+theorem msb_rotateRight {r w: Nat} {x : BitVec w} :
+    (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w) := by
+  simp only [BitVec.msb, getMsbD_rotateRight]
+  by_cases h₀ : 0 < w
+  · simp only [h₀, decide_True, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and,
+    ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq]
+    intro h₁
+    simp [h₁]
+  · simp [show w = 0 by omega]
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by