internlm/Lean-Github huggingface dataset:
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ ¬Holds D I V M E phi ↔ ¬Holds D I (Function.updateITE V v d) M E phi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ ¬Holds D I V M E phi ↔ ¬Holds D I (Function.updateITE V v d) M E phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
Tactic:
exact phi_ih h1 V d
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v (phi.imp_ psi)
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold IsNotFree at phi_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold IsNotFree at psi_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
left✝ : NotFree Γ v phi
right✝ : NotFree Γ v psi
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi
Tactic:
congr! 1
Proof state after:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
a✝ : Holds D I (Function.updateITE V v d) M E phi
⊢ Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
Tactic:
exact phi_ih h1_left V d
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
a✝ : Holds D I (Function.updateITE V v d) M E phi
⊢ Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
Tactic:
exact psi_ih h1_right V d
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v (forall_ x phi)
⊢ IsNotFree D I M E (forall_ x phi) v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v
Tactic:
unfold IsNotFree at phi_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E phi) ↔
    ∀ (d_1 : D), Holds D I (Function.updateITE (Function.updateITE V v d) x d_1) M E phi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E phi) ↔
    ∀ (d_1 : D), Holds D I (Function.updateITE (Function.updateITE V v d) x d_1) M E phi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x a) M E phi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x a) M E phi
Tactic:
intro d'
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
by_cases c1 : x = v
Proof state after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
c1 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

case neg
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
c1 : ¬x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi