Restore extractLsb_or

pennyannn · Sep 30, 2024 · 1becfad · 1becfad
1 parent 83a63f4
commit 1becfad
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
@@ -932,6 +932,16 @@ def extractLsByte (val : BitVec w₁) (n : Nat) : BitVec 8 :=
 theorem extractLsByte_def (val : BitVec w₁) (n : Nat) :
     val.extractLsByte n = val.extractLsb' (n * 8) 8 := rfl
 
+-- TODO: upstream
+theorem extractLsb_or (x y : BitVec w₁) (n : Nat) :
+    (x ||| y).extractLsb n lo = (x.extractLsb n lo ||| y.extractLsb n lo) := by
+  apply BitVec.eq_of_getLsbD_eq
+  simp only [getLsbD_extract, getLsbD_or]
+  intros i
+  by_cases h : (i : Nat) ≤ n - lo
+  · simp only [h, decide_True, Bool.true_and]
+  · simp only [h, decide_False, Bool.false_and, Bool.or_self]
+
 -- TODO: upstream
 theorem extractLsb'_or (x y : BitVec w₁) (n : Nat) :
     (x ||| y).extractLsb' lo n = (x.extractLsb' lo n ||| y.extractLsb' lo n) := by