internlm/Lean-Github huggingface dataset:
Theorem: Function.updateListITE_map_updateIte
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
⊢ f y = updateITE f v a y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Tactic:
simp only [Function.updateITE]
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
⊢ f y = if y = v then a else f y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Theorem: Function.updateListITE_map_updateIte
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
⊢ f y = if y = v then a else f y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
h✝ : y = v
⊢ f y = a

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
h✝ : ¬y = v
⊢ f y = f y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c1 : y = v
⊢ f y = a
Tactic:
case _ c1 =>
  specialize h1 y a1
  contradiction
Proof state after:
no goals
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c2 : ¬y = v
⊢ f y = f y
Tactic:
case _ c2 =>
  rfl
Proof state after:
no goals
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Tactic:
exact Function.updateListITE_map_mem_ext xs ys f g f (Function.updateITE f v a) x s1 h2 h3
Proof state after:
no goals
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c1 : y = v
⊢ f y = a
Tactic:
specialize h1 y a1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c1 : y = v
h1 : ¬y = v
⊢ f y = a
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c1 : y = v
h1 : ¬y = v
⊢ f y = a
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c2 : ¬y = v
⊢ f y = f y
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H F : Formula
h1 : F.predVarSet = ∅
⊢ replace P zs H F = F
Tactic:
induction F
Proof state after:
case pred_const_
P : PredName
zs : List VarName
H : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
P : PredName
zs : List VarName
H : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
P : PredName
zs : List VarName
H : Formula
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
P : PredName
zs : List VarName
H : Formula
h1 : true_.predVarSet = ∅
⊢ replace P zs H true_ = true_

case false_
P : PredName
zs : List VarName
H : Formula
h1 : false_.predVarSet = ∅
⊢ replace P zs H false_ = false_

case not_
P : PredName
zs : List VarName
H a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : a✝.not_.predVarSet = ∅
⊢ replace P zs H a✝.not_ = a✝.not_

case imp_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.imp_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.and_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.or_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.iff_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
P : PredName
zs : List VarName
H : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (forall_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
P : PredName
zs : List VarName
H : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (exists_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
P : PredName
zs : List VarName
H : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (def_ a✝¹ a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_const_ X xs) = pred_const_ X xs
Tactic:
case pred_const_ X xs =>
  simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Tactic:
case pred_var_ X xs =>
  simp only [predVarSet] at h1
  simp at h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ replace P zs H (eq_ x y) = eq_ x y
Tactic:
case eq_ x y =>
  simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
h1 : false_.predVarSet = ∅
⊢ replace P zs H false_ = false_
Tactic:
case true_ | false_ =>
  simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [replace]
  congr!
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [replace]
  congr!
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ replace P zs H (def_ X xs) = def_ X xs
Tactic:
case def_ X xs =>
  simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_const_ X xs) = pred_const_ X xs
Tactic:
simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp only [predVarSet] at h1
Proof state after:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp at h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ replace P zs H (eq_ x y) = eq_ x y
Tactic:
simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
h1 : false_.predVarSet = ∅
⊢ replace P zs H false_ = false_
Tactic:
simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Tactic:
simp only [predVarSet] at h1
Proof state after:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Tactic:
simp only [replace]
Proof state after:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ (replace P zs H phi).not_ = phi.not_
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ (replace P zs H phi).not_ = phi.not_
Tactic:
congr!
Proof state after:
case h.e'_1
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
case h.e'_1
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : (phi.iff_ psi).predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [predVarSet] at h1
Proof state after:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [Finset.union_eq_empty] at h1
Proof state after:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
cases h1
Proof state after:
case intro
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
left✝ : phi.predVarSet = ∅
right✝ : psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [replace]
Proof state after:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (replace P zs H phi).iff_ (replace P zs H psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (replace P zs H phi).iff_ (replace P zs H psi) = phi.iff_ psi
Tactic:
congr!
Proof state after:
case h.e'_1
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H phi = phi

case h.e'_2
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H psi = psi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
case h.e'_1
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H phi = phi
Tactic:
exact phi_ih h1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
case h.e'_2
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H psi = psi
Tactic:
exact psi_ih h1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Tactic:
simp only [predVarSet] at h1
Proof state after:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Tactic:
simp only [replace]
Proof state after:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (replace P zs H phi) = exists_ x phi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (replace P zs H phi) = exists_ x phi
Tactic:
congr!
Proof state after:
case h.e'_2
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
case h.e'_2
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar
Proof state before:
P : PredName
zs : List VarName
H : Formula
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ replace P zs H (def_ X xs) = def_ X xs
Tactic:
simp only [replace]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E P zs H) V E F ↔ Holds D I V E (replace P zs H F)
Tactic:
set E_ref := E
Proof state after:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := E
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := E
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
Tactic:
induction E generalizing F binders V
Proof state after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
V : VarAssignment D
F : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := []
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
V : VarAssignment D
F : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := head✝ :: tail✝
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (replace P zs H (def_ X xs))
Tactic:
case nil.def_ X xs =>
  simp only [replace]
  simp only [E_ref]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [replace]
  simp only [Holds]
  simp only [I']
  simp only [Interpretation.usingPred]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (replace P zs H (eq_ x y))
Tactic:
case eq_ x y =>
  simp only [replace]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref (replace P zs H false_)
Tactic:
case true_ | false_ =>
  simp only [replace]
  simp only [Holds]
Proof state after:
no goals