-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w)
    (assign : α → Bool)
    (htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.get idx hidx, assign⟧ = value.getLsbD idx) :

    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastNeg aig target).aig, (blastNeg aig target).vec.get idx hidx, assign⟧
          =
        (-value).getLsbD idx

Proof state:
case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (blastNot aig target).aig,
        ref :=
          {
            gate :=
              ({ lhs := (blastNot aig target).vec.cast ⋯,
                        rhs := (blastConst (blastNot aig target).aig 1#w).vec }.lhs.get
                  idx hidx).gate,
            hgate := ?hleft } }⟧ =
    (~~~value).getLsbD idx

Tactic:
simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true,
  Bool.true_and]

Result:
case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (blastNot aig target).aig,
        ref := { gate := ((blastNot aig target).vec.get idx hidx).gate, hgate := ⋯ } }⟧ =
    !value.getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastNeg aig target).aig, ref := (blastNeg aig target).vec.get idx hidx }⟧ =
    (~~~value + 1#w).getLsbD idx

Tactic:
unfold blastNeg

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (let res := blastNot aig target;
            let aig_1 := res.aig;
            let notInput := res.vec;
            let res_1 := blastConst aig_1 1#w;
            let aig_2 := res_1.aig;
            let one := res_1.vec;
            let notInput := notInput.cast ⋯;
            blastAdd aig_2 { lhs := notInput, rhs := one }).aig,
        ref :=
          (let res := blastNot aig target;
                let aig_1 := res.aig;
                let notInput := res.vec;
                let res_1 := blastConst aig_1 1#w;
                let aig_2 := res_1.aig;
                let one := res_1.vec;
                let notInput := notInput.cast ⋯;
                blastAdd aig_2 { lhs := notInput, rhs := one }).vec.get
            idx hidx }⟧ =
    (~~~value + 1#w).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (let res := blastNot aig target;
            let aig_1 := res.aig;
            let notInput := res.vec;
            let res_1 := blastConst aig_1 1#w;
            let aig_2 := res_1.aig;
            let one := res_1.vec;
            let notInput := notInput.cast ⋯;
            blastAdd aig_2 { lhs := notInput, rhs := one }).aig,
        ref :=
          (let res := blastNot aig target;
                let aig_1 := res.aig;
                let notInput := res.vec;
                let res_1 := blastConst aig_1 1#w;
                let aig_2 := res_1.aig;
                let one := res_1.vec;
                let notInput := notInput.cast ⋯;
                blastAdd aig_2 { lhs := notInput, rhs := one }).vec.get
            idx hidx }⟧ =
    (~~~value + 1#w).getLsbD idx

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (blastAdd (blastConst (blastNot aig target).aig 1#w).aig
              { lhs := (blastNot aig target).vec.cast ⋯, rhs := (blastConst (blastNot aig target).aig 1#w).vec }).aig,
        ref :=
          (blastAdd (blastConst (blastNot aig target).aig 1#w).aig
                  { lhs := (blastNot aig target).vec.cast ⋯,
                    rhs := (blastConst (blastNot aig target).aig 1#w).vec }).vec.get
            idx hidx }⟧ =
    (~~~value + 1#w).getLsbD idx

Proof state:
case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (blastNot aig target).aig,
        ref := { gate := ((blastNot aig target).vec.get idx hidx).gate, hgate := ⋯ } }⟧ =
    !value.getLsbD idx

Tactic:
rw [denote_blastNot, htarget]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastNeg aig target).aig, ref := (blastNeg aig target).vec.get idx hidx }⟧ = (-value).getLsbD idx

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastNeg aig target).aig, ref := (blastNeg aig target).vec.get idx hidx }⟧ = (-value).getLsbD idx

Proof state:
case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (blastConst (blastNot aig target).aig 1#w).aig,
          ref :=
            { lhs := (blastNot aig target).vec.cast ⋯, rhs := (blastConst (blastNot aig target).aig 1#w).vec }.lhs.get
              idx hidx }⟧ =
      (~~~value).getLsbD idx

Tactic:
intro idx hidx

Result:
case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
value : BitVec w
target : aig.RefVec w
assign : α → Bool
htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (blastConst (blastNot aig target).aig 1#w).aig,
        ref :=
          { lhs := (blastNot aig target).vec.cast ⋯, rhs := (blastConst (blastNot aig target).aig 1#w).vec }.lhs.get idx
            hidx }⟧ =
    (~~~value).getLsbD idx