feat: make BitVec.getElem the simp normal form and use it in ext (#5498)

This PR makes `BitVec.getElem` the simp normal form in case a proof is
available and changes `ext` to return `x[i]` + a hypothesis that proves
that we are in-bounds. This aligns `BitVec` further with the API
conventions of the Lean standard datatypes.

We move our proofs to this new normal form, which results in slightly
smaller proofs. With the exception of `getElem_ofFin`, no new API
surface is added as the `getElem` API has already been completed over
the previous months. We also move `getElem_shiftConcat_*` a bit higher
as they are needed in earlier proofs. To keep the changeset small, we do
not update the API of `BVDecide` but insert `←
BitVec.getLsbD_eq_getElem` at the few locations where it is needed.
Finally, we add a simproc for getElem, mirroring the existing ones for
getLsbD/getMsdD.

---------

Co-authored-by: Alex Keizer <alex@keizer.dev>

src/Init/Data/BitVec/Basic.lean

@@ -127,6 +127,7 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
 theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
   x[i] = x.toNat.testBit i := rfl
 
+@[simp]
 theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
     x.getLsbD i = x[i] := rfl
 

src/Init/Data/BitVec/Bitblast.lean

@@ -285,7 +285,7 @@ theorem adc_spec (x y : BitVec w) (c : Bool) :
     simp [carry, Nat.mod_one]
     cases c <;> rfl
   case step =>
-    simp [adcb, Prod.mk.injEq, carry_succ, getLsbD_add_add_bool]
+    simp [adcb, Prod.mk.injEq, carry_succ, getElem_add_add_bool]
 
 theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := by
   simp [adc_spec]
@@ -295,7 +295,7 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 theorem getMsbD_add {i : Nat} {i_lt : i < w} {x y : BitVec w} :
     getMsbD (x + y) i =
       Bool.xor (getMsbD x i) (Bool.xor (getMsbD y i) (carry (w - 1 - i) x y false)) := by
-  simp [getMsbD, getLsbD_add, i_lt, show w - 1 - i < w by omega]
+  simp [getMsbD, getElem_add, i_lt, show w - 1 - i < w by omega]
 
 theorem msb_add {w : Nat} {x y: BitVec w} :
     (x + y).msb =
@@ -359,24 +359,25 @@ theorem msb_sub {x y: BitVec w} :
 /-! ### Negation -/
 
 theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
-  getLsbD (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) i.val = !(getLsbD x i.val) := by
+  (((iunfoldr (fun (i : Fin w) c => (c, !(x[i.val])))) ()).snd)[i.val] = !(getLsbD x i.val) := by
   apply iunfoldr_getLsbD (fun _ => ()) i (by simp)
 
 theorem bit_not_add_self (x : BitVec w) :
-  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd + x  = -1 := by
+  ((iunfoldr (fun (i : Fin w) c => (c, !(x[i.val])))) ()).snd + x  = -1 := by
   simp only [add_eq_adc]
   apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
-  intro i; simp only [ BitVec.not, adcb, testBit_toNat]
-  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd)]
-  <;> simp [bit_not_testBit, negOne_eq_allOnes, getLsbD_allOnes]
+  intro i; simp only [adcb, Fin.is_lt, getLsbD_eq_getElem, atLeastTwo_false_right, bne_false,
+    ofNat_eq_ofNat, Fin.getElem_fin, Prod.mk.injEq, and_eq_false_imp]
+  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x[i.val])))) ()).snd)]
+  <;> simp [bit_not_testBit, negOne_eq_allOnes, getElem_allOnes]
 
 theorem bit_not_eq_not (x : BitVec w) :
-  ((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd = ~~~ x := by
+  ((iunfoldr (fun i c => (c, !(x[i])))) ()).snd = ~~~ x := by
   simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
 
-theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
+theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x[i.val])))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
   simp only [← add_eq_adc]
-  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) _ rfl]
+  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x[i.val])))) ()).snd) _ rfl]
   · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
     simp [← sub_toAdd, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
@@ -575,16 +576,18 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
       setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
   · ext k h
-    simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+    simp only [getElem_setWidth, getLsbD_setWidth, h, getLsbD_eq_getElem, getElem_or, getElem_and,
+      getElem_twoPow]
     by_cases hik : i = k
     · subst hik
       simp [h]
-    · simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]
-      by_cases hik' : k < (i + 1)
+    · by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega
         simp [hik', hik'']
+        omega
       · have hik'' : ¬ (k < i) := by omega
         simp [hik', hik'']
+        omega
   · ext k
     simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and,
       getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]

src/Init/Data/BitVec/Folds.lean

@@ -101,14 +101,14 @@ Correctness theorem for `iunfoldr`.
 theorem iunfoldr_replace
     {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
     (init : state 0 = a)
-    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value[i.val])) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
 
 theorem iunfoldr_replace_snd
   {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
     (init : state 0 = a)
-    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value[i.val])) :
     (iunfoldr f a).snd = value := by
   simp [iunfoldr.eq_test state value a init step]
 

src/Init/Data/BitVec/Lemmas.lean

@@ -22,6 +22,9 @@ namespace BitVec
 @[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
+@[simp] theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) :
+    (BitVec.ofFin x)[i] = x.val.testBit i := rfl
+
 @[simp] theorem getLsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
   let ⟨x, x_lt⟩ := x
   simp only [getLsbD_ofFin]
@@ -90,6 +93,11 @@ theorem getLsbD_eq_getElem?_getD {x : BitVec w} {i : Nat} :
   · rfl
   · simp_all
 
+@[simp]
+theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = true) :
+    (x[i]'(lt_of_getLsbD h) = true) = True := by
+  simp [← BitVec.getLsbD_eq_getElem, h]
+
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
 -/
@@ -178,9 +186,7 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
       intros
       omega
 
--- We choose `eq_of_getLsbD_eq` as the `@[ext]` theorem for `BitVec`
--- somewhat arbitrarily over `eq_of_getMsbD_eq`.
-@[ext] theorem eq_of_getLsbD_eq {x y : BitVec w}
+theorem eq_of_getLsbD_eq {x y : BitVec w}
     (pred : ∀ i, i < w → x.getLsbD i = y.getLsbD i) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
@@ -191,6 +197,21 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
     have p : i ≥ w := Nat.le_of_not_gt i_lt
     simp [testBit_toNat, getLsbD_ge _ _ p]
 
+@[ext] theorem eq_of_getElem_eq {x y : BitVec n} :
+        (∀ i (hi : i < n), x[i] = y[i]) → x = y :=
+  fun h => BitVec.eq_of_getLsbD_eq (h ↑·)
+
+theorem eq_of_getLsbD_eq_iff {w : Nat} {x y : BitVec w} :
+    x = y ↔ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i := by
+  have iff := @BitVec.eq_of_getElem_eq_iff w x y
+  constructor
+  · intros heq i lt
+    have hext := iff.mp heq i lt
+    simp only [← getLsbD_eq_getElem] at hext
+    exact hext
+  · intros heq
+    exact iff.mpr heq
+
 theorem eq_of_getMsbD_eq {x y : BitVec w}
     (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y := by
   simp only [getMsbD] at pred
@@ -211,7 +232,7 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
 -- This cannot be a `@[simp]` lemma, as it would be tried at every term.
-theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp [← getLsbD_eq_getElem]
 
 theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
 theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp
@@ -385,7 +406,12 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-theorem getElem_ofBool {b : Bool} : (ofBool b)[0] = b := by simp
+@[simp] theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
+
+@[simp]
+theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
+  simp [← getLsbD_eq_getElem]
+  omega
 
 @[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
   cases b <;> simp [getMsbD]
@@ -546,7 +572,7 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
 @[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
-  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]
+  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [←getLsbD_eq_getElem, getLsbD, h, BitVec.toInt]
 
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
@@ -761,10 +787,8 @@ theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v
 @[simp] theorem setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) :
     (x.setWidth l).setWidth k = x.setWidth k := by
   ext i
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and]
-  have p := lt_of_getLsbD (x := x) (i := i)
-  revert p
-  cases getLsbD x i <;> simp; omega
+  simp [getElem_setWidth, Fin.is_lt, decide_true, Bool.true_and]
+  omega
 
 @[simp] theorem setWidth_cast {x : BitVec w} {h : w = v} : (x.cast h).setWidth k = x.setWidth k := by
   apply eq_of_getLsbD_eq
@@ -792,11 +816,10 @@ theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
 theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
   ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
+  simp only [getElem_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
-  intros hi₁
-  have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
-  omega
+  have hv := (@Nat.testBit_one_eq_true_iff_self_eq_zero i)
+  by_cases h : Nat.testBit 1 i = true <;> simp_all
 
 /-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
 theorem setWidth_one {x : BitVec w} :
@@ -819,12 +842,9 @@ and the second `setWidth` is a non-trivial extension.
 -- `simp` can discharge the side condition itself.
 @[simp] theorem setWidth_setWidth {x : BitVec u} {w v : Nat} (h : ¬ (v < u ∧ v < w)) :
     setWidth w (setWidth v x) = setWidth w x := by
-  ext
-  simp_all only [getLsbD_setWidth, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp,
-    decide_eq_true_eq]
-  intro h
-  replace h := lt_of_getLsbD h
-  omega
+  ext i ih
+  have := @lt_of_getLsbD u x i
+  by_cases h' : x.getLsbD i = true <;> simp [h'] at * <;> omega
 
 /-! ## extractLsb -/
 
@@ -896,12 +916,13 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by
   ext
-  simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_true]
+  simp only [Fin.rev, getElem_ofFin, getElem_allOnes, Fin.is_lt, decide_true]
   rw [Fin.add_def]
   simp only [Nat.testBit_mod_two_pow, Fin.is_lt, decide_true, Bool.true_and]
   have h : (x : Nat) + (2 ^ n - (x + 1)) = 2 ^ n - 1 := by omega
   rw [h, Nat.testBit_two_pow_sub_one]
   simp
+  omega
 
 /-! ### or -/
 
@@ -983,8 +1004,8 @@ theorem or_eq_zero_iff {x y : BitVec w} : (x ||| y) = 0#w ↔ x = 0#w ∧ y = 0#
     constructor
     all_goals
     · ext i ih
-      have := BitVec.eq_of_getLsbD_eq_iff.mp h i ih
-      simp only [getLsbD_or, getLsbD_zero, Bool.or_eq_false_iff] at this
+      have := BitVec.eq_of_getElem_eq_iff.mp h i ih
+      simp only [getElem_or, getElem_zero, Bool.or_eq_false_iff] at this
       simp [this]
   · intro h
     simp [h]
@@ -1080,8 +1101,8 @@ theorem and_eq_allOnes_iff {x y : BitVec w} :
     constructor
     all_goals
     · ext i ih
-      have := BitVec.eq_of_getLsbD_eq_iff.mp h i ih
-      simp only [getLsbD_and, getLsbD_allOnes, ih, decide_true, Bool.and_eq_true] at this
+      have := BitVec.eq_of_getElem_eq_iff.mp h i ih
+      simp only [getElem_and, getElem_allOnes, Bool.and_eq_true] at this
       simp [this, ih]
   · intro h
     simp [h]
@@ -1166,8 +1187,8 @@ theorem xor_left_inj {x y : BitVec w} (z : BitVec w) : (x ^^^ z = y ^^^ z) ↔ x
   constructor
   · intro h
     ext i ih
-    have := BitVec.eq_of_getLsbD_eq_iff.mp h i
-    simp only [getLsbD_xor, Bool.xor_left_inj] at this
+    have := BitVec.eq_of_getElem_eq_iff.mp h i
+    simp only [getElem_xor, Bool.xor_left_inj] at this
     exact this ih
   · intro h
     rw [h]
@@ -1395,19 +1416,19 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
   ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]
+  simp only [getElem_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]
   by_cases h' : i < n <;> simp [h']
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
   ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]
+  simp only [getElem_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]
   by_cases h' : i < n <;> simp [h']
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
   ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]
+  simp only [getElem_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]
   by_cases h' : i < n <;> simp [h']
 
 @[simp] theorem getMsbD_shiftLeft (x : BitVec w) (i) :
@@ -1466,7 +1487,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x <<< (n + m) = (x <<< n) <<< m := by
   ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and]
+  simp only [getElem_shiftLeft, Fin.is_lt, decide_true, Bool.true_and]
   rw [show i - (n + m) = (i - m - n) by omega]
   cases h₂ : decide (i < m) <;>
   cases h₃ : decide (i - m < w) <;>
@@ -1723,7 +1744,7 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
   ext i
-  simp only [getLsbD_sshiftRight, getLsbD_xor, msb_xor]
+  simp only [getElem_sshiftRight, getElem_xor, msb_xor]
   split
     <;> by_cases w ≤ i
     <;> simp [*]
@@ -1731,7 +1752,7 @@ theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
 theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y).sshiftRight n = (x.sshiftRight n) &&& (y.sshiftRight n) := by
   ext i
-  simp only [getLsbD_sshiftRight, getLsbD_and, msb_and]
+  simp only [getElem_sshiftRight, getElem_and, msb_and]
   split
     <;> by_cases w ≤ i
     <;> simp [*]
@@ -1739,7 +1760,7 @@ theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) :
 theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y).sshiftRight n = (x.sshiftRight n) ||| (y.sshiftRight n) := by
   ext i
-  simp only [getLsbD_sshiftRight, getLsbD_or, msb_or]
+  simp only [getElem_sshiftRight, getElem_or, msb_or]
   split
     <;> by_cases w ≤ i
     <;> simp [*]
@@ -1761,31 +1782,28 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
   ext i h
-  simp [getLsbD_sshiftRight, h]
+  simp [getElem_sshiftRight, h]
 
 @[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
   ext i h
-  simp [getLsbD_sshiftRight, h]
+  simp [getElem_sshiftRight, h]
 
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp only [getLsbD_sshiftRight, Nat.add_assoc]
-  by_cases h₁ : w ≤ (i : Nat)
-  · simp [h₁]
-  · simp only [h₁, decide_false, Bool.not_false, Bool.true_and]
-    by_cases h₂ : n + ↑i < w
-    · simp [h₂]
-    · simp only [h₂, ↓reduceIte]
-      by_cases h₃ : m + (n + ↑i) < w
-      · simp [h₃]
-        omega
-      · simp [h₃, msb_sshiftRight]
+  simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
+  by_cases h₂ : n + i < w
+  · simp [h₂]
+  · simp only [h₂, ↓reduceIte]
+    by_cases h₃ : m + (n + ↑i) < w
+    · simp [h₃]
+      omega
+    · simp [h₃, msb_sshiftRight]
 
 theorem not_sshiftRight {b : BitVec w} :
     ~~~b.sshiftRight n = (~~~b).sshiftRight n := by
   ext i
-  simp only [getLsbD_not, Fin.is_lt, decide_true, getLsbD_sshiftRight, Bool.not_and, Bool.not_not,
+  simp only [getElem_not, Fin.is_lt, decide_true, getElem_sshiftRight, Bool.not_and, Bool.not_not,
     Bool.true_and, msb_not]
   by_cases h : w ≤ i
   <;> by_cases h' : n + i < w
@@ -1856,12 +1874,10 @@ theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.m
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
-  · simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_true, Bool.true_and, toNat_ofInt,
+  · simp only [signExtend, getLsbD, getElem_setWidth, hv, decide_true, Bool.true_and, toNat_ofInt,
       BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
-    rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
     simp [BitVec.testBit_toNat]
-  · simp only [getLsbD_setWidth, hv, decide_false, Bool.false_and]
-    apply getLsbD_ge
+  · simp only [getElem_setWidth, hv, decide_false, Bool.false_and]
     omega
 
 /--
@@ -1917,7 +1933,7 @@ theorem msb_signExtend {x : BitVec w} :
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
   ext i h
-  simp only [getLsbD_signExtend, h, decide_true, Bool.true_and, getLsbD_setWidth,
+  simp only [getElem_signExtend, h, decide_true, Bool.true_and, getElem_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -2018,11 +2034,11 @@ theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
   · simp_all [h]
 
 theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
-    (x ++ y)[i] = if i < m then getLsbD y i else getLsbD x (i - m) := by
-  simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
+    (x ++ y)[i] = if h : i < m then y[i] else x[i - m] := by
+  simp only [append_def]
   by_cases h' : i < m
   · simp [h']
-  · simp_all [h']
+  · simp [h', show m ≤ i by omega, show i - m < n by omega]
 
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
     getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i := by
@@ -2044,23 +2060,22 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
     simp [h, q, t, BitVec.msb, getMsbD]
 
 @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by
-  ext
-  rw [getLsbD_append] -- Why does this not work with `simp [getLsbD_append]`?
-  simp
+  ext i ih
+  rw [getElem_append] -- Why does this not work with `simp [getElem_append]`?
+  simp [show i < w by omega]
 
 @[simp] theorem zero_width_append (x : BitVec 0) (y : BitVec v) : x ++ y = y.cast (by omega) := by
-  ext
-  rw [getLsbD_append]
-  simpa using lt_of_getLsbD
+  ext i ih
+  simp [getElem_append, show i < v by omega]
 
 @[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
   ext
-  simp only [getLsbD_append, getLsbD_zero, ite_self]
+  simp [getElem_append]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     (x ++ y).cast h = x ++ y.cast (by omega) := by
   ext
-  simp only [getLsbD_cast, getLsbD_append, cond_eq_if, decide_eq_true_eq]
+  simp only [getElem_cast, getElem_append]
   split <;> split
   · rfl
   · omega
@@ -2071,57 +2086,54 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem cast_append_left (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) :
     (x ++ y).cast h = x.cast (by omega) ++ y := by
   ext
-  simp [getLsbD_append]
+  simp [getElem_append]
 
 theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
   ext i h
-  simp only [getLsbD_setWidth, h, getLsbD_append]
+  simp only [getElem_setWidth, h, getLsbD_append, getElem_append]
   split <;> rename_i h₁ <;> split <;> rename_i h₂
   · simp [h]
-  · simp [getLsbD_append, h₁]
+  · simp [getElem_append, h₁]
   · omega
-  · simp [getLsbD_append, h₁]
-    omega
+  · simp [getElem_append, h₁]
 
-@[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
+@[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) :
+    setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_append, cond_eq_if,
-    decide_eq_true_eq, Bool.true_and, setWidth_eq]
+  ext i h'
+  simp only [getElem_setWidth, getLsbD_append, getElem_append]
   split
-  · simp_all
-  · simp_all only [Bool.iff_and_self, decide_eq_true_eq]
-    intro h
-    omega
+  · simp
+  · simp
 
 @[simp] theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by
   simp [cons, setWidth_append]
 
 @[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
   ext i
-  simp only [getLsbD_not, getLsbD_append, cond_eq_if]
+  simp only [getElem_not, getElem_append, cond_eq_if]
   split
   · simp_all
-  · simp_all; omega
+  · simp_all
 
 @[simp] theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
   ext i
-  simp only [getLsbD_append, cond_eq_if]
-  split <;> simp [getLsbD_append, *]
+  simp only [getElem_and, getElem_append]
+  split <;> simp
 
 @[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
   ext i
-  simp only [getLsbD_append, cond_eq_if]
-  split <;> simp [getLsbD_append, *]
+  simp only [getElem_or, getElem_append]
+  split <;> simp
 
 @[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
   ext i
-  simp only [getLsbD_append, cond_eq_if]
-  split <;> simp [getLsbD_append, *]
+  simp only [getElem_xor, getElem_append]
+  split <;> simp
 
 theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x >>> (n + m) = (x >>> n) >>> m:= by
@@ -2151,21 +2163,19 @@ theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
 theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by
   ext i hi
-  simp only [getLsbD_ushiftRight, getLsbD_cast, getLsbD_append, getLsbD_extractLsb', getLsbD_zero,
-    Bool.if_false_right, Bool.and_self_left, Bool.iff_and_self, decide_eq_true_eq]
-  intros h
-  have := lt_of_getLsbD h
-  omega
+  simp only [getElem_cast, getElem_append, getElem_zero, getElem_ushiftRight, getElem_extractLsb']
+  split
+  · simp
+  · exact getLsbD_ge x (n+i) (by omega)
 
 theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x <<< n = (x.extractLsb' 0 (w - n) ++ 0#n).cast (by omega) := by
   ext i hi
-  simp only [getLsbD_shiftLeft, hi, decide_true, Bool.true_and, getLsbD_cast, getLsbD_append,
-    getLsbD_zero, getLsbD_extractLsb', Nat.zero_add, Bool.if_false_left]
+  simp only [getElem_shiftLeft, getElem_cast, getElem_append, getLsbD_zero, getLsbD_extractLsb',
+    Nat.zero_add, Bool.if_false_left]
   by_cases hi' : i < n
   · simp [hi']
   · simp [hi']
-    omega
 
 /-! ### rev -/
 
@@ -2241,7 +2251,7 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
 theorem setWidth_succ (x : BitVec w) :
     setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
   ext j h
-  simp only [getLsbD_setWidth, getLsbD_cons, h, decide_true, Bool.true_and]
+  simp only [getElem_setWidth, getElem_cons]
   if j_eq : j = i then
     simp [j_eq]
   else
@@ -2250,7 +2260,7 @@ theorem setWidth_succ (x : BitVec w) :
 
 @[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
   ext i
-  simp only [getLsbD_cons]
+  simp only [getElem_cons]
   split <;> rename_i h
   · simp [BitVec.msb, getMsbD, h]
   · by_cases h' : i < w
@@ -2289,7 +2299,7 @@ theorem cons_append (x : BitVec w₁) (y : BitVec w₂) (a : Bool) :
 theorem cons_append_append (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃) (a : Bool) :
     (cons a x) ++ y ++ z = (cons a (x ++ y ++ z)).cast (by omega) := by
   ext i h
-  simp only [cons, getLsbD_append, getLsbD_cast, getLsbD_ofBool, cast_cast]
+  simp only [cons, getElem_append, getElem_cast, getElem_ofBool, cast_cast, getLsbD_append, getLsbD_cast, getLsbD_ofBool]
   by_cases h₀ : i < w₁ + w₂ + w₃
   · simp only [h₀, ↓reduceIte]
     by_cases h₁ : i < w₃
@@ -2297,8 +2307,7 @@ theorem cons_append_append (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃)
     · simp only [h₁, ↓reduceIte]
       by_cases h₂ : i - w₃ < w₂
       · simp [h₂]
-      · simp [h₂]
-        omega
+      · simp [h₂, show i - w₃ - w₂ < w₁ by omega]
   · simp only [show ¬i - w₃ - w₂ < w₁ by omega, ↓reduceIte, show i - w₃ - w₂ - w₁ = 0 by omega,
       decide_true, Bool.true_and, h₀, show i - (w₁ + w₂ + w₃) = 0 by omega]
     by_cases h₂ : i < w₃
@@ -2332,7 +2341,7 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
 @[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
-  simp [getLsbD_concat]
+  simp [getElem_concat]
 
 @[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
   simp [getElem_concat]
@@ -2402,7 +2411,7 @@ theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
 
 @[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
   ext
-  simp [getLsbD_concat]
+  simp [getElem_concat]
 
 /-! ### shiftConcat -/
 
@@ -2411,6 +2420,20 @@ theorem getLsbD_shiftConcat (x : BitVec w) (b : Bool) (i : Nat) :
     = (decide (i < w) && (if (i = 0) then b else x.getLsbD (i - 1))) := by
   simp only [shiftConcat, getLsbD_setWidth, getLsbD_concat]
 
+theorem getElem_shiftConcat {x : BitVec w} {b : Bool} (h : i < w) :
+    (x.shiftConcat b)[i] = if i = 0 then b else x[i-1] := by
+  rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h, Bool.true_and]
+
+@[simp]
+theorem getElem_shiftConcat_zero {x : BitVec w} (b : Bool) (h : 0 < w) :
+    (x.shiftConcat b)[0] = b := by
+  simp [getElem_shiftConcat]
+
+@[simp]
+theorem getElem_shiftConcat_succ {x : BitVec w} {b : Bool} (h : i + 1 < w) :
+    (x.shiftConcat b)[i+1] = x[i] := by
+  simp [getElem_shiftConcat]
+
 theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
     (shiftConcat x b).getLsbD i
     = (decide (i < w) && ((decide (i = 0) && b) || (decide (0 < i) && x.getLsbD (i - 1)))) := by
@@ -2420,7 +2443,7 @@ theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
 theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
     n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
   ext i h
-  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, h, decide_true, Bool.true_and]
+  simp only [getElem_ushiftRight, getElem_shiftConcat, h, decide_true, Bool.true_and]
   split
   · simp [*]
   · congr 1; omega
@@ -2448,20 +2471,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
   have := Bool.toNat_lt b
   omega
 
-theorem getElem_shiftConcat {x : BitVec w} {b : Bool} (h : i < w) :
-    (x.shiftConcat b)[i] = if i = 0 then b else x[i-1] := by
-  rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h, Bool.true_and]
-
-@[simp]
-theorem getElem_shiftConcat_zero {x : BitVec w} (b : Bool) (h : 0 < w) :
-    (x.shiftConcat b)[0] = b := by
-  simp [getElem_shiftConcat]
-
-@[simp]
-theorem getElem_shiftConcat_succ {x : BitVec w} {b : Bool} (h : i + 1 < w) :
-    (x.shiftConcat b)[i+1] = x[i] := by
-  simp [getElem_shiftConcat]
-
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -3532,8 +3541,7 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
 @[simp]
 theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
     (x.rotateRight r)[i] = if h' : i < w - (r % w) then x[(r % w) + i] else x[(i - (w - (r % w)))] := by
-  simp only [← BitVec.getLsbD_eq_getElem]
-  simp [getLsbD_rotateRight, h]
+  simp [← BitVec.getLsbD_eq_getElem, getLsbD_rotateRight, h]
 
 theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
     (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r)) := by
@@ -3644,9 +3652,9 @@ theorem msb_twoPow {i w: Nat} :
 
 theorem and_twoPow (x : BitVec w) (i : Nat) :
     x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
-  ext j
-  simp only [getLsbD_and, getLsbD_twoPow]
-  by_cases hj : i = j <;> by_cases hx : x.getLsbD i <;> simp_all
+  ext j h
+  simp only [getElem_and, getLsbD_twoPow]
+  by_cases hj : i = j <;> by_cases hx : x.getLsbD i <;> simp_all <;> omega
 
 theorem twoPow_and (x : BitVec w) (i : Nat) :
     (twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w := by
@@ -3697,16 +3705,15 @@ theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x
 
 @[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by
   ext
-  simp [getLsbD_cons]
-  omega
+  simp [getElem_cons]
 
 @[simp] theorem false_cons_zero : cons false 0#w = 0#(w + 1) := by
   ext
-  simp [getLsbD_cons]
+  simp [getElem_cons]
 
 @[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
   ext
-  simp [getLsbD_concat]
+  simp [getElem_concat]
 
 /- ### setWidth, setWidth, and bitwise operations -/
 
@@ -3719,7 +3726,6 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) := by
   ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -3735,16 +3741,18 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) ||| (twoPow w i) := by
   ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  simp only [getElem_setWidth, h, getElem_or, getElem_twoPow]
   by_cases hik : i = k
   · subst hik
-    simp [hx, h]
-  · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
+    simp [hx]
+  · by_cases hik' : k < i + 1
+    <;> simp [hik, hik', show ¬ (k = i) by omega]
+    <;> omega
 
 /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
 theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
     (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
-  ext (_ | i) h <;> simp [Bool.and_comm]
+  ext (_ | i) h <;> simp [Bool.and_comm, h]
 
 @[simp]
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
@@ -3772,7 +3780,8 @@ theorem getLsbD_replicate {n w : Nat} {x : BitVec w} :
     by_cases hi : i < w * (n + 1)
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
-      · simp [hi', ih]
+      · rw [ih]
+        simp_all
       · simp only [hi', ↓reduceIte]
         rw [Nat.sub_mul_eq_mod_of_lt_of_le (by omega) (by omega)]
     · rw [Nat.mul_succ] at hi ⊢
@@ -3793,7 +3802,7 @@ theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w
     specialize @ih (setWidth n x₁)
     rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]
     ext j h
-    simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]
+    simp [getElem_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]
 
 theorem replicate_append_self {x : BitVec w} :
     x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
@@ -4112,6 +4121,10 @@ theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
       simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]
       congr; omega
 
+theorem getElem_reverse (x : BitVec w) (h : i < w) :
+    x.reverse[i] = x.getMsbD i := by
+  rw [← getLsbD_eq_getElem, getLsbD_reverse]
+
 theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
     (x.reverse).getMsbD i = x.getLsbD i := by
   simp only [getMsbD_eq_getLsbD, getLsbD_reverse]
@@ -4127,14 +4140,14 @@ theorem msb_reverse {x : BitVec w} :
 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]
+  simp only [getElem_reverse, getElem_cast, getElem_append]
   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]
+    · simp [getLsbD_reverse, hw]
+    · simp [getElem_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 [hw, show ¬ i < w by omega, getLsbD_reverse]
+    · simp [hw, show i < w by omega, getElem_reverse]
 
 @[simp]
 theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -158,6 +158,14 @@ builtin_dsimproc [simp, seval] reduceGetLsb (getLsbD _ _) := reduceGetBit ``getL
 /-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceGetMsb (getMsbD _ _) := reduceGetBit ``getMsbD getMsbD
 
+/-- Simplification procedure for `getElem`  on `BitVec`. -/
+builtin_dsimproc [simp, seval] reduceGetElem ((_ : BitVec _)[_]) := fun e => do
+  let_expr getElem _coll _idx _elem _valid _inst v i _h  := e | return .continue
+  let some v ← fromExpr? v | return .continue
+  let some i ← Nat.fromExpr? i | return .continue
+  let b := v.value.getLsbD i
+  return .done <| toExpr b
+
 /-- Simplification procedure for shift left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
   reduceShift ``BitVec.shiftLeft 3 BitVec.shiftLeft

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -79,7 +79,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     split
     · next hsplit => rw [rih]
     · next hsplit => rw [go_denote_mem_prefix, lih]
-  | replicate n expr ih => simp [go, ih, hidx]
+  | replicate n expr ih => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
   | signExtend v inner ih =>
     rename_i originalWidth
     generalize hgo : (go aig (signExtend v inner)).val = res
@@ -237,8 +237,8 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
       intro h
       apply BitVec.lt_of_getLsbD
       assumption
-    | rotateLeft => simp [go, ih, hidx]
-    | rotateRight => simp [go, ih, hidx]
+    | rotateLeft => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
+    | rotateRight => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
     | arithShiftRightConst n =>
       rename_i w
       have : ¬(w ≤ idx) := by omega

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean

@@ -31,7 +31,7 @@ theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign :
   constructor
   · intro h
     ext i h'
-    rw [← hleft, ← hright]
+    rw [← BitVec.getLsbD_eq_getElem, ← BitVec.getLsbD_eq_getElem, ← hleft, ← hright]
     · simp [h, h']
     · omega
     · omega

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean

@@ -426,10 +426,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       split
       · next hlt =>
         rw [hleft]
-        simp [hmod, BitVec.getLsbD_sshiftRight, hlt, hidx]
+        simp [hmod, BitVec.getElem_sshiftRight, hlt, hidx]
       · next hlt =>
         rw [hleft]
-        simp [BitVec.getLsbD_sshiftRight, hmod, hlt, hidx, BitVec.msb_eq_getLsbD_last]
+        simp [BitVec.getElem_sshiftRight, hmod, hlt, hidx, BitVec.msb_eq_getLsbD_last]
     · next hif1 =>
       simp only [Bool.not_eq_true] at hif1
       rw [← hg]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean

@@ -54,7 +54,8 @@ theorem denote_blastShiftConcat_eq_shiftConcat (aig : AIG α) (target : ShiftCon
         =
       (BitVec.shiftConcat x b).getLsbD idx := by
   intro idx hidx
-  simp [BitVec.getLsbD_shiftConcat, hidx, denote_blastShiftConcat, hx, hb]
+  simp [BitVec.getLsbD_shiftConcat, hidx, denote_blastShiftConcat, hx, hb, ← BitVec.getLsbD_eq_getElem]
+
 
 theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
     (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :

tests/lean/run/bitvec_simproc.lean

@@ -47,6 +47,10 @@ example (h : x = false) : x = (4#3).getLsbD 0:= by
   simp; guard_target =ₛ x = false; assumption
 example (h : x = true) : x = (4#3).getLsbD 2:= by
   simp; guard_target =ₛ x = true; assumption
+example (h : x = false) : x = (4#3)[0] := by
+  simp; guard_target =ₛ x = false; assumption
+example (h : x = true) : x = (4#3)[2] := by
+  simp; guard_target =ₛ x = true; assumption
 example (h : x = true) : x = (4#3).getMsbD 0:= by
   simp; guard_target =ₛ x = true; assumption
 example (h : x = false) : x = (4#3).getMsbD 2:= by