internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.confirmRupHint_of_insertRup_fold_entails_hsat
Proof state before:
case neg.intro.intro.inl.intro.inr.intro.intro.inr.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRupUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝¹ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
left✝ : (v', true) ∈ c.toList
v'_eq_v : negateLiteral (v', true) = (v, true)
⊢ False
Tactic:
. simp only [negateLiteral, Bool.not_true, Prod.mk.injEq, and_false] at v'_eq_v
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_of_insertRup_fold_entails_hsat
Proof state before:
case neg.intro.intro.inl.intro.inr.intro.intro.inl.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRupUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide True = false
⊢ False
Tactic:
cases pv
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_of_insertRup_fold_entails_hsat
Proof state before:
case neg.intro.intro.inl.intro.inr.intro.intro.inr.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRupUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝¹ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
left✝ : (v', true) ∈ c.toList
v'_eq_v : negateLiteral (v', true) = (v, true)
⊢ False
Tactic:
simp only [negateLiteral, Bool.not_true, Prod.mk.injEq, and_false] at v'_eq_v
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_of_insertRup_fold_entails_hsat
Proof state before:
case neg.intro.intro.inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
fc : DefaultFormula n × Bool := f.insertRupUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
unsat_c_in_f : unsat_c ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ False
Tactic:
exact p_unsat_c $ pf unsat_c unsat_c_in_f
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
⊢ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true → limplies (PosFin n) f (f.insert c)
Tactic:
intro performRupCheck_success p pf
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRupUnits 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
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ p ⊨ f.insert c
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
Proof state after:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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_insertRup_fold_entails_hsat f f_readyForRupAdd c rupHints p pf performRupCheck_success
Proof state after:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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]
Proof state after:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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_insertRup_fold_entails_hsat f f_readyForRupAdd c rupHints p pf performRupCheck_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
Proof state after:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRup_entails_safe_insert
Proof state before:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
⊢ liff (PosFin n) f f'
Tactic:
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd rupAddSuccess
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'
Tactic:
rw [performRupAdd] at rupAddSuccess
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess :
  (let negC := c.negate;
    match f.insertRupUnits negC with
    | (f, foundContradiction) =>
      if foundContradiction = true then
        let f := f.clearRupUnits;
        (f.insert c, true)
      else
        match f.performRupCheck rupHints with
        | (f, derivedLits, derivedEmpty, encounteredError) =>
          if encounteredError = true then (f, false)
          else
            if (!derivedEmpty) = true then (f, false)
            else
              match f with
              | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                let assignments := restoreAssignments assignments derivedLits;
                let f :=
                  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                      assignments := assignments }.clearRupUnits;
                (f.insert c, true)) =
    (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'