feat: bv_decide introduces uninterpreted symbols everywhere (#5781)

Co-authored-by: Tobias Grosser <tobias@grosser.es>

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean

@@ -65,202 +65,218 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   | _ => return none
 
 /--
-Reify an `Expr` that's a `BitVec`.
+Construct an uninterpreted `BitVec` atom from `x`.
+-/
+def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+  let t ← instantiateMVars (← whnfR (← inferType x))
+  let_expr BitVec widthExpr := t | return none
+  let some width ← getNatValue? widthExpr | return none
+  let atom ← mkAtom x width
+  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`.
 -/
 partial def of (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
-  | 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
+  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
+    | 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
-        .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 ← ofAtom x
-    shiftConstLikeReflection
-      distance
-      innerExpr
-      .arithShiftRightConst
-      ``BVUnOp.arithShiftRightConst
-      ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
-  | BitVec.zeroExtend _ newWidthExpr innerExpr =>
-    let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x
-    let some inner ← ofOrAtom innerExpr | return none
-    let bvExpr := .zeroExtend newWidth inner.bvExpr
-    let expr :=
-      mkApp3
-        (mkConst ``BVExpr.zeroExtend)
+        .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)
-        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 ← ofAtom x
-    let some inner ← ofOrAtom 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 ← ofOrAtom lhsExpr | return none
-    let some rhs ← ofOrAtom 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 ← ofOrAtom innerExpr | return none
-    let some n ← getNatValue? nExpr | return ← ofAtom x
-    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)
+        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)
-        innerExpr
-        innerEval
-        innerProof
-    return some ⟨inner.width * n, bvExpr, proof, expr⟩
-  | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
-    let some start ← getNatValue? startExpr | return ← ofAtom x
-    let some len ← getNatValue? lenExpr | return ← ofAtom x
-    let some inner ← ofOrAtom 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)
+        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
-        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
-  | _ => ofAtom x
-where
-  ofAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-    let t ← instantiateMVars (← whnfR (← inferType x))
-    let_expr BitVec widthExpr := t | return none
-    let some width ← getNatValue? widthExpr | return none
-    let atom ← mkAtom x width
-    return some atom
+        .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
 
-  ofOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-    let res ← of x
+  /--
+  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 => ofAtom x
+    | none => bitVecAtom x
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some inner ← ofOrAtom innerExpr | return none
+    let some inner ← goOrAtom innerExpr | return none
     let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
     let expr :=
       mkApp3
@@ -278,24 +294,22 @@ where
   rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
       (rotateOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    -- Either the shift values are constant or we abstract the entire term as atoms
-    let some distance ← getNatValue? distanceExpr | return ← ofAtom x
+    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
-    -- Either the shift values are constant or we abstract the entire term as atoms
-    let some distance ← getNatOrBvValue? β distanceExpr | return ← ofAtom x
+    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 ← ofAtom x
-    let some inner ← of innerExpr | return none
-    let some distance ← of distanceExpr | return none
+    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
@@ -314,8 +328,8 @@ where
 
   binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some lhs ← ofOrAtom lhsExpr | return none
-    let some rhs ← ofOrAtom rhsExpr | return none
+    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
@@ -335,7 +349,7 @@ where
 
   unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some inner ← ofOrAtom innerExpr | return none
+    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)
@@ -347,7 +361,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← ofAtom x
+    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

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -44,40 +44,75 @@ def mkTrans (x y z : Expr) (hxy hyz : Expr) : Expr :=
 def mkEvalExpr (expr : Expr) : M Expr := do
   return mkApp2 (mkConst ``BVLogicalExpr.eval) (← M.atomsAssignment) expr
 
+/--
+Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
+-/
+def ofPred  (bvPred : ReifiedBVPred) : M (Option 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⟩
+
+/--
+Construct an uninterrpeted `Bool` atom from `t`.
+-/
+def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do
+  let some pred ← ReifiedBVPred.boolAtom t | return none
+  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`.
+-/
 partial def of (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 := return 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 := return mkRefl (mkConst ``Bool.false)
-    return some ⟨boolExpr, proof, expr⟩
-  | Bool.not subExpr =>
-    let some sub ← of 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
+  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
+
   gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (congrThm : Name) :
       M (Option ReifiedBVLogical) := do
-    let some lhs ← of lhsExpr | return none
-    let some rhs ← of rhsExpr | return none
+    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
@@ -99,11 +134,8 @@ where
     return some ⟨boolExpr, proof, expr⟩
 
   goPred (t : Expr) : M (Option ReifiedBVLogical) := do
-    let some bvPred ← ReifiedBVPred.of t | return none
-    let boolExpr := .literal bvPred.bvPred
-    let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
-    let proof := bvPred.evalsAtAtoms
-    return some ⟨boolExpr, proof, expr⟩
+    let some pred ← ReifiedBVPred.of t | return none
+    ofPred pred
 
 end ReifiedBVLogical
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean

@@ -37,54 +37,68 @@ structure ReifiedBVPred where
 namespace ReifiedBVPred
 
 /--
-Reify an `Expr` that is a proof of a predicate about `BitVec`.
+Construct an uninterpreted `Bool` atom from `t`.
 -/
-def of (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⟩
-  | _ =>
-    /-
-    Idea: we have t : Bool here, let's construct:
-      BitVec.ofBool t : BitVec 1
-    as an atom. Then construct the BVPred corresponding to
-      BitVec.getLsb (BitVec.ofBool t) 0 : Bool
-    We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
-    -/
-    let ty ← inferType t
-    let_expr Bool := ty | return none
-    let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
-    let bvExpr : BVPred := .getLsbD atom.bvExpr 0
-    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
-    let proof := do
-      let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
-      let atomProof ← atom.evalsAtAtoms
-      return mkApp3
-        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
-        t
-        atomEval
-        atomProof
-    return some ⟨bvExpr, proof, expr⟩
+def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
+  /-
+  Idea: we have t : Bool here, let's construct:
+    BitVec.ofBool t : BitVec 1
+  as an atom. Then construct the BVPred corresponding to
+    BitVec.getLsb (BitVec.ofBool t) 0 : Bool
+  We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
+  -/
+  let ty ← inferType t
+  let_expr Bool := ty | return none
+  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
+  let bvExpr : BVPred := .getLsbD atom.bvExpr 0
+  let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
+  let proof := do
+    let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
+    let atomProof ← atom.evalsAtAtoms
+    return mkApp3
+      (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
+      t
+      atomEval
+      atomProof
+  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`.
+-/
+partial def of (t : Expr) : M (Option ReifiedBVPred) := do
+  match ← go t with
+  | some pred => return some pred
+  | none => boolAtom t
 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

tests/lean/run/bv_uninterpreted.lean

@@ -0,0 +1,22 @@
+import Std.Tactic.BVDecide
+
+-- Demonstrate some arbitrary width reasoning
+example {x y z : BitVec w} :
+    (x &&& y) ||| (x &&& z) ||| (y &&& z) ||| x ||| y ||| z
+      =
+    ~~~ ((~~~ x) &&& (~~~ y) &&& (~~~ z)) := by
+  ext
+  simp
+  bv_decide
+
+@[irreducible]
+def ufBv (x : BitVec w) : BitVec w := x
+
+example (x y : BitVec 16) : (ufBv x) + (ufBv y) = (ufBv y) + (ufBv x) := by bv_decide
+
+@[irreducible]
+def ufBool (x : Bool) : Bool := x
+
+example (x y : BitVec 16) (z : Bool) : ((ufBool (x < y)) ∧ z) ↔ (z ∧ ufBool (x < y)) := by bv_decide
+
+example (x y z : BitVec 16) (h1 : x < z) (h2 : z < (ufBv y)) : x < (ufBv y) := by bv_decide