internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet

case pos
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
apply Finset.mem_image_update
Proof state after:
case s1.h1
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ ¬v = x

case s1.h2
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ v ∈ phi.freeVarSet

case pos
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case pos
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.h1
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ ¬v = x
Tactic:
exact c2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.h2
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ v ∈ phi.freeVarSet
Tactic:
simp only [← isFreeIn_iff_mem_freeVarSet]
Proof state after:
case s1.h2
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ isFreeIn v phi
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.h2
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ isFreeIn v phi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [Function.updateITE]
Proof state after:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if (if v = x then x' else σ v) = x' then d else V (if v = x then x' else σ v)) = if v = x then d else (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if (if v = x then x' else σ v) = x' then d else V (if v = x then x' else σ v)) = if v = x then d else (V ∘ σ) v
Tactic:
simp only [if_neg c2]
Proof state after:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if σ v = x' then d else V (σ v)) = (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if σ v = x' then d else V (σ v)) = (V ∘ σ) v
Tactic:
simp only [if_neg c3]
Proof state after:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ V (σ v) = (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ V (σ v) = (V ∘ σ) v
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
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
by_cases c2 : v = x
Proof state after:
case pos
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v

case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case pos
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
subst c2
Proof state after:
case pos
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
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ Function.updateITE V v d (Function.updateITE σ v v v) = Function.updateITE (V ∘ σ) v d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case pos
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
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ Function.updateITE V v d (Function.updateITE σ v v v) = Function.updateITE (V ∘ σ) v d v
Tactic:
simp only [Function.updateITE]
Proof state after:
case pos
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
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ (if (if True then v else σ v) = v then d else V (if True then v else σ v)) = if True then d else (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case pos
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
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ (if (if True then v else σ v) = v then d else V (if True then v else σ v)) = if True then d else (V ∘ σ) v
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
have s1 : ¬ σ v = x
Proof state after:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ ¬σ v = x

case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [Function.updateITE]
Proof state after:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if (if v = x then x else σ v) = x then d else V (if v = x then x else σ v)) = if v = x then d else (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if (if v = x then x else σ v) = x then d else V (if v = x then x else σ v)) = if v = x then d else (V ∘ σ) v
Tactic:
simp only [if_neg c2]
Proof state after:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if σ v = x then d else V (σ v)) = (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if σ v = x then d else V (σ v)) = (V ∘ σ) v
Tactic:
simp only [if_neg s1]
Proof state after:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ V (σ v) = (V ∘ σ) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case neg
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ V (σ v) = (V ∘ σ) v
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ ¬σ v = x
Tactic:
intro contra
Proof state after:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ False
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ False
Tactic:
apply c1
Proof state after:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
Tactic:
apply Exists.intro v
Proof state after:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x} ∧ σ v = x
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x} ∧ σ v = x
Tactic:
constructor
Proof state after:
case s1.left
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x}

case s1.right
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ σ v = x
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.left
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x}
Tactic:
simp
Proof state after:
case s1.left
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet ∧ ¬v = x
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.left
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet ∧ ¬v = x
Tactic:
simp only [← isFreeIn_iff_mem_freeVarSet]
Proof state after:
case s1.left
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ isFreeIn v phi ∧ ¬v = x
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.left
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ isFreeIn v phi ∧ ¬v = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case s1.right
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
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ σ v = x
Tactic:
exact contra
Proof state after:
no goals