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.

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

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