internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : (ExtractTarget.mk input hi lo hnew).lo + idx < (ExtractTarget.mk input hi lo hnew).w then
      ⟦{ aig := aig,
          ref := (ExtractTarget.mk input hi lo hnew).stream.getRef ((ExtractTarget.mk input hi lo hnew).lo + idx) h },
        assign⟧
    else false
Tactic:
dsimp
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
unfold blastExtract at hextract
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (match ExtractTarget.mk input hi lo hnew with
    | ExtractTarget.mk input hi lo hnew =>
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let falseRef := res.ref;
      let input := input.cast ⋯;
      if h : lo ≤ hi then { aig := aig_1, stream := blastExtract.go input lo 0 ⋯ falseRef RefStream.empty }
      else
        let_fun this := ⋯;
        let base := RefStream.empty;
        let base := base.pushRef (input.getRefD lo falseRef);
        { aig := aig_1, stream := this ▸ base }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (match ExtractTarget.mk input hi lo hnew with
    | ExtractTarget.mk input hi lo hnew =>
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let falseRef := res.ref;
      let input := input.cast ⋯;
      if h : lo ≤ hi then { aig := aig_1, stream := blastExtract.go input lo 0 ⋯ falseRef RefStream.empty }
      else
        let_fun this := ⋯;
        let base := RefStream.empty;
        let base := base.pushRef (input.getRefD lo falseRef);
        { aig := aig_1, stream := this ▸ base }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
dsimp at hextract
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (if h : lo ≤ hi then
      { aig := (aig.mkConstCached false).aig,
        stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }
    else
      { aig := (aig.mkConstCached false).aig,
        stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (if h : lo ≤ hi then
      { aig := (aig.mkConstCached false).aig,
        stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }
    else
      { aig := (aig.mkConstCached false).aig,
        stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
split at hextract
Proof state after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
. rw [← hextract]
  rw [blastExtract.go_getRef]
  . dsimp
    split
    . rw [RefStream.getRef_in_bound]
      rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
      . congr 1
      . assumption
    . rw [RefStream.getRef_out_bound]
      . simp
      . omega
  . omega
Proof state after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
. have : idx = 0 := by omega
  simp only [this]
  have : 1 = newWidth := by omega
  subst this
  rw [← hextract]
  split
  . rw [RefStream.getRef_in_bound]
    dsimp
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    . congr 2
    . omega
  . rw [RefStream.getRef_out_bound]
    . simp
    . omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
rw [← hextract]
Proof state after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
rw [blastExtract.go_getRef]
Proof state after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Tactic:
. dsimp
  split
  . rw [RefStream.getRef_in_bound]
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    . congr 1
    . assumption
  . rw [RefStream.getRef_out_bound]
    . simp
    . omega
Proof state after:
case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
dsimp
Proof state after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
split
Proof state after:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_in_bound]
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  . congr 1
  . assumption
Proof state after:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_out_bound]
  . simp
  . omega
Proof state after:
no goals