Theorem: LRAT.DefaultFormula.insertRup_entails_safe_insert (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
⊢ (f.insertRupUnits c.negate).snd = true → limplies (PosFin n) f (f.insert c)
Tactic:
intro h p pf
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
Tactic:
intro c' c'_in_fc
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'
Tactic:
rw [insert_iff] at c'_in_fc
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
rcases c'_in_fc with c'_eq_c | c'_in_f
State after:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

State before:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
. rw [c'_eq_c]
  exact insertRup_entails_hsat f f_readyForRupAdd c p pf h
State after:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

State before:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
. simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
  exact pf c' c'_in_f
State after:
no goals

State before:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'
Tactic:
rw [c'_eq_c]
State after:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c

State before:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c
Tactic:
exact insertRup_entails_hsat f f_readyForRupAdd c p pf h
State after:
no goals

State before:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
State after:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'

State before:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'
Tactic:
exact pf c' c'_in_f
State after:
no goals