internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [blastShiftLeftConst.go_decl_eq]
Proof state after:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (aig.mkConstCached false).aig.decls[idx] = aig.decls[idx]

case isTrue.isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (aig.mkConstCached false).aig.decls[idx] = aig.decls[idx]

case isTrue.isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
Proof state after:
case isTrue.isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
Proof state after:
case isTrue.isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < aig.decls.size
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : curr < distance
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
rw [← hgo]
Proof state after:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls.size),
    (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls.size),
    (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls[idx] = aig.decls[idx]
Tactic:
intro idx h1 h2
Proof state after:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls.size
⊢ (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls.size
⊢ (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [blastShiftLeftConst.go_decl_eq]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
simp [← hgo]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
hr : ¬idx < target.rw
this : newWidth = target.rw + target.lw
⊢ idx - target.rw < target.lw
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦{ aig := (blastAppend aig target).aig, ref := (blastAppend aig target).stream.getRef idx hidx }, assign⟧ =
      if hr : idx < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx hr }, assign⟧
      else
        let_fun this := ⋯;
        ⟦{ aig := aig, ref := target.lhs.getRef (idx - target.rw) ⋯ }, assign⟧
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{ aig := (blastAppend aig target).aig, ref := (blastAppend aig target).stream.getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{ aig := (blastAppend aig target).aig, ref := (blastAppend aig target).stream.getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
Tactic:
unfold blastAppend
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
Tactic:
rcases target with ⟨lw, rw, lhs, rhs, ht⟩
Proof state after:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.getRef (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.getRef (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }, assign⟧
Tactic:
dsimp
Proof state after:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := (rw.append lw).getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := (rw.append lw).getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
Tactic:
rw [AIG.RefStream.getRef_append]
Proof state after:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := if h : idx✝ < rw✝ then rw.getRef idx✝ h else lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb
Proof state before:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := if h : idx✝ < rw✝ then rw.getRef idx✝ h else lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
hfoo : aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size
⊢ idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size),
    (go aig input distance curr hcurr s).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size),
    (go aig input distance curr hcurr s).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size),
    (go aig input distance curr hcurr s).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
generalize hgo : go aig input distance curr hcurr s = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo : go aig input distance curr hcurr s = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo : go aig input distance curr hcurr s = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      if hdist : curr < distance then
        let res := aig.mkConstCached false;
        let aig_1 := res.aig;
        let zeroRef := res.ref;
        let_fun hfinal := ⋯;
        let s := s.cast hfinal;
        let input := input.cast hfinal;
        let s := s.pushRef zeroRef;
        go aig_1 input distance (curr + 1) ⋯ s
      else
        let s := s.pushRef (input.getRef (curr - distance) ⋯);
        go aig input distance (curr + 1) ⋯ s
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      if hdist : curr < distance then
        let res := aig.mkConstCached false;
        let aig_1 := res.aig;
        let zeroRef := res.ref;
        let_fun hfinal := ⋯;
        let s := s.cast hfinal;
        let input := input.cast hfinal;
        let s := s.pushRef zeroRef;
        go aig_1 input distance (curr + 1) ⋯ s
      else
        let s := s.pushRef (input.getRef (curr - distance) ⋯);
        go aig input distance (curr + 1) ⋯ s
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
split at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  (if hdist : curr < distance then
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let zeroRef := res.ref;
      let_fun hfinal := ⋯;
      let s := s.cast hfinal;
      let input := input.cast hfinal;
      let s := s.pushRef zeroRef;
      go aig_1 input distance (curr + 1) ⋯ s
    else
      let s := s.pushRef (input.getRef (curr - distance) ⋯);
      go aig input distance (curr + 1) ⋯ s) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo