internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ v' ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
Proof state after:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
Proof state after:
no goals
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
simp at c1
Proof state after:
case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
cases c1
Proof state after:
case h1.h2.intro
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
left✝ : X = hd.name
right✝ : xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
case intro c1_left c1_right =>
  simp
  simp only [eq_comm]
  exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = xs.length
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = xs.length
Tactic:
simp only [eq_comm]
Proof state after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ xs.length = hd.args.length
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ xs.length = hd.args.length
Tactic:
exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ Holds D I (fun c => if c = u then a else V c) tl (def_ X xs) ↔
    Holds D I (fun c => if c = v then a else V c) tl (def_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
apply ih
Proof state after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isFreeIn v (def_ X xs)

case h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isBoundIn v (def_ X xs)
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isFreeIn v (def_ X xs)
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isBoundIn v (def_ X xs)
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_y (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi))
Tactic:
case rename_forall_ h1_phi h1_x h1_y h1_1 h1_2 | rename_exists_ h1_phi h1_x h1_y h1_1 h1_2 =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  exact replace_empty_Holds D I V E h1_x h1_y h1_phi d h1_1 h1_2
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
case compat_not_ h1_phi h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  exact h1_ih V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_psi)
Tactic:
case compat_forall_ h1_phi h1_psi h1_x _ h1_ih | compat_exists_ h1_phi h1_psi h1_x _ h1_ih =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  exact h1_ih (Function.updateITE V h1_x d)
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1 : Formula
V : VarAssignment D
⊢ Holds D I V E h1 ↔ Holds D I V E h1
Tactic:
case refl_ h1 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi
Tactic:
case symm_ h1_phi h1_phi' _ h1_ih =>
  symm
  exact h1_ih V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_y (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
exact replace_empty_Holds D I V E h1_x h1_y h1_phi d h1_1 h1_2
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I V E h1_phi ↔ ¬Holds D I V E h1_phi'
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I V E h1_phi ↔ ¬Holds D I V E h1_phi'
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E (h1_phi.iff_ h1_psi) ↔ Holds D I V E (h1_phi'.iff_ h1_psi')
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I V E h1_phi ↔ Holds D I V E h1_psi) ↔ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')