internlm/Lean-Github huggingface dataset:
Theorem: AIG.ofBoolExprCached.go_IsPrefix_aig
Proof state before:
case idx_eq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
. intro idx h
  apply ofBoolExprCached.go_decl_eq
Proof state after:
case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Theorem: AIG.ofBoolExprCached.go_IsPrefix_aig
Proof state before:
case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
. apply ofBoolExprCached.go_decls_size_le
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_IsPrefix_aig
Proof state before:
case idx_eq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
intro idx h
Proof state after:
case idx_eq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
idx : Nat
h : idx < aig.decls.size
⊢ (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_IsPrefix_aig
Proof state before:
case idx_eq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
idx : Nat
h : idx < aig.decls.size
⊢ (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
apply ofBoolExprCached.go_decl_eq
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_IsPrefix_aig
Proof state before:
case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
apply ofBoolExprCached.go_decls_size_le
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_denote_entry
Proof state before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
assign : β → Bool
entry : Entrypoint β
h : entry.ref.gate < (go expr entry.aig atomHandler).val.aig.decls.size
⊢ ⟦{ aig := (go expr entry.aig atomHandler).val.aig, ref := { gate := entry.ref.gate, hgate := h } }, assign⟧ =
    ⟦entry, assign⟧
Tactic:
apply denote.eq_of_aig_eq
Proof state after:
case hprefix
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
assign : β → Bool
entry : Entrypoint β
h : entry.ref.gate < (go expr entry.aig atomHandler).val.aig.decls.size
⊢ IsPrefix entry.aig.decls (go expr entry.aig atomHandler).val.aig.decls
Theorem: AIG.ofBoolExprCached.go_denote_entry
Proof state before:
case hprefix
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
assign : β → Bool
entry : Entrypoint β
h : entry.ref.gate < (go expr entry.aig atomHandler).val.aig.decls.size
⊢ IsPrefix entry.aig.decls (go expr entry.aig atomHandler).val.aig.decls
Tactic:
apply ofBoolExprCached.go_IsPrefix_aig
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_eval_eq_eval
Proof state before:
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
aig : AIG α
assign : α → Bool
⊢ ⟦(go expr aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign expr
Tactic:
induction expr generalizing aig with
| const => simp [go]
| literal => simp [go]
| not expr ih => simp [go, ih]
| gate g lhs rhs lih rih => cases g <;> simp [go, Gate.eval, lih, rih]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_eval_eq_eval
Proof state before:
case const
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
a✝ : Bool
aig : AIG α
⊢ ⟦(go (BoolExpr.const a✝) aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign (BoolExpr.const a✝)
Tactic:
simp [go]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_eval_eq_eval
Proof state before:
case literal
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
a✝ : α
aig : AIG α
⊢ ⟦(go (BoolExpr.literal a✝) aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign (BoolExpr.literal a✝)
Tactic:
simp [go]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_eval_eq_eval
Proof state before:
case not
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
expr : BoolExpr α
ih : ∀ (aig : AIG α), ⟦(go expr aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign expr
aig : AIG α
⊢ ⟦(go expr.not aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign expr.not
Tactic:
simp [go, ih]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_eval_eq_eval
Proof state before:
case gate
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
g : Gate
lhs rhs : BoolExpr α
lih : ∀ (aig : AIG α), ⟦(go lhs aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign lhs
rih : ∀ (aig : AIG α), ⟦(go rhs aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign rhs
aig : AIG α
⊢ ⟦(go (BoolExpr.gate g lhs rhs) aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign (BoolExpr.gate g lhs rhs)
Tactic:
cases g <;> simp [go, Gate.eval, lih, rih]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCachedDirect_eval_eq_eval
Proof state before:
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
assign : α → Bool
⊢ ⟦ofBoolExprCachedDirect expr, assign⟧ = BoolExpr.eval assign expr
Tactic:
apply ofBoolExprCached.go_eval_eq_eval
Proof state after:
no goals
Theorem: AIG.ofBoolExprCachedDirect_unsat_iff
Proof state before:
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
⊢ (ofBoolExprCachedDirect expr).unsat ↔ expr.unsat
Tactic:
constructor
Proof state after:
case mp
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
⊢ (ofBoolExprCachedDirect expr).unsat → expr.unsat

case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
⊢ expr.unsat → (ofBoolExprCachedDirect expr).unsat
Theorem: AIG.ofBoolExprCachedDirect_unsat_iff
Proof state before:
case mp
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
⊢ (ofBoolExprCachedDirect expr).unsat → expr.unsat

case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
⊢ expr.unsat → (ofBoolExprCachedDirect expr).unsat
Tactic:
all_goals
  intro h assign
  specialize h assign
  simpa using h
Proof state after:
no goals
Theorem: AIG.ofBoolExprCachedDirect_unsat_iff
Proof state before:
case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
⊢ expr.unsat → (ofBoolExprCachedDirect expr).unsat
Tactic:
intro h assign
Proof state after:
case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
h : expr.unsat
assign : α → Bool
⊢ ⟦{ aig := (ofBoolExprCachedDirect expr).aig, ref := { gate := (ofBoolExprCachedDirect expr).ref.gate, hgate := ⋯ } },
      assign⟧ =
    false
Theorem: AIG.ofBoolExprCachedDirect_unsat_iff
Proof state before:
case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
h : expr.unsat
assign : α → Bool
⊢ ⟦{ aig := (ofBoolExprCachedDirect expr).aig, ref := { gate := (ofBoolExprCachedDirect expr).ref.gate, hgate := ⋯ } },
      assign⟧ =
    false
Tactic:
specialize h assign
Proof state after:
case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
assign : α → Bool
h : BoolExpr.eval assign expr = false
⊢ ⟦{ aig := (ofBoolExprCachedDirect expr).aig, ref := { gate := (ofBoolExprCachedDirect expr).ref.gate, hgate := ⋯ } },
      assign⟧ =
    false
Theorem: AIG.ofBoolExprCachedDirect_unsat_iff
Proof state before:
case mpr
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
assign : α → Bool
h : BoolExpr.eval assign expr = false
⊢ ⟦{ aig := (ofBoolExprCachedDirect expr).aig, ref := { gate := (ofBoolExprCachedDirect expr).ref.gate, hgate := ⋯ } },
      assign⟧ =
    false
Tactic:
simpa using h
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
⊢ aig.decls.size ≤ (go aig w input newWidth curr hcurr s).aig.decls.size
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
⊢ aig.decls.size ≤
    (if hcurr1 : curr < newWidth then
            if hcurr2 : curr < w then
              let s := s.pushRef (input.getRef curr hcurr2);
              go aig w input newWidth (curr + 1) ⋯ s
            else
              let res := aig.mkConstCached false;
              let aig_1 := res.aig;
              let zeroRef := res.ref;
              let_fun hcast := ⋯;
              let input := input.cast hcast;
              let s := s.cast hcast;
              let s := s.pushRef zeroRef;
              go aig_1 w input newWidth (curr + 1) ⋯ s
          else
            let_fun hcurr := ⋯;
            { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
⊢ aig.decls.size ≤
    (if hcurr1 : curr < newWidth then
            if hcurr2 : curr < w then
              let s := s.pushRef (input.getRef curr hcurr2);
              go aig w input newWidth (curr + 1) ⋯ s
            else
              let res := aig.mkConstCached false;
              let aig_1 := res.aig;
              let zeroRef := res.ref;
              let_fun hcast := ⋯;
              let input := input.cast hcast;
              let s := s.cast hcast;
              let s := s.pushRef zeroRef;
              go aig_1 w input newWidth (curr + 1) ⋯ s
          else
            let_fun hcurr := ⋯;
            { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : curr < newWidth
⊢ aig.decls.size ≤
    (if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go aig w input newWidth (curr + 1) ⋯ s
          else
            let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let zeroRef := res.ref;
            let_fun hcast := ⋯;
            let input := input.cast hcast;
            let s := s.cast hcast;
            let s := s.pushRef zeroRef;
            go aig_1 w input newWidth (curr + 1) ⋯ s).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : ¬curr < newWidth
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : curr < newWidth
⊢ aig.decls.size ≤
    (if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go aig w input newWidth (curr + 1) ⋯ s
          else
            let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let zeroRef := res.ref;
            let_fun hcast := ⋯;
            let input := input.cast hcast;
            let s := s.cast hcast;
            let s := s.pushRef zeroRef;
            go aig_1 w input newWidth (curr + 1) ⋯ s).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : ¬curr < newWidth
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
. dsimp
  split
  . refine Nat.le_trans ?_ (by apply go_le_size)
    omega
  . refine Nat.le_trans ?_ (by apply go_le_size)
    apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : ¬curr < newWidth
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : ¬curr < newWidth
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
. simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : curr < newWidth
⊢ aig.decls.size ≤
    (if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go aig w input newWidth (curr + 1) ⋯ s
          else
            let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let zeroRef := res.ref;
            let_fun hcast := ⋯;
            let input := input.cast hcast;
            let s := s.cast hcast;
            let s := s.pushRef zeroRef;
            go aig_1 w input newWidth (curr + 1) ⋯ s).aig.decls.size
Tactic:
dsimp
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : curr < newWidth
⊢ aig.decls.size ≤
    (if hcurr2 : curr < w then go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr hcurr2))
          else
            go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
              ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝ : curr < newWidth
⊢ aig.decls.size ≤
    (if hcurr2 : curr < w then go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr hcurr2))
          else
            go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
              ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Tactic:
split
Proof state after:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ aig.decls.size ≤ (go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr h✝))).aig.decls.size

case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ aig.decls.size ≤ (go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr h✝))).aig.decls.size

case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Tactic:
. refine Nat.le_trans ?_ (by apply go_le_size)
  omega
Proof state after:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Tactic:
. refine Nat.le_trans ?_ (by apply go_le_size)
  apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ aig.decls.size ≤ (go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr h✝))).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)
Proof state after:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ aig.decls.size ≤ aig.decls.size
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ aig.decls.size ≤ aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ ?m.16246 ≤ (go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr h✝))).aig.decls.size
Tactic:
apply go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_le_size
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)
Proof state after:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ aig.decls.size ≤ (aig.mkConstCached false).aig.decls.size