internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) E (def_ X xs)
Tactic:
induction E
Proof state after:
case nil
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)

case cons
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I V tail✝ (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) tail✝ (def_ X xs)
⊢ Holds D I V (head✝ :: tail✝) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (head✝ :: tail✝) (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Tactic:
case nil =>
  simp only [sub]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [sub] at E_ih
Proof state after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q

case neg
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
case neg c1 =>
  exact E_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Tactic:
apply Holds_coincide_Var
Proof state after:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v E_hd.q →
      Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
        Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v E_hd.q →
      Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
        Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
intro v a1
Proof state after:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
apply Function.updateListITE_map_mem_ext
Proof state after:
case h1.h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ ∀ y ∈ xs, (V ∘ σ) y = (V ∘ σ) y

case h1.h2
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ E_hd.args.length = xs.length

case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ v ∈ E_hd.args
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1.h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ ∀ y ∈ xs, (V ∘ σ) y = (V ∘ σ) y
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1.h2
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ E_hd.args.length = xs.length
Tactic:
cases c1
Proof state after:
case h1.h2.intro
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
case _ c1_left c1_right =>
  symm
  exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
symm
Proof state after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ xs.length = E_hd.args.length
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ xs.length = E_hd.args.length
Tactic:
exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ v ∈ E_hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args
Tactic:
simp only [← List.mem_toFinset]
Proof state after:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args.toFinset
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args.toFinset
Tactic:
apply Finset.mem_of_subset E_hd.h1 a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
exact E_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_is_valid
Proof state before:
σ : VarName → VarName
c : Char
F : Formula
h1 : F.IsValid
⊢ (sub σ c F).IsValid
Tactic:
simp only [IsValid] at h1
Proof state after:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (sub σ c F).IsValid
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_is_valid
Proof state before:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (sub σ c F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (sub σ c F)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_is_valid
Proof state before:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (sub σ c F)
Tactic:
intro D I V E
Proof state after:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (sub σ c F)
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_is_valid
Proof state before:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (sub σ c F)
Tactic:
simp only [substitution_theorem]
Proof state after:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (V ∘ σ) E F
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_is_valid
Proof state before:
σ : VarName → VarName
c : Char
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (V ∘ σ) E F
Tactic:
apply h1
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
F : Formula
⊢ occursIn v F ↔ v ∈ F.varSet
Tactic:
induction F
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ occursIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).varSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ occursIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).varSet

case eq_
v a✝¹ a✝ : VarName
⊢ occursIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).varSet

case true_
v : VarName
⊢ occursIn v true_ ↔ v ∈ true_.varSet

case false_
v : VarName
⊢ occursIn v false_ ↔ v ∈ false_.varSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v a✝.not_ ↔ v ∈ a✝.not_.varSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ↔ v ∈ a✝¹.varSet
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).varSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ↔ v ∈ a✝¹.varSet
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).varSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ↔ v ∈ a✝¹.varSet
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).varSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ↔ v ∈ a✝¹.varSet
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).varSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).varSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).varSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ occursIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).varSet
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
X : DefName
xs : List VarName
⊢ v ∈ xs ↔ v ∈ xs.toFinset
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v x y : VarName
⊢ v = x ∨ v = y ↔ v ∈ {x, y}
Tactic:
case eq_ x y =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
case true_ | false_ =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ v = x ∨ occursIn v phi ↔ v ∈ phi.varSet ∪ {x}
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ occursIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).varSet
Tactic:
simp only [occursIn]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).varSet
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).varSet
Tactic:
simp only [Formula.varSet]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
X : DefName
xs : List VarName
⊢ v ∈ xs ↔ v ∈ xs.toFinset
Tactic:
simp
Proof state after:
no goals