resolve tobi comments

opencompl · Sep 5, 2024 · 4404af4 · 4404af4
1 parent 7756c4b
commit 4404af4
Showing 1 changed file with 7 additions and 7 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -769,12 +769,12 @@ def divSubtractShiftProof (qr : DivModState w) (h : qr.LawfulShiftSubtract  wr w
       apply toNat_shiftConcat_lt_of_lt_of_lt_two_pow <;> omega
     case neg.hdiv =>
       have rltd' := (BitVec.le_iff_not_lt.mp rltd)
-      simp only [qr.toNat_shiftRight_sub_one_eq h]
-      simp only [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le rltd']
-      simp only [toNat_shiftConcat_eq_of_lt_of_lt_two_pow (hk := qr.wr_lt_w h) (hx := h.hrWidth)]
-      simp only [BitVec.le_def, toNat_shiftConcat_eq_of_lt_of_lt_two_pow (hk := qr.wr_lt_w h) (hx := h.hrWidth)] at rltd'
-      simp only [toNat_shiftConcat_eq_of_lt_of_lt_two_pow (hk := qr.wr_lt_w h) (hx := h.hqWidth),
-        h.hdiv, Nat.mul_add]
+      simp only [qr.toNat_shiftRight_sub_one_eq h,
+        BitVec.toNat_sub_eq_toNat_sub_toNat_of_le rltd',
+        toNat_shiftConcat_eq_of_lt_of_lt_two_pow (qr.wr_lt_w h) h.hrWidth]
+      simp only [BitVec.le_def,
+        toNat_shiftConcat_eq_of_lt_of_lt_two_pow (qr.wr_lt_w h) h.hrWidth] at rltd'
+      simp only [toNat_shiftConcat_eq_of_lt_of_lt_two_pow (qr.wr_lt_w h) h.hqWidth, h.hdiv, Nat.mul_add]
       bv_omega
 
 /-! ### Core divsion algorithm circuit -/
@@ -834,7 +834,7 @@ theorem divRec_succ' (wn : Nat) (qr : DivModState w) :
     let input : DivModState w :=
       if r' < d then ⟨qr.q.shiftConcat false, r'⟩ else ⟨qr.q.shiftConcat true, r' - d⟩
     divRec w (wr + 1) wn n d input := by
-    simp only [divRec_succ, divSubtractShift, Nat.add_one_sub_one, decide_eq_true_eq]
+  simp [divRec_succ, divSubtractShift]
 
 /- ### Arithmetic shift right (sshiftRight) recurrence -/