Theorem: AIG.ofBoolExprCached.go_eval_eq_eval (LeanSAT/AIG/BoolExprCached.lean)

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

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

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

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

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