Theorem: AIG.mkConstCached_eval_eq_mkConst_eval (LeanSAT/AIG/CachedLemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧
Tactic:
simp only [mkConstCached]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦match aig.cache.find? (Decl.const val) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦match aig.cache.find? (Decl.const val) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
split
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
. next heq1 =>
  rw [denote_mkConst_cached heq1]
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
. simp [mkConst, denote]
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
next heq1 =>
rw [denote_mkConst_cached heq1]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq1 : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
rw [denote_mkConst_cached heq1]
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
simp [mkConst, denote]
State after:
no goals