From fa05bccd581c0883f84d7555321c1ae0cbeb07ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 10 Feb 2025 14:48:20 +0100
Subject: [PATCH] feat: add basic extract theorems for bv_decide (#7021)

This PR adds theorems for interactions of extractLsb with `&&&`, `^^^`,
`~~~` and `bif` to bv_decide's preprocessor.
---
 .../BVDecide/Frontend/Normalize/Enums.lean    |  9 ++-------
 .../BVDecide/Frontend/Normalize/Simproc.lean  | 14 +++++++++++++
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean |  8 ++++++++
 tests/lean/run/bv_decide_rewriter.lean        | 20 +++++++++++++++++++
 4 files changed, 44 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean
index a940d67a05..95bfc9fd7e 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean
@@ -196,13 +196,8 @@ def getEnumToBitVecLeFor (declName : Name) : MetaM Name := do
         let recOn := mkApp2 (mkConst (mkRecOnName declName) [0]) motive x
         let folder acc ctor := do
           let statement := mkStatement (mkConst ctor)
-          let decidable ← synthInstance (mkApp (mkConst ``Decidable) statement)
-          let decideEqTrue :=
-            mkApp2
-              (mkConst ``Eq.refl [1])
-              (mkConst ``Bool)
-              (mkApp2 (mkConst ``decide) statement decidable)
-          return mkApp acc <| mkApp3 (mkConst ``of_decide_eq_true) statement decidable decideEqTrue
+          let proof ← mkDecideProof statement
+          return mkApp acc proof
         let cases ← List.foldlM (init := recOn) folder ctors
         mkLambdaFVars #[x] cases
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index 3453efcbec..3e0cb24761 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -218,5 +218,19 @@ builtin_simproc [bv_normalize] bv_allOnes_eq_and ((_ : BitVec _) == (_ : BitVec
         rrhs
     return .visit { expr := expr, proof? := some proof }
 
+builtin_simproc [bv_normalize] bv_extractLsb'_not (BitVec.extractLsb' _ _ (~~~(_ : BitVec _))) :=
+  fun e => do
+    let_expr BitVec.extractLsb' initialWidth start len inner := e | return .continue
+    let some initialWidthVal ← getNatValue? initialWidth | return .continue
+    let some startVal ← getNatValue? start | return .continue
+    let some lenVal ← getNatValue? len | return .continue
+    if !(startVal + lenVal) < initialWidthVal then return .continue
+    let_expr Complement.complement _ _ inner := inner | return .continue
+    let newInner := mkApp4 (mkConst ``BitVec.extractLsb') initialWidth start len inner
+    let expr ← mkAppM ``Complement.complement #[newInner]
+    let lt ← mkDecideProof (← mkAppM ``LT.lt #[(← mkAppM ``HAdd.hAdd #[start, len]), initialWidth])
+    let proof := mkApp5 (mkConst ``BitVec.extractLsb'_not_of_lt) initialWidth inner start len lt
+    return .visit { expr := expr, proof? := some proof }
+
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 7ac21d8e83..3f1c06c3bf 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -339,5 +339,13 @@ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat)
   have : BitVec.ofNat w n = BitVec.twoPow w k := by simp [bv_toNat, hk]
   rw [this, BitVec.udiv_twoPow_eq_of_lt (hk := by omega)]
 
+attribute [bv_normalize] BitVec.extractLsb'_and
+attribute [bv_normalize] BitVec.extractLsb'_xor
+
+@[bv_normalize]
+theorem BitVec.exctractLsb'_if {x y : BitVec w} (s l : Nat) :
+    BitVec.extractLsb' s l (bif c then x else y) = bif c then (BitVec.extractLsb' s l x) else (BitVec.extractLsb' s l y) := by
+  cases c <;> simp
+
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 27fa3164f1..680c965bd8 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -252,6 +252,26 @@ example (a b : BitVec 16) : (a &&& b == -1#16) = (a == -1#16 && b == -1#16) := b
 example (a b : BitVec 16) : (-1#16 == a &&& b) = (a == -1#16 && b == -1#16) := by
   bv_normalize
 
+-- extractLsb'_and
+example (a b : BitVec 16) :
+    BitVec.extractLsb' 1 12 (a &&& b) = BitVec.extractLsb' 1 12 a &&& BitVec.extractLsb' 1 12 b := by
+  bv_normalize
+
+-- extractLsb'_xor
+example (a b : BitVec 16) :
+    BitVec.extractLsb' 1 12 (a ^^^ b) = BitVec.extractLsb' 1 12 a ^^^ BitVec.extractLsb' 1 12 b := by
+  bv_normalize
+
+-- extractLsb'_not_of_lt
+example (a b : BitVec 16) :
+    BitVec.extractLsb' 1 12 (~~~(a &&& b)) = ~~~(BitVec.extractLsb' 1 12 a &&& BitVec.extractLsb' 1 12 b) := by
+  bv_normalize
+
+-- extractLsb'_if
+example (a b : BitVec 16) (c : Bool) :
+    BitVec.extractLsb' 1 12 (if c then a else b) = if c then BitVec.extractLsb' 1 12 a else BitVec.extractLsb' 1 12 b := by
+  bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by