From f1ff9cebf29edfc40fab70967274d3fb9b3cda1b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 7 Oct 2024 18:26:23 +0100
Subject: [PATCH] feat: more getLsbD bitblaster theory (#5637)

---
 .../BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean  | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

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
index 78a8e92ede04..c3ba9d088f2a 100644
--- 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) :