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

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

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

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

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

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

case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Tactic:
. simp
Proof state after:
case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Tactic:
omega
Proof state after:
no goals
Theorem: BVPred.bitblast_le_size
Proof state before:
aig : AIG BVBit
pred : BVPred
⊢ aig.decls.size ≤ (bitblast aig pred).aig.decls.size
Tactic:
cases pred with
| bin lhs op rhs =>
  cases op with
  | eq =>
    simp [bitblast]
    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
  | ult =>
    simp [bitblast]
    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
| getLsb expr idx =>
  simp only [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
Proof state after:
no goals
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin
aig : AIG BVBit
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs op rhs)).aig.decls.size
Tactic:
cases op with
| eq =>
  simp [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
| ult =>
  simp [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
Proof state after:
no goals
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs BVBinPred.eq rhs)).aig.decls.size
Tactic:
simp [bitblast]
Proof state after:
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
Proof state after:
case bin.eq.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.eq.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.eq.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.eq.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
Proof state after:
no goals
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs BVBinPred.ult rhs)).aig.decls.size
Tactic:
simp [bitblast]
Proof state after:
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
Proof state after:
case bin.ult.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.ult.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.ult.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case bin.ult.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
Proof state after:
no goals
Theorem: BVPred.bitblast_le_size
Proof state before:
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (bitblast aig (getLsb expr idx)).aig.decls.size
Tactic:
simp only [bitblast]
Proof state after:
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤
    (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤
    (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
Proof state after:
case getLsb.h
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (BVExpr.bitblast aig expr).aig.decls.size
Theorem: BVPred.bitblast_le_size
Proof state before:
case getLsb.h
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (BVExpr.bitblast aig expr).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
idx : Nat
aig : AIG BVBit
pred : BVPred
h : idx < aig.decls.size
this : aig.decls.size ≤ (bitblast aig pred).aig.decls.size
⊢ idx < (bitblast aig pred).aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
idx : Nat
aig : AIG BVBit
pred : BVPred
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (bitblast aig pred).aig.decls[idx] = aig.decls[idx]
Tactic:
cases pred with
| bin lhs op rhs =>
  cases op with
  | eq =>
    simp only [bitblast]
    rw [AIG.LawfulOperator.decl_eq (f := mkEq)]
    rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
    rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
    . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
      assumption
    . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
      apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
      assumption
  | ult =>
    simp only [bitblast]
    rw [AIG.LawfulOperator.decl_eq (f := mkUlt)]
    rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
    rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
    . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
      assumption
    . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
      apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
      assumption
| getLsb expr idx =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := blastGetLsb)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  assumption
Proof state after:
no goals