internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkConstCached (val.getLsb idx);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go aig_1 (idx + 1) s val ⋯).aig.decls.size
Tactic:
dsimp
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached (val.getLsb idx)).aig (idx + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb idx)).ref)
            val ⋯).aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached (val.getLsb idx)).aig (idx + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb idx)).ref)
            val ⋯).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤ (aig.mkConstCached (val.getLsb idx)).aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤ (aig.mkConstCached (val.getLsb idx)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ ?m.9372 ≤
    (go (aig.mkConstCached (val.getLsb idx)).aig (idx + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb idx)).ref)
            val ⋯).aig.decls.size
Tactic:
apply go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
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.blastConst_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
⊢ aig.decls.size ≤ (blastConst aig val).aig.decls.size
Tactic:
unfold blastConst
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
⊢ aig.decls.size ≤ (blastConst.go aig 0 AIG.RefStream.empty val ⋯).aig.decls.size
Theorem: BVExpr.bitblast.blastConst_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
⊢ aig.decls.size ≤ (blastConst.go aig 0 AIG.RefStream.empty val ⋯).aig.decls.size
Tactic:
apply blastConst.go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig i s val hi).aig.decls.size),
    (go aig i s val hi).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hgo : go aig i s val hi = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
hgo : go aig i s val 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.blastConst.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
hgo : go aig i s val 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:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : i < w then
      let res := aig.mkConstCached (val.getLsb i);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go aig_1 (i + 1) s val ⋯
    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.blastConst.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : i < w then
      let res := aig.mkConstCached (val.getLsb i);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go aig_1 (i + 1) s val ⋯
    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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  (let res := aig.mkConstCached (val.getLsb i);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go aig_1 (i + 1) s val ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  (let res := aig.mkConstCached (val.getLsb i);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go aig_1 (i + 1) s val ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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 [blastConst.go_decl_eq]
  rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
  apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
  assumption
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  (let res := aig.mkConstCached (val.getLsb i);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go aig_1 (i + 1) s val ⋯) =
    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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref)
                val ⋯).aig.decls.size),
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
              ⋯).aig.decls[idx] =
      aig.decls[idx]
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref)
                val ⋯).aig.decls.size),
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
              ⋯).aig.decls[idx] =
      aig.decls[idx]
Tactic:
intro idx h1 h2
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [blastConst.go_decl_eq]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ (aig.mkConstCached (val.getLsb i)).aig.decls[idx] = aig.decls[idx]

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

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < (aig.mkConstCached (val.getLsb i)).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
Proof state after:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < (aig.mkConstCached (val.getLsb i)).aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < (aig.mkConstCached (val.getLsb i)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
Proof state after:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α 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.blastConst_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (blastConst aig val).aig.decls.size),
    (blastConst aig val).aig.decls[idx] = aig.decls[idx]
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (blastConst aig val).aig.decls.size
⊢ (blastConst aig val).aig.decls[idx✝] = aig.decls[idx✝]
Theorem: BVExpr.bitblast.blastConst_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (blastConst aig val).aig.decls.size
⊢ (blastConst aig val).aig.decls[idx✝] = aig.decls[idx✝]
Tactic:
unfold blastConst
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (blastConst aig val).aig.decls.size
⊢ (blastConst.go aig 0 AIG.RefStream.empty val ⋯).aig.decls[idx✝] = aig.decls[idx✝]
Theorem: BVExpr.bitblast.blastConst_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
val : BitVec w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (blastConst aig val).aig.decls.size
⊢ (blastConst.go aig 0 AIG.RefStream.empty val ⋯).aig.decls[idx✝] = aig.decls[idx✝]
Tactic:
apply blastConst.go_decl_eq
Proof state after:
no goals
Theorem: bitvec_AddSub_1309
Proof state before:
⊢ ∀ (a b : BitVec 64), (a &&& b) + (a ||| b) = a + b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (a✝ &&& b✝) + (a✝ ||| b✝) = a✝ + b✝
Theorem: bitvec_AddSub_1309
Proof state before:
a✝ b✝ : BitVec 64
⊢ (a✝ &&& b✝) + (a✝ ||| b✝) = a✝ + b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: Decl.constToCNF_eval
Proof state before:
α✝ : Type
output : α✝
b : Bool
assign : α✝ → Bool
⊢ CNF.eval assign (constToCNF output b) = (assign output == b)
Tactic:
simp [constToCNF, CNF.eval, CNF.Clause.eval]
Proof state after:
no goals