Theorem: canonical_forms (STLC.lean)

State before:
ty₁ ty₂ : Ty
v : Value
h :
  ∅ ⊢
    match v with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, v = Value.abs ty₁ t
Tactic:
cases v
State after:
case abs
ty₁ ty₂ ty✝ : Ty
body✝ : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body✝ = Value.abs ty₁ t

State before:
ty₁ ty₂ ty✝ : Ty
body : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Tactic:
case abs body =>
  simp at h
  exists body
  have ⟨_, h, _⟩ := inversion_abs h
  injection h with h
  rw [h]
State after:
no goals

State before:
ty₁ ty₂ ty✝ : Ty
body : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Tactic:
simp at h
State after:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t

State before:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Tactic:
exists body
State after:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ Value.abs ty✝ body = Value.abs ty₁ body

State before:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Tactic:
have ⟨_, h, _⟩ := inversion_abs h
State after:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
h : Ty.arrow ty₁ ty₂ = Ty.arrow ty✝ w✝
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body

State before:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
h : Ty.arrow ty₁ ty₂ = Ty.arrow ty✝ w✝
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Tactic:
injection h with h
State after:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
h : ty₁ = ty✝
ty₂_eq✝ : ty₂ = w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body

State before:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
h : ty₁ = ty✝
ty₂_eq✝ : ty₂ = w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Tactic:
rw [h]
State after:
no goals