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 : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
Tactic:
clear s1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
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 : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
Tactic:
apply Holds_coincide_Var
Proof state after:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
⊢ ∀ (v : VarName),
    isFreeIn v H →
      Function.updateListITE V'' zs (List.map V' xs) v = Function.updateListITE V zs (List.map (V ∘ σ) xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
⊢ ∀ (v : VarName),
    isFreeIn v H →
      Function.updateListITE V'' zs (List.map V' xs) v = Function.updateListITE V zs (List.map (V ∘ σ) xs) v
Tactic:
intro x a1
Proof state after:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
⊢ Function.updateListITE V'' zs (List.map V' xs) x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
⊢ Function.updateListITE V'' zs (List.map V' xs) x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Tactic:
by_cases c3 : x ∈ zs
Proof state after:
case pos
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ Function.updateListITE V'' zs (List.map V' xs) x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ Function.updateListITE V'' zs (List.map V' xs) x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ Function.updateListITE V'' zs (List.map V' xs) x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Tactic:
apply Function.updateListITE_map_mem_ext
Proof state after:
case pos.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ ∀ y ∈ xs, V' y = (V ∘ σ) y

case pos.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ zs.length = xs.length

case pos.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ x ∈ zs
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case pos.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ ∀ y ∈ xs, V' y = (V ∘ σ) y
Tactic:
simp
Proof state after:
case pos.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ ∀ y ∈ xs, V' y = V (σ y)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case pos.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ ∀ y ∈ xs, V' y = V (σ y)
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case pos.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ zs.length = xs.length
Tactic:
simp only [← c2]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case pos.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∈ zs
⊢ x ∈ zs
Tactic:
exact c3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ Function.updateListITE V'' zs (List.map V' xs) x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Tactic:
simp only [Function.updateListITE_not_mem V'' x zs (List.map V' xs) c3]
Proof state after:
case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ V'' x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ V'' x = Function.updateListITE V zs (List.map (V ∘ σ) xs) x
Tactic:
simp only [Function.updateListITE_not_mem V x zs (List.map (V ∘ σ ) xs) c3]
Proof state after:
case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ V'' x = V x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ V'' x = V x
Tactic:
apply h2
Proof state after:
case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ x ∈ H.freeVarSet

case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ x ∉ zs
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ x ∈ H.freeVarSet
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
c3 : x ∉ zs
a1 : x ∈ H.freeVarSet
⊢ x ∈ H.freeVarSet
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
c3 : x ∉ zs
a1 : x ∈ H.freeVarSet
⊢ x ∈ H.freeVarSet
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ x ∉ zs
Tactic:
exact c3
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 : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
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 : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map (V ∘ σ) xs)
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 : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map (V ∘ σ) xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ List.map V' xs = List.map (V ∘ σ) xs
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ List.map V' xs = List.map (V ∘ σ) xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x
Tactic:
intro x a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
x : VarName
a1 : x ∈ xs
⊢ V' x = (V ∘ σ) x