internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
simp at a1
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
obtain s1 := Sub.Pred.All.Rec.Option.Fresh.substitution_theorem D I V E freshChar τ
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
simp only [← s1] at a1
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
simp only [← s1]
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E phi
Tactic:
apply ih_2
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ ∀ H ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E H
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ ∀ H ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E H
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.not_IsDeduct_false
Proof state before:
⊢ ¬IsDeduct [] false_
Tactic:
intro contra
Proof state after:
contra : IsDeduct [] false_
⊢ False
Theorem: FOL.NV.Program.Backend.not_IsDeduct_false
Proof state before:
contra : IsDeduct [] false_
⊢ False
Tactic:
obtain s1 := soundness [] false_ contra Unit default default default
Proof state after:
contra : IsDeduct [] false_
s1 : (∀ H ∈ [], Holds Unit default default default H) → Holds Unit default default default false_
⊢ False
Theorem: FOL.NV.Program.Backend.not_IsDeduct_false
Proof state before:
contra : IsDeduct [] false_
s1 : (∀ H ∈ [], Holds Unit default default default H) → Holds Unit default default default false_
⊢ False
Tactic:
simp at s1
Proof state after:
contra : IsDeduct [] false_
s1 : Holds Unit default default default false_
⊢ False
Theorem: FOL.NV.Program.Backend.not_IsDeduct_false
Proof state before:
contra : IsDeduct [] false_
s1 : Holds Unit default default default false_
⊢ False
Tactic:
simp only [Holds] at s1
Proof state after:
no goals
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 : PredName
xs : List VarName
V : VarAssignment D
⊢ I.pred_var_ X (List.map (V ∘ σ) xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  simp
Proof state after:
no goals
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 y : VarName
V : VarAssignment D
⊢ (V ∘ σ) x = (V ∘ σ) y ↔ V (σ x) = V (σ y)
Tactic:
case eq_ x y =>
  simp
Proof state after:
no goals
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 σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ¬Holds D I (V ∘ σ) E phi ↔ ¬Holds D I V E (replaceAll σ phi)
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V
Proof state after:
no goals
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:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  first | apply forall_congr' | apply exists_congr
  intro a
  have s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
  apply Function.updateITE_comp_right_injective
  apply h1
  simp only [← s1]
  exact phi_ih (Function.updateITE V (σ x) a)
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case def_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (def_ a✝¹ a✝) ↔ Holds D I V E (replaceAll σ (def_ a✝¹ a✝))
Tactic:
simp only [replaceAll]
Proof state after:
case def_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ (List.map σ a✝))
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case exists_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (exists_ a✝¹ a✝) ↔ Holds D I V E (exists_ (σ a✝¹) (replaceAll σ a✝))
Tactic:
simp only [Holds]
Proof state after:
case exists_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝)
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) a✝¹ d) E a✝) ↔
    ∃ d, Holds D I (Function.updateITE V (σ a✝¹) d) E (replaceAll σ a✝)
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 : PredName
xs : List VarName
V : VarAssignment D
⊢ I.pred_var_ X (List.map (V ∘ σ) xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
Tactic:
simp
Proof state after:
no goals
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 y : VarName
V : VarAssignment D
⊢ (V ∘ σ) x = (V ∘ σ) y ↔ V (σ x) = V (σ y)
Tactic:
simp
Proof state after:
no goals
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 σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ¬Holds D I (V ∘ σ) E phi ↔ ¬Holds D I V E (replaceAll σ phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
Tactic:
exact phi_ih V
Proof state after:
no goals
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 σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi) ↔
    (Holds D I V E (replaceAll σ phi) ↔ Holds D I V E (replaceAll σ psi))
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
Tactic:
exact phi_ih V
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
Tactic:
exact psi_ih V
Proof state after:
no goals
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:
first | apply forall_congr' | 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:
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)
Tactic:
intro a
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:
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)
Tactic:
have s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
Proof state after:
case s1
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
⊢ Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a

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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ 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:
case s1
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
⊢ Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a

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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
apply Function.updateITE_comp_right_injective
Proof state after:
case s1.h1
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
⊢ Function.Injective σ

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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ 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:
case s1.h1
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
⊢ Function.Injective σ

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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
apply h1
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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ 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:
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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
simp only [← s1]
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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ 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:
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
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE V (σ x) a ∘ σ) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
exact phi_ih (Function.updateITE V (σ x) a)
Proof state after:
no goals
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 : D), Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
Tactic:
apply forall_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)