internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
⊢ ∀ (a : Formula), IsSub F v u a → Rec.fastAdmitsAux v u binders F
Tactic:
intro F' h1_1
Proof state after:
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
F' : Formula
h1_1 : IsSub F v u F'
⊢ Rec.fastAdmitsAux v u binders F
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
F' : Formula
h1_1 : IsSub F v u F'
⊢ Rec.fastAdmitsAux v u binders F
Tactic:
clear h1
Proof state after:
F : Formula
v u : VarName
binders : Finset VarName
h2 : u ∉ binders
F' : Formula
h1_1 : IsSub F v u F'
⊢ Rec.fastAdmitsAux v u binders F
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
case
    forall_free_in h1_1_x h1_1_phi h1_1_v h1_1_t _ _ h1_1_2 _ h1_1_ih
  | exists_free_in h1_1_x h1_1_phi h1_1_v h1_1_t _ _ h1_1_2 _ h1_1_ih =>
  right
  apply h1_1_ih
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case pred_const_
F : Formula
v u : VarName
F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders

case pred_var_
F : Formula
v u : VarName
F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders

case eq_
F : Formula
v u : VarName
F' : Formula
x✝ y✝ v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ = x✝ ∨ v✝ = y✝ → t✝ ∉ binders

case not_
F : Formula
v u : VarName
F' phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝

case imp_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case and_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case or_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case iff_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case def_
F : Formula
v u : VarName
F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case def_
F : Formula
v u : VarName
F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (def_ X✝ xs✝)
Tactic:
simp only [Rec.fastAdmitsAux]
Proof state after:
case def_
F : Formula
v u : VarName
F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_1 : ¬isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
simp only [isFreeIn] at h1_1_1
Proof state after:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_1 : ¬(¬h1_1_v = h1_1_x ∧ isFreeIn h1_1_v h1_1_phi)
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_1 : ¬(¬h1_1_v = h1_1_x ∧ isFreeIn h1_1_v h1_1_phi)
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
simp at h1_1_1
Proof state after:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
by_cases c1 : h1_1_v = h1_1_x
Proof state after:
case pos
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : h1_1_v = h1_1_x
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi

case neg
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case pos
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : h1_1_v = h1_1_x
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
left
Proof state after:
case pos.h
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : h1_1_v = h1_1_x
⊢ h1_1_v = h1_1_x
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case pos.h
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : h1_1_v = h1_1_x
⊢ h1_1_v = h1_1_x
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case neg
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
right
Proof state after:
case neg.h
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case neg.h
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
apply Rec.not_isFreeIn_imp_fastAdmitsAux
Proof state after:
case neg.h.h1
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ ¬isFreeIn h1_1_v h1_1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case neg.h.h1
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ ¬isFreeIn h1_1_v h1_1_phi
Tactic:
exact h1_1_1 c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
right
Proof state after:
case h
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case h
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
Tactic:
apply h1_1_ih
Proof state after:
case h.h2
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_t ∉ binders ∪ {h1_1_x}
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case h.h2
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_t ∉ binders ∪ {h1_1_x}
Tactic:
simp
Proof state after:
case h.h2
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_t ∉ binders ∧ ¬h1_1_t = h1_1_x
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case h.h2
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_t ∉ binders ∧ ¬h1_1_t = h1_1_x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case def_
F : Formula
v u : VarName
F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).not_ = h1_phi'.not_
Tactic:
case not_ h1_phi h1_v h1_t h1_phi' h1_1 h1_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
h1_1 : IsSub h1_phi h1_v h1_t h1_phi'
h1_2 : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_ih_2 : Rec.fastReplaceFree h1_v h1_t h1_psi = h1_psi'
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) = h1_phi'.iff_ h1_psi'
Tactic:
case
  imp_ h1_phi h1_psi h1_v h1_t h1_phi' h1_psi' h1_1 h1_2 h1_ih_1 h1_ih_2
| and_ h1_phi h1_psi h1_v h1_t h1_phi' h1_psi' h1_1 h1_2 h1_ih_1 h1_ih_2
| or_ h1_phi h1_psi h1_v h1_t h1_phi' h1_psi' h1_1 h1_2 h1_ih_1 h1_ih_2
| iff_ h1_phi h1_psi h1_v h1_t h1_phi' h1_psi' h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  subst h1_ih_1
  subst h1_ih_2
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
Tactic:
case
  forall_not_free_in h1_x h1_phi h1_v h1_t h1_1
| exists_not_free_in h1_x h1_phi h1_v h1_t h1_1 =>
  simp only [isFreeIn] at h1_1
  simp at h1_1
  split_ifs
  case pos c1 =>
    rfl
  case neg c1 =>
    congr!
    apply Rec.not_free_in_fastReplaceFree_self
    exact h1_1 c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Tactic:
case
  forall_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 _ _ h1_ih
| exists_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 _ _ h1_ih =>
  simp only [isFreeIn] at h1_1
  cases h1_1
  case intro h1_1_left h1_1_right =>
    simp only [if_neg h1_1_left]
    subst h1_ih
    rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
case def_
F F' : Formula
v u : VarName
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ (def_ X✝ xs✝) = def_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝)
Tactic:
simp only [Rec.fastReplaceFree]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).not_ = h1_phi'.not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
h1_1 : IsSub h1_phi h1_v h1_t h1_phi'
h1_2 : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_ih_2 : Rec.fastReplaceFree h1_v h1_t h1_psi = h1_psi'
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) = h1_phi'.iff_ h1_psi'
Tactic:
subst h1_ih_1
Proof state after:
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_psi' : Formula
h1_2 : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_2 : Rec.fastReplaceFree h1_v h1_t h1_psi = h1_psi'
h1_1 : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) =
    (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ h1_psi'
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_psi' : Formula
h1_2 : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_2 : Rec.fastReplaceFree h1_v h1_t h1_psi = h1_psi'
h1_1 : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) =
    (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ h1_psi'
Tactic:
subst h1_ih_2
Proof state after:
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_1 : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
h1_2 : IsSub h1_psi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_psi)
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) =
    (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi)
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_1 : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
h1_2 : IsSub h1_psi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_psi)
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) =
    (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi)
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
Tactic:
simp only [isFreeIn] at h1_1
Proof state after:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
Tactic:
simp at h1_1
Proof state after:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
Tactic:
split_ifs
Proof state after:
case pos
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
h✝ : h1_v = h1_x
⊢ exists_ h1_x h1_phi = exists_ h1_x h1_phi

case neg
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
h✝ : ¬h1_v = h1_x
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : h1_v = h1_x
⊢ exists_ h1_x h1_phi = exists_ h1_x h1_phi
Tactic:
case pos c1 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : ¬h1_v = h1_x
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x h1_phi
Tactic:
case neg c1 =>
  congr!
  apply Rec.not_free_in_fastReplaceFree_self
  exact h1_1 c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : h1_v = h1_x
⊢ exists_ h1_x h1_phi = exists_ h1_x h1_phi
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : ¬h1_v = h1_x
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x h1_phi
Tactic:
congr!
Proof state after:
case h.e'_2
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : ¬h1_v = h1_x
⊢ Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
case h.e'_2
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : ¬h1_v = h1_x
⊢ Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi
Tactic:
apply Rec.not_free_in_fastReplaceFree_self
Proof state after:
case h.e'_2.h1
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : ¬h1_v = h1_x
⊢ ¬isFreeIn h1_v h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
case h.e'_2.h1
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
c1 : ¬h1_v = h1_x
⊢ ¬isFreeIn h1_v h1_phi
Tactic:
exact h1_1 c1
Proof state after:
no goals