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

Tactic:
split

Result:
case mk.isTrue
α : 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 }⟧ =
    ⟦assign, { aig := aig, ref := input.get (start + idx) h✝ }⟧

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

Proof state:
case mk.isTrue
α : 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 ⋯).get (start + idx) ?mk.isTrue.hidx }⟧ =
    ⟦assign, { aig := aig, ref := input.get (start + idx) h✝ }⟧

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:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]

Result:
case mk.isTrue
α : 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, ref := { gate := ((input.cast ⋯).get (start + idx) ?mk.isTrue.hidx).gate, hgate := ?mk.isTrue } }⟧ =
    ⟦assign, { aig := aig, ref := input.get (start + idx) h✝ }⟧

case mk.isTrue
α : 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✝
⊢ ((input.cast ⋯).get (start + idx) ?mk.isTrue.hidx).gate < aig.decls.size

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✝

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✝

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

Tactic:
generalize hextract : blastExtract aig target = res

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

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 := (aig.mkConstCached false).ref }⟧ = false

Tactic:
simp

Result:
no goals

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

Tactic:
rcases target with ⟨input, start⟩

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