-- 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.add.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:
simp [Ref.hgate]

Result:
no goals

Proof state:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
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
n : Nat
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.vec.get idx hidx }⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsbD idx

Tactic:
have : ¬(w ≤ idx) := by omega

Result:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
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
n : Nat
this : ¬w ≤ idx
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.vec.get idx hidx }⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).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 } }⟧ =
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx✝ ?bin.udiv.hleft.hidx }⟧

Tactic:
simp

Result:
no goals

Proof state:
case append
w : Nat
assign : Assignment
l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < l✝),
    ⟦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 < r✝),
    ⟦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 < l✝ + r✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.vec.get idx hidx }⟧ =
    (eval assign (lhs.append rhs)).getLsbD idx

Tactic:
rename_i lw rw

Result:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦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 < rw),
    ⟦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 < lw + rw
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.vec.get idx hidx }⟧ =
    (eval assign (lhs.append rhs)).getLsbD idx

Proof state:
case arithShiftRight.hleft
w : Nat
assign : Assignment
m✝ n✝ : Nat
lhs : BVExpr m✝
rhs : BVExpr n✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < m✝),
    ⟦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 < n✝),
    ⟦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 < m✝
idx✝ : Nat
hidx✝ : idx✝ < m✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.target.get
            idx✝ hidx✝ }⟧ =
    (eval assign lhs).getLsbD idx✝

Tactic:
dsimp only

Result:
case arithShiftRight.hleft
w : Nat
assign : Assignment
m✝ n✝ : Nat
lhs : BVExpr m✝
rhs : BVExpr n✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < m✝),
    ⟦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 < n✝),
    ⟦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 < m✝
idx✝ : Nat
hidx✝ : idx✝ < m✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝ }⟧ =
    (eval assign lhs).getLsbD idx✝

Proof state:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦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 < rw),
    ⟦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 < lw + rw
hsplit : idx < rw
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.vec.get idx ⋯ }⟧ =
    (eval assign rhs).getLsbD idx

Tactic:
rw [rih]

Result:
no goals