-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean
theorem denote_blastSignExtend (aig : AIG α) (target : ExtendTarget aig newWidth)
    (assign : α → Bool) (htarget : 0 < target.w) :
    ∀ (idx : Nat) (hidx : idx < newWidth),
        ⟦(blastSignExtend aig target).aig, (blastSignExtend aig target).vec.get idx hidx, assign⟧
          =
        if hidx : idx < target.w then
           ⟦aig, target.vec.get idx hidx, assign⟧
        else
           ⟦aig, target.vec.get (target.w - 1) (by omega), assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
hg :
  (match target with
    | { w := width, vec := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, vec := input }
      else { aig := aig, vec := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefVec.empty }) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Tactic:
dsimp only at hg

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, vec := target.vec }
    else { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty }) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦assign, { aig := (blastSignExtend aig target).aig, ref := (blastSignExtend aig target).vec.get idx hidx }⟧ =
      if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
      else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign, { aig := (blastSignExtend aig target).aig, ref := (blastSignExtend aig target).vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign, { aig := (blastSignExtend aig target).aig, ref := (blastSignExtend aig target).vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Tactic:
generalize hg : blastSignExtend aig target = res

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
hg : blastSignExtend aig target = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty } = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Tactic:
rw [← hg]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty } = res
⊢ ⟦assign,
      { aig := { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty }.aig,
        ref :=
          { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty }.vec.get idx
            hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty } = res
⊢ 0 ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty } = res
⊢ ⟦assign,
      { aig := { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty }.aig,
        ref :=
          { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty }.vec.get idx
            hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty } = res
⊢ ⟦assign, { aig := aig, ref := (blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty).get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefVecEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, vec := target.vec }
    else { aig := aig, vec := blastSignExtend.go target.w ⋯ target.vec newWidth 0 ⋯ RefVec.empty }) =
    res
⊢ ¬target.w = 0

Tactic:
omega

Result:
no goals