Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert (LeanSAT/LRAT/Formula/RatAddSound.lean)

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
⊢ ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true → limplies (PosFin n) f (f.insert c)
Tactic:
intro performRupCheck_success p pf
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c
Tactic:
simp only [performRupCheck, Prod.mk.eta] at performRupCheck_success
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ p ⊨ f.insert c

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ p ⊨ f.insert c
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
Tactic:
intro c' c'_in_fc
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
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
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
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
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

State before:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
. rw [c'_eq_c]
  exact confirmRupHint_of_insertRat_fold_entails_hsat f hf c rupHints p pf performRupCheck_success
State after:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

State before:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
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
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'
Tactic:
rw [c'_eq_c]
State after:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c

State before:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c
Tactic:
exact confirmRupHint_of_insertRat_fold_entails_hsat f hf c rupHints p pf performRupCheck_success
State after:
no goals

State before:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
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
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
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
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
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