Theorem: AIG.ofBoolExprCachedDirect_unsat_iff (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 α
⊢ (ofBoolExprCachedDirect expr).unsat ↔ expr.unsat
Tactic:
constructor
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

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

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

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

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