-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (expr.eval assign).getLsbD idx

Proof state:
case bin.udiv.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝).gate, hgate := ?bin.udiv.hleft.hstart } }⟧ =
    (eval assign lhs).getLsbD idx✝

case bin.udiv.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

Tactic:
rw [← lih (aig := aig)]

Result:
case bin.udiv.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝).gate, hgate := ?bin.udiv.hleft.hstart } }⟧ =
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx✝ ?bin.udiv.hleft.hidx }⟧

case bin.udiv.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝

case bin.udiv.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

Proof state:
case bin.udiv.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment,
        { aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref := { lhs := (go aig lhs).1.vec.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.vec }.rhs.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx

Tactic:
intros

Result:
case bin.udiv.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { lhs := (go aig lhs).1.vec.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.vec }.rhs.get idx✝ hidx✝ }⟧ =
    (eval assign rhs).getLsbD idx✝

Proof state:
case un
w : Nat
assign : Assignment
w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig expr).val.aig, ref := (go aig expr).val.vec.get idx hidx }⟧ =
      (eval assign expr).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (un op expr)).val.aig, ref := (go aig (un op expr)).val.vec.get idx hidx }⟧ =
    (eval assign (un op expr)).getLsbD idx

Tactic:
cases op with
| not => simp [go, ih, hidx]
| shiftLeftConst => simp [go, ih, hidx]
| shiftRightConst =>
  simp only [go, denote_blastShiftRightConst, ih, dite_eq_ite, Bool.if_false_right, eval_un,
    BVUnOp.eval_shiftRightConst, BitVec.getLsbD_ushiftRight, Bool.and_iff_right_iff_imp,
    decide_eq_true_eq]
  intro h
  apply BitVec.lt_of_getLsbD
  assumption
| rotateLeft => simp [go, ih, hidx]
| rotateRight => simp [go, ih, hidx]
| arithShiftRightConst n =>
  rename_i w
  have : ¬(w ≤ idx) := by omega
  simp [go, ih, this, BitVec.getLsbD_sshiftRight, BitVec.msb_eq_getLsbD_last ]

Result:
no goals

Proof state:
case const
w : Nat
assign : Assignment
w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (const val✝)).val.aig, ref := (go aig (const val✝)).val.vec.get idx hidx }⟧ =
    (eval assign (const val✝)).getLsbD idx

Tactic:
simp [go, denote_blastConst]

Result:
no goals