Theorem: appl_rule (Nederpelt/STLC.lean)

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

case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (Γ ⊢ Λ.App M N : τ) → ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

State before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)) → (Γ ⊢ Λ.App M N : τ)
Tactic:
rintro ⟨σ, h, h'⟩
State after:
case mp.intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ σ : 𝕋 𝕍
h : Γ ⊢ M : σ →' τ
h' : Γ ⊢ N : σ
⊢ Γ ⊢ Λ.App M N : τ

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

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

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (Γ ⊢ Λ.App M N : τ) → ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
intro h
State after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h : Γ ⊢ Λ.App M N : τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h : Γ ⊢ Λ.App M N : τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp only [typingJudgement, typeOf] at h
State after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h :
  (match typeOf Γ M with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

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

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

State before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
h :
  (match x with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
match x with
  | none => simp at h
  | some val => 
    match val with
    | .To σ τ' => 
      use σ
      simp only at h 
      split_ifs at h with h''
      simp only [Option.some.injEq] at h 
      rw [h] at h'
      exact ⟨h', h''⟩
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
h :
  (match none with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = none
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp at h
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val : 𝕋 𝕍
h :
  (match some val with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some val
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
match val with
| .To σ τ' => 
  use σ
  simp only at h 
  split_ifs at h with h''
  simp only [Option.some.injEq] at h 
  rw [h] at h'
  exact ⟨h', h''⟩
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h :
  (match some (σ →' τ') with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
use σ
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h :
  (match some (σ →' τ') with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

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

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h : (if typeOf Γ N = some σ then some τ' else none) = some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
split_ifs at h with h''
State after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : some τ' = some τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

State before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : some τ' = some τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp only [Option.some.injEq] at h
State after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

State before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
rw [h] at h'
State after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ)
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)

State before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ)
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
exact ⟨h', h''⟩
State after:
no goals