Theorem: abst_rule (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ ((Γ;; x : σ) ⊢ M : τ) ↔ (Γ ⊢ λ' x : σ, M : σ →' τ)
Tactic:
apply Iff.intro
State after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ ((Γ;; x : σ) ⊢ M : τ) → (Γ ⊢ λ' x : σ, M : σ →' τ)

case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ (Γ ⊢ λ' x : σ, M : σ →' τ) → ((Γ;; x : σ) ⊢ M : τ)

State before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ ((Γ;; x : σ) ⊢ M : τ) → (Γ ⊢ λ' x : σ, M : σ →' τ)
Tactic:
intros h
State after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : (Γ;; x : σ) ⊢ M : τ
⊢ Γ ⊢ λ' x : σ, M : σ →' τ

State before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : (Γ;; x : σ) ⊢ M : τ
⊢ Γ ⊢ λ' x : σ, M : σ →' τ
Tactic:
unfold typingJudgement at *
State after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : typeOf (Γ;; x : σ) M = some τ
⊢ typeOf Γ (λ' x : σ, M) = some (σ →' τ)

State before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : typeOf (Γ;; x : σ) M = some τ
⊢ typeOf Γ (λ' x : σ, M) = some (σ →' τ)
Tactic:
simp [h]
State after:
no goals

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ (Γ ⊢ λ' x : σ, M : σ →' τ) → ((Γ;; x : σ) ⊢ M : τ)
Tactic:
intros h
State after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : Γ ⊢ λ' x : σ, M : σ →' τ
⊢ (Γ;; x : σ) ⊢ M : τ

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : Γ ⊢ λ' x : σ, M : σ →' τ
⊢ (Γ;; x : σ) ⊢ M : τ
Tactic:
simp at *
State after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
⊢ typeOf (Γ;; x : σ) M = some τ

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
⊢ typeOf (Γ;; x : σ) M = some τ
Tactic:
generalize h' : typeOf (Γ;; x : σ) M = aux
State after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
aux : Option (𝕋 𝕍)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
aux : Option (𝕋 𝕍)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ
Tactic:
rw [h'] at h
State after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
h :
  (match aux with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
h :
  (match aux with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ
Tactic:
match aux with
| .some τ' => simp at h; simp [h]
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
τ' : 𝕋 𝕍
h :
  (match some τ' with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
h' : typeOf (Γ;; x : σ) M = some τ'
⊢ some τ' = some τ
Tactic:
simp at h
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
τ' : 𝕋 𝕍
h' : typeOf (Γ;; x : σ) M = some τ'
h : τ' = τ
⊢ some τ' = some τ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
τ' : 𝕋 𝕍
h' : typeOf (Γ;; x : σ) M = some τ'
h : τ' = τ
⊢ some τ' = some τ
Tactic:
simp [h]
State after:
no goals