Theorem: MM0.lem_1 (FOL/MM0/MM0.lean)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
⊢ ∀ (v : VarName) (X : MetaVarName),
    (v, X) ∈ Γ → IsNotFree D I (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) v
Tactic:
intro v X a1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ IsNotFree D I (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ IsNotFree D I (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) ↔
      Holds D I (Function.updateITE V v d) (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) ↔
      Holds D I (Function.updateITE V v d) (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D), Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D), Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)
Tactic:
simp only [Function.updateITE_comp_right σ' σ.1 V v d h1_left h1_right]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE (V ∘ σ') (↑σ v) d) M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE (V ∘ σ') (↑σ v) d) M E (τ X)
Tactic:
apply not_free_imp_is_not_free D I M E (τ X) Γ' (σ.1 v)
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ NotFree Γ' (↑σ v) (τ X)

case h2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ ∀ (X : MetaVarName), (↑σ v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) (↑σ v)

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ NotFree Γ' (↑σ v) (τ X)
Tactic:
exact h3 v X a1
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ ∀ (X : MetaVarName), (↑σ v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) (↑σ v)
Tactic:
intro X' a2
State after:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
X' : MetaVarName
a2 : (↑σ v, X') ∈ Γ'
⊢ IsNotFree D I M E (meta_var_ X') (↑σ v)

State before:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
X' : MetaVarName
a2 : (↑σ v, X') ∈ Γ'
⊢ IsNotFree D I M E (meta_var_ X') (↑σ v)
Tactic:
exact h2 (σ.1 v) X' a2
State after:
no goals