internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ ?m.9293 ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).aig (idx + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).ref) a ⋯).aig.decls.size
Tactic:
apply go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar_le_size
Proof state before:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ aig.decls.size ≤ (blastVar aig var).aig.decls.size
Tactic:
unfold blastVar
Proof state after:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ aig.decls.size ≤ (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size
Theorem: BVExpr.bitblast.blastVar_le_size
Proof state before:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ aig.decls.size ≤ (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size
Tactic:
apply blastVar.go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go w aig i s a hi).aig.decls.size),
    (go w aig i s a hi).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hgo : go w aig i s a hi = res
Proof state after:
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
hgo : go w aig i s a hi = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
hgo : go w aig i s a hi = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
unfold go at hgo
Proof state after:
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
hgo :
  (if hidx : i < w then
      let res := aig.mkAtomCached (BVBit.mk a ⟨i, hidx⟩);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go w aig_1 (i + 1) s a ⋯
    else
      let_fun hidx := ⋯;
      { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
hgo :
  (if hidx : i < w then
      let res := aig.mkAtomCached (BVBit.mk a ⟨i, hidx⟩);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go w aig_1 (i + 1) s a ⋯
    else
      let_fun hidx := ⋯;
      { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
split at hgo
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (i + 1) s a ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

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

case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. dsimp at hgo
  rw [← hgo]
  intro idx h1 h2
  rw [blastVar.go_decl_eq]
  rw [AIG.LawfulOperator.decl_eq (f := AIG.mkAtomCached)]
  apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkAtomCached)
  assumption
Proof state after:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. dsimp at hgo
  rw [← hgo]
  intros
  simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (i + 1) s a ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp at hgo
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    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
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
                ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size),
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls[idx] =
      aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
                ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size),
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls[idx] =
      aig.decls[idx]
Tactic:
intro idx h1 h2
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [blastVar.go_decl_eq]
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig.decls[idx] = aig.decls[idx]

case isTrue.h1
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig.decls[idx] = aig.decls[idx]

case isTrue.h1
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkAtomCached)]
Proof state after:
case isTrue.h2
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue.h2
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkAtomCached)
Proof state after:
case isTrue.h2.h
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isTrue.h2.h
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp at hgo
Proof state after:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo : { aig := aig, stream := ⋯ ▸ s } = 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 isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < { aig := aig, stream := ⋯ ▸ s }.aig.decls.size),
    { aig := aig, stream := ⋯ ▸ s }.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < { aig := aig, stream := ⋯ ▸ s }.aig.decls.size),
    { aig := aig, stream := ⋯ ▸ s }.aig.decls[idx] = aig.decls[idx]
Tactic:
intros
Proof state after:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
⊢ { aig := aig, stream := ⋯ ▸ s }.aig.decls[idx✝] = aig.decls[idx✝]
Theorem: BVExpr.bitblast.blastVar.go_decl_eq
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : ¬i < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
⊢ { aig := aig, stream := ⋯ ▸ s }.aig.decls[idx✝] = aig.decls[idx✝]
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (blastVar aig var).aig.decls.size),
    (blastVar aig var).aig.decls[idx] = aig.decls[idx]
Tactic:
unfold blastVar
Proof state after:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size),
    (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastVar_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size),
    (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls[idx] = aig.decls[idx]
Tactic:
apply blastVar.go_decl_eq
Proof state after:
no goals
Theorem: List.map_replicate
Proof state before:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f (replicate n a) = replicate n (f a)
Tactic:
induction n <;> simp_all
Proof state after:
no goals
Theorem: List.map_congr
Proof state before:
α : Type u_1
β : Type u_2
f g : α → β
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → f x = g x
⊢ map f (a :: l) = map g (a :: l)
Tactic:
let ⟨h₁, h₂⟩ := forall_mem_cons.1 h
Proof state after:
α : Type u_1
β : Type u_2
f g : α → β
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → f x = g x
h₁ : f a = g a
h₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ map f (a :: l) = map g (a :: l)
Theorem: List.map_congr
Proof state before:
α : Type u_1
β : Type u_2
f g : α → β
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → f x = g x
h₁ : f a = g a
h₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ map f (a :: l) = map g (a :: l)
Tactic:
rw [map, map, h₁, map_congr h₂]
Proof state after:
no goals
Theorem: CNF.Clause.eval_relabel
Proof state before:
α β : Type
f : α → β
g : β → Bool
x : Clause α
⊢ eval g (relabel f x) = eval (g ∘ f) x
Tactic:
induction x <;> simp_all [relabel]
Proof state after:
no goals
Theorem: CNF.Clause.relabel_id'
Proof state before:
α : Type
⊢ relabel id = id
Tactic:
funext
Proof state after:
case h
α : Type
x✝ : Clause α
⊢ relabel id x✝ = id x✝
Theorem: CNF.Clause.relabel_id'
Proof state before:
case h
α : Type
x✝ : Clause α
⊢ relabel id x✝ = id x✝
Tactic:
simp [relabel]
Proof state after:
no goals
Theorem: CNF.Clause.relabel_congr
Proof state before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ relabel f x = relabel g x
Tactic:
simp only [relabel]
Proof state after:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (fun x => (f x.fst, x.snd)) x = List.map (fun x => (g x.fst, x.snd)) x
Theorem: CNF.Clause.relabel_congr
Proof state before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (fun x => (f x.fst, x.snd)) x = List.map (fun x => (g x.fst, x.snd)) x
Tactic:
rw [List.map_congr]
Proof state after:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : α × Bool), x_1 ∈ x → (f x_1.fst, x_1.snd) = (g x_1.fst, x_1.snd)
Theorem: CNF.Clause.relabel_congr
Proof state before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : α × Bool), x_1 ∈ x → (f x_1.fst, x_1.snd) = (g x_1.fst, x_1.snd)
Tactic:
intro ⟨i, b⟩ h
Proof state after:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ (f (i, b).fst, (i, b).snd) = (g (i, b).fst, (i, b).snd)
Theorem: CNF.Clause.relabel_congr
Proof state before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ (f (i, b).fst, (i, b).snd) = (g (i, b).fst, (i, b).snd)
Tactic:
congr
Proof state after:
case e_fst
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ f (i, b).fst = g (i, b).fst
Theorem: CNF.Clause.relabel_congr
Proof state before:
case e_fst
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ f (i, b).fst = g (i, b).fst
Tactic:
apply w _ (mem_of h)
Proof state after:
no goals
Theorem: CNF.Clause.relabel_relabel'
Proof state before:
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
⊢ relabel f ∘ relabel g = relabel (f ∘ g)
Tactic:
funext i
Proof state after:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ (relabel f ∘ relabel g) i = relabel (f ∘ g) i
Theorem: CNF.Clause.relabel_relabel'
Proof state before:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ (relabel f ∘ relabel g) i = relabel (f ∘ g) i
Tactic:
simp only [Function.comp_apply, relabel, List.map_map]
Proof state after:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (f x.fst, x.snd)) ∘ fun x => (g x.fst, x.snd)) i = List.map (fun x => (f (g x.fst), x.snd)) i
Theorem: CNF.Clause.relabel_relabel'
Proof state before:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (f x.fst, x.snd)) ∘ fun x => (g x.fst, x.snd)) i = List.map (fun x => (f (g x.fst), x.snd)) i
Tactic:
rfl
Proof state after:
no goals
Theorem: CNF.eval_relabel
Proof state before:
α β : Type
f : α → β
g : β → Bool
x : CNF α
⊢ eval g (relabel f x) = eval (g ∘ f) x
Tactic:
induction x <;> simp_all [relabel]
Proof state after:
no goals
Theorem: CNF.relabel_relabel
Proof state before:
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
x : CNF α✝
⊢ relabel f (relabel g x) = relabel (f ∘ g) x
Tactic:
simp only [relabel, List.map_map, Clause.relabel_relabel']
Proof state after:
no goals
Theorem: CNF.relabel_id
Proof state before:
α✝ : Type
x : CNF α✝
⊢ relabel id x = x
Tactic:
simp [relabel]
Proof state after:
no goals
Theorem: CNF.relabel_congr
Proof state before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ relabel f x = relabel g x
Tactic:
dsimp only [relabel]
Proof state after:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (Clause.relabel f) x = List.map (Clause.relabel g) x
Theorem: CNF.relabel_congr
Proof state before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (Clause.relabel f) x = List.map (Clause.relabel g) x
Tactic:
rw [List.map_congr]
Proof state after:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : Clause α), x_1 ∈ x → Clause.relabel f x_1 = Clause.relabel g x_1