internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case mp
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
h : ∃ x, x ∈ f.toList ∧ ¬((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
⊢ False
Tactic:
rcases h with ⟨c', c'_in_f, pc'⟩
Proof state after:
case mp.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case mp.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ False
Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by rw [insert_iff]; exact Or.inr c'_in_f
Proof state after:
case mp.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
c'_in_fc : c' ∈ (f.insert c).toList
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case mp.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
c'_in_fc : c' ∈ (f.insert c).toList
⊢ False
Tactic:
exact pc' $ pfc c' c'_in_fc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ c' ∈ (f.insert c).toList
Tactic:
rw [insert_iff]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ c' = c ∨ c' ∈ f.toList
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ c' = c ∨ c' ∈ f.toList
Tactic:
exact Or.inr c'_in_f
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case mpr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
⊢ unsatisfiable (PosFin n) (f.insert c) → unsatisfiable (PosFin n) f
Tactic:
intro fc_unsat p pf
Proof state after:
case mpr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case mpr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
⊢ False
Tactic:
by_cases pc : p ⊨ c
Proof state after:
case pos
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
⊢ False

case neg
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
⊢ False
Tactic:
specialize fc_unsat p
Proof state after:
case pos
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
fc_unsat : ¬(p ⊨ f.insert c)
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
fc_unsat : ∃ x, x ∈ (f.insert c).toList ∧ ¬decide (Clause.instHSat.1 p x) = true
⊢ False
Tactic:
rcases fc_unsat with ⟨c', c'_in_fc, pc'⟩
Proof state after:
case pos.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False
Tactic:
rw [insert_iff] at c'_in_fc
Proof state after:
case pos.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False
Tactic:
rcases c'_in_fc with c'_eq_c | c'_in_f
Proof state after:
case pos.intro.intro.inl
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_eq_c : c' = c
⊢ False

case pos.intro.intro.inr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos.intro.intro.inl
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_eq_c : c' = c
⊢ False

case pos.intro.intro.inr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
⊢ False
Tactic:
. simp only [c'_eq_c, decide_eq_true_eq] at pc'
  exact pc' pc
Proof state after:
case pos.intro.intro.inr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos.intro.intro.inl
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_eq_c : c' = c
⊢ False
Tactic:
simp only [c'_eq_c, decide_eq_true_eq] at pc'
Proof state after:
case pos.intro.intro.inl
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
c'_eq_c : c' = c
pc' : ¬Clause.instHSat.1 p c
⊢ False
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos.intro.intro.inl
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
c' : DefaultClause n
c'_eq_c : c' = c
pc' : ¬Clause.instHSat.1 p c
⊢ False
Tactic:
exact pc' pc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case pos.intro.intro.inr
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → decide (Clause.instHSat.1 p x) = true
⊢ False
Tactic:
exact pc' $ pf c' c'_in_f
Proof state after:
no goals