-- 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 signExtend.inl
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastZeroExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ (eval assign inner).getLsbD idx = true → idx < originalWidth

Tactic:
apply BitVec.lt_of_getLsbD

Result:
no goals

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 := { gate := ((go aig lhs).1.vec.get (idx - rw) ⋯).gate, hgate := ⋯ } }⟧ =
    (eval assign lhs).getLsbD (idx - rw)

Tactic:
rw [go_denote_mem_prefix, lih]

Result:
no goals

Proof state:
case bin.udiv
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✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (lhs.bin BVBinOp.udiv rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.udiv rhs)).val.vec.get idx hidx }⟧ =
    (eval assign (lhs.bin BVBinOp.udiv rhs)).getLsbD idx

Tactic:
simp only [go, eval_bin, BVBinOp.eval_udiv]

Result:
case bin.udiv
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✝
⊢ ⟦assign.toAIGAssignment,
      {
        aig :=
          (blastUdiv (go (go aig lhs).1.aig rhs).1.aig
              { lhs := (go aig lhs).1.vec.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.vec }).aig,
        ref :=
          (blastUdiv (go (go aig lhs).1.aig rhs).1.aig
                  { lhs := (go aig lhs).1.vec.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.vec }).vec.get
            idx hidx }⟧ =
    (eval assign lhs / eval assign rhs).getLsbD idx

Proof state:
case bin.and
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✝
⊢ (⟦assign.toAIGAssignment,
        { aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).vec.get idx hidx).cast ⋯ }⟧ &&
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx && (eval assign rhs).getLsbD idx)

Tactic:
rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]

Result:
case bin.and
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✝
⊢ (⟦assign.toAIGAssignment, { aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).vec.get idx hidx }⟧ &&
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx && (eval assign rhs).getLsbD idx)

Proof state:
case un.shiftRightConst
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
⊢ (eval assign expr).getLsbD (n✝ + idx) = true → n✝ + idx < w✝

Tactic:
intro h

Result:
case un.shiftRightConst
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
h : (eval assign expr).getLsbD (n✝ + idx) = true
⊢ n✝ + idx < w✝

Proof state:
case signExtend
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig (signExtend v inner)).val.aig, ref := (go aig (signExtend v inner)).val.vec.get idx hidx }⟧ =
    (eval assign (signExtend v inner)).getLsbD idx

Tactic:
generalize hgo : (go aig (signExtend v inner)).val = res

Result:
case signExtend
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : (go aig (signExtend v inner)).val = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (eval assign (signExtend v inner)).getLsbD idx