feat: add BitVec.getLsb_concat (#3457)

First (baby)-step to a `concat`-based `bitblast`: a characterization of
`concat` in terms of `getLsb`.

The proof might benefit slightly from a `toNat_concat` lemma, but I
wasn't sure what the normal form there should be, so I avoided it.

---------

Co-authored-by: Scott Morrison <scott@tqft.net>

src/Init/Data/BitVec/Lemmas.lean

@@ -443,6 +443,21 @@ theorem truncate_succ (x : BitVec w) :
     have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
+/-! ### concat -/
+
+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

src/Init/Data/Bool.lean

@@ -220,6 +220,14 @@ def toNat (b:Bool) : Nat := cond b 1 0
 theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
+theorem toNat_lt (b : Bool) : b.toNat < 2 :=
+  Nat.lt_succ_of_le (toNat_le_one _)
+
+@[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
+  cases b <;> simp
+@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
+  cases b <;> simp
+
 end Bool
 
 /-! ### cond -/