internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_17_7
Proof state before:
F : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ F
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
⊢ IsDeduct Δ (forall_ v F)
Tactic:
induction h1
Proof state after:
case axiom_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ (forall_ v phi✝)

case assume_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ : Formula
a✝ : phi✝ ∈ Δ
⊢ IsDeduct Δ (forall_ v phi✝)

case mp_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ phi✝
a_ih✝¹ : IsDeduct Δ (forall_ v (phi✝.imp_ psi✝))
a_ih✝ : IsDeduct Δ (forall_ v phi✝)
⊢ IsDeduct Δ (forall_ v psi✝)
Theorem: FOL.NV.T_17_7
Proof state before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
case axiom_ h1_phi h1_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.gen_
  exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_17_7
Proof state before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (forall_ v h1_phi)
Theorem: FOL.NV.T_17_7
Proof state before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (forall_ v h1_phi)
Tactic:
apply IsAxiom.gen_
Proof state after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v 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_17_7
Proof state before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
apply IsDeduct.mp_ h1_phi
Proof state after:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (forall_ v h1_phi))

case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi
Theorem: FOL.NV.T_17_7
Proof state before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (forall_ v h1_phi))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (forall_ v h1_phi))
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (forall_ v h1_phi))
Tactic:
apply IsAxiom.pred_3_
Proof state after:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ ¬isFreeIn v h1_phi
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ ¬isFreeIn v h1_phi
Tactic:
exact h2 h1_phi h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_17_7
Proof state before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.assume_
Proof state after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_17_7
Proof state before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v h1_psi)
Tactic:
apply IsDeduct.mp_ (forall_ v h1_phi)
Proof state after:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v h1_phi).imp_ (forall_ v h1_psi))

case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v h1_phi)
Theorem: FOL.NV.T_17_7
Proof state before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v h1_phi).imp_ (forall_ v h1_psi))
Tactic:
apply IsDeduct.mp_ (forall_ v (h1_phi.imp_ h1_psi))
Proof state after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))

case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsAxiom ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsAxiom ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))
Tactic:
apply IsAxiom.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.T_17_7
Proof state before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
Tactic:
exact h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.T_17_7
Proof state before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
exact h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.univIntro
Proof state before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v P)
Tactic:
rw [← fastReplaceFree_inverse P v t h1]
Proof state after:
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Theorem: FOL.NV.univIntro
Proof state before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Tactic:
apply IsDeduct.mp_ (forall_ t (fastReplaceFree v t P))
Proof state after:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))

case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P))
Theorem: FOL.NV.univIntro
Proof state before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))
Tactic:
apply proof_imp_deduct
Proof state after:
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsProof ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsProof ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))
Tactic:
apply deduction_theorem
Proof state after:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct (∅ ∪ {forall_ t (fastReplaceFree v t P)}) (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct (∅ ∪ {forall_ t (fastReplaceFree v t P)}) (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Tactic:
simp
Proof state after:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Tactic:
apply generalization
Proof state after:
case a.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (fastReplaceFree t v (fastReplaceFree v t P))

case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ∀ H ∈ {forall_ t (fastReplaceFree v t P)}, ¬isFreeIn v H
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (fastReplaceFree t v (fastReplaceFree v t P))
Tactic:
apply spec
Proof state after:
case a.h1.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ t (fastReplaceFree v t P))

case a.h1.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ fastAdmits t v (fastReplaceFree v t P)
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ t (fastReplaceFree v t P))
Tactic:
apply IsDeduct.assume_
Proof state after:
case a.h1.h1.h1.h1.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ forall_ t (fastReplaceFree v t P) ∈ {forall_ t (fastReplaceFree v t P)}
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h1.h1.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ forall_ t (fastReplaceFree v t P) ∈ {forall_ t (fastReplaceFree v t P)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ fastAdmits t v (fastReplaceFree v t P)
Tactic:
apply fastReplaceFree_fastAdmits
Proof state after:
case a.h1.h1.h1.h2.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬occursIn t P
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h1.h2.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬occursIn t P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ∀ H ∈ {forall_ t (fastReplaceFree v t P)}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn v (forall_ t (fastReplaceFree v t P))
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn v (forall_ t (fastReplaceFree v t P))
Tactic:
simp only [isFreeIn]
Proof state after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬(¬v = t ∧ isFreeIn v (fastReplaceFree v t P))
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬(¬v = t ∧ isFreeIn v (fastReplaceFree v t P))
Tactic:
simp
Proof state after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬v = t → ¬isFreeIn v (fastReplaceFree v t P)
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬v = t → ¬isFreeIn v (fastReplaceFree v t P)
Tactic:
intro a1 contra
Proof state after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
a1 : ¬v = t
contra : isFreeIn v (fastReplaceFree v t P)
⊢ False
Theorem: FOL.NV.univIntro
Proof state before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
a1 : ¬v = t
contra : isFreeIn v (fastReplaceFree v t P)
⊢ False
Tactic:
exact not_isFreeIn_fastReplaceFree P v t a1 contra
Proof state after:
no goals
Theorem: FOL.NV.univIntro
Proof state before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P))
Tactic:
exact generalization (fastReplaceFree v t P) t Δ h2 h3
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1 : IsProofAlt F
⊢ IsDeduct ∅ F
Tactic:
induction h1
Proof state after:
case prop_true_
F : Formula
⊢ IsDeduct ∅ true_

case prop_1_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2_
F phi✝ psi✝ chi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case pred_1_
F : Formula
v✝ : VarName
phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((forall_ v✝ (phi✝.imp_ psi✝)).imp_ ((forall_ v✝ phi✝).imp_ (forall_ v✝ psi✝)))

case pred_2_
F : Formula
v✝ t✝ : VarName
phi✝ phi'✝ : Formula
a✝¹ : fastAdmits v✝ t✝ phi✝
a✝ : fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ IsDeduct ∅ ((forall_ v✝ phi✝).imp_ phi'✝)

case pred_3_
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : ¬isFreeIn v✝ phi✝
⊢ IsDeduct ∅ (phi✝.imp_ (forall_ v✝ phi✝))

case eq_1_
F : Formula
v✝ : VarName
⊢ IsDeduct ∅ (forall_ v✝ (eq_ v✝ v✝))

case eq_2_pred_const_
F : Formula
name✝ : PredName
n✝ : ℕ
xs✝ ys✝ : Fin n✝ → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn xs✝)
      (Forall_ (List.ofFn ys✝)
        ((And_ (List.ofFn fun i => eq_ (xs✝ i) (ys✝ i))).imp_
          ((pred_const_ name✝ (List.ofFn xs✝)).iff_ (pred_const_ name✝ (List.ofFn ys✝))))))

case eq_2_eq_
F : Formula
x_0✝ x_1✝ y_0✝ y_1✝ : VarName
⊢ IsDeduct ∅
    (forall_ x_0✝
      (forall_ x_1✝
        (forall_ y_0✝
          (forall_ y_1✝ (((eq_ x_0✝ y_0✝).and_ (eq_ x_1✝ y_1✝)).imp_ ((eq_ x_0✝ x_1✝).iff_ (eq_ y_0✝ y_1✝)))))))

case gen_
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : IsProofAlt phi✝
a_ih✝ : IsDeduct ∅ phi✝
⊢ IsDeduct ∅ (forall_ v✝ phi✝)

case mp_
F phi✝ psi✝ : Formula
a✝¹ : IsProofAlt (phi✝.imp_ psi✝)
a✝ : IsProofAlt phi✝
a_ih✝¹ : IsDeduct ∅ (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct ∅ phi✝
⊢ IsDeduct ∅ psi✝

case def_false_
F : Formula
⊢ IsDeduct ∅ (false_.iff_ true_.not_)

case def_and_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
⊢ IsDeduct ∅ true_
Tactic:
case prop_true_ =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_true_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_1_ h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_1_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi h1_chi : Formula
⊢ IsDeduct ∅ ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
case prop_2_ h1_phi h1_psi h1_chi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_2_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_3_ h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Tactic:
case pred_1_ h1_v h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsDeduct ∅ ((forall_ h1_v h1_phi).imp_ h1_phi')
Tactic:
case pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1 =>
  apply IsDeduct.axiom_
  exact IsAxiom.pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsDeduct ∅ (h1_phi.imp_ (forall_ h1_v h1_phi))
Tactic:
case pred_3_ h1_v h1_phi h1_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.pred_3_
  exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1 : VarName
⊢ IsDeduct ∅ (forall_ h1 (eq_ h1 h1))
Tactic:
case eq_1_ h1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Tactic:
case eq_2_pred_const_ h1_name h1_n h1_xs h1_ys =>
  apply IsDeduct.axiom_
  apply IsAxiom.eq_2_pred_const_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsDeduct ∅
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Tactic:
case eq_2_eq_ h1_x_0 h1_y_0 h1_x_1 h1_y_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.eq_2_eq_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi : Formula
h1_1 : IsProofAlt (h1_phi.imp_ h1_psi)
h1_2 : IsProofAlt 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_1 h1_2 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.isProofAltImpIsDeduct
Proof state before:
case def_false_
F : Formula
⊢ IsDeduct ∅ (false_.iff_ true_.not_)

case def_and_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Tactic:
all_goals
  sorry
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
⊢ IsDeduct ∅ true_
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
⊢ IsAxiom true_
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
⊢ IsAxiom true_
Tactic:
apply IsAxiom.prop_true_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom (h1_phi.imp_ (h1_psi.imp_ h1_phi))