WIP

src/Init/Data/BitVec/Bitblast.lean

@@ -362,12 +362,9 @@ theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
   inherit_doc mulRec_eq_mul_signExtend_setWidth]
 abbrev mulRec_eq_mul_signExtend_truncate := @mulRec_eq_mul_signExtend_setWidth
 
-theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
-    (x * y).getLsbD i = (mulRec x y w).getLsbD i := by
-  simp only [mulRec_eq_mul_signExtend_setWidth]
-  rw [setWidth_setWidth_of_le]
-  · simp
-  · omega
+theorem getElem_mul (x y : BitVec w) (i : Nat) (h : i < w) :
+    (x * y)[i] = (mulRec x y w)[i] := by
+  simp [mulRec_eq_mul_signExtend_setWidth]
 
 /-! ## shiftLeft recurrence for bitblasting -/
 

src/Init/Data/BitVec/Lemmas.lean

@@ -263,7 +263,7 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
   simp [getLsbD, BitVec.ofNat, Fin.val_ofNat']
 
 @[simp] theorem getLsbD_zero : (0#w).getLsbD i = false := by simp [getLsbD]
-
+@[simp] theorem getElem_zero (h : i < w) : (0#w)[i] = false := by simp [getElem_eq_testBit_toNat]
 @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
 
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
@@ -635,6 +635,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 @[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
   (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
 
+@[simp] theorem getElem_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) (h : i < len):
+    (extractLsb' start len x)[i] = x.getLsbD (start+i) := by
+  simp [getElem_eq_testBit_toNat, getLsbD, h]
+
 @[simp] theorem getLsbD_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
@@ -1464,7 +1468,6 @@ theorem setWidth_succ (x : BitVec w) :
     have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
-@[simp]
 theorem getElem_eq_msb {x : BitVec (w + 1)} : x[w] = x.msb := by
   simp [BitVec.msb, BitVec.getMsbD]
 
@@ -1475,7 +1478,7 @@ theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)
   · simp [h]
   · simp only [Fin.is_lt, getLsbD_eq_getElem, getElem_cast, getElem_append, getLsbD_setWidth,
     getLsbD_ofBool]
-    simp [show i = w by omega]
+    simp [show i = w by omega, getElem_eq_msb]
 
 @[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
   simp [cons]

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

@@ -204,14 +204,14 @@ end blastAdd
 
 theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
       (input : BinaryRefVec aig w)
-      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
-      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
+      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs[idx])
+      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs[idx]) :
       ∀ (idx : Nat) (hidx : idx < w),
           ⟦(blastAdd aig input).aig, (blastAdd aig input).vec.get idx hidx, assign⟧
             =
-          (lhs + rhs).getLsbD idx := by
+          (lhs + rhs)[idx] := by
   intro idx hidx
-  rw [BitVec.getLsbD_add]
+  rw [BitVec.getElem_add]
   · rw [← hleft idx hidx]
     rw [← hright idx hidx]
     unfold blastAdd
@@ -222,15 +222,16 @@ theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Boo
       rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
     · simp
     · omega
-    · intros
+    · intros idx hidx
       simp only [BinaryRefVec.lhs_get_cast, Ref.cast_eq]
       rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
       rw [hleft]
-    · intros
+      simp [hidx]
+    · intros idx hidx
       simp only [BinaryRefVec.rhs_get_cast, Ref.cast_eq]
       rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
       rw [hright]
-  · assumption
+      simp [hidx]
 
 end bitblast
 end BVExpr

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

@@ -27,20 +27,20 @@ namespace blastMul
 
 theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
     (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr[idx])
+    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr[idx])
     (hacc : ∀ (idx : Nat) (hidx : idx < w),
                 ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                   =
-                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
+                (BitVec.mulRec lexpr rexpr curr)[idx]) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
           (go aig lhs rhs (curr + 1) hcurr acc).aig,
           (go aig lhs rhs (curr + 1) hcurr acc).vec.get idx hidx,
           assign.toAIGAssignment
         ⟧
           =
-        (BitVec.mulRec lexpr rexpr w).getLsbD idx := by
+        (BitVec.mulRec lexpr rexpr w)[idx] := by
   intro idx hidx
   generalize hgo: go aig lhs rhs (curr + 1) hcurr acc = res
   unfold go at hgo
@@ -65,7 +65,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, BitVec.ofNat_eq_ofNat]
       split
       · next hdiscr =>
-        have : rexpr.getLsbD (curr + 1) = true := by
+        have : rexpr[curr + 1] = true := by
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
           rw [hright] at hdiscr
@@ -77,12 +77,13 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
           rw [hacc]
         · intros
-          simp only [denote_blastShiftLeftConst, BitVec.getLsbD_shiftLeft]
+          simp only [denote_blastShiftLeftConst, BitVec.getElem_shiftLeft]
           split
           · next hdiscr => simp [hdiscr]
           · next hidx hdiscr =>
             rw [hleft]
             simp [hdiscr, hidx]
+
       · next hdiscr =>
         have : rexpr.getLsbD (curr + 1) = false := by
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr
@@ -112,14 +113,14 @@ end blastMul
 
 theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
       (input : BinaryRefVec aig w)
-      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
-      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
+      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs[idx])
+      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs[idx]) :
       ∀ (idx : Nat) (hidx : idx < w),
         ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
           =
-        (lhs * rhs).getLsbD idx := by
+        (lhs * rhs)[idx] := by
   intro idx hidx
-  rw [BitVec.getLsbD_mul]
+  rw [BitVec.getElem_mul]
   generalize hb : blastMul aig input = res
   unfold blastMul at hb
   dsimp only at hb
@@ -145,8 +146,8 @@ theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignm
       rw [BitVec.mulRec_zero_eq]
       simp only [Nat.succ_eq_add_one, RefVec.denote_ite, BinaryRefVec.rhs_get_cast,
         Ref.gate_cast, BinaryRefVec.lhs_get_cast, denote_blastConst,
-        BitVec.ofNat_eq_ofNat, eval_const, BitVec.getLsbD_zero, Bool.if_false_right,
-        Bool.decide_eq_true]
+        BitVec.ofNat_eq_ofNat, eval_const, BitVec.getElem_zero, Bool.if_false_right,
+        Bool.decide_eq_true, hidx]
       split
       · next heq =>
         rw [← hright] at heq