Theorem: BoolExprNat.unsat_iff (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.unsat
Tactic:
rw [← BoolExpr.attach_unsat]
State after:
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.attach.unsat

State before:
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.attach.unsat
Tactic:
simp only [unsat, BoolExpr.unsat]
State after:
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) ↔
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false

State before:
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) ↔
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
constructor
State after:
case mp
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) →
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false

case mpr
x : BoolExprNat
⊢ (∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false) →
    ∀ (f : List Bool), eval f x = false

State before:
case mp
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) →
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
intro h f
State after:
case mp
x : BoolExprNat
h : ∀ (f : List Bool), eval f x = false
f : Fin x.toBoolExpr.vars → Bool
⊢ BoolExpr.eval f x.toBoolExpr.attach = false

State before:
case mp
x : BoolExprNat
h : ∀ (f : List Bool), eval f x = false
f : Fin x.toBoolExpr.vars → Bool
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
specialize h (List.ofFn f)
State after:
case mp
x : BoolExprNat
f : Fin x.toBoolExpr.vars → Bool
h : eval (List.ofFn f) x = false
⊢ BoolExpr.eval f x.toBoolExpr.attach = false

State before:
case mp
x : BoolExprNat
f : Fin x.toBoolExpr.vars → Bool
h : eval (List.ofFn f) x = false
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
simpa using h
State after:
no goals

State before:
case mpr
x : BoolExprNat
⊢ (∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false) →
    ∀ (f : List Bool), eval f x = false
Tactic:
intro h f
State after:
case mpr
x : BoolExprNat
h : ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
f : List Bool
⊢ eval f x = false

State before:
case mpr
x : BoolExprNat
f : List Bool
h : BoolExpr.eval (fun x_1 => f.getD (↑x_1) false) x.toBoolExpr.attach = false
⊢ eval f x = false
Tactic:
simpa using h
State after:
no goals