Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/SignExtend.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx✝ : idx < newWidth
hidx : ¬idx < target.w
⊢ target.w - 1 < target.w
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦{ aig := (blastSignExtend aig target).aig, ref := (blastSignExtend aig target).stream.getRef idx hidx }, assign⟧ =
      if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
      else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
intro idx hidx
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
⊢ ⟦{ aig := (blastSignExtend aig target).aig, ref := (blastSignExtend aig target).stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
⊢ ⟦{ aig := (blastSignExtend aig target).aig, ref := (blastSignExtend aig target).stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
generalize hg : blastSignExtend aig target = res
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg : blastSignExtend aig target = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg : blastSignExtend aig target = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
unfold blastSignExtend at hg
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (match target with
    | { w := width, stream := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, stream := input }
      else { aig := aig, stream := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (match target with
    | { w := width, stream := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, stream := input }
      else { aig := aig, stream := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
dsimp at hg
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
have : ¬ (target.w = 0) := by omega
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
this : ¬target.w = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
this : ¬target.w = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
simp only [this, ↓reduceDite] at hg
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
rw [← hg]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.aig,
        ref :=
          { aig := aig,
                  stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.aig,
        ref :=
          { aig := aig,
                  stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig, ref := (blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty).getRef idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig, ref := (blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty).getRef idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
rw [blastSignExtend.go_getRef]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig,
        ref := if hidx2 : idx < target.w then target.stream.getRef idx ⋯ else target.stream.getRef (target.w - 1) ⋯ },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig,
        ref := if hidx2 : idx < target.w then target.stream.getRef idx ⋯ else target.stream.getRef (target.w - 1) ⋯ },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Tactic:
. split <;> simp only
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Tactic:
. omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ¬target.w = 0
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig,
        ref := if hidx2 : idx < target.w then target.stream.getRef idx ⋯ else target.stream.getRef (target.w - 1) ⋯ },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
split <;> simp only
State after:
no goals

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Tactic:
omega
State after:
no goals