internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ (S.not_.imp_ P).not_)
Tactic:
apply IsDeduct.mp_ S.not_
Proof state after:
case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))

case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) S.not_
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1.a.a.h1
P S : Formula
⊢ IsProof (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.h1
P S : Formula
⊢ IsProof (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))
Tactic:
apply T_14_8
Proof state after:
no goals
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) S.not_
Tactic:
apply IsDeduct.mp_ P.not_
Proof state after:
case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ S.not_)

case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ S.not_)
Tactic:
apply IsDeduct.mp_ (S.imp_ P)
Proof state after:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) ((S.imp_ P).imp_ (P.not_.imp_ S.not_))

case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.imp_ P)
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) ((S.imp_ P).imp_ (P.not_.imp_ S.not_))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1.a.a.a.a.h1
P S : Formula
⊢ IsProof ((S.imp_ P).imp_ (P.not_.imp_ S.not_))
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a.a.h1
P S : Formula
⊢ IsProof ((S.imp_ P).imp_ (P.not_.imp_ S.not_))
Tactic:
apply T_14_7
Proof state after:
no goals
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.imp_ P)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a.a.a.a
P S : Formula
⊢ S.imp_ P ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a.a.a
P S : Formula
⊢ S.imp_ P ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.deductionTheoremConverse
Proof state before:
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ {P}) Q
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ {P}) (P.imp_ Q)

case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ {P}) P
Theorem: FOL.NV.deductionTheoremConverse
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ {P}) (P.imp_ Q)
Tactic:
exact T_14_10 (P.imp_ Q) Δ h1 {P}
Proof state after:
no goals
Theorem: FOL.NV.deductionTheoremConverse
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ {P}) P
Tactic:
apply IsDeduct.assume_
Proof state after:
case a.a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ P ∈ Δ ∪ {P}
Theorem: FOL.NV.deductionTheoremConverse
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ P ∈ Δ ∪ {P}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_12
Proof state before:
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) Q
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case a
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) (P.imp_ Q)

case a
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) P
Theorem: FOL.NV.T_14_12
Proof state before:
case a
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) (P.imp_ Q)
Tactic:
apply T_14_10_comm
Proof state after:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ (P.imp_ Q)
Theorem: FOL.NV.T_14_12
Proof state before:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ (P.imp_ Q)
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.T_14_12
Proof state before:
case a
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) P
Tactic:
apply T_14_10
Proof state after:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Δ P
Theorem: FOL.NV.T_14_12
Proof state before:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Δ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.C_14_14
Proof state before:
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ Q
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case a
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ (P.imp_ Q)

case a
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ P
Theorem: FOL.NV.C_14_14
Proof state before:
case a
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ (P.imp_ Q)
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.C_14_14
Proof state before:
case a
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ P
Tactic:
apply proof_imp_deduct
Proof state after:
case a.h1
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsProof P
Theorem: FOL.NV.C_14_14
Proof state before:
case a.h1
P Q : Formula
Γ : Set Formula
h1 : IsProof P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsProof P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.C_14_15
Proof state before:
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ Q
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ (P.imp_ Q)

case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ P
Theorem: FOL.NV.C_14_15
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ (P.imp_ Q)
Tactic:
apply proof_imp_deduct
Proof state after:
case a.h1
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsProof (P.imp_ Q)
Theorem: FOL.NV.C_14_15
Proof state before:
case a.h1
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsProof (P.imp_ Q)
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.C_14_15
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h1 : IsDeduct Γ F
h2 : ∀ H ∈ Γ, IsDeduct Δ H
⊢ IsDeduct Δ F
Tactic:
induction h1
Proof state after:
case axiom_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ phi✝

case assume_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ : Formula
a✝ : phi✝ ∈ Γ
⊢ IsDeduct Δ phi✝

case mp_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Γ (phi✝.imp_ psi✝)
a✝ : IsDeduct Γ phi✝
a_ih✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct Δ phi✝
⊢ IsDeduct Δ psi✝
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Tactic:
case axiom_ h1_phi h1_1 =>
  apply IsDeduct.axiom_
  exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : h1_phi ∈ Γ
⊢ IsDeduct Δ h1_phi
Tactic:
case assume_ h1_phi h1_1 => exact h2 h1_phi h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Γ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Γ h1_phi
h1_ih_1 : IsDeduct Δ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct Δ h1_phi
⊢ IsDeduct Δ h1_psi
Tactic:
case mp_ h1_phi h1_psi _ _ h1_ih_1 h1_ih_2 =>
  exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Theorem: FOL.NV.T_14_16
Proof state before:
case a
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : h1_phi ∈ Γ
⊢ IsDeduct Δ h1_phi
Tactic:
exact h2 h1_phi h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_16
Proof state before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Γ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Γ h1_phi
h1_ih_1 : IsDeduct Δ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct Δ h1_phi
⊢ IsDeduct Δ h1_psi
Tactic:
exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.C_14_17
Proof state before:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsProof P
⊢ IsProof Q
Tactic:
simp only [IsProof] at h2
Proof state after:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsProof Q
Theorem: FOL.NV.C_14_17
Proof state before:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsProof Q
Tactic:
simp only [IsProof]
Proof state after:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsDeduct ∅ Q
Theorem: FOL.NV.C_14_17
Proof state before:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsDeduct ∅ Q
Tactic:
exact T_14_16 Q ∅ Γ h1 h2
Proof state after:
no goals
Theorem: FOL.NV.eval_not
Proof state before:
P : Formula
V : VarBoolAssignment
⊢ evalPrime V P.not_ ↔ ¬evalPrime V P
Tactic:
simp only [Formula.evalPrime]
Proof state after:
no goals
Theorem: FOL.NV.eval_imp
Proof state before:
P Q : Formula
V : VarBoolAssignment
⊢ evalPrime V (P.imp_ Q) ↔ evalPrime V P → evalPrime V Q
Tactic:
simp only [Formula.evalPrime]
Proof state after:
no goals
Theorem: FOL.NV.eval_false
Proof state before:
V : VarBoolAssignment
⊢ evalPrime V false_ ↔ False
Tactic:
simp only [Formula.evalPrime]
Proof state after:
no goals
Theorem: FOL.NV.eval_and
Proof state before:
P Q : Formula
V : VarBoolAssignment
⊢ evalPrime V (P.and_ Q) ↔ evalPrime V P ∧ evalPrime V Q
Tactic:
simp only [Formula.evalPrime]
Proof state after:
no goals
Theorem: FOL.NV.eval_or
Proof state before:
P Q : Formula
V : VarBoolAssignment
⊢ evalPrime V (P.or_ Q) ↔ evalPrime V P ∨ evalPrime V Q
Tactic:
simp only [Formula.evalPrime]
Proof state after:
no goals
Theorem: FOL.NV.eval_iff
Proof state before:
P Q : Formula
V : VarBoolAssignment
⊢ evalPrime V (P.iff_ Q) ↔ (evalPrime V P ↔ evalPrime V Q)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_prop_true
Proof state before:
⊢ true_.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
⊢ ∀ (V : VarBoolAssignment), evalPrime V true_
Theorem: FOL.NV.is_tauto_prop_true
Proof state before:
⊢ ∀ (V : VarBoolAssignment), evalPrime V true_
Tactic:
simp only [Formula.evalPrime]
Proof state after:
⊢ VarBoolAssignment → True
Theorem: FOL.NV.is_tauto_prop_true
Proof state before:
⊢ VarBoolAssignment → True
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_prop_1
Proof state before:
P Q : Formula
⊢ (P.imp_ (Q.imp_ P)).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (P.imp_ (Q.imp_ P))
Theorem: FOL.NV.is_tauto_prop_1
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (P.imp_ (Q.imp_ P))
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_prop_2
Proof state before:
P Q R : Formula
⊢ ((P.imp_ (Q.imp_ R)).imp_ ((P.imp_ Q).imp_ (P.imp_ R))).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P Q R : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.imp_ (Q.imp_ R)).imp_ ((P.imp_ Q).imp_ (P.imp_ R)))
Theorem: FOL.NV.is_tauto_prop_2
Proof state before:
P Q R : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.imp_ (Q.imp_ R)).imp_ ((P.imp_ Q).imp_ (P.imp_ R)))
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_prop_3
Proof state before:
P Q : Formula
⊢ ((P.not_.imp_ Q.not_).imp_ (Q.imp_ P)).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.not_.imp_ Q.not_).imp_ (Q.imp_ P))
Theorem: FOL.NV.is_tauto_prop_3
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.not_.imp_ Q.not_).imp_ (Q.imp_ P))
Tactic:
simp only [eval_not, eval_imp]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), (¬evalPrime V P → ¬evalPrime V Q) → evalPrime V Q → evalPrime V P
Theorem: FOL.NV.is_tauto_prop_3
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), (¬evalPrime V P → ¬evalPrime V Q) → evalPrime V Q → evalPrime V P
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_mp
Proof state before:
P Q : Formula
h1 : (P.imp_ Q).IsTautoPrime
h2 : P.IsTautoPrime
⊢ Q.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime] at h1
Proof state after:
P Q : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V (P.imp_ Q)
h2 : P.IsTautoPrime
⊢ Q.IsTautoPrime
Theorem: FOL.NV.is_tauto_mp
Proof state before:
P Q : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V (P.imp_ Q)
h2 : P.IsTautoPrime
⊢ Q.IsTautoPrime
Tactic:
simp only [eval_imp] at h1
Proof state after:
P Q : Formula
h2 : P.IsTautoPrime
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
Theorem: FOL.NV.is_tauto_mp
Proof state before:
P Q : Formula
h2 : P.IsTautoPrime
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime] at h2
Proof state after:
P Q : Formula
h2 : ∀ (V : VarBoolAssignment), evalPrime V P
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
Theorem: FOL.NV.is_tauto_mp
Proof state before:
P Q : Formula
h2 : ∀ (V : VarBoolAssignment), evalPrime V P
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_def_false
Proof state before:
⊢ (false_.iff_ true_.not_).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
⊢ ∀ (V : VarBoolAssignment), evalPrime V (false_.iff_ true_.not_)
Theorem: FOL.NV.is_tauto_def_false
Proof state before:
⊢ ∀ (V : VarBoolAssignment), evalPrime V (false_.iff_ true_.not_)
Tactic:
simp only [eval_not, eval_iff]
Proof state after:
⊢ ∀ (V : VarBoolAssignment), evalPrime V false_ ↔ ¬evalPrime V true_
Theorem: FOL.NV.is_tauto_def_false
Proof state before:
⊢ ∀ (V : VarBoolAssignment), evalPrime V false_ ↔ ¬evalPrime V true_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_def_and
Proof state before:
P Q : Formula
⊢ ((P.and_ Q).iff_ (P.imp_ Q.not_).not_).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.and_ Q).iff_ (P.imp_ Q.not_).not_)
Theorem: FOL.NV.is_tauto_def_and
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.and_ Q).iff_ (P.imp_ Q.not_).not_)
Tactic:
simp only [eval_and, eval_not, eval_imp, eval_iff]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∧ evalPrime V Q ↔ ¬(evalPrime V P → ¬evalPrime V Q)
Theorem: FOL.NV.is_tauto_def_and
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∧ evalPrime V Q ↔ ¬(evalPrime V P → ¬evalPrime V Q)
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_def_or
Proof state before:
P Q : Formula
⊢ ((P.or_ Q).iff_ (P.not_.imp_ Q)).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.or_ Q).iff_ (P.not_.imp_ Q))
Theorem: FOL.NV.is_tauto_def_or
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.or_ Q).iff_ (P.not_.imp_ Q))
Tactic:
simp only [eval_or, eval_not, eval_imp, eval_iff]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∨ evalPrime V Q ↔ ¬evalPrime V P → evalPrime V Q
Theorem: FOL.NV.is_tauto_def_or
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∨ evalPrime V Q ↔ ¬evalPrime V P → evalPrime V Q
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.is_tauto_def_iff
Proof state before:
P Q : Formula
⊢ (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
        (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    evalPrime V
      (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_
Theorem: FOL.NV.is_tauto_def_iff
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    evalPrime V
      (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_
Tactic:
simp only [eval_iff, eval_not, eval_imp]
Proof state after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    ¬(((evalPrime V P ↔ evalPrime V Q) → ¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P))) →
        ¬(¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P)) → (evalPrime V P ↔ evalPrime V Q)))
Theorem: FOL.NV.is_tauto_def_iff
Proof state before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    ¬(((evalPrime V P ↔ evalPrime V Q) → ¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P))) →
        ¬(¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P)) → (evalPrime V P ↔ evalPrime V Q)))
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F F' : Formula
h1 : F' ∈ F.primeSet
⊢ F'.IsPrime
Tactic:
induction F
Proof state after:
case pred_const_
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_const_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case pred_var_
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_var_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case eq_
F' : Formula
a✝¹ a✝ : VarName
h1 : F' ∈ (eq_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case true_
F' : Formula
h1 : F' ∈ true_.primeSet
⊢ F'.IsPrime

case false_
F' : Formula
h1 : F' ∈ false_.primeSet
⊢ F'.IsPrime

case not_
F' a✝ : Formula
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ a✝.not_.primeSet
⊢ F'.IsPrime

case imp_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.imp_ a✝).primeSet
⊢ F'.IsPrime

case and_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.and_ a✝).primeSet
⊢ F'.IsPrime

case or_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.or_ a✝).primeSet
⊢ F'.IsPrime

case iff_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.iff_ a✝).primeSet
⊢ F'.IsPrime

case forall_
F' : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (forall_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case exists_
F' : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case def_
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_var_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
case pred_const_ | pred_var_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
h1 : F' ∈ false_.primeSet
⊢ F'.IsPrime
Tactic:
case true_ | false_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
x y : VarName
h1 : F' ∈ (eq_ x y).primeSet
⊢ F'.IsPrime
Tactic:
case eq_ x y =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.not_.primeSet
⊢ F'.IsPrime
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.primeSet] at h1
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ (phi.iff_ psi).primeSet
⊢ F'.IsPrime
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp only [Formula.primeSet] at h1
  simp at h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝ x).primeSet
⊢ F'.IsPrime
Tactic:
case forall_ x phi | exists_ x phi =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
case def_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_var_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ {pred_var_ a✝¹ a✝}
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ {pred_var_ a✝¹ a✝}
⊢ F'.IsPrime
Tactic:
simp at h1
Proof state after:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' = pred_var_ a✝¹ a✝
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' = pred_var_ a✝¹ a✝
⊢ F'.IsPrime
Tactic:
subst h1
Proof state after:
a✝¹ : PredName
a✝ : List VarName
⊢ (pred_var_ a✝¹ a✝).IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
a✝¹ : PredName
a✝ : List VarName
⊢ (pred_var_ a✝¹ a✝).IsPrime
Tactic:
simp only [Formula.IsPrime]
Proof state after:
no goals