Theorem: sat_of_contained_sat (Saturn/Containment.lean)

State before:
n : ℕ
cl1 cl2 : Clause n
⊢ cl1⊇cl2 → ∀ (valuation : Valuation n), ClauseSat cl2 valuation → ClauseSat cl1 valuation
Tactic:
intro num_clauses valuation
State after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
⊢ ClauseSat cl2 valuation → ClauseSat cl1 valuation

State before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
⊢ ClauseSat cl2 valuation → ClauseSat cl1 valuation
Tactic:
intro ⟨j, jw, vs⟩
State after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
⊢ ClauseSat cl1 valuation

State before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
⊢ ClauseSat cl1 valuation
Tactic:
let lem0 :  cl2.get' j jw = some (valuation.get' j jw) := vs
State after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
⊢ ClauseSat cl1 valuation

State before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
⊢ ClauseSat cl1 valuation
Tactic:
let lem1 : get' cl1 j jw = some (get' valuation j jw) := num_clauses j jw (valuation.get' j jw) lem0
State after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
lem1 : get' cl1 j jw = some (get' valuation j jw) := num_clauses j jw (get' valuation j jw) lem0
⊢ ClauseSat cl1 valuation

State before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
lem1 : get' cl1 j jw = some (get' valuation j jw) := num_clauses j jw (get' valuation j jw) lem0
⊢ ClauseSat cl1 valuation
Tactic:
exact ⟨j, jw, lem1⟩
State after:
no goals