From 8b5443eb22252c9982c23e8fd15eb67d902da65d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 26 Oct 2024 21:08:07 +0200
Subject: [PATCH] feat: support BitVec.ofBool in bv_decide (#5852)

This is the first step towards fixing the issue of not having mutual
recursion between the `Bool` and `BitVec` fragment of `QF_BV` in
`bv_decide`. This PR adds support for `BitVec.ofBool` by doing the
following:
1. Introduce a new mechanism into the reification engine that allows us
to add additional lemmas to the top level on the fly as we are
traversing the expression tree.
2. If we encounter an expression `BitVec.ofBool boolExpr` we reify
`boolExpr` and then abstract `BitVec.ofBool boolExpr` as some atom `a`
3. We add two lemmas `boolExpr = true -> a = 1#1` and `boolExpr = false
-> a = 0#1`. This mirrors the full behavior of `BitVec.ofBool` and thus
makes our atom `a` correctly interpreted again.

In order to do the reification in step 2 mutual recursion in the
reification engine is required. For this reason I started pulling out
logic from the, now rather large, mutual block into other files and
document the invariants that they assume explicitly.
---
 .../Tactic/BVDecide/Frontend/BVDecide.lean    |   4 +-
 .../BVDecide/Frontend/BVDecide/Reflect.lean   | 100 +++++
 .../Frontend/BVDecide/ReifiedBVExpr.lean      | 332 +--------------
 .../Frontend/BVDecide/ReifiedBVLogical.lean   | 146 +++----
 .../Frontend/BVDecide/ReifiedBVPred.lean      | 135 +++---
 .../Frontend/BVDecide/ReifiedLemmas.lean      |  76 ++++
 .../BVDecide/Frontend/BVDecide/Reify.lean     | 398 ++++++++++++++++++
 .../Frontend/BVDecide/SatAtBVLogical.lean     |  21 +-
 .../BVDecide/Bitblast/BoolExpr/Basic.lean     |   3 +
 .../BVDecide/Bitblast/BoolExpr/Circuit.lean   |   7 +
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean |   8 +-
 src/Std/Tactic/BVDecide/Reflect.lean          |  17 +
 tests/lean/run/bv_bitwise.lean                |   8 +
 tests/lean/run/bv_decide_rewriter.lean        |   4 +-
 14 files changed, 743 insertions(+), 516 deletions(-)
 create mode 100644 src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
 create mode 100644 src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
index 1416e58716f7..01ce8224aadb 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -225,8 +225,8 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
-    if let some reflected ← SatAtBVLogical.of (mkFVar hyp) then
-      sats := sats.push reflected
+    if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
+      sats := (sats ++ lemmas).push reflected
     else
       unusedHypotheses := unusedHypotheses.insert hyp
   if h : sats.size = 0 then
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index 7a1395adfd14..13af0cd31e81 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -80,6 +80,7 @@ instance : ToExpr Gate where
     | .and => mkConst ``Gate.and
     | .xor => mkConst ``Gate.xor
     | .beq => mkConst ``Gate.beq
+    | .imp => mkConst ``Gate.imp
   toTypeExpr := mkConst ``Gate
 
 instance : ToExpr BVPred where
@@ -125,6 +126,76 @@ The reflection monad, used to track `BitVec` variables that we see as we travers
 -/
 abbrev M := StateRefT State MetaM
 
+/--
+A reified version of an `Expr` representing a `BVExpr`.
+-/
+structure ReifiedBVExpr where
+  width : Nat
+  /--
+  The reified expression.
+  -/
+  bvExpr : BVExpr width
+  /--
+  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
+  -/
+  evalsAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvExpr`.
+  -/
+  expr : Expr
+
+/--
+A reified version of an `Expr` representing a `BVPred`.
+-/
+structure ReifiedBVPred where
+  /--
+  The reified expression.
+  -/
+  bvPred : BVPred
+  /--
+  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
+  -/
+  evalsAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvPred`
+  -/
+  expr : Expr
+
+/--
+A reified version of an `Expr` representing a `BVLogicalExpr`.
+-/
+structure ReifiedBVLogical where
+  /--
+  The reified expression.
+  -/
+  bvExpr : BVLogicalExpr
+  /--
+  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
+  -/
+  evalsAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvExpr`
+  -/
+  expr : Expr
+
+/--
+A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
+-/
+structure SatAtBVLogical where
+  /--
+  The reified expression.
+  -/
+  bvExpr : BVLogicalExpr
+  /--
+  A proof that `bvExpr.eval atomsAssignment = true`.
+  -/
+  satAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvExpr`
+  -/
+  expr : Expr
+
+
 namespace M
 
 /--
@@ -172,5 +243,34 @@ where
 
 end M
 
+/--
+The state of the lemma reflection monad.
+-/
+structure LemmaState where
+  /--
+  The list of top level lemmas that got created on the fly during reflection.
+  -/
+  lemmas : Array SatAtBVLogical := #[]
+
+/--
+The lemma reflection monad. It extends the usual reflection monad `M` by adding the ability to
+add additional top level lemmas on the fly.
+-/
+abbrev LemmaM := StateRefT LemmaState M
+
+namespace LemmaM
+
+def run (m : LemmaM α) (state : LemmaState := {}) : M (α × Array SatAtBVLogical) := do
+  let (res, state) ← StateRefT'.run m state
+  return (res, state.lemmas)
+
+/--
+Add another top level lemma.
+-/
+def addLemma (lemma : SatAtBVLogical) : LemmaM Unit := do
+  modify fun s => { s with lemmas := s.lemmas.push lemma }
+
+end LemmaM
+
 end Frontend
 end Lean.Elab.Tactic.BVDecide
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
index 64c2f9552de7..aeb0526e97ed 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
@@ -14,30 +14,14 @@ Provides the logic for reifying `BitVec` expressions.
 namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
 
-open Lean.Meta
 open Std.Tactic.BVDecide
-open Std.Tactic.BVDecide.Reflect.BitVec
-
-/--
-A reified version of an `Expr` representing a `BVExpr`.
--/
-structure ReifiedBVExpr where
-  width : Nat
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVExpr width
-  /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`.
-  -/
-  expr : Expr
+open Lean.Meta
 
 namespace ReifiedBVExpr
 
+/--
+Build `BVExpr.eval atoms expr` where `atoms` is the assignment stored in the monad.
+-/
 def mkEvalExpr (w : Nat) (expr : Expr) : M Expr := do
   return mkApp3 (mkConst ``BVExpr.eval) (toExpr w) (← M.atomsAssignment) expr
 
@@ -47,6 +31,9 @@ def mkBVRefl (w : Nat) (expr : Expr) : Expr :=
    (mkApp (mkConst ``BitVec) (toExpr w))
    expr
 
+/--
+Register `e` as an atom of width `width`.
+-/
 def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
   let ident ← M.lookup e width
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
@@ -55,6 +42,9 @@ def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
     return mkBVRefl width evalExpr
   return ⟨width, .var ident, proof, expr⟩
 
+/--
+Parse `expr` as a `Nat` or `BitVec` constant depending on `ty`.
+-/
 def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   match_expr ty with
   | Nat =>
@@ -75,301 +65,15 @@ def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
   return some atom
 
 /--
-Reify an `Expr` that's a constant-width `BitVec`.
-Unless this function is called on something that is not a constant-width `BitVec` it is always
-going to return `some`.
+Build a reified version of the constant `val`.
 -/
-partial def of (x : Expr) : M (Option ReifiedBVExpr) := do
-  goOrAtom x
-where
-  /--
-  Reify `x`, returns `none` if the reification procedure failed.
-  -/
-  go (x : Expr) : M (Option ReifiedBVExpr) := do
-    match_expr x with
-    | BitVec.ofNat _ _ => goBvLit x
-    | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
-    | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
-    | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
-    | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
-    | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
-    | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
-    | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | BitVec.sdiv _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
-    | Complement.complement _ _ innerExpr =>
-      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
-    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeftConst
-          ``BVUnOp.shiftLeftConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeft
-          ``BVExpr.shiftLeft
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
-    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRightConst
-          ``BVUnOp.shiftRightConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRight
-          ``BVExpr.shiftRight
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
-    | BitVec.sshiftRight _ innerExpr distanceExpr =>
-      let some distance ← getNatValue? distanceExpr | return none
-      shiftConstLikeReflection
-        distance
-        innerExpr
-        .arithShiftRightConst
-        ``BVUnOp.arithShiftRightConst
-        ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
-    | BitVec.zeroExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .zeroExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.zeroExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | BitVec.signExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .signExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.signExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
-      let some lhs ← goOrAtom lhsExpr | return none
-      let some rhs ← goOrAtom rhsExpr | return none
-      let bvExpr := .append lhs.bvExpr rhs.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.append)
-        (toExpr lhs.width)
-        (toExpr rhs.width)
-        lhs.expr rhs.expr
-      let proof := do
-        let lhsEval ← mkEvalExpr lhs.width lhs.expr
-        let lhsProof ← lhs.evalsAtAtoms
-        let rhsProof ← rhs.evalsAtAtoms
-        let rhsEval ← mkEvalExpr rhs.width rhs.expr
-        return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
-          (toExpr lhs.width) (toExpr rhs.width)
-          lhsExpr lhsEval
-          rhsExpr rhsEval
-          lhsProof rhsProof
-      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
-    | BitVec.replicate _ nExpr innerExpr =>
-      let some inner ← goOrAtom innerExpr | return none
-      let some n ← getNatValue? nExpr | return none
-      let bvExpr := .replicate n inner.bvExpr
-      let expr := mkApp3 (mkConst ``BVExpr.replicate)
-        (toExpr inner.width)
-        (toExpr n)
-        inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
-          (toExpr n)
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨inner.width * n, bvExpr, proof, expr⟩
-    | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
-      let some start ← getNatValue? startExpr | return none
-      let some len ← getNatValue? lenExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .extract start len inner.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.extract)
-        (toExpr inner.width)
-        startExpr
-        lenExpr
-        inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
-          startExpr
-          lenExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨len, bvExpr, proof, expr⟩
-    | BitVec.rotateLeft _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
-        innerExpr
-        .rotateLeft
-        ``BVUnOp.rotateLeft
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
-    | BitVec.rotateRight _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
-        innerExpr
-        .rotateRight
-        ``BVUnOp.rotateRight
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | _ => return none
-
-  /--
-  Reify `x` or abstract it as an atom.
-  Unless this function is called on something that is not a fixed-width `BitVec` it is always going
-  to return `some`.
-  -/
-  goOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-    let res ← go x
-    match res with
-    | some exp => return some exp
-    | none => bitVecAtom x
-
-  shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
-      (shiftOpName : Name) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
-    let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
-    let expr :=
-      mkApp3
-        (mkConst ``BVExpr.un)
-        (toExpr inner.width)
-        (mkApp (mkConst shiftOpName) (toExpr distance))
-        inner.expr
-    let congrProof :=
-      mkApp
-        (mkConst congrThm)
-        (toExpr distance)
-    let proof := unaryCongrProof inner innerExpr congrProof
-    return some ⟨inner.width, bvExpr, proof, expr⟩
-
-  rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
-      (rotateOpName : Name) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some distance ← getNatValue? distanceExpr | return none
-    shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
-
-  shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
-      (shiftOpName : Name) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some distance ← getNatOrBvValue? β distanceExpr | return none
-    shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
-
-  shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
-      (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
-      (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let_expr BitVec _ ← β | return none
-    let some inner ← goOrAtom innerExpr | return none
-    let some distance ← goOrAtom distanceExpr | return none
-    let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr
-    let expr :=
-      mkApp4
-        (mkConst shiftOpName)
-        (toExpr inner.width)
-        (toExpr distance.width)
-        inner.expr
-        distance.expr
-    let congrProof :=
-      mkApp2
-        (mkConst congrThm)
-        (toExpr inner.width)
-        (toExpr distance.width)
-    let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof
-    return some ⟨inner.width, bvExpr, proof, expr⟩
-
-  binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
-    if h : rhs.width = lhs.width then
-      let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr)
-      let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
-      let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width)
-      let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm
-      return some ⟨lhs.width, bvExpr, proof, expr⟩
-    else
-      return none
-
-  binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (congrThm : Expr) :
-      M Expr := do
-    let lhsEval ← mkEvalExpr lhs.width lhs.expr
-    let lhsProof ← lhs.evalsAtAtoms
-    let rhsProof ← rhs.evalsAtAtoms
-    let rhsEval ← mkEvalExpr rhs.width rhs.expr
-    return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
-
-  unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
-    let bvExpr := .un op inner.bvExpr
-    let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
-    let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
-    return some ⟨inner.width, bvExpr, proof, expr⟩
-
-  unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M Expr := do
-    let innerEval ← mkEvalExpr inner.width inner.expr
-    let innerProof ← inner.evalsAtAtoms
-    return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
-
-  goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← bitVecAtom x
-    let bvExpr : BVExpr width := .const bvVal
-    let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal)
-    let proof := do
-      let evalExpr ← mkEvalExpr width expr
-      return mkBVRefl width evalExpr
-    return some ⟨width, bvExpr, proof, expr⟩
+def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do
+  let bvExpr : BVExpr w := .const val
+  let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
+  let proof := do
+    let evalExpr ← ReifiedBVExpr.mkEvalExpr w expr
+    return ReifiedBVExpr.mkBVRefl w evalExpr
+  return ⟨w, bvExpr, proof, expr⟩
 
 end ReifiedBVExpr
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
index 39c014e3ac44..da62556ac44d 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
@@ -14,24 +14,7 @@ namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
 
 open Std.Tactic.BVDecide
-open Std.Tactic.BVDecide.Reflect.Bool
-
-/--
-A reified version of an `Expr` representing a `BVLogicalExpr`.
--/
-structure ReifiedBVLogical where
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVLogicalExpr
-  /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`
-  -/
-  expr : Expr
+open Lean.Meta
 
 namespace ReifiedBVLogical
 
@@ -47,11 +30,11 @@ def mkEvalExpr (expr : Expr) : M Expr := do
 /--
 Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
 -/
-def ofPred  (bvPred : ReifiedBVPred) : M (Option ReifiedBVLogical) := do
+def ofPred (bvPred : ReifiedBVPred) : M ReifiedBVLogical := do
   let boolExpr := .literal bvPred.bvPred
   let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
   let proof := bvPred.evalsAtAtoms
-  return some ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, proof, expr⟩
 
 /--
 Construct an uninterrpeted `Bool` atom from `t`.
@@ -61,81 +44,60 @@ def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do
   ofPred pred
 
 /--
-Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+Build a reified version of the constant `val`.
 -/
-partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
-  goOrAtom t
-where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVLogical) := do
-    match_expr t with
-    | Bool.true =>
-      let boolExpr := .const true
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true)
-      let proof := pure <| mkRefl (mkConst ``Bool.true)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.false =>
-      let boolExpr := .const false
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
-      let proof := pure <| mkRefl (mkConst ``Bool.false)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.not subExpr =>
-      let some sub ← goOrAtom subExpr | return none
-      let boolExpr := .not sub.bvExpr
-      let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
-      let proof := do
-        let subEvalExpr ← mkEvalExpr sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
-    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      match_expr α with
-      | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-      | BitVec _ => goPred t
-      | _ => return none
-    | _ => goPred t
-
-  /--
-  Reify `t` or abstract it as an atom.
-  Unless this function is called on something that is not a `Bool` it is always going to return `some`.
-  -/
-  goOrAtom (t : Expr) : M (Option ReifiedBVLogical) := do
-    match ← go t with
-    | some boolExpr => return some boolExpr
-    | none => boolAtom t
+def mkBoolConst (val : Bool) : M ReifiedBVLogical := do
+  let boolExpr := .const val
+  let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val)
+  let proof := pure <| ReifiedBVLogical.mkRefl (toExpr val)
+  return ⟨boolExpr, proof, expr⟩
 
-  gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (congrThm : Name) :
-      M (Option ReifiedBVLogical) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
-    let boolExpr := .gate  gate lhs.bvExpr rhs.bvExpr
-    let expr :=
-      mkApp4
-        (mkConst ``BoolExpr.gate)
-        (mkConst ``BVPred)
-        (toExpr gate)
-        lhs.expr
-        rhs.expr
-    let proof := do
-      let lhsEvalExpr ← mkEvalExpr lhs.expr
-      let rhsEvalExpr ← mkEvalExpr rhs.expr
-      let lhsProof ← lhs.evalsAtAtoms
-      let rhsProof ← rhs.evalsAtAtoms
-      return mkApp6
-        (mkConst congrThm)
-        lhsExpr rhsExpr
-        lhsEvalExpr rhsEvalExpr
-        lhsProof rhsProof
-    return some ⟨boolExpr, proof, expr⟩
+/--
+Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
+This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
+and `rhs`.
+-/
+def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : M ReifiedBVLogical := do
+  let congrThm := congrThmOfGate gate
+  let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
+  let expr :=
+    mkApp4
+      (mkConst ``BoolExpr.gate)
+      (mkConst ``BVPred)
+      (toExpr gate)
+      lhs.expr
+      rhs.expr
+  let proof := do
+    let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr
+    let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
+    return mkApp6
+      (mkConst congrThm)
+      lhsExpr rhsExpr
+      lhsEvalExpr rhsEvalExpr
+      lhsProof rhsProof
+  return ⟨boolExpr, proof, expr⟩
+where
+  congrThmOfGate (gate : Gate) : Name :=
+    match gate with
+    | .and => ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
+    | .xor => ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
+    | .beq => ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
+    | .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
 
-  goPred (t : Expr) : M (Option ReifiedBVLogical) := do
-    let some pred ← ReifiedBVPred.of t | return none
-    ofPred pred
+/--
+Construct the reified version of `Bool.not subExpr`.
+This function assumes that `subExpr` is the expression corresponding to `sub`.
+-/
+def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
+  let boolExpr := .not sub.bvExpr
+  let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
+  let proof := do
+    let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr
+    let subProof ← sub.evalsAtAtoms
+    return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
+  return ⟨boolExpr, proof, expr⟩
 
 end ReifiedBVLogical
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
index 108b2ebc15d8..76dae112c4b3 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
@@ -7,32 +7,14 @@ prelude
 import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVExpr
 
 /-!
-Provides the logic for reifying expressions consisting of predicates over `BitVec`s.
+Provides the logic for reifying predicates on `BitVec`.
 -/
 
 namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
 
-open Lean.Meta
 open Std.Tactic.BVDecide
-open Std.Tactic.BVDecide.Reflect.BitVec
-
-/--
-A reified version of an `Expr` representing a `BVPred`.
--/
-structure ReifiedBVPred where
-  /--
-  The reified expression.
-  -/
-  bvPred : BVPred
-  /--
-  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvPred`
-  -/
-  expr : Expr
+open Lean.Meta
 
 namespace ReifiedBVPred
 
@@ -63,70 +45,61 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
   return some ⟨bvExpr, proof, expr⟩
 
 /--
-Reify an `Expr` that is a predicate about `BitVec`.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+Construct the reified version of applying the predicate in `pred` to `lhs` and `rhs`.
+This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
+and `rhs`.
 -/
-partial def of (t : Expr) : M (Option ReifiedBVPred) := do
-  match ← go t with
-  | some pred => return some pred
-  | none => boolAtom t
+def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred) :
+    M (Option ReifiedBVPred) := do
+  if h : lhs.width = rhs.width then
+    let congrThm := congrThmofBinPred pred
+    let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
+    let expr :=
+      mkApp4
+        (mkConst ``BVPred.bin)
+        (toExpr lhs.width)
+        lhs.expr
+        (toExpr pred)
+        rhs.expr
+    let proof := do
+      let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+      let lhsProof ← lhs.evalsAtAtoms
+      let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
+      let rhsProof ← rhs.evalsAtAtoms
+      return mkApp7
+        (mkConst congrThm)
+        (toExpr lhs.width)
+        lhsExpr rhsExpr lhsEval rhsEval
+        lhsProof
+        rhsProof
+    return some ⟨bvExpr, proof, expr⟩
+  else
+    return none
 where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVPred) := do
-    match_expr t with
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      let_expr BitVec _ := α | return none
-      binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
-    | BitVec.ult _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
-    | BitVec.getLsbD _ subExpr idxExpr =>
-      let some sub ← ReifiedBVExpr.of subExpr | return none
-      let some idx ← getNatValue? idxExpr | return none
-      let bvExpr : BVPred := .getLsbD sub.bvExpr idx
-      let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
-      let proof := do
-        let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp5
-          (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
-          idxExpr
-          (toExpr sub.width)
-          subExpr
-          subEval
-          subProof
-      return some ⟨bvExpr, proof, expr⟩
-    | _ => return none
-
-  binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (congrThm : Name) :
-      M (Option ReifiedBVPred) := do
-    let some lhs ← ReifiedBVExpr.of lhsExpr | return none
-    let some rhs ← ReifiedBVExpr.of rhsExpr | return none
-    if h : lhs.width = rhs.width then
-      let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
-      let expr :=
-        mkApp4
-          (mkConst ``BVPred.bin)
-          (toExpr lhs.width)
-          lhs.expr
-          (toExpr pred)
-          rhs.expr
-      let proof := do
-        let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
-        let lhsProof ← lhs.evalsAtAtoms
-        let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
-        let rhsProof ← rhs.evalsAtAtoms
-        return mkApp7
-          (mkConst congrThm)
-          (toExpr lhs.width)
-          lhsExpr rhsExpr lhsEval rhsEval
-          lhsProof
-          rhsProof
-      return some ⟨bvExpr, proof, expr⟩
-    else
-      return none
+  congrThmofBinPred (pred : BVBinPred) : Name :=
+    match pred with
+    | .eq => ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
+    | .ult => ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
 
+/--
+Construct the reified version of `BitVec.getLsbD subExpr idx`.
+This function assumes that `subExpr` is the expression corresponding to `sub`.
+-/
+def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPred := do
+  let bvExpr : BVPred := .getLsbD sub.bvExpr idx
+  let idxExpr := toExpr idx
+  let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
+  let proof := do
+    let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
+    let subProof ← sub.evalsAtAtoms
+    return mkApp5
+      (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
+      idxExpr
+      (toExpr sub.width)
+      subExpr
+      subEval
+      subProof
+  return ⟨bvExpr, proof, expr⟩
 
 end ReifiedBVPred
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
new file mode 100644
index 000000000000..deb3fb3926e7
--- /dev/null
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical
+
+/-!
+Provides the logic for generating auxiliary lemmas during reification.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend
+
+open Std.Tactic.BVDecide
+open Lean.Meta
+
+/--
+This function adds the two lemmas:
+- `boolExpr = true → atomExpr = 1#1`
+- `boolExpr = false → atomExpr = 0#1`
+It assumes that `boolExpr` and `atomExpr` are the expressions corresponding to `bool` and `atom`.
+Furthermore it assumes that `atomExpr` is of the form `BitVec.ofBool boolExpr`.
+-/
+def addOfBoolLemmas (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
+    LemmaM Unit := do
+  let some ofBoolTrueLemma ← mkOfBoolTrueLemma bool atom boolExpr atomExpr | return ()
+  LemmaM.addLemma ofBoolTrueLemma
+  let some ofBoolFalseLemma ← mkOfBoolFalseLemma bool atom boolExpr atomExpr | return ()
+  LemmaM.addLemma ofBoolFalseLemma
+where
+  mkOfBoolTrueLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
+      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr true 1#1
+
+  mkOfBoolFalseLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
+      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr false 0#1
+
+  mkOfBoolLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr)
+     (boolVal : Bool) (resVal : BitVec 1) : M (Option SatAtBVLogical) := do
+    let lemmaName :=
+      match boolVal with
+      | .true => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_true
+      | .false => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_false
+
+    let boolValExpr := toExpr boolVal
+    let boolVal ← ReifiedBVLogical.mkBoolConst boolVal
+    let resExpr := toExpr resVal
+    let resValExpr ← ReifiedBVExpr.mkBVConst resVal
+
+    let eqBoolExpr ← mkAppM ``BEq.beq #[boolExpr, boolValExpr]
+    let eqBool ← ReifiedBVLogical.mkGate bool boolVal boolExpr boolValExpr .beq
+
+    let eqBVExpr ← mkAppM ``BEq.beq #[mkApp (mkConst ``BitVec.ofBool) boolExpr, resExpr]
+    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
+    let eqBV ← ReifiedBVLogical.ofPred eqBVPred
+
+    let trueExpr := mkConst ``Bool.true
+    let impExpr ← mkArrow (← mkEq eqBoolExpr trueExpr) (← mkEq eqBVExpr trueExpr)
+    let decideImpExpr ← mkAppOptM ``Decidable.decide #[some impExpr, none]
+    let imp ← ReifiedBVLogical.mkGate eqBool eqBV eqBoolExpr eqBVExpr .imp
+
+    let proof := do
+      let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
+      let congrProof ← imp.evalsAtAtoms
+      let lemmaProof := mkApp (mkConst lemmaName) boolExpr
+      return mkApp4
+        (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
+        decideImpExpr
+        evalExpr
+        congrProof
+        lemmaProof
+    return some ⟨imp.bvExpr, proof, imp.expr⟩
+
+end Frontend
+end Lean.Elab.Tactic.BVDecide
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
new file mode 100644
index 000000000000..dffe381999f3
--- /dev/null
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -0,0 +1,398 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedLemmas
+
+/-!
+Reifies `BitVec` problems with boolean substructure.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend
+
+open Std.Tactic.BVDecide
+open Lean.Meta
+
+mutual
+
+/--
+Reify an `Expr` that's a constant-width `BitVec`.
+Unless this function is called on something that is not a constant-width `BitVec` it is always
+going to return `some`.
+-/
+partial def ReifiedBVExpr.of (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
+  goOrAtom x
+where
+  /--
+  Reify `x`, returns `none` if the reification procedure failed.
+  -/
+  go (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    match_expr x with
+    | BitVec.ofNat _ _ => goBvLit x
+    | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
+    | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
+    | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
+    | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
+    | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
+    | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
+    | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
+    | BitVec.sdiv _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
+    | Complement.complement _ _ innerExpr =>
+      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
+    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
+      let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
+      if distance?.isSome then
+        shiftConstReflection
+          β
+          distanceExpr
+          innerExpr
+          .shiftLeftConst
+          ``BVUnOp.shiftLeftConst
+          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
+      else
+        shiftReflection
+          β
+          distanceExpr
+          innerExpr
+          .shiftLeft
+          ``BVExpr.shiftLeft
+          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
+    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
+      let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
+      if distance?.isSome then
+        shiftConstReflection
+          β
+          distanceExpr
+          innerExpr
+          .shiftRightConst
+          ``BVUnOp.shiftRightConst
+          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
+      else
+        shiftReflection
+          β
+          distanceExpr
+          innerExpr
+          .shiftRight
+          ``BVExpr.shiftRight
+          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
+    | BitVec.sshiftRight _ innerExpr distanceExpr =>
+      let some distance ← getNatValue? distanceExpr | return none
+      shiftConstLikeReflection
+        distance
+        innerExpr
+        .arithShiftRightConst
+        ``BVUnOp.arithShiftRightConst
+        ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
+    | BitVec.zeroExtend _ newWidthExpr innerExpr =>
+      let some newWidth ← getNatValue? newWidthExpr | return none
+      let some inner ← goOrAtom innerExpr | return none
+      let bvExpr := .zeroExtend newWidth inner.bvExpr
+      let expr :=
+        mkApp3
+          (mkConst ``BVExpr.zeroExtend)
+          (toExpr inner.width)
+          newWidthExpr
+          inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
+          newWidthExpr
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨newWidth, bvExpr, proof, expr⟩
+    | BitVec.signExtend _ newWidthExpr innerExpr =>
+      let some newWidth ← getNatValue? newWidthExpr | return none
+      let some inner ← goOrAtom innerExpr | return none
+      let bvExpr := .signExtend newWidth inner.bvExpr
+      let expr :=
+        mkApp3
+          (mkConst ``BVExpr.signExtend)
+          (toExpr inner.width)
+          newWidthExpr
+          inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
+          newWidthExpr
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨newWidth, bvExpr, proof, expr⟩
+    | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
+      let some lhs ← goOrAtom lhsExpr | return none
+      let some rhs ← goOrAtom rhsExpr | return none
+      let bvExpr := .append lhs.bvExpr rhs.bvExpr
+      let expr := mkApp4 (mkConst ``BVExpr.append)
+        (toExpr lhs.width)
+        (toExpr rhs.width)
+        lhs.expr rhs.expr
+      let proof := do
+        let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+        let lhsProof ← lhs.evalsAtAtoms
+        let rhsProof ← rhs.evalsAtAtoms
+        let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
+        return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
+          (toExpr lhs.width) (toExpr rhs.width)
+          lhsExpr lhsEval
+          rhsExpr rhsEval
+          lhsProof rhsProof
+      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
+    | BitVec.replicate _ nExpr innerExpr =>
+      let some inner ← goOrAtom innerExpr | return none
+      let some n ← getNatValue? nExpr | return none
+      let bvExpr := .replicate n inner.bvExpr
+      let expr := mkApp3 (mkConst ``BVExpr.replicate)
+        (toExpr inner.width)
+        (toExpr n)
+        inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
+          (toExpr n)
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨inner.width * n, bvExpr, proof, expr⟩
+    | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
+      let some start ← getNatValue? startExpr | return none
+      let some len ← getNatValue? lenExpr | return none
+      let some inner ← goOrAtom innerExpr | return none
+      let bvExpr := .extract start len inner.bvExpr
+      let expr := mkApp4 (mkConst ``BVExpr.extract)
+        (toExpr inner.width)
+        startExpr
+        lenExpr
+        inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
+          startExpr
+          lenExpr
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨len, bvExpr, proof, expr⟩
+    | BitVec.rotateLeft _ innerExpr distanceExpr =>
+      rotateReflection
+        distanceExpr
+        innerExpr
+        .rotateLeft
+        ``BVUnOp.rotateLeft
+        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
+    | BitVec.rotateRight _ innerExpr distanceExpr =>
+      rotateReflection
+        distanceExpr
+        innerExpr
+        .rotateRight
+        ``BVUnOp.rotateRight
+        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
+    | BitVec.ofBool boolExpr =>
+      let some bool ← ReifiedBVLogical.of boolExpr | return none
+      let atomExpr := (mkApp (mkConst ``BitVec.ofBool) boolExpr)
+      let some atom ← ReifiedBVExpr.bitVecAtom atomExpr | return none
+      addOfBoolLemmas bool atom boolExpr atomExpr
+      return some atom
+    | _ => return none
+
+  /--
+  Reify `x` or abstract it as an atom.
+  Unless this function is called on something that is not a fixed-width `BitVec` it is always going
+  to return `some`.
+  -/
+  goOrAtom (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    let res ← go x
+    match res with
+    | some exp => return some exp
+    | none => ReifiedBVExpr.bitVecAtom x
+
+  shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
+      (shiftOpName : Name) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some inner ← goOrAtom innerExpr | return none
+    let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
+    let expr :=
+      mkApp3
+        (mkConst ``BVExpr.un)
+        (toExpr inner.width)
+        (mkApp (mkConst shiftOpName) (toExpr distance))
+        inner.expr
+    let congrProof :=
+      mkApp
+        (mkConst congrThm)
+        (toExpr distance)
+    let proof := unaryCongrProof inner innerExpr congrProof
+    return some ⟨inner.width, bvExpr, proof, expr⟩
+
+  rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
+      (rotateOpName : Name) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some distance ← getNatValue? distanceExpr | return none
+    shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
+
+  shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
+      (shiftOpName : Name) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some distance ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr | return none
+    shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
+
+  shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
+      (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
+      (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let_expr BitVec _ ← β | return none
+    let some inner ← goOrAtom innerExpr | return none
+    let some distance ← goOrAtom distanceExpr | return none
+    let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr
+    let expr :=
+      mkApp4
+        (mkConst shiftOpName)
+        (toExpr inner.width)
+        (toExpr distance.width)
+        inner.expr
+        distance.expr
+    let congrProof :=
+      mkApp2
+        (mkConst congrThm)
+        (toExpr inner.width)
+        (toExpr distance.width)
+    let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof
+    return some ⟨inner.width, bvExpr, proof, expr⟩
+
+  binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some lhs ← goOrAtom lhsExpr | return none
+    let some rhs ← goOrAtom rhsExpr | return none
+    if h : rhs.width = lhs.width then
+      let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr)
+      let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
+      let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width)
+      let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm
+      return some ⟨lhs.width, bvExpr, proof, expr⟩
+    else
+      return none
+
+  binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (congrThm : Expr) :
+      M Expr := do
+    let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
+    let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
+    return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
+
+  unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some inner ← goOrAtom innerExpr | return none
+    let bvExpr := .un op inner.bvExpr
+    let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
+    let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
+    return some ⟨inner.width, bvExpr, proof, expr⟩
+
+  unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M Expr := do
+    let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+    let innerProof ← inner.evalsAtAtoms
+    return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
+
+  goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
+    let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x
+    ReifiedBVExpr.mkBVConst bvVal
+
+/--
+Reify an `Expr` that is a predicate about `BitVec`.
+Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+-/
+partial def ReifiedBVPred.of (t : Expr) : LemmaM (Option ReifiedBVPred) := do
+  match ← go t with
+  | some pred => return some pred
+  | none => ReifiedBVPred.boolAtom t
+where
+  /--
+  Reify `t`, returns `none` if the reification procedure failed.
+  -/
+  go (t : Expr) : LemmaM (Option ReifiedBVPred) := do
+    match_expr t with
+    | BEq.beq α _ lhsExpr rhsExpr =>
+      let_expr BitVec _ := α | return none
+      binaryReflection lhsExpr rhsExpr .eq
+    | BitVec.ult _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .ult
+    | BitVec.getLsbD _ subExpr idxExpr =>
+      let some sub ← ReifiedBVExpr.of subExpr | return none
+      let some idx ← getNatValue? idxExpr | return none
+      return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx)
+    | _ => return none
+
+  binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) : LemmaM (Option ReifiedBVPred) := do
+    let some lhs ← ReifiedBVExpr.of lhsExpr | return none
+    let some rhs ← ReifiedBVExpr.of rhsExpr | return none
+    ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred
+
+/--
+Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
+Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+-/
+partial def ReifiedBVLogical.of (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+  goOrAtom t
+where
+  /--
+  Reify `t`, returns `none` if the reification procedure failed.
+  -/
+  go (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    match_expr t with
+    | Bool.true => ReifiedBVLogical.mkBoolConst true
+    | Bool.false => ReifiedBVLogical.mkBoolConst false
+    | Bool.not subExpr =>
+      let some sub ← goOrAtom subExpr | return none
+      return some (← ReifiedBVLogical.mkNot sub subExpr)
+    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and
+    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor
+    | BEq.beq α _ lhsExpr rhsExpr =>
+      match_expr α with
+      | Bool => gateReflection lhsExpr rhsExpr .beq
+      | BitVec _ => goPred t
+      | _ => return none
+    | _ => goPred t
+
+  /--
+  Reify `t` or abstract it as an atom.
+  Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+  -/
+  goOrAtom (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    match ← go t with
+    | some boolExpr => return some boolExpr
+    | none => ReifiedBVLogical.boolAtom t
+
+  gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) :
+      LemmaM (Option ReifiedBVLogical) := do
+    let some lhs ← goOrAtom lhsExpr | return none
+    let some rhs ← goOrAtom rhsExpr | return none
+    ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate
+
+  goPred (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    let some pred ← ReifiedBVPred.of t | return none
+    ReifiedBVLogical.ofPred pred
+
+end
+
+end Frontend
+end Lean.Elab.Tactic.BVDecide
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
index 9f653f5f6f73..64f0349fcef1 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reify
 
 /-!
 This module is the main entry point for reifying `BitVec` problems with boolean substructure.
@@ -19,29 +19,12 @@ namespace Frontend
 open Lean.Meta
 open Std.Tactic.BVDecide
 
-/--
-A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
--/
-structure SatAtBVLogical where
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVLogicalExpr
-  /--
-  A proof that `bvExpr.eval atomsAssignment = true`.
-  -/
-  satAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`
-  -/
-  expr : Expr
-
 namespace SatAtBVLogical
 
 /--
 Reify an `Expr` that is a proof of some boolean structure on top of predicates about `BitVec`s.
 -/
-partial def of (h : Expr) : M (Option SatAtBVLogical) := do
+partial def of (h : Expr) : LemmaM (Option SatAtBVLogical) := do
   let t ← instantiateMVars (← whnfR (← inferType h))
   match_expr t with
   | Eq α lhsExpr rhsExpr =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
index 8797391ebafd..e389699cb177 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
@@ -18,6 +18,7 @@ inductive Gate
   | and
   | xor
   | beq
+  | imp
 
 namespace Gate
 
@@ -25,11 +26,13 @@ def toString : Gate → String
   | and => "&&"
   | xor => "^^"
   | beq => "=="
+  | imp => "->"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
+  | imp => (· → ·)
 
 end Gate
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
index b2143d654408..d6443b8323a5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
@@ -59,6 +59,10 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
+      | .imp =>
+        let ret := aig.mkImpCached input
+        have := LawfulOperator.le_size (f := mkImpCached) aig input
+        ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
 
 variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]
 
@@ -96,6 +100,9 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
+    | imp =>
+      simp only [go]
+      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
 
 theorem ofBoolExprCached.go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 95c2a7ce3c44..35824b3d76ff 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -59,6 +59,8 @@ attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
 attribute [bv_normalize] BitVec.not_not
+attribute [bv_normalize] BitVec.ofBool_true
+attribute [bv_normalize] BitVec.ofBool_false
 
 end Constant
 
@@ -240,12 +242,6 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
 
-@[bv_normalize]
-theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
-    BitVec.ofBool (a.getLsbD i) = a.extractLsb' i 1 := by
-  ext j
-  simp
-
 @[bv_normalize]
 theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
     a[i] = a.getLsbD i := by
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index 93e729b537ed..09142cd69b1f 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -122,6 +122,16 @@ theorem sdiv_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (BitVec.sdiv lhs' rhs') = (BitVec.sdiv lhs rhs) := by
   simp[*]
 
+theorem ofBool_true (b : Bool) :
+    decide ((b == true) = true → (BitVec.ofBool b == 1#1) = true) = true := by
+  revert b
+  decide
+
+theorem ofBool_false (b : Bool) :
+    decide ((b == false) = true → (BitVec.ofBool b == 0#1) = true) = true := by
+  revert b
+  decide
+
 end BitVec
 
 namespace Bool
@@ -141,9 +151,16 @@ theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' == rhs') = (lhs == rhs) := by
   simp[*]
 
+theorem imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
+    (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
+  simp[*]
+
 theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by
   cases h₁; cases h₂
 
+theorem lemma_congr (x x' : Bool) (h1 : x' = x) (h2 : x = true) : x' = true := by
+  simp[*]
+
 end Bool
 
 open Std.Sat
diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean
index 26e5f517935f..a9fe997c165c 100644
--- a/tests/lean/run/bv_bitwise.lean
+++ b/tests/lean/run/bv_bitwise.lean
@@ -30,3 +30,11 @@ theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 63 = (x ^^^ ~~~x).
 
 theorem bitwise_unit_7 (x : BitVec 32) : x ^^^ 123#32 = 123#'(by decide) ^^^ x := by
   bv_decide
+
+theorem bitwise_unit_8 (x : BitVec 32) : BitVec.ofBool (x.getLsbD 0) = x.extractLsb' 0 1 := by
+  bv_decide
+
+theorem bitwise_unit_9 (x y : BitVec 32) :
+    BitVec.ofBool (x.getLsbD 0 ^^ y.getLsbD 0) = BitVec.ofBool ((x ^^^ y).getLsbD 0) := by
+  bv_decide
+
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 90982c1af2b6..c9cc36676968 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -62,8 +62,8 @@ example {x : BitVec 16} : x >>> 0 = x := by bv_normalize
 example {x : BitVec 16} : 0 < x ↔ (x != 0) := by bv_normalize
 example {x : BitVec 16} : ¬(-1#16 < x) := by bv_normalize
 example {x : BitVec 16} : BitVec.replicate 0 x = 0 := by bv_normalize
-example {x : BitVec 16} : BitVec.ofBool (x.getLsbD i) = x.extractLsb' i 1 := by bv_normalize
-example {x : BitVec 16} {i} {h} : BitVec.ofBool (x[i]'h) = x.extractLsb' i 1 := by bv_normalize
+example : BitVec.ofBool true = 1 := by bv_normalize
+example : BitVec.ofBool false = 0 := by bv_normalize
 example {x : BitVec 16} {i} {h} : x[i] = x.getLsbD i := by bv_normalize
 example {x y : BitVec 1} : x + y = x ^^^ y := by bv_normalize
 example {x y : BitVec 1} : x * y = x &&& y := by bv_normalize