internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.propCompleteAux
Proof state before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ IsDeduct ∅ P
Tactic:
apply Δ_U_2
Proof state after:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ Δ_U ⊆ P.primeSet

case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ Δ_U ⊆ P.primeSet
Tactic:
simp only [Finset.insert_subset_iff] at h1
Proof state after:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Tactic:
cases h1
Proof state after:
case h1.intro
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
left✝ : U ∈ P.primeSet
right✝ : Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Theorem: FOL.NV.propCompleteAux
Proof state before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Tactic:
case intro h1_left h1_right =>
  exact h1_right
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Tactic:
exact h1_right
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
simp only [Finset.insert_subset_iff] at h1
Proof state after:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
simp at h2
Proof state after:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
cases h1
Proof state after:
case h2.intro
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
left✝ : U ∈ P.primeSet
right✝ : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
simp
Proof state after:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U) P
Tactic:
apply propCompleteAuxAux P U Δ_U
Proof state after:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ U' ∈ ↑Δ_U, U'.IsPrime

case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U.IsPrime

case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∉ ↑Δ_U

case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U ∪ {evalPrimeFfToNot V U}) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ U' ∈ ↑Δ_U, U'.IsPrime
Tactic:
intro U' a1
Proof state after:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U'.IsPrime
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U'.IsPrime
Tactic:
apply mem_primeSet_isPrime P U'
Proof state after:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ P.primeSet
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ P.primeSet
Tactic:
apply h1_right
Proof state after:
case h1_Δ.a
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ Δ_U
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1_Δ.a
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ Δ_U
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U.IsPrime
Tactic:
apply mem_primeSet_isPrime P U
Proof state after:
case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∈ P.primeSet
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∈ P.primeSet
Tactic:
exact h1_left
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∉ ↑Δ_U
Tactic:
exact Δ_U_1
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U ∪ {evalPrimeFfToNot V U}) P
Tactic:
simp
Proof state after:
case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
Theorem: FOL.NV.propCompleteAux
Proof state before:
case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.prop_complete
Proof state before:
P : Formula
h1 : P.IsTautoPrime
⊢ IsProof P
Tactic:
simp only [IsProof]
Proof state after:
P : Formula
h1 : P.IsTautoPrime
⊢ IsDeduct ∅ P
Theorem: FOL.NV.prop_complete
Proof state before:
P : Formula
h1 : P.IsTautoPrime
⊢ IsDeduct ∅ P
Tactic:
apply propCompleteAux P P.primeSet
Proof state after:
case h1
P : Formula
h1 : P.IsTautoPrime
⊢ P.primeSet ⊆ P.primeSet

case h2
P : Formula
h1 : P.IsTautoPrime
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
Theorem: FOL.NV.prop_complete
Proof state before:
case h1
P : Formula
h1 : P.IsTautoPrime
⊢ P.primeSet ⊆ P.primeSet
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.prop_complete
Proof state before:
case h2
P : Formula
h1 : P.IsTautoPrime
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
Tactic:
intro V
Proof state after:
case h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
Theorem: FOL.NV.prop_complete
Proof state before:
case h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
Tactic:
apply L_15_7 P P P.primeSet V (P.primeSet.image (evalPrimeFfToNot V))
Proof state after:
case h2.h1
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑P.primeSet ⊆ ↑P.primeSet

case h2.h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑(Finset.image (evalPrimeFfToNot V) P.primeSet) = evalPrimeFfToNot V '' ↑P.primeSet

case h2.h3
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
Theorem: FOL.NV.prop_complete
Proof state before:
case h2.h1
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑P.primeSet ⊆ ↑P.primeSet
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.prop_complete
Proof state before:
case h2.h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑(Finset.image (evalPrimeFfToNot V) P.primeSet) = evalPrimeFfToNot V '' ↑P.primeSet
Tactic:
simp only [Finset.coe_image]
Proof state after:
no goals
Theorem: FOL.NV.prop_complete
Proof state before:
case h2.h3
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
Tactic:
simp only [Formula.IsTautoPrime] at h1
Proof state after:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
Theorem: FOL.NV.prop_complete
Proof state before:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = if evalPrime V P then P else P.not_
Theorem: FOL.NV.prop_complete
Proof state before:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = if evalPrime V P then P else P.not_
Tactic:
specialize h1 V
Proof state after:
case h2.h3
P : Formula
V : VarBoolAssignment
h1 : evalPrime V P
⊢ P = if evalPrime V P then P else P.not_
Theorem: FOL.NV.prop_complete
Proof state before:
case h2.h3
P : Formula
V : VarBoolAssignment
h1 : evalPrime V P
⊢ P = if evalPrime V P then P else P.not_
Tactic:
simp only [if_pos h1]
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x : VarName
xs : Finset VarName
h1 : x ∈ xs
⊢ x.length ≤ finset_var_name_max_len xs
Tactic:
induction xs using Finset.induction_on
Proof state after:
case empty
x : VarName
h1 : x ∈ ∅
⊢ x.length ≤ finset_var_name_max_len ∅

case insert
x a✝² : VarName
s✝ : Finset VarName
a✝¹ : a✝² ∉ s✝
a✝ : x ∈ s✝ → x.length ≤ finset_var_name_max_len s✝
h1 : x ∈ insert a✝² s✝
⊢ x.length ≤ finset_var_name_max_len (insert a✝² s✝)
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x : VarName
h1 : x ∈ ∅
⊢ x.length ≤ finset_var_name_max_len ∅
Tactic:
case empty =>
  simp at h1
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x ∈ insert hd tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
case insert hd tl a1 ih =>
  simp at h1
  cases h1
  case inl c1 =>
    subst c1
    simp only [finset_var_name_max_len]
    simp
  case inr c1 =>
    simp only [finset_var_name_max_len] at ih
    simp only [finset_var_name_max_len]
    simp
    right
    exact ih c1
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x : VarName
h1 : x ∈ ∅
⊢ x.length ≤ finset_var_name_max_len ∅
Tactic:
simp at h1
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x ∈ insert hd tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
simp at h1
Proof state after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x = hd ∨ x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x = hd ∨ x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
cases h1
Proof state after:
case inl
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h✝ : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)

case inr
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h✝ : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
case inl c1 =>
  subst c1
  simp only [finset_var_name_max_len]
  simp
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
case inr c1 =>
  simp only [finset_var_name_max_len] at ih
  simp only [finset_var_name_max_len]
  simp
  right
  exact ih c1
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
subst c1
Proof state after:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ finset_var_name_max_len (insert x tl)
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ finset_var_name_max_len (insert x tl)
Tactic:
simp only [finset_var_name_max_len]
Proof state after:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert x tl)
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert x tl)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
simp only [finset_var_name_max_len] at ih
Proof state after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
simp only [finset_var_name_max_len]
Proof state after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert hd tl)