internlm/Lean-Github huggingface dataset:
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
⊢ V' v = d
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
⊢ V' v = d
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
⊢ V' v = d
Tactic:
obtain s2 := Finset.mem_image_of_mem (Function.updateITE σ (σ v) (σ v)) a1
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : Function.updateITE σ (σ v) (σ v) v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ V' v = d
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : Function.updateITE σ (σ v) (σ v) v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ V' v = d
Tactic:
simp only [Function.updateITE] at s2
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : (if v = σ v then σ v else σ v) ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ V' v = d
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : (if v = σ v then σ v else σ v) ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ V' v = d
Tactic:
simp only [ite_self] at s2
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ V' v = d
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ V' v = d
Tactic:
exfalso
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ False
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ False
Tactic:
apply c1
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
    σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
    σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
Tactic:
left
Proof state after:
case h
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h
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
c2 : ¬v = x
c3 : σ v = x
s1 :
  (Var.All.Rec.Fresh.sub (Function.updateITE σ x x) c phi).freeVarSet =
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1 :
  ¬(σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet ∨
      σ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ))
a1 : v ∈ phi.freeVarSet
s2 : σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ (σ v) (σ v)) phi.freeVarSet
Tactic:
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 = x
⊢ V' v = V (σ v)
Tactic:
apply h1
Proof state after:
case a
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 = x
⊢ ¬v = x ∧ isFreeIn v phi
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a
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 = x
⊢ ¬v = x ∧ isFreeIn v phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h.h2
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 ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ),
    V'' 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 x_1
Tactic:
intro v a1
Proof state after:
case h.h2
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 : v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ V'' 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 v