feat: BitVec.[toInt|toFin]_concat and Bool.toInt (#6182)

This PR adds `BitVec.[toInt|toFin]_concat` and moves a couple of
theorems into the concat section, as `BitVec.msb_concat` is needed for
the `toInt_concat` proof.

We also add `Bool.toInt`.

src/Init/Data/BitVec/Lemmas.lean

@@ -2057,6 +2057,46 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
     (concat x b)[i + 1] = x[i] := by
   simp [getElem_concat, h, getLsbD_eq_getElem]
 
+@[simp]
+theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
+    (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b := by
+  simp only [getMsbD_eq_getLsbD, Nat.add_sub_cancel, getLsbD_concat]
+  by_cases h₀ : i = w
+  · simp [h₀]
+  · by_cases h₁ : i < w
+    · simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm]
+    · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_false, Bool.false_and,
+        Bool.and_eq_false_imp, decide_eq_true_eq]
+      intro
+      omega
+
+@[simp]
+theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
+    (x.concat b).msb = if 0 < w then x.msb else b := by
+  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_true, Nat.add_one_sub_one,
+    Nat.sub_zero, Bool.true_and]
+  by_cases h₀ : 0 < w
+  · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true,
+      Bool.true_and, ite_eq_right_iff]
+    intro
+    omega
+  · simp [h₀, show w = 0 by omega]
+
+@[simp] theorem toInt_concat (x : BitVec w) (b : Bool) :
+    (concat x b).toInt = if w = 0 then -b.toInt else x.toInt * 2 + b.toInt := by
+  simp only [BitVec.toInt, toNat_concat]
+  cases w
+  · cases b <;> simp [eq_nil x]
+  · cases b <;> simp <;> omega
+
+@[simp] theorem toFin_concat (x : BitVec w) (b : Bool) :
+    (concat x b).toFin = Fin.mk (x.toNat * 2 + b.toNat) (by
+      have := Bool.toNat_lt b
+      simp [← Nat.two_pow_pred_add_two_pow_pred, Bool.toNat_lt b]
+      omega
+    ) := by
+  simp [← Fin.val_inj]
+
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
   ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
 
@@ -2072,6 +2112,10 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
+@[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
+  ext
+  simp [getLsbD_concat]
+
 /-! ### shiftConcat -/
 
 theorem getLsbD_shiftConcat (x : BitVec w) (b : Bool) (i : Nat) :
@@ -2117,35 +2161,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
   have := Bool.toNat_lt b
   omega
 
-@[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
-  ext
-  simp [getLsbD_concat]
-
-@[simp]
-theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
-    (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b := by
-  simp only [getMsbD_eq_getLsbD, Nat.add_sub_cancel, getLsbD_concat]
-  by_cases h₀ : i = w
-  · simp [h₀]
-  · by_cases h₁ : i < w
-    · simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm]
-    · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_false, Bool.false_and,
-        Bool.and_eq_false_imp, decide_eq_true_eq]
-      intro
-      omega
-
-@[simp]
-theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
-    (x.concat b).msb = if 0 < w then x.msb else b := by
-  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_true, Nat.add_one_sub_one,
-    Nat.sub_zero, Bool.true_and]
-  by_cases h₀ : 0 < w
-  · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true,
-      Bool.true_and, ite_eq_right_iff]
-    intro
-    omega
-  · simp [h₀, show w = 0 by omega]
-
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl

src/Init/Data/Bool.lean

@@ -384,6 +384,15 @@ theorem toNat_lt (b : Bool) : b.toNat < 2 :=
 @[simp] theorem toNat_eq_one  {b : Bool} : b.toNat = 1 ↔ b = true := by
   cases b <;> simp
 
+/-! ## toInt -/
+
+/-- convert a `Bool` to an `Int`, `false -> 0`, `true -> 1` -/
+def toInt (b : Bool) : Int := cond b 1 0
+
+@[simp] theorem toInt_false : false.toInt = 0 := rfl
+
+@[simp] theorem toInt_true : true.toInt = 1 := rfl
+
 /-! ### ite -/
 
 @[simp] theorem if_true_left  (p : Prop) [h : Decidable p] (f : Bool) :