internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ ∃ a, (a ∈ phi.predVarSet ∨ a ∈ psi.predVarSet) ∧ x ∈ predVarFreeVarSet τ a
Tactic:
apply Exists.intro a
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ (a ∈ phi.predVarSet ∨ a ∈ psi.predVarSet) ∧ x ∈ predVarFreeVarSet τ a
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ (a ∈ phi.predVarSet ∨ a ∈ psi.predVarSet) ∧ x ∈ predVarFreeVarSet τ a
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), isFreeIn x_1 (exists_ x phi) → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (exists_ x phi).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (exists_ x phi) ↔ Holds D I V E (subAux c τ σ (exists_ x phi))
Tactic:
simp only [isFreeIn] at h1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (exists_ x phi).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (exists_ x phi) ↔ Holds D I V E (subAux c τ σ (exists_ x phi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (exists_ x phi).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (exists_ x phi) ↔ Holds D I V E (subAux c τ σ (exists_ x phi))
Tactic:
simp only [predVarSet] at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (exists_ x phi) ↔ Holds D I V E (subAux c τ σ (exists_ x phi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (exists_ x phi) ↔ Holds D I V E (subAux c τ σ (exists_ x phi))
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (exists_ x phi) ↔
    Holds D I V E
      (exists_
        (if
            x ∈
              Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ) then
          fresh x c
            (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
        else x)
        (subAux c τ
          (Function.updateITE σ x
            (if
                x ∈
                  Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪
                    phi.predVarSet.biUnion (predVarFreeVarSet τ) then
              fresh x c
                (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
            else x))
          phi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
⊢ ∀ (x_1 : VarName),
    isFreeIn x_1 phi →
      Function.updateITE V' x d x_1 =
        Function.updateITE V
          (if
              x ∈
                Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪
                  phi.predVarSet.biUnion (predVarFreeVarSet τ) then
            fresh x c
              (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
          else x)
          d
          (Function.updateITE σ x
            (if
                x ∈
                  Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪
                    phi.predVarSet.biUnion (predVarFreeVarSet τ) then
              fresh x c
                (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
            else x)
            x_1)
Tactic:
intro v a1
Proof state after:
case h.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V' x d v =
    Function.updateITE V
      (if x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ) then
        fresh x c
          (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
      else x)
      d
      (Function.updateITE σ x
        (if
            x ∈
              Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ) then
          fresh x c
            (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
        else x)
        v)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ Function.updateITE V' x d v =
    Function.updateITE V
      (fresh x c
        (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
      d
      (Function.updateITE σ x
        (fresh x c
          (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
        v)
Tactic:
case _ c1 =>
  simp only [Function.updateITE]
  split_ifs
  case _ c2 c3 =>
    rfl
  case _ c2 c3 =>
    contradiction
  case _ c2 c3 =>
    obtain s1 := fresh_not_mem x c ((Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ∪ (Finset.biUnion (predVarSet phi) (predVarFreeVarSet τ)))
    simp only [← c3] at s1
    simp only [Finset.mem_union] at s1
    simp only [isFreeIn_iff_mem_freeVarSet] at a1
    obtain s2 := Finset.mem_image_of_mem (Function.updateITE σ x x) a1
    simp only [Function.updateITE] at s2
    simp only [if_neg c2] at s2
    exfalso
    apply s1
    left
    exact s2
  case _ c2 c3 =>
    apply h1
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ Function.updateITE V' x d v =
    Function.updateITE V
      (fresh x c
        (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
      d
      (Function.updateITE σ x
        (fresh x c
          (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
        v)
Tactic:
simp only [Function.updateITE]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ (if v = x then d else V' v) =
    if
        (if v = x then
            fresh x c
              (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
          else σ v) =
          fresh x c
            (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)) then
      d
    else
      V
        (if v = x then
          fresh x c
            (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
        else σ v)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c2 : v = x
c3 :
  fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)) =
    fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ d = d
Tactic:
case _ c2 c3 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c2 : v = x
c3 :
  ¬fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)) =
      fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ d =
    V
      (fresh x c
        (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
Tactic:
case _ c2 c3 =>
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c2 : ¬v = x
c3 :
  σ v =
    fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ V' v = d
Tactic:
case _ c2 c3 =>
  obtain s1 := fresh_not_mem x c ((Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ∪ (Finset.biUnion (predVarSet phi) (predVarFreeVarSet τ)))
  simp only [← c3] at s1
  simp only [Finset.mem_union] at s1
  simp only [isFreeIn_iff_mem_freeVarSet] at a1
  obtain s2 := Finset.mem_image_of_mem (Function.updateITE σ x x) a1
  simp only [Function.updateITE] at s2
  simp only [if_neg c2] at s2
  exfalso
  apply s1
  left
  exact s2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c2 : ¬v = x
c3 :
  ¬σ v =
      fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ V' v = V (σ v)
Tactic:
case _ c2 c3 =>
  apply h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c2 : v = x
c3 :
  fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)) =
    fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ d = d
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c2 : v = x
c3 :
  ¬fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)) =
      fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ d =
    V
      (fresh x c
        (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
Tactic:
contradiction
Proof state after:
no goals