-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
          ⟦(blastAdd aig input).aig, (blastAdd aig input).vec.get idx hidx, assign⟧
            =
          (lhs + rhs).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ (⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.get idx hidx }⟧ ^^
        BitVec.carry idx lhs rhs false)) =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Tactic:
simp only [BinaryRefVec.lhs_get_cast, Ref.cast_eq, BinaryRefVec.rhs_get_cast]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ (⟦assign, { aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.get idx hidx).gate, hgate := ⋯ } }⟧ ^^
      (⟦assign,
          { aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.get idx hidx).gate, hgate := ⋯ } }⟧ ^^
        BitVec.carry idx lhs rhs false)) =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let cin := res.ref;
            let input := input.cast ⋯;
            match input with
            | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 lhs rhs 0 ⋯ cin RefVec.empty).aig,
        ref :=
          (let res := aig.mkConstCached false;
                let aig_1 := res.aig;
                let cin := res.ref;
                let input := input.cast ⋯;
                match input with
                | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 lhs rhs 0 ⋯ cin RefVec.empty).vec.get
            idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (blastAdd.go (aig.mkConstCached false).aig (input.cast ⋯).lhs (input.cast ⋯).rhs 0 ⋯
              (aig.mkConstCached false).ref RefVec.empty).aig,
        ref :=
          (blastAdd.go (aig.mkConstCached false).aig (input.cast ⋯).lhs (input.cast ⋯).rhs 0 ⋯
                  (aig.mkConstCached false).ref RefVec.empty).vec.get
            idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.get idx✝ hidx✝).gate, hgate := ⋯ } }⟧ =
    lhs.getLsbD idx✝

Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := aig, ref := { gate := (input.lhs.get idx✝ hidx✝).gate, hgate := ?m.44531 } }⟧ = lhs.getLsbD idx✝

α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ (input.lhs.get idx✝ hidx✝).gate < aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ 0 ≤ w

Tactic:
omega

Result:
no goals

Proof state:
case i_lt
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ idx < w

Tactic:
assumption

Result:
no goals