refactor: apply fording to BVExpr to enable deriving DecidableEq (#7619)

This PR applies fording to bv_decide's BVExpr type to enable deriving
DecidableEq.

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

@@ -50,10 +50,14 @@ where
   | .const val => mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
   | .bin lhs op rhs => mkApp4 (mkConst ``BVExpr.bin) (toExpr w) (go lhs) (toExpr op) (go rhs)
   | .un op operand => mkApp3 (mkConst ``BVExpr.un) (toExpr w) (toExpr op) (go operand)
-  | .append (l := l) (r := r) lhs rhs =>
-    mkApp4 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) (go lhs) (go rhs)
-  | .replicate (w := oldWidth) w inner =>
-    mkApp3 (mkConst ``BVExpr.replicate) (toExpr oldWidth) (toExpr w) (go inner)
+  | .append (w := w) (l := l) (r := r) lhs rhs _ =>
+    let wExpr := toExpr w
+    let proof := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Nat) wExpr
+    mkApp6 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) wExpr (go lhs) (go rhs) proof
+  | .replicate (w' := newWidth) (w := oldWidth) w inner _ =>
+    let newWExpr := toExpr newWidth
+    let proof := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Nat) newWExpr
+    mkApp5 (mkConst ``BVExpr.replicate) (toExpr oldWidth) newWExpr (toExpr w) (go inner) proof
   | .extract (w := oldWidth) hi lo expr =>
     mkApp4 (mkConst ``BVExpr.extract) (toExpr oldWidth) (toExpr hi) (toExpr lo) (go expr)
   | .shiftLeft (m := m) (n := n) lhs rhs =>

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

@@ -85,11 +85,16 @@ where
     | 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 bvExpr := .append lhs.bvExpr rhs.bvExpr rfl
+      let wExpr := toExpr (lhs.width + rhs.width)
+      let expr :=
+        mkApp6 (mkConst ``BVExpr.append)
+          (toExpr lhs.width)
+          (toExpr rhs.width)
+          wExpr
+          lhs.expr
+          rhs.expr
+          (← mkEqRefl wExpr)
       let proof := do
         let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
         let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
@@ -108,11 +113,15 @@ where
     | 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 bvExpr := .replicate n inner.bvExpr rfl
+      let newWExpr := toExpr (inner.width * n)
+      let expr :=
+        mkApp5 (mkConst ``BVExpr.replicate)
+          (toExpr inner.width)
+          newWExpr
+          (toExpr n)
+          inner.expr
+          (← mkEqRefl newWExpr)
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
         -- This is safe as `replicate_congr` holds definitionally if the arguments are defeq.

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -74,6 +74,7 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
+  deriving DecidableEq, Hashable
 
 namespace BVBinOp
 
@@ -134,6 +135,7 @@ inductive BVUnOp where
   constant `Nat` value.
   -/
   | arithShiftRightConst (n : Nat)
+  deriving DecidableEq, Hashable
 
 namespace BVUnOp
 
@@ -197,11 +199,11 @@ inductive BVExpr : Nat → Type where
   /--
   Concatenate two bit vectors.
   -/
-  | append (lhs : BVExpr l) (rhs : BVExpr r) : BVExpr (l + r)
+  | append (lhs : BVExpr l) (rhs : BVExpr r) (h : w = l + r) : BVExpr w
   /--
   Concatenate a bit vector with itself `n` times.
   -/
-  | replicate (n : Nat) (expr : BVExpr w) : BVExpr (w * n)
+  | replicate (n : Nat) (expr : BVExpr w) (h : w' = w * n) : BVExpr w'
   /--
   shift left by another BitVec expression. For constant shifts there exists a `BVUnop`.
   -/
@@ -214,6 +216,7 @@ inductive BVExpr : Nat → Type where
   shift right arithmetically by another BitVec expression. For constant shifts there exists a `BVUnop`.
   -/
   | arithShiftRight (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m
+  deriving DecidableEq, Hashable
 
 namespace BVExpr
 
@@ -223,8 +226,8 @@ def toString : BVExpr w → String
   | .extract start len expr => s!"{expr.toString}[{start}, {len}]"
   | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
   | .un op operand => s!"({op.toString} {toString operand})"
-  | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})"
-  | .replicate n expr => s!"(replicate {n} {toString expr})"
+  | .append lhs rhs _ => s!"({toString lhs} ++ {toString rhs})"
+  | .replicate n expr _ => s!"(replicate {n} {toString expr})"
   | .shiftLeft lhs rhs => s!"({lhs.toString} << {rhs.toString})"
   | .shiftRight lhs rhs => s!"({lhs.toString} >> {rhs.toString})"
   | .arithShiftRight lhs rhs => s!"({lhs.toString} >>a {rhs.toString})"
@@ -268,8 +271,8 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
   | .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
   | .bin lhs op rhs => op.eval (eval assign lhs) (eval assign rhs)
   | .un op operand => op.eval (eval assign operand)
-  | .append lhs rhs => (eval assign lhs) ++ (eval assign rhs)
-  | .replicate n expr => BitVec.replicate n (eval assign expr)
+  | .append lhs rhs h => h ▸ ((eval assign lhs) ++ (eval assign rhs))
+  | .replicate n expr h => h ▸ (BitVec.replicate n (eval assign expr))
   | .shiftLeft lhs rhs => (eval assign lhs) <<< (eval assign rhs)
   | .shiftRight lhs rhs => (eval assign lhs) >>> (eval assign rhs)
   | .arithShiftRight lhs rhs => BitVec.sshiftRight' (eval assign lhs) (eval assign rhs)
@@ -299,11 +302,11 @@ theorem eval_un : eval assign (.un op operand) = op.eval (operand.eval assign) :
   rfl
 
 @[simp]
-theorem eval_append : eval assign (.append lhs rhs) = (lhs.eval assign) ++ (rhs.eval assign) := by
+theorem eval_append : eval assign (.append lhs rhs h) = (lhs.eval assign) ++ (rhs.eval assign) := by
   rfl
 
 @[simp]
-theorem eval_replicate : eval assign (.replicate n expr) = BitVec.replicate n (expr.eval assign) := by
+theorem eval_replicate : eval assign (.replicate n expr h) = BitVec.replicate n (expr.eval assign) := by
   rfl
 
 @[simp]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Init.Data.AC
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
@@ -130,21 +129,21 @@ where
           dsimp only at heaig
           assumption
         ⟨res, this⟩
-    | .append lhs rhs =>
+    | .append lhs rhs _ =>
       let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs
       let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs
       let lhs := lhs.cast <| by
         dsimp only at hlaig hraig
         omega
-      let res := bitblast.blastAppend aig ⟨lhs, rhs, by ac_rfl⟩
+      let res := bitblast.blastAppend aig ⟨lhs, rhs, by omega⟩
       have := by
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAppend)
         dsimp only at hlaig hraig
         omega
       ⟨res, this⟩
-    | .replicate n expr =>
+    | .replicate n expr _ =>
       let ⟨⟨aig, expr⟩, haig⟩ := go aig expr
-      let res := bitblast.blastReplicate aig ⟨n, expr, rfl⟩
+      let res := bitblast.blastReplicate aig ⟨n, expr, by omega⟩
       have := by
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate)
         dsimp only at haig
@@ -226,7 +225,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
       rw [ih]
       have := (go aig expr).property
       omega
-  | append lhs rhs lih rih =>
+  | append lhs rhs _ lih rih =>
     dsimp only [go]
     have := (bitblast.go aig lhs).property
     have := (bitblast.go aig lhs).property
@@ -236,7 +235,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
     · omega
     · apply Nat.lt_of_lt_of_le h1
       apply Nat.le_trans <;> assumption
-  | replicate n inner ih =>
+  | replicate n inner _ ih =>
     dsimp only [go]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastReplicate)]
     rw [ih]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -65,14 +65,17 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp [go, denote_blastConst]
   | var =>
     simp [go, hidx, denote_blastVar]
-  | append lhs rhs lih rih =>
+  | append lhs rhs hw lih rih =>
     rename_i lw rw
+    subst hw
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
       BitVec.getLsbD_append]
     split
     · next hsplit => rw [rih]
     · next hsplit => rw [go_denote_mem_prefix, lih]
-  | replicate n expr ih => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
+  | replicate n expr hw ih =>
+    subst hw
+    simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
   | @extract w start len inner ih =>
     simp only [go, denote_blastExtract, Bool.if_false_right, eval_extract,
       BitVec.getLsbD_extractLsb', hidx, decide_true, Bool.true_and]