internlm/Lean-Github huggingface dataset:
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
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
Tactic:
cases h1
Proof state after:
case pos.inl
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
V : Valuation D
d d' : D
c1 h✝ : 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 pos.inr
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
V : Valuation D
d d' : D
c1 : x = v
h✝ : NotFree Γ v phi
⊢ 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:
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
V : Valuation D
d d' : D
c1 c2 : 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
Tactic:
case _ c2 =>
  subst c1
  simp only [Function.updateITE_idem]
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 → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : x = v
c2 : NotFree Γ v phi
⊢ 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:
case _ c2 =>
  subst c1
  simp only [Function.updateITE_idem]
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 → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 c2 : 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
Tactic:
subst c1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : x = x
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x 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)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : x = x
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi
Tactic:
simp only [Function.updateITE_idem]
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 → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : x = v
c2 : NotFree Γ v phi
⊢ 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:
subst c1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : NotFree Γ x phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x 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)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : NotFree Γ x phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi
Tactic:
simp only [Function.updateITE_idem]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
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
Tactic:
cases h1
Proof state after:
case neg.inl
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
V : Valuation D
d d' : D
c1 : ¬x = v
h✝ : 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.inr
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
V : Valuation D
d d' : D
c1 : ¬x = v
h✝ : NotFree Γ v phi
⊢ 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:
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
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : 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
Tactic:
case _ c2 =>
  contradiction
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 → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ 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:
case _ c2 =>
  simp only [← Function.updateITE_comm V x v d d' c1]
  exact phi_ih c2 (Function.updateITE V x d') 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 → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : 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
Tactic:
contradiction
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 → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ 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:
simp only [← Function.updateITE_comm V x v d d' c1]
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
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d') 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
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
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d') v d) M E phi
Tactic:
exact phi_ih c2 (Function.updateITE V x d') 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 : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
⊢ IsNotFree D I M E (def_ X xs) v
Tactic:
induction E
Proof state after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v

case cons
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M tail✝ (meta_var_ X) v) → IsNotFree D I M tail✝ (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (head✝ :: tail✝) (meta_var_ X) v
⊢ IsNotFree D I M (head✝ :: tail✝) (def_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v
Tactic:
case nil =>
  unfold IsNotFree
  intro V d
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
V : Valuation D
d : D
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
V : Valuation D
d : D
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold IsNotFree at h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 :
  ∀ (X : MetaVarName),
    (v, X) ∈ Γ →
      ∀ (V : Valuation D) (d : D),
        Holds D I V M (E_hd :: E_tl) (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (meta_var_ X)
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 :
  ∀ (X : MetaVarName),
    (v, X) ∈ Γ →
      ∀ (V : Valuation D) (d : D),
        Holds D I V M (E_hd :: E_tl) (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (meta_var_ X)
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
simp only [Holds] at h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold IsNotFree at E_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  (∀ (X : MetaVarName),
      (v, X) ∈ Γ →
        ∀ (V : Valuation D) (d : D),
          Holds D I V M E_tl (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M E_tl (meta_var_ X)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  (∀ (X : MetaVarName),
      (v, X) ∈ Γ →
        ∀ (V : Valuation D) (d : D),
          Holds D I V M E_tl (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M E_tl (meta_var_ X)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
simp only [Holds] at E_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (def_ X xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    (if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
      else Holds D I V M E_tl (def_ X xs)) ↔
      if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE (Function.updateITE V v d) E_hd.args (List.map (Function.updateITE V v d) xs))
          M E_tl E_hd.F
      else Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)