feat: add Bitvec reverse definition, getLsbD_reverse, getMsbD_reverse, reverse_append, reverse_replicate and Nat.mod_sub_eq_sub_mod

src/Init/Data/BitVec/Basic.lean

@@ -669,4 +669,11 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 | [] => 0#0
 | b :: bs => concat (ofBoolListLE bs) b
 
+/- ### reverse -/
+
+/-- Reverse the bits in a bitvector. -/
+def reverse : {w : Nat} → BitVec w → BitVec w
+  | 0, x => x
+  | w + 1, x => concat (reverse (x.truncate w)) (x.msb)
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -2030,6 +2030,20 @@ theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)
   ext i
   simp [cons]
 
+theorem cons_append (x y : BitVec w) (a : Bool) :
+    cons a (x ++ y) = ((cons a x) ++ y).cast (by omega) := by
+  ext i
+  simp [cons, getLsbD_cast, getLsbD_append]
+  by_cases hi₀ : i < w
+  · simp only [hi₀, ↓reduceIte, show (i - (w + w) = 0) by omega, decide_true, Bool.true_and,
+      ite_eq_left_iff, Nat.not_lt]
+    omega
+  · simp only [hi₀, ↓reduceIte]
+    by_cases hi₁ : i < w + w
+    · simp [hi₁, show i - w < w by omega]
+    · simp [hi₁, show ¬ i - w < w by omega, Nat.sub_add_eq]
+
+
 /-! ### concat -/
 
 @[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
@@ -3184,11 +3198,11 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
   ext (_ | i) h <;> simp [Bool.and_comm]
 
 @[simp]
-theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
+theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
 @[simp]
-theorem replicate_succ_eq {x : BitVec w} :
+theorem replicate_succ {x : BitVec w} :
     x.replicate (n + 1) =
     (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
   simp [replicate]
@@ -3200,7 +3214,7 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
   induction n generalizing x
   case zero => simp
   case succ n ih =>
-    simp only [replicate_succ_eq, getLsbD_cast, getLsbD_append]
+    simp only [replicate_succ, getLsbD_cast, getLsbD_append]
     by_cases hi : i < w * (n + 1)
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
@@ -3217,6 +3231,78 @@ theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
   simp only [← getLsbD_eq_getElem, getLsbD_replicate]
   by_cases h' : w = 0 <;> simp [h'] <;> omega
 
+theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
+    (x₁ ++ x₂)++ x₃ = (x₁ ++ (x₂ ++ x₃)).cast (by omega) := by
+  induction w₁ generalizing x₂ x₃
+  case zero => simp
+  case succ n ih =>
+    rw [← cons_msb_setWidth x₁]
+
+    rw [cons_]
+    sorry
+  ext i
+  simp only [getLsbD_append, getLsbD_cast]
+  by_cases hi₁ : i < w₁ <;> by_cases hi₂ : i < w₂ <;> by_cases hi₃ : i < w₃
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']
+    · omega
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']; intro; omega
+    · omega
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']
+    · omega
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']; intro; omega
+    · simp [hi']
+      by_cases hi'' : i - w₃ < w₂
+      · simp [hi'']; omega
+      · simp [hi'', Nat.sub_add_eq, show i - w₃ - w₂ = i - w₂ - w₃ by omega]
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']
+    · simp [hi']; omega
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']; intro; omega
+    · simp [hi']
+      by_cases hi'' : i - w₃ < w₂
+      · simp [hi'']; omega
+      · simp [hi'', Nat.sub_add_eq, show i - w₃ - w₂ = i - w₂ - w₃ by omega]
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']
+    · simp [hi']; omega
+  · simp [hi₁, hi₂, hi₃]
+    by_cases hi' : i < w₂ + w₃
+    · simp [hi']; intro; omega
+    · simp [hi']
+      by_cases hi'' : i - w₃ < w₂
+      · simp [hi'']; omega
+      · simp [hi'', Nat.sub_add_eq, show i - w₃ - w₂ = i - w₂ - w₃ by omega]
+
+
+theorem replicate_append_self {x : BitVec w} :
+    x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [replicate_succ]
+    conv => lhs; rw [ih]
+    simp [cast_cast, cast_eq]
+    rw [← cast_append_left]
+    · rw [append_assoc]; congr
+    · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega
+
+theorem replicate_succ' {x : BitVec w} :
+    x.replicate (n + 1) =
+    (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by
+  simp [replicate_append_self]
+
 /-! ### intMin -/
 
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
@@ -3502,6 +3588,57 @@ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
     x.abs.toInt = x.toInt.natAbs := by
   simp [toInt_abs_eq_natAbs, hx]
 
+/-! ### Reverse -/
+
+theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
+    (x.reverse).getLsbD i = x.getMsbD i := by
+  induction w generalizing i
+  case zero => simp
+  case succ n ih =>
+    simp only [reverse, truncate_eq_setWidth, getLsbD_concat]
+    rcases i with rfl | i
+    · rfl
+    · simp only [Nat.add_one_ne_zero, ↓reduceIte, Nat.add_one_sub_one, ih]
+      rw [getMsbD_setWidth]
+      simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]
+      congr; omega
+
+theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
+    (x.reverse).getMsbD i = x.getLsbD i := by
+  simp only [getMsbD_eq_getLsbD, getLsbD_reverse]
+  by_cases hi : i < w
+  · simp only [hi, decide_true, show w - 1 - i < w by omega, Bool.true_and]
+    congr; omega
+  · simp [hi, show i ≥ w by omega]
+
+theorem msb_reverse {x : BitVec w} :
+    (x.reverse).msb = x.getLsbD 0 :=
+  by rw [BitVec.msb, getMsbD_reverse]
+
+theorem reverse_append {x : BitVec w} {y : BitVec v} :
+    (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega) := by
+  ext i h
+  simp only [getLsbD_append, getLsbD_reverse]
+  by_cases hi : i < v
+  · by_cases hw : w ≤ i
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw]
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw, show i < w by omega]
+  · by_cases hw : w ≤ i
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show ¬ i < w by omega, getLsbD_reverse]
+    · simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show i < w by omega, getLsbD_reverse]
+
+@[simp]
+theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
+    (x.cast h).reverse = x.reverse.cast h := by
+  subst h; simp
+
+theorem reverse_replicate {n : Nat} {x : BitVec w} :
+    (x.replicate n).reverse = (x.reverse).replicate n := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    conv => lhs; simp only [replicate_succ']
+    simp [reverse_append, ih]
 
 /-! ### Decidable quantifiers -/
 
@@ -3717,4 +3854,10 @@ abbrev shiftLeft_zero_eq := @shiftLeft_zero
 @[deprecated ushiftRight_zero (since := "2024-10-27")]
 abbrev ushiftRight_zero_eq := @ushiftRight_zero
 
+@[deprecated replicate_zero (since := "2025-01-08")]
+abbrev replicate_zero_eq := @replicate_zero
+
+@[deprecated replicate_succ (since := "2025-01-08")]
+abbrev replicate_succ_eq := @replicate_succ
+
 end BitVec