internlm/Lean-Github huggingface dataset:
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'
f'_readyForRatAdd : readyForRatAdd f'
⊢ unsatisfiable α f
Tactic:
specialize ih f' f'_readyForRupAdd f'_readyForRatAdd restPrfWellFormed f'_success
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α 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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
⊢ unsatisfiable α f
Tactic:
have f_liff_f' : liff α f f' := rupAdd_sound 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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_liff_f' : liff α f 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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_liff_f' : liff α f f'
⊢ 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
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_liff_f' : liff α f f'
p : α → Bool
pf : p ⊨ f
⊢ False
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_liff_f' : liff α f f'
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
rw [f_liff_f' p] 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
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_liff_f' : liff α f f'
p : α → Bool
pf : p ⊨ f'
⊢ False
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_liff_f' : liff α f f'
p : α → Bool
pf : p ⊨ f'
⊢ False
Tactic:
exact ih p pf
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
f'_def : f' = Formula.insert f c
⊢ readyForRupAdd f'
Tactic:
rw [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
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
⊢ readyForRupAdd (Formula.insert f c)
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
⊢ readyForRupAdd (Formula.insert f c)
Tactic:
exact insert_readyForRupAdd f c f_readyForRupAdd
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
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
⊢ readyForRatAdd f'
Tactic:
rw [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
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'
⊢ readyForRatAdd (Formula.insert f c)
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'
⊢ readyForRatAdd (Formula.insert f c)
Tactic:
exact insert_readyForRatAdd f c f_readyForRatAdd
Proof state after:
no goals
Theorem: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : limplies α pivot c
heq : performRatAdd f c pivot rupHints ratHints = (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:
rw [limplies_iff_mem] at pivot_limplies_c
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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
Theorem: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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 := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c 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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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
Theorem: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (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
Tactic:
specialize ih f' f'_readyForRupAdd f'_readyForRatAdd restPrfWellFormed f'_success
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
⊢ unsatisfiable α f
Theorem: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
⊢ unsatisfiable α f
Tactic:
have f_equisat_f' : equisat α f f' := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c 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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_equisat_f' : equisat α f f'
⊢ unsatisfiable α f
Theorem: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_equisat_f' : equisat α f f'
⊢ 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
f_readyForRatAdd : readyForRatAdd f
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_equisat_f' : equisat α f f'
p : α → Bool
pf : p ⊨ f
⊢ False
Theorem: addRatCaseSound
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_equisat_f' : equisat α f f'
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
rw [equisat] at f_equisat_f'
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 : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
f'_readyForRatAdd : readyForRatAdd f'
ih : unsatisfiable α f'
f_equisat_f' : unsatisfiable α f ↔ unsatisfiable α f'
p : α → Bool
pf : p ⊨ f
⊢ False