internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (def_ X xs) ↔ Holds D I V E (def_ X (List.map σ xs))
Tactic:
induction E
Proof state after:
case nil
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))

case cons
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I (V ∘ σ) tail✝ (def_ X xs) ↔ Holds D I V tail✝ (def_ X (List.map σ xs))
⊢ Holds D I (V ∘ σ) (head✝ :: tail✝) (def_ X xs) ↔ Holds D I V (head✝ :: tail✝) (def_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))
Tactic:
case nil =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs) ↔ Holds D I V (E_hd :: E_tl) (def_ X (List.map σ xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ 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)) ↔
    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))
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ 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)) ↔
    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))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ 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)) ↔
    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))
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ 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)) ↔
    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))
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ 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
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
case _ c1 =>
  apply E_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ 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:
cases c1
Proof state after:
case intro
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
left✝ : X = E_hd.name
right✝ : 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
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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.Inj.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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.Inj.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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:
simp only [isFreeIn_iff_mem_freeVarSet v E_hd.q] at a1
Proof state after:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ 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.Inj.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ 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_mem_eq_len
Proof state after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = (List.map (V ∘ σ) xs).length
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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.Inj.substitution_theorem
Proof state before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : 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.Inj.substitution_theorem
Proof state before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = (List.map (V ∘ σ) xs).length
Tactic:
simp
Proof state after:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = xs.length
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = xs.length
Tactic:
simp only [c1_right]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
apply E_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_is_valid
Proof state before:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : F.IsValid
⊢ (replaceAll σ F).IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (replaceAll σ F).IsValid
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_is_valid
Proof state before:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (replaceAll σ F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (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 (replaceAll σ F)
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_is_valid
Proof state before:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (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 (replaceAll σ F)
Tactic:
intro D I V E
Proof state after:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (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 (replaceAll σ F)
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_is_valid
Proof state before:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (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 (replaceAll σ F)
Tactic:
simp only [← substitution_theorem D I V E F σ h1]
Proof state after:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (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.Inj.substitution_is_valid
Proof state before:
F : Formula
σ : VarName → VarName
h1 : Function.Injective σ
h2 : ∀ (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 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
σ σ' : VarName → VarName
binders : Finset VarName
F : Formula
h1 : admitsAux σ binders F
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
⊢ Holds D I V E F ↔ Holds D I V' E (fastReplaceFree σ' F)
Tactic:
induction E generalizing F binders V V' σ σ'
Proof state after:
case nil
D : Type
I : Interpretation D
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
F : Formula
h1 : admitsAux σ binders F
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
⊢ Holds D I V [] F ↔ Holds D I V' [] (fastReplaceFree σ' F)

case cons
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
F : Formula
h1 : admitsAux σ binders F
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I V' (head✝ :: tail✝) (fastReplaceFree σ' F)
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName),
    admitsAux σ binders phi →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) →
            (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) (fastReplaceFree σ' phi))
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : admitsAux σ binders phi
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
⊢ ¬Holds D I V (head✝ :: tail✝) phi ↔ ¬Holds D I V' (head✝ :: tail✝) (fastReplaceFree σ' phi)
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V V' σ σ' binders h1 h2 h2' h3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : admitsAux σ binders (def_ a✝¹ a✝)
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (fastReplaceFree σ' (def_ a✝¹ a✝))
Tactic:
simp only [admitsAux] at h1
Proof state after:
case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ a✝, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (fastReplaceFree σ' (def_ a✝¹ a✝))