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

State before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
⊢ limplies (PosFin n) f f.assignments
Tactic:
intro p pf
State after:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments

State before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments
Tactic:
rcases f_assignments_invariant with ⟨hsize, f_assignments_invariant⟩
State after:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
⊢ p ⊨ f.assignments

State before:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
⊢ ∀ (i : PosFin n), hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
intro i
State after:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

State before:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
specialize f_assignments_invariant i (decide (p i = false))
State after:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

State before:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
by_cases hasAssignment (decide (p i = false)) (f.assignments[i.1]'(by rw [hsize]; exact i.2.2))
State after:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

State before:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
. next h =>
  specialize f_assignments_invariant h p pf
  by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
State after:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

State before:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
. next h => simp_all [getElem!, i.2.2]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < f.assignments.size
Tactic:
rw [hsize]
State after:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < n

State before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < n
Tactic:
exact i.2.2
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
next h =>
specialize f_assignments_invariant h p pf
by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
specialize f_assignments_invariant h p pf
State after:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
f_assignments_invariant : p ⊨ (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

State before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
f_assignments_invariant : p ⊨ (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
next h => simp_all [getElem!, i.2.2]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
simp_all [getElem!, i.2.2]
State after:
no goals