-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.lean
theorem denote_blastSub (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),
          ⟦(blastSub aig input).aig, (blastSub 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 :=
          (match input with
            | { lhs := lhs, rhs := rhs } =>
              let res := blastNeg aig rhs;
              let aig_1 := res.aig;
              let negRhs := res.vec;
              let lhs := lhs.cast ⋯;
              blastAdd aig_1 { lhs := lhs, rhs := negRhs }).aig,
        ref :=
          (match input with
                | { lhs := lhs, rhs := rhs } =>
                  let res := blastNeg aig rhs;
                  let aig_1 := res.aig;
                  let negRhs := res.vec;
                  let lhs := lhs.cast ⋯;
                  blastAdd aig_1 { lhs := lhs, rhs := negRhs }).vec.get
            idx hidx }⟧ =
    (lhs + -rhs).getLsbD idx

Tactic:
rw [denote_blastAdd]

Result:
case hleft
α : 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 := (blastNeg aig input.rhs).aig,
          ref := { lhs := input.lhs.cast ⋯, rhs := (blastNeg aig input.rhs).vec }.lhs.get idx hidx }⟧ =
      lhs.getLsbD idx

case hright
α : 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 := (blastNeg aig input.rhs).aig,
          ref := { lhs := input.lhs.cast ⋯, rhs := (blastNeg aig input.rhs).vec }.rhs.get idx hidx }⟧ =
      (-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 := (blastSub aig input).aig, ref := (blastSub aig input).vec.get idx hidx }⟧ = (lhs - rhs).getLsbD idx

Tactic:
rw [BitVec.sub_toAdd]

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

Proof state:
case hleft
α : 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 := (blastNeg aig input.rhs).aig,
        ref := { lhs := input.lhs.cast ⋯, rhs := (blastNeg aig input.rhs).vec }.lhs.get idx✝ hidx✝ }⟧ =
    lhs.getLsbD idx✝

Tactic:
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastNeg)]

Result:
case hleft
α : 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 := ({ lhs := input.lhs.cast ⋯, rhs := (blastNeg aig input.rhs).vec }.lhs.get idx✝ hidx✝).gate,
            hgate := ?hleft } }⟧ =
    lhs.getLsbD idx✝

case hleft
α : 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
⊢ ({ lhs := input.lhs.cast ⋯, rhs := (blastNeg aig input.rhs).vec }.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 := (blastSub aig input).aig, ref := (blastSub aig input).vec.get idx hidx }⟧ =
      (lhs - rhs).getLsbD idx

Tactic:
intro idx hidx

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

Proof state:
case hleft
α : 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 := ({ lhs := input.lhs.cast ⋯, rhs := (blastNeg aig input.rhs).vec }.lhs.get idx✝ hidx✝).gate,
            hgate := ?hleft } }⟧ =
    lhs.getLsbD idx✝

Tactic:
simp [hleft]

Result:
no goals