internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp only [Finset.mem_image]
Proof state after:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ¬∃ a ∈ phi.freeVarSet \ {x}, Function.updateITE σ x x a = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ¬∃ a ∈ phi.freeVarSet \ {x}, Function.updateITE σ x x a = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp
Proof state after:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬Function.updateITE σ x x x_1 = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬Function.updateITE σ x x x_1 = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp only [Function.updateITE]
Proof state after:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬(if x_1 = x then x else σ x_1) = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬(if x_1 = x then x else σ x_1) = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp
Proof state after:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬x_1 = x ∧ ¬σ x_1 = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬x_1 = x ∧ ¬σ x_1 = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
tauto
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp only [Finset.sdiff_singleton_eq_self s2]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (eq_ x y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y =>
  simp only [sub]
  simp only [Holds]
  simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c false_) ↔ Holds D I (V ∘ σ) E false_
Tactic:
case true_ | false_ =>
  simp only [sub]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi.not_) ↔ Holds D I (V ∘ σ) E phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [sub]
  simp only [Holds]
  congr! 1
  exact phi_ih V σ
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (eq_ x y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (eq_ (σ x) (σ y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (eq_ (σ x) (σ y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ V (σ x) = V (σ y) ↔ (V ∘ σ) x = (V ∘ σ) y
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ V (σ x) = V (σ y) ↔ (V ∘ σ) x = (V ∘ σ) y
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c false_) ↔ Holds D I (V ∘ σ) E false_
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E false_ ↔ Holds D I (V ∘ σ) E false_
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E false_ ↔ Holds D I (V ∘ σ) E false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi.not_) ↔ Holds D I (V ∘ σ) E phi.not_
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi).not_ ↔ Holds D I (V ∘ σ) E phi.not_
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi).not_ ↔ Holds D I (V ∘ σ) E phi.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ¬Holds D I V E (sub σ c phi) ↔ ¬Holds D I (V ∘ σ) E phi
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ¬Holds D I V E (sub σ c phi) ↔ ¬Holds D I (V ∘ σ) E phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
Tactic:
exact phi_ih V σ
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (phi.iff_ psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E ((sub σ c phi).iff_ (sub σ c psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E ((sub σ c phi).iff_ (sub σ c psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ (Holds D I V E (sub σ c phi) ↔ Holds D I V E (sub σ c psi)) ↔ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ (Holds D I V E (sub σ c phi) ↔ Holds D I V E (sub σ c psi)) ↔ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
Tactic:
exact phi_ih V σ
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
Tactic:
exact psi_ih V σ
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (exists_ x phi)) ↔ Holds D I (V ∘ σ) E (exists_ x phi)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E
      (exists_
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    Holds D I (V ∘ σ) E (exists_ x phi)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E
      (exists_
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    Holds D I (V ∘ σ) E (exists_ x phi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ (∃ d,
      Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    ∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ (∃ d,
      Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    ∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ∀ (a : D),
    Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          a)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi) ↔
      Holds D I (Function.updateITE (V ∘ σ) x a) E phi
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ∀ (a : D),
    Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          a)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi) ↔
      Holds D I (Function.updateITE (V ∘ σ) x a) E phi
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ Holds D I
      (Function.updateITE V
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        d)
      E
      (sub
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
        c phi) ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi