internlm/Lean-Github huggingface dataset:
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
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
Tactic:
simp only [phi_ih]
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 ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      E phi ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) 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
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 ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      E phi ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
apply Holds_coincide_Var
Proof state after:
case h.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),
    isFreeIn v phi →
      (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 ∘
            Function.updateITE σ x
              (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
              else x))
          v =
        Function.updateITE (V ∘ σ) x d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h.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),
    isFreeIn v phi →
      (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 ∘
            Function.updateITE σ x
              (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
              else x))
          v =
        Function.updateITE (V ∘ σ) x d v
Tactic:
intro v a1
Proof state after:
case h.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
⊢ (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 ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      v =
    Function.updateITE (V ∘ σ) x d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h.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
⊢ (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 ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      v =
    Function.updateITE (V ∘ σ) x d v
Tactic:
simp
Proof state after:
case h.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
⊢ 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
      (Function.updateITE σ x
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        v) =
    Function.updateITE (V ∘ σ) x d v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h.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
⊢ 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
      (Function.updateITE σ x
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        v) =
    Function.updateITE (V ∘ σ) x d v
Tactic:
split_ifs
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
h✝ : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) 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
h✝ : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = 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:
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)) ↔
    ∀ (d : D), Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
apply forall_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:
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:
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:
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 (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v
Tactic:
obtain s0 := fresh_not_mem x c (freeVarSet (sub (Function.updateITE σ x x) c phi))
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 : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
s0 : fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v
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
s0 : fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v
Tactic:
generalize (fresh x c (freeVarSet (sub (Function.updateITE σ x x) c phi))) = x' at *
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 : 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
⊢ 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:
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
⊢ 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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [c2]
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' x) = Function.updateITE (V ∘ σ) x d x
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' x) = Function.updateITE (V ∘ σ) x d x
Tactic:
simp only [Function.updateITE]
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ (if (if True then x' else σ x) = x' then d else V (if True then x' else σ x)) = if True then d else (V ∘ σ) x
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ (if (if True then x' else σ x) = x' then d else V (if True then x' else σ x)) = if True then d else (V ∘ σ) x
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
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
by_cases c3 : σ 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
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

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
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
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:
subst c3
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
s0 : σ v ∉ (sub (Function.updateITE σ x x) c 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 ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [freeVarSet_sub_eq_freeVarSet_image] at s0
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
s0 : σ 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
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
have s1 : σ v ∈ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
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
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