Theorem: LRAT.unsat_of_cons_none_unsat (LeanSAT/Reflect/Glue.lean)

State before:
n : Nat
clauses : List (Option (DefaultClause n))
⊢ unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses))) →
    unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray clauses))
Tactic:
intro h assign hassign
State after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ False

State before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ False
Tactic:
apply h assign
State after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ assign ⊨ DefaultFormula.ofArray (List.toArray (none :: clauses))

State before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ assign ⊨ DefaultFormula.ofArray (List.toArray (none :: clauses))
Tactic:
simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at *
State after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses))) → assign ⊨ x

State before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses))) → assign ⊨ x
Tactic:
intro clause hclause
State after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses)))
⊢ assign ⊨ clause

State before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses)))
⊢ assign ⊨ clause
Tactic:
simp_all[LRAT.DefaultFormula.ofArray, LRAT.Formula.toList, LRAT.DefaultFormula.toList]
State after:
no goals