Theorem: ctxtTypeOfPreservation (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M : Λ V 𝕍
⊢ ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Tactic:
induction M with
| Var x => intro Γ Γ' h; apply h; simp
| App M N ih₁ ih₂ =>
  intro Γ Γ' h
  have h₁ (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x Γ = getType x Γ' := by
    exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', true_or])
  have h₂ (x : V) (h' : x ∈ freeVarsOfTerm N) : getType x Γ = getType x Γ' := by
    exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', or_true])
  simp [ih₁ h₁, ih₂ h₂]
| Lam y σ M ih => 
  intro Γ Γ' h
  have h (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x (Γ;; y : σ) = getType x (Γ';; y : σ) := by
    by_cases h'' : x = y <;> simp[h'']
    exact h x (Finset.mem_erase_of_ne_of_mem h'' h')
  simp [ih h]
State after:
no goals

State before:
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ') →
      typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)
Tactic:
intro Γ Γ' h
State after:
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)

State before:
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)
Tactic:
apply h
State after:
case Var.a
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ x ∈ freeVarsOfTerm (Λ.Var x)

State before:
case Var.a
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ x ∈ freeVarsOfTerm (Λ.Var x)
Tactic:
simp
State after:
no goals

State before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ') →
      typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
intro Γ Γ' h
State after:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)

State before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
have h₁ (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x Γ = getType x Γ' := by
  exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', true_or])
State after:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)

State before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
have h₂ (x : V) (h' : x ∈ freeVarsOfTerm N) : getType x Γ = getType x Γ' := by
  exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', or_true])
State after:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
h₂ : ∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)

State before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
h₂ : ∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
simp [ih₁ h₁, ih₂ h₂]
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
⊢ getType x Γ = getType x Γ'
Tactic:
exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', true_or])
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
⊢ x ∈ freeVarsOfTerm (Λ.App M N)
Tactic:
simp only [freeVarsOfTerm, Finset.mem_union, h', true_or]
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm N
⊢ getType x Γ = getType x Γ'
Tactic:
exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', or_true])
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm N
⊢ x ∈ freeVarsOfTerm (Λ.App M N)
Tactic:
simp only [freeVarsOfTerm, Finset.mem_union, h', or_true]
State after:
no goals

State before:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ') →
      typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Tactic:
intro Γ Γ' h
State after:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)

State before:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Tactic:
have h (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x (Γ;; y : σ) = getType x (Γ';; y : σ) := by
  by_cases h'' : x = y <;> simp[h'']
  exact h x (Finset.mem_erase_of_ne_of_mem h'' h')
State after:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h✝ : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
h : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)

State before:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h✝ : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
h : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Tactic:
simp [ih h]
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
⊢ getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
Tactic:
by_cases h'' : x = y <;> simp[h'']
State after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
h'' : ¬x = y
⊢ getType x Γ = getType x Γ'

State before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
h'' : ¬x = y
⊢ getType x Γ = getType x Γ'
Tactic:
exact h x (Finset.mem_erase_of_ne_of_mem h'' h')
State after:
no goals