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

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
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⟧

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]
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

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
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

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
State after:
no goals