chore: the theorem was useless lol

Author: luisacicolini

src/Init/Data/BitVec/Bitblast.lean

@@ -3049,42 +3049,54 @@ theorem cpopNatRec_cons_eq_cpopNatRec_of_le {x : BitVec w} {b : Bool} (hn : n 
 
 theorem getLsbD_extractAndExtendPopulate_add  {x : BitVec w} (hk : k < w):
     (x.extractAndExtendPopulate w).getLsbD (pos * w + k) = ((x.extractLsb' pos 1).zeroExtend w).getLsbD k := by
+
   simp [← extractLsb'_extractAndExtendPopulate_eq (w := w) (len := w) (i := pos) (x := x)]
   omega
 
-theorem getLsbD_extractAndExtendPopulate {x : BitVec w} (hw : 0 < w) (hk : k ≤ w * w):
-    (x.extractAndExtendPopulate w).getLsbD k =
-      let idx := k % w
-      let pos := (k - idx)/w
-      (x.extractLsb' pos 1).getLsbD idx := by
-  simp
-  let idx := k % w
-  let pos := (k - idx) / w
-  have hk : k = pos * w + idx := by
-    subst pos idx
-    have : (k = (k - k % w) / w * w + k % w) ↔  (k - k % w = (k - k % w) / w * w) := by
-      sorry
-    sorry
-  have hidx : idx < w := by sorry
-  rw [hk]
-  rw [getLsbD_extractAndExtendPopulate_add (by omega)]
-  simp
-  by_cases hmod0 : idx = 0
-  · simp [hmod0, hw]
-  · simp [hmod0]
-    intros hmod
-    simp [hmod]
-    rw [Nat.add_div hw]
-    simp  [hmod, show ¬ w = 0 by omega]
-    rw [Nat.mul_div_cancel (H := by omega)]
-    have : idx / w = 0 := by exact mod_div_self k w
-    simp [this]
+theorem getLsbD_extractAndExtend_of_le_of_lt (w idx currIdx : Nat) (hw : 0 < w) (x : BitVec w)
+    (_hcurr : currIdx < w)
+    (hlt : idx < w * (currIdx + 1)) (hle : w * currIdx ≤ idx) :
+    (BitVec.zeroExtend w (BitVec.extractLsb' currIdx 1 x)).getLsbD (idx - w * currIdx) =
+    (BitVec.extractAndExtendPopulate w x).getLsbD idx := by
+  unfold BitVec.extractAndExtendPopulate
+  have ⟨res, proof⟩ := BitVec.extractAndExtendPopulateAux 0 w x (BitVec.cast (by omega) 0#0) (by omega) (by omega)
+  simp [Nat.mul_add] at hlt
+  simp [show idx - w * currIdx < w by omega]
+  by_cases h2 : idx - w * currIdx = 0
+  · have hidx : idx = currIdx * w := by rw [Nat.mul_comm]; omega
+    simp [h2]
+    simp [hidx]
+    specialize proof currIdx
+    have : res.getLsbD (currIdx * w) = (BitVec.extractLsb' (currIdx * w) w res)[0] := by
+      simp
+    simp [this, proof]
+  · have hidx : ∃ j, idx = currIdx * w + j := by
+      refine Nat.exists_eq_add_of_le (by rw [Nat.mul_comm]; omega)
+    obtain ⟨j, hj⟩ := hidx
+    simp [h2]
+    rw [hj]
+    specialize proof currIdx
+    have : res.getLsbD (currIdx * w + j) = (BitVec.extractLsb' (currIdx * w) w res).getLsbD j := by
+      simp
+      intros ht
+      by_cases hlt : j < w
+      · omega
+      · rw [Nat.mul_comm] at hj
+        omega
+    rw [this]
+    rw [proof]
+    simp
+    intros hj' hj''
+    subst hj''
+    simp
+    rw [Nat.mul_comm] at hj
+    omega
 
-    sorry
 
 theorem th3 :
     (extractAndExtendPopulate w (setWidth n x)).addRecAux n 0#w = (extractAndExtendPopulate w x).addRecAux n 0#w := by
   have : extractAndExtendPopulate w (setWidth n x) = (extractAndExtendPopulate w x).setWidth (n * w) := by
+    generalize hgen : extractAndExtendPopulate w x = gen
 
     sorry
 
@@ -3150,7 +3162,6 @@ theorem thm1 {x : BitVec (w' + 1)} (hn : n ≤ w'):
       apply eq_of_toNat_eq
       simp
 
-
       sorry
     · simp [show n' = w' + 1 by omega]
       have hext1 := extractLsb'_extractAndExtendPopulate_eq (w := w' + 1) (len := w' + 1) (i := w') (x := x)

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

@@ -95,44 +95,7 @@ theorem blastExtractAndExtend_denote_mem_prefix {w : Nat} (aig : AIG α) (curr :
   · intros
     apply extractAndExtend_le_size
 
-theorem BitVec.getLsbD_extractAndExtend_of_le_of_lt (w idx currIdx : Nat) (hw : 0 < w) (x : BitVec w)
-    (_hcurr : currIdx < w)
-    (hlt : idx < w * (currIdx + 1)) (hle : w * currIdx ≤ idx) :
-    (BitVec.zeroExtend w (BitVec.extractLsb' currIdx 1 x)).getLsbD (idx - w * currIdx) =
-    (BitVec.extractAndExtendPopulate w x).getLsbD idx := by
-  unfold BitVec.extractAndExtendPopulate
-  have ⟨res, proof⟩ := BitVec.extractAndExtendPopulateAux 0 w x (BitVec.cast (by omega) 0#0) (by omega) (by omega)
-  simp [Nat.mul_add] at hlt
-  simp [show idx - w * currIdx < w by omega]
-  by_cases h2 : idx - w * currIdx = 0
-  · have hidx : idx = currIdx * w := by rw [Nat.mul_comm]; omega
-    simp [h2]
-    simp [hidx]
-    specialize proof currIdx
-    have : res.getLsbD (currIdx * w) = (BitVec.extractLsb' (currIdx * w) w res)[0] := by
-      simp
-    simp [this, proof]
-  · have hidx : ∃ j, idx = currIdx * w + j := by
-      refine Nat.exists_eq_add_of_le (by rw [Nat.mul_comm]; omega)
-    obtain ⟨j, hj⟩ := hidx
-    simp [h2]
-    rw [hj]
-    specialize proof currIdx
-    have : res.getLsbD (currIdx * w + j) = (BitVec.extractLsb' (currIdx * w) w res).getLsbD j := by
-      simp
-      intros ht
-      by_cases hlt : j < w
-      · omega
-      · rw [Nat.mul_comm] at hj
-        omega
-    rw [this]
-    rw [proof]
-    simp
-    intros hj' hj''
-    subst hj''
-    simp
-    rw [Nat.mul_comm] at hj
-    omega
+
 
 theorem denote_blastExtractAndExtendPopulate
   (assign : α → Bool)