internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
case h_3.inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h✝ : ¬id < f.clauses.size
h1 : some c ∈ f.clauses.data
⊢ some c ∈ f.clauses.data
Tactic:
exact h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
case h_3.inr.inl
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
    List.map unit
      { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.rupUnits.toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList ∨
    c ∈ List.map unit f.rupUnits.toList ∨ c ∈ List.map unit f.ratUnits.toList
Tactic:
exact (Or.inr ∘ Or.inl) h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
case h_3.inr.inr
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
    List.map unit
      { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.ratUnits.toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList ∨
    c ∈ List.map unit f.rupUnits.toList ∨ c ∈ List.map unit f.ratUnits.toList
Tactic:
exact (Or.inr ∘ Or.inr) h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_subset
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (f.delete arr).toList → c ∈ f.toList
Tactic:
simp only [delete, Array.foldl_eq_foldl_data]
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Theorem: LRAT.DefaultFormula.delete_subset
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Tactic:
have hb : c ∈ toList f → c ∈ toList f := id
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Theorem: LRAT.DefaultFormula.delete_subset
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Tactic:
have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.data) :
  c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih $ deleteOne_subset f' id c h
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.data → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Theorem: LRAT.DefaultFormula.delete_subset
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.data → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_subset
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
⊢ c ∈ (f'.deleteOne id).toList → c ∈ f.toList
Tactic:
intro h
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList
Theorem: LRAT.DefaultFormula.delete_subset
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList
Tactic:
exact ih $ deleteOne_subset f' id c h
Proof state after:
no goals
Theorem: bitvec_AddSub_1539
Proof state before:
⊢ ∀ (a x : BitVec 64), x - (0 - a) = x + a
Tactic:
intros
Proof state after:
a✝ x✝ : BitVec 64
⊢ x✝ - (0 - a✝) = x✝ + a✝
Theorem: bitvec_AddSub_1539
Proof state before:
a✝ x✝ : BitVec 64
⊢ x✝ - (0 - a✝) = x✝ + a✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2367
Proof state before:
⊢ ∀ (A C1 op1 : BitVec 64), A ||| C1 ||| op1 = A ||| op1 ||| C1
Tactic:
intros
Proof state after:
A✝ C1✝ op1✝ : BitVec 64
⊢ A✝ ||| C1✝ ||| op1✝ = A✝ ||| op1✝ ||| C1✝
Theorem: bitvec_AndOrXor_2367
Proof state before:
A✝ C1✝ op1✝ : BitVec 64
⊢ A✝ ||| C1✝ ||| op1✝ = A✝ ||| op1✝ ||| C1✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
let f' := (performRupAdd f empty rupHints).1
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
⊢ unsatisfiable α f
Tactic:
have f'_def := rupAdd_result f empty rupHints f' f_readyForRupAdd
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', true) → f' = Formula.insert f empty
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', true) → f' = Formula.insert f empty
⊢ unsatisfiable α f
Tactic:
rw [← rupAddSuccess] at f'_def
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → f' = Formula.insert f empty
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → f' = Formula.insert f empty
⊢ unsatisfiable α f
Tactic:
specialize f'_def rfl
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
⊢ unsatisfiable α f
Tactic:
have f_liff_f' := rupAdd_sound f empty rupHints f' f_readyForRupAdd
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', true) → liff α f f'
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', true) → liff α f f'
⊢ unsatisfiable α f
Tactic:
rw [← rupAddSuccess] at f_liff_f'
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → liff α f f'
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → liff α f f'
⊢ unsatisfiable α f
Tactic:
specialize f_liff_f' rfl
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : liff α f f'
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : liff α f f'
⊢ unsatisfiable α f
Tactic:
rw [f'_def] at f_liff_f'
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : liff α f (Formula.insert f empty)
⊢ unsatisfiable α f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : liff α f (Formula.insert f empty)
⊢ unsatisfiable α f
Tactic:
intro p pf
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : liff α f (Formula.insert f empty)
p : α → Bool
pf : p ⊨ f
⊢ False
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : liff α f (Formula.insert f empty)
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
specialize f_liff_f' p
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : p ⊨ f
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : p ⊨ f
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False
Tactic:
rw [f_liff_f', sat_iff_forall] at pf
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False
Tactic:
have empty_in_f' : empty ∈ toList (Formula.insert f empty) := by
  rw [Formula.insert_iff]
  exact Or.inl rfl
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
⊢ False
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
⊢ False
Tactic:
specialize pf empty empty_in_f'
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
pf : p ⊨ empty
⊢ False
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
pf : p ⊨ empty
⊢ False
Tactic:
simp only [HSat.eval, Clause.instHSat, List.any_eq_true, decide_eq_true_eq, Misc.Prod.exists, Misc.Bool.exists_bool,
  empty_eq, List.any_nil] at pf
Proof state after:
no goals
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ empty ∈ Formula.toList (Formula.insert f empty)
Tactic:
rw [Formula.insert_iff]
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ empty = empty ∨ empty ∈ Formula.toList f
Theorem: addEmptyCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ empty = empty ∨ empty ∈ Formula.toList f
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: addRupCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
⊢ unsatisfiable α f
Tactic:
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd heq
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
⊢ unsatisfiable α f
Theorem: addRupCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
⊢ unsatisfiable α f
Tactic:
have f'_readyForRupAdd : readyForRupAdd f' := by
  rw [f'_def]
  exact insert_readyForRupAdd f c f_readyForRupAdd
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
⊢ unsatisfiable α f
Theorem: addRupCaseSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
⊢ unsatisfiable α f
Tactic:
have f'_readyForRatAdd : readyForRatAdd f' := by
  rw [f'_def]
  exact insert_readyForRatAdd f c f_readyForRatAdd
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
⊢ unsatisfiable α f