Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
⊢ f.strong_assignments_invariant → f.assignments_invariant
Tactic:
intro ⟨hsize, h⟩
State after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.assignments_invariant

State before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.assignments_invariant
Tactic:
apply Exists.intro hsize
State after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)

State before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
Tactic:
intro i b hb p pf
State after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ (i, b)

State before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ (i, b)
Tactic:
specialize h i b hb
State after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
h : unit (i, b) ∈ f.toList
⊢ p ⊨ (i, b)

State before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → decide (Clause.instHSat.1 p x) = true
⊢ p ⊨ (i, b)
Tactic:
specialize pf (unit (i, b)) h
State after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : decide (Clause.instHSat.1 p (unit (i, b))) = true
⊢ p ⊨ (i, b)

State before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : decide (Clause.instHSat.1 p (unit (i, b))) = true
⊢ p ⊨ (i, b)
Tactic:
simp [Clause.instHSat, unit_eq, Clause.toList] at pf
State after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : p ⊨ (i, b)
⊢ p ⊨ (i, b)

State before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : p ⊨ (i, b)
⊢ p ⊨ (i, b)
Tactic:
exact pf
State after:
no goals