-- 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
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

Tactic:
rw [hleft]

Result:
no goals

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 := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ = (lhs + rhs).getLsbD idx

Tactic:
rw [BitVec.getLsbD_add]

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 aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ =
    (lhs.getLsbD idx ^^ (rhs.getLsbD idx ^^ BitVec.carry idx lhs rhs false))

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

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 := (input.cast ⋯).lhs.get idx✝ hidx✝ }⟧ = lhs.getLsbD idx✝

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

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.mkConstCached false).aig, ref := { gate := (input.lhs.get idx✝ hidx✝).gate, hgate := ⋯ } }⟧ =
    lhs.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 := { 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))

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
⊢ (⟦assign, { aig := aig, ref := { gate := (input.lhs.get idx hidx).gate, hgate := ?m.42585 } }⟧ ^^
      (⟦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))

α : 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
⊢ (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
⊢ (⟦assign, { aig := aig, ref := { gate := (input.lhs.get idx hidx).gate, hgate := ?m.42585 } }⟧ ^^
      (⟦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))

α : 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
⊢ (input.lhs.get idx hidx).gate < aig.decls.size

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

Result:
no goals