Theorem: addEmptyCaseSound (LeanSAT/LRAT/LRATCheckerSound.lean)

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
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

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
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

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
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

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
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

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
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

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'
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

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
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

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'
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

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
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

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
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

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
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

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
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

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'
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

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
State after:
no goals

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]
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

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
State after:
no goals