internlm/Lean-Github huggingface dataset:
Theorem: BoolExpr.eval_attach
Proof state before:
x : BoolExpr Nat
f : Fin x.vars → Bool
f' : Nat → Bool
h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
⊢ f = fun i => f' ↑i
Tactic:
subst h
Proof state after:
x : BoolExpr Nat
f : Fin x.vars → Bool
⊢ f = fun i => (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) ↑i
Theorem: BoolExpr.eval_attach
Proof state before:
x : BoolExpr Nat
f : Fin x.vars → Bool
⊢ f = fun i => (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) ↑i
Tactic:
simp
Proof state after:
no goals
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
h : x.attach.unsat
f : Nat → Bool
⊢ eval f x = false
Tactic:
specialize h fun i => f i
Proof state after:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => f ↑i) x.attach = false
⊢ eval f x = false
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => f ↑i) x.attach = false
⊢ eval f x = false
Tactic:
rw [eval_attach] at h
Proof state after:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ eval f x = false
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ eval f x = false
Tactic:
rw [← h]
Proof state after:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ eval f x = eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ eval f x = eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x
Tactic:
apply eval_congr
Proof state after:
case w
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ ∀ (i : Nat), i < x.vars → f i = if h : i < x.vars then f ↑⟨i, h⟩ else false
Theorem: BoolExpr.attach_unsat
Proof state before:
case w
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ ∀ (i : Nat), i < x.vars → f i = if h : i < x.vars then f ↑⟨i, h⟩ else false
Tactic:
simp_all
Proof state after:
no goals
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
h : x.unsat
f : Fin x.vars → Bool
⊢ eval f x.attach = false
Tactic:
specialize h fun i => if h : i < x.vars then f ⟨i, h⟩ else false
Proof state after:
x : BoolExpr Nat
f : Fin x.vars → Bool
h : eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
⊢ eval f x.attach = false
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
f : Fin x.vars → Bool
h : eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
⊢ eval f x.attach = false
Tactic:
rw [eval_attach]
Proof state after:
x : BoolExpr Nat
f : Fin x.vars → Bool
h : eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
⊢ eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
Theorem: BoolExpr.attach_unsat
Proof state before:
x : BoolExpr Nat
f : Fin x.vars → Bool
h : eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
⊢ eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.denote_mkAtom_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
⊢ aig.cache.find? (Decl.atom v) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkAtom v, assign⟧
Tactic:
have := hit.hvalid
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
this : aig.decls[hit.idx] = Decl.atom v
⊢ aig.cache.find? (Decl.atom v) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkAtom v, assign⟧
Theorem: AIG.denote_mkAtom_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
this : aig.decls[hit.idx] = Decl.atom v
⊢ aig.cache.find? (Decl.atom v) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkAtom v, assign⟧
Tactic:
simp only [denote_mkAtom]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
this : aig.decls[hit.idx] = Decl.atom v
⊢ aig.cache.find? (Decl.atom v) = some hit → ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = assign v
Theorem: AIG.denote_mkAtom_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
this : aig.decls[hit.idx] = Decl.atom v
⊢ aig.cache.find? (Decl.atom v) = some hit → ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = assign v
Tactic:
unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
this : aig.decls[hit.idx] = Decl.atom v
⊢ aig.cache.find? (Decl.atom v) = some hit →
    (match elem :
        { aig := aig,
                ref :=
                  { gate := hit.idx,
                    hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
      | Decl.const b => b
      | Decl.atom v_1 => assign v_1
      | Decl.gate lhs rhs linv rinv =>
        let_fun this := ⋯;
        let lval := denote.go lhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
        let rval := denote.go rhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
        xor lval linv && xor rval rinv) =
      assign v
Theorem: AIG.denote_mkAtom_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
v : α
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.atom v)
this : aig.decls[hit.idx] = Decl.atom v
⊢ aig.cache.find? (Decl.atom v) = some hit →
    (match elem :
        { aig := aig,
                ref :=
                  { gate := hit.idx,
                    hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
      | Decl.const b => b
      | Decl.atom v_1 => assign v_1
      | Decl.gate lhs rhs linv rinv =>
        let_fun this := ⋯;
        let lval := denote.go lhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
        let rval := denote.go rhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
        xor lval linv && xor rval rinv) =
      assign v
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.mkAtomCached_hit_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some hit
⊢ (aig.mkAtomCached var).aig = aig
Tactic:
simp only [mkAtomCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some hit
⊢ (match aig.cache.find? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig
Theorem: AIG.mkAtomCached_hit_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some hit
⊢ (match aig.cache.find? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.mkAtomCached_miss_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hcache : aig.cache.find? (Decl.atom var) = none
⊢ (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
Tactic:
simp only [mkAtomCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hcache : aig.cache.find? (Decl.atom var) = none
⊢ (match aig.cache.find? (Decl.atom var) with
        | some hit =>
          { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
        | none =>
          {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls =
    aig.decls.push (Decl.atom var)
Theorem: AIG.mkAtomCached_miss_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hcache : aig.cache.find? (Decl.atom var) = none
⊢ (match aig.cache.find? (Decl.atom var) with
        | some hit =>
          { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
        | none =>
          {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls =
    aig.decls.push (Decl.atom var)
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Tactic:
match hcache:aig.cache.find? (.atom var) with
| some gate =>
  have := mkAtomCached_hit_aig aig hcache
  simp [this]
| none =>
  have := mkAtomCached_miss_aig aig hcache
  simp only [this, Array.get_push]
  split
  . rfl
  . contradiction
Proof state after:
no goals
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
gate : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some gate
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Tactic:
have := mkAtomCached_hit_aig aig hcache
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
gate : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some gate
this : (aig.mkAtomCached var).aig = aig
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
gate : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some gate
this : (aig.mkAtomCached var).aig = aig
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Tactic:
simp [this]
Proof state after:
no goals
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Tactic:
have := mkAtomCached_miss_aig aig hcache
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
⊢ (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [this, Array.get_push]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.atom var) = aig.decls[idx]
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.atom var) = aig.decls[idx]
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. rfl
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. contradiction
Proof state after:
no goals
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
rfl
Proof state after:
no goals
Theorem: AIG.mkAtomCached_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtomCached var).aig.decls.size
hcache : aig.cache.find? (Decl.atom var) = none
this : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
contradiction
Proof state after:
no goals
Theorem: AIG.mkAtomCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size
Tactic:
dsimp [mkAtomCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤
    (match aig.cache.find? (Decl.atom var) with
          | some hit =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
          | none =>
            {
              aig :=
                { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                  inv := ⋯ },
              ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls.size
Theorem: AIG.mkAtomCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤
    (match aig.cache.find? (Decl.atom var) with
          | some hit =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
          | none =>
            {
              aig :=
                { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                  inv := ⋯ },
              ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls.size
Tactic:
split
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }.aig.decls.size
Theorem: AIG.mkAtomCached_le_size
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }.aig.decls.size
Tactic:
. simp
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }.aig.decls.size
Theorem: AIG.mkAtomCached_le_size
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }.aig.decls.size
Tactic:
. simp_arith
Proof state after:
no goals
Theorem: AIG.mkAtomCached_le_size
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.mkAtomCached_le_size
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }.aig.decls.size
Tactic:
simp_arith
Proof state after:
no goals
Theorem: AIG.mkAtomCached_eval_eq_mkAtom_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
⊢ ⟦aig.mkAtomCached var, assign⟧ = ⟦aig.mkAtom var, assign⟧
Tactic:
simp only [mkAtomCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
⊢ ⟦match aig.cache.find? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkAtom var, assign⟧