Update src/Init/Data/BitVec/Lemmas.lean

leanprover · Feb 23, 2024 · a8dba5d · a8dba5d
1 parent 044a7c0
commit a8dba5d
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -423,15 +423,19 @@ theorem truncate_succ (x : BitVec w) :
 
 /-! ### concat -/
 
-@[simp] theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
-    (concat x b).getLsb i = match i with
-      | 0 => b
-      | i+1 => x.getLsb i := by
+theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
+    (concat x b).getLsb i = if i = 0 then b else x.getLsb (i - 1) := by
   simp only [concat, getLsb, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
   cases i
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt]
 
+@[simp] theorem getLsb_concat_zero : (concat x b).getLsb 0 = b := by
+  simp [getLsb_concat]
+
+@[simp] theorem getLsb_concat_succ : (concat x b).getLsb (i + 1) = x.getLsb i := by
+  simp [getLsb_concat]
+
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl