feat: more getLsbD bitblaster theory (#5637)

leanprover · Oct 7, 2024 · f1ff9ce · f1ff9ce
1 parent 99a9d9b
commit f1ff9ce
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
@@ -20,6 +20,20 @@ namespace BVPred
 
 variable [Hashable α] [DecidableEq α]
 
+theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec w)
+    (xv : AIG.RefVec aig w) (falseRef : AIG.Ref aig)
+    (hx : ∀ idx hidx, ⟦aig, xv.get idx hidx, assign⟧ = x.getLsbD idx)
+    (hfalse : ⟦aig, falseRef, assign⟧ = false) :
+    ∀ idx, ⟦aig, xv.getD idx falseRef, assign⟧ = x.getLsbD idx := by
+  intro idx
+  rw [AIG.RefVec.getD]
+  split
+  · rw [hx]
+  · rw [hfalse]
+    symm
+    apply BitVec.getLsbD_ge
+    omega
+
 @[simp]
 theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig)
     (assign : α → Bool) :