-- 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.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✝ }⟧

Tactic:
congr 1

Result:
no goals

Proof state:
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

Tactic:
omega

Result:
no goals

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 : start + idx < w✝ then ⟦assign, { aig := aig, ref := input.get (start + idx) h }⟧ else false

Tactic:
unfold blastExtract 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 :
  (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

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

Tactic:
rw [blastExtract.go_get]

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

case mk.a
α : 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
⊢ 0 ≤ idx

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:
intro idx hidx

Result:
α : 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

Proof state:
case mk.a
α : 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
⊢ 0 ≤ idx

Tactic:
omega

Result:
no goals

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 ⋯).getD (start + idx) (aig.mkConstCached false).ref }⟧ =
    ⟦assign, { aig := aig, ref := input.get (start + idx) h✝ }⟧

Tactic:
rw [RefVec.get_in_bound]

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 ⋯).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✝