chore: remove BitVec simps with complicated RHS (#5240)

leanprover · Sep 3, 2024 · 66688e1 · 66688e1
1 parent 4a2458b
commit 66688e1
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 8 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -322,7 +322,8 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
       · have hik'' : ¬ (k < i) := by omega
         simp [hik', hik'']
   · ext k
-    simp
+    simp only [and_twoPow, getLsbD_and, getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and,
+      getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]
     by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
 
 /--
@@ -414,7 +415,7 @@ theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
     · simp only [h, ↓reduceIte]
       rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
         shiftLeft_or_of_and_eq_zero]
-      simp
+      simp [and_twoPow]
     · simp only [h, false_eq_true, ↓reduceIte, shiftLeft_zero']
       rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)]
       simp [h]
@@ -474,7 +475,7 @@ theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
     simp only [sshiftRightRec_succ_eq, and_twoPow, ih]
     by_cases h : y.getLsbD (n + 1)
     · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
-        sshiftRight'_or_of_and_eq_zero (by simp), h]
+        sshiftRight'_or_of_and_eq_zero (by simp [and_twoPow]), h]
       simp
     · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)
         (by simp [h])]
@@ -540,7 +541,7 @@ theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
     by_cases h : y.getLsbD (n + 1) <;> simp only [h, ↓reduceIte]
     · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
         ushiftRight'_or_of_and_eq_zero]
-      simp
+      simp [and_twoPow]
     · simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false, h]
 
 /--

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1166,7 +1166,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
     have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
     simp [h, q, t, BitVec.msb, getMsbD]
 
-@[simp] theorem truncate_append {x : BitVec w} {y : BitVec v} :
+theorem truncate_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).truncate k = if h : k ≤ v then y.truncate k else (x.truncate (k - v) ++ y).cast (by omega) := by
   apply eq_of_getLsbD_eq
   intro i
@@ -1180,7 +1180,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
       simp [t, t']
 
 @[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
-  simp [cons]
+  simp [cons, truncate_append]
 
 @[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
   ext i
@@ -1765,14 +1765,12 @@ theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j
           simp at hi
         simp_all
 
-@[simp]
 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
 
-@[simp]
 theorem twoPow_and (x : BitVec w) (i : Nat) :
     (twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w := by
   rw [BitVec.and_comm, and_twoPow]