From 48711ce6ebefd6805b01c697703a8e6389e6b8cf Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Fri, 27 Sep 2024 11:36:17 +0100
Subject: [PATCH] feat: BitVec.(not_sshiftRight, not_sshiftRight_not,
 getMsb_not, msb_not) (#5492)

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a599cf2dcff5..58a147a6e527 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -949,6 +949,16 @@ theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
   ext i
   simp
 
+@[simp] theorem getMsb_not {x : BitVec w} :
+    (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by
+  simp only [getMsbD]
+  by_cases h : i < w
+  · simp [h]; omega
+  · simp [h];
+
+@[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
+  simp [BitVec.msb]
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -1293,6 +1303,22 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
         omega
       · simp [h₃, sshiftRight_msb_eq_msb]
 
+theorem not_sshiftRight {b : BitVec w} :
+    ~~~b.sshiftRight n = (~~~b).sshiftRight n := by
+  ext i
+  simp only [getLsbD_not, Fin.is_lt, decide_True, getLsbD_sshiftRight, Bool.not_and, Bool.not_not,
+    Bool.true_and, msb_not]
+  by_cases h : w ≤ i
+  <;> by_cases h' : n + i < w
+  <;> by_cases h'' : 0 < w
+  <;> simp [h, h', h'']
+  <;> omega
+
+@[simp]
+theorem not_sshiftRight_not {x : BitVec w} {n : Nat} :
+    ~~~((~~~x).sshiftRight n) = x.sshiftRight n := by
+  simp [not_sshiftRight]
+
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
 @[simp]