-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
theorem denote_blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth)
    (assign : α → Bool) :
    ∀ (idx : Nat) (hidx : idx < newWidth),
        ⟦(blastExtract aig target).aig, (blastExtract aig target).vec.get idx hidx, assign⟧
          =
        if h : (target.start + idx) < target.w then
          ⟦aig, target.vec.get (target.start + idx) h, assign⟧
        else
          false

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  (match ExtractTarget.mk input start with
    | ExtractTarget.mk input start =>
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let falseRef := res.ref;
      let input := input.cast ⋯;
      { aig := aig_1, vec := blastExtract.go input start falseRef 0 ⋯ RefVec.empty }) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Tactic:
dsimp only at hextract

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Proof state:
case mk.isTrue.hidx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
h✝ : start + idx < w✝
⊢ start + idx < w✝

Tactic:
assumption

Result:
no goals

Proof state:
case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
h✝ : ¬start + idx < w✝
⊢ ⟦assign,
      { aig := (aig.mkConstCached false).aig,
        ref := (input.cast ⋯).getD (start + idx) (aig.mkConstCached false).ref }⟧ =
    false

Tactic:
rw [RefVec.get_out_bound]

Result:
case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
h✝ : ¬start + idx < w✝
⊢ ⟦assign, { aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }⟧ = false

case mk.isFalse.hidx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
h✝ : ¬start + idx < w✝
⊢ w✝ ≤ start + idx

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Tactic:
rw [← hextract]

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
⊢ ⟦assign,
      {
        aig :=
          { aig := (aig.mkConstCached false).aig,
              vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty }.vec.get
            idx hidx }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract : blastExtract aig (ExtractTarget.mk input start) = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if h : (ExtractTarget.mk input start).start + idx < (ExtractTarget.mk input start).w then
      ⟦assign,
        { aig := aig, ref := (ExtractTarget.mk input start).vec.get ((ExtractTarget.mk input start).start + idx) h }⟧
    else false

Tactic:
dsimp only

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract : blastExtract aig (ExtractTarget.mk input start) = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
⊢ ⟦assign,
      {
        aig :=
          { aig := (aig.mkConstCached false).aig,
              vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty }.aig,
        ref := (input.cast ⋯).getD (start + idx) (aig.mkConstCached false).ref }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Tactic:
dsimp only

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
w✝ : Nat
input : aig.RefVec w✝
start : Nat
hextract :
  { aig := (aig.mkConstCached false).aig,
      vec := blastExtract.go (input.cast ⋯) start (aig.mkConstCached false).ref 0 ⋯ RefVec.empty } =
    res
⊢ ⟦assign,
      { aig := (aig.mkConstCached false).aig,
        ref := (input.cast ⋯).getD (start + idx) (aig.mkConstCached false).ref }⟧ =
    if h : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false