internlm/Lean-Github huggingface dataset:
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }
Tactic:
simp [Ref.mk.injEq]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = lhs.refs[idx]
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = lhs.refs[idx]
Tactic:
rw [Array.get_append_left]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
simp only [Ref.mk.injEq]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = rhs.refs[idx - lw]
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = rhs.refs[idx - lw]
Tactic:
rw [Array.get_append_right]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Tactic:
. simp [lhs.hlen]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Tactic:
. rw [lhs.hlen]
  omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]
Tactic:
simp [lhs.hlen]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Tactic:
rw [lhs.hlen]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lw ≤ idx
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lw ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_in_bound
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : idx < len
⊢ s.getRefD idx alt = s.getRef idx hidx
Tactic:
unfold getRefD
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : idx < len
⊢ (if hidx : idx < len then s.getRef idx hidx else alt) = s.getRef idx hidx
Theorem: AIG.RefStream.getRef_in_bound
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : idx < len
⊢ (if hidx : idx < len then s.getRef idx hidx else alt) = s.getRef idx hidx
Tactic:
simp [hidx]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_out_bound
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ s.getRefD idx alt = alt
Tactic:
unfold getRefD
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ (if hidx : idx < len then s.getRef idx hidx else alt) = alt
Theorem: AIG.RefStream.getRef_out_bound
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ (if hidx : idx < len then s.getRef idx hidx else alt) = alt
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.getRef idx h✝ = alt

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Theorem: AIG.RefStream.getRef_out_bound
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.getRef idx h✝ = alt

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Tactic:
. omega
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Theorem: AIG.RefStream.getRef_out_bound
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Tactic:
. rfl
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_out_bound
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.getRef idx h✝ = alt
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_out_bound
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Tactic:
rfl
Proof state after:
no goals
Theorem: AIG.BinaryRefStream.lhs_getRef_cast
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
aig1 aig2 : AIG α
s : aig1.BinaryRefStream len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).lhs.getRef idx hidx = (s.lhs.getRef idx hidx).cast hcast
Tactic:
simp [cast]
Proof state after:
no goals
Theorem: AIG.BinaryRefStream.rhs_getRef_cast
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
aig1 aig2 : AIG α
s : aig1.BinaryRefStream len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).rhs.getRef idx hidx = (s.rhs.getRef idx hidx).cast hcast
Tactic:
simp [cast]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
hfoo : aig.decls.size ≤ (go w aig curr s a hcurr).aig.decls.size
⊢ idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go w aig curr s a hcurr).aig.decls.size),
    (go w aig curr s a hcurr).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
intro idx hidx
Proof state after:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go w aig curr s a hcurr).aig.decls.size),
    (go w aig curr s a hcurr).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go w aig curr s a hcurr).aig.decls.size),
    (go w aig curr s a hcurr).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
generalize hgo : go w aig curr s a hcurr = res
Proof state after:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
hgo : go w aig curr s a hcurr = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
hgo : go w aig curr s a hcurr = 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:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
hgo :
  (if hidx : curr < w then
      let res := aig.mkAtomCached (BVBit.mk a ⟨curr, hidx⟩);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go w aig_1 (curr + 1) s a ⋯
    else
      let_fun hidx := ⋯;
      { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
hgo :
  (if hidx : curr < w then
      let res := aig.mkAtomCached (BVBit.mk a ⟨curr, hidx⟩);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go w aig_1 (curr + 1) s a ⋯
    else
      let_fun hidx := ⋯;
      { aig := aig, stream := hidx ▸ 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
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (curr + 1) s a ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo

case isFalse
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (curr + 1) s a ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo

case isFalse
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
. dsimp at hgo
  rw [← hgo]
  intro hfoo
  rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
  . simp only [Ref.cast, Ref.mk.injEq]
    rw [AIG.RefStream.getRef_cast]
    . simp
    . assumption
  . apply go_le_size
Proof state after:
case isFalse
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
. dsimp at hgo
  rw [← hgo]
  simp only [Nat.le_refl, RefStream.getRef, Ref_cast', Ref.mk.injEq, true_implies]
  congr
  . omega
  . simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (curr + 1) s a ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
dsimp at hgo
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
rw [← hgo]
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀
    (hfoo :
      aig.decls.size ≤
        (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
                ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size),
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).stream.getRef
        idx ⋯ =
      (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀
    (hfoo :
      aig.decls.size ≤
        (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
                ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size),
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).stream.getRef
        idx ⋯ =
      (s.getRef idx hidx).cast hfoo
Tactic:
intro hfoo
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).stream.getRef
      idx ⋯ =
    (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).stream.getRef
      idx ⋯ =
    (s.getRef idx hidx).cast hfoo
Tactic:
rw [go_getRef_aux]
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref).getRef idx ?isTrue.hidx).cast ?isTrue.hfoo =
    (s.getRef idx hidx).cast hfoo

case isTrue.hidx
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < curr + 1

case isTrue.hfoo
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue.hfoo
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size

case isTrue.hfoo
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
Tactic:
. apply go_le_size
Proof state after:
no goals