Theorem: progress (STLC.lean)

State before:
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Tactic:
generalize hc : (∅ : Ctx) = ctx
State after:
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
ctx : Ctx
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'

State before:
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
ctx : Ctx
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Tactic:
rw [hc] at h
State after:
t : Term
ty : Ty
ctx : Ctx
h : ctx ⊢ t ⋮ ty
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
h : ctx ⊢ t ⋮ ty
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Tactic:
induction h <;> (subst hc; simp at *)
State after:
case var
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'

case abs
t : Term
ty : Ty
ctx : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁✝] → (∃ v, t✝ = Term.abs v.1 v.2) ∨ ∃ t', t✝ ⇒ t'
⊢ (∃ v, ty₁✝ = v.1 ∧ t✝ = v.2) ∨ ∃ t', Term.abs ty₁✝ t✝ ⇒ t'

case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
a_ih✝ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
h : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'
Tactic:
case var h => injection h
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
ty₁ : Ty
t₁ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁] ⊢ t₁ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁] → (∃ v, t₁ = Term.abs v.1 v.2) ∨ ∃ t', t₁ ⇒ t'
⊢ (∃ v, ty₁ = v.1 ∧ t₁ = v.2) ∨ ∃ t', Term.abs ty₁ t₁ ⇒ t'
Tactic:
case abs ty₁ t₁ _ _ _ => exact .inl ⟨⟨_, _⟩, rfl, rfl⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case app hi₁ hi₂ =>
  cases hi₁ <;> apply Or.inr
  case inr h =>
    have ⟨_, h⟩ := h
    exact ⟨_, .app₁ _ h⟩
  case inl ty₁ _ _ ht₁ _ h₁ =>
    cases hi₂ 
    case inl h₂ =>
      have ⟨v₁, hv₁⟩ := h₁ 
      have ⟨v₂, hv₂⟩ := h₂
      subst hv₁ hv₂
      have ⟨body₁, hv₁⟩ := canonical_forms ht₁
      subst hv₁
      exact ⟨_, .beta ..⟩ 
    case inr h₂ =>
      have ⟨_, h₁⟩ := h₁
      have ⟨_, h₂⟩ := h₂
      subst h₁
      exact ⟨_, .app₂ _ h₂⟩
State after:
no goals

State before:
case app
t : Term
ty : Ty
ctx ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∅ = ctx✝ →
    (∃ v,
        t₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ctx✝ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
hc : ∅ = ctx✝
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
subst hc
State after:
case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∅ = ∅ →
    (∃ v,
        t₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ∅ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∅ = ∅ →
    (∃ v,
        t₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ∅ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
simp at *
State after:
case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
a_ih✝ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
h : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'
Tactic:
injection h
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
ty₁ : Ty
t₁ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁] ⊢ t₁ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁] → (∃ v, t₁ = Term.abs v.1 v.2) ∨ ∃ t', t₁ ⇒ t'
⊢ (∃ v, ty₁ = v.1 ∧ t₁ = v.2) ∨ ∃ t', Term.abs ty₁ t₁ ⇒ t'
Tactic:
exact .inl ⟨⟨_, _⟩, rfl, rfl⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
cases hi₁ <;> apply Or.inr
State after:
case inl.h
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

case inr.h
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ t', t₁✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h : ∃ t', t₁✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inr h =>
  have ⟨_, h⟩ := h
  exact ⟨_, .app₁ _ h⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inl ty₁ _ _ ht₁ _ h₁ =>
  cases hi₂ 
  case inl h₂ =>
    have ⟨v₁, hv₁⟩ := h₁ 
    have ⟨v₂, hv₂⟩ := h₂
    subst hv₁ hv₂
    have ⟨body₁, hv₁⟩ := canonical_forms ht₁
    subst hv₁
    exact ⟨_, .beta ..⟩ 
  case inr h₂ =>
    have ⟨_, h₁⟩ := h₁
    have ⟨_, h₂⟩ := h₂
    subst h₁
    exact ⟨_, .app₂ _ h₂⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h : ∃ t', t₁✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨_, h⟩ := h
State after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ t', t₁✝ ⇒ t'
w✝ : Term
h : t₁✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ t', t₁✝ ⇒ t'
w✝ : Term
h : t₁✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
exact ⟨_, .app₁ _ h⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
cases hi₂
State after:
case inl
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h✝ : ∃ v, t₂✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

case inr
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h✝ : ∃ t', t₂✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inl h₂ =>
  have ⟨v₁, hv₁⟩ := h₁ 
  have ⟨v₂, hv₂⟩ := h₂
  subst hv₁ hv₂
  have ⟨body₁, hv₁⟩ := canonical_forms ht₁
  subst hv₁
  exact ⟨_, .beta ..⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inr h₂ =>
  have ⟨_, h₁⟩ := h₁
  have ⟨_, h₂⟩ := h₂
  subst h₁
  exact ⟨_, .app₂ _ h₂⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨v₁, hv₁⟩ := h₁
State after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨v₂, hv₂⟩ := h₂
State after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
v₂ : Value
hv₂ : t₂✝ = Term.abs v₂.1 v₂.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
v₂ : Value
hv₂ : t₂✝ = Term.abs v₂.1 v₂.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
subst hv₁ hv₂
State after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'
Tactic:
have ⟨body₁, hv₁⟩ := canonical_forms ht₁
State after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
hv₁ : v₁ = Value.abs ty₁ body₁
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
hv₁ : v₁ = Value.abs ty₁ body₁
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'
Tactic:
subst hv₁
State after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₂ : Value
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
ht₁ : ∅ ⊢ Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2) (Term.abs v₂.1 v₂.2) ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₂ : Value
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
ht₁ : ∅ ⊢ Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2) (Term.abs v₂.1 v₂.2) ⇒ t'
Tactic:
exact ⟨_, .beta ..⟩
State after:
no goals

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨_, h₁⟩ := h₁
State after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
w✝ : Value
h₁ : t₁✝ = Term.abs w✝.1 w✝.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
w✝ : Value
h₁ : t₁✝ = Term.abs w✝.1 w✝.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨_, h₂⟩ := h₂
State after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
h₁ : t₁✝ = Term.abs w✝¹.1 w✝¹.2
w✝ : Term
h₂ : t₂✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
h₁ : t₁✝ = Term.abs w✝¹.1 w✝¹.2
w✝ : Term
h₂ : t₂✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
subst h₁
State after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
t₂✝ : Term
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
w✝ : Term
h₂ : t₂✝ ⇒ w✝
ht₁ : ∅ ⊢ Term.abs w✝¹.1 w✝¹.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs w✝¹.1 w✝¹.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs w✝¹.1 w✝¹.2) t₂✝ ⇒ t'

State before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
t₂✝ : Term
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
w✝ : Term
h₂ : t₂✝ ⇒ w✝
ht₁ : ∅ ⊢ Term.abs w✝¹.1 w✝¹.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs w✝¹.1 w✝¹.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs w✝¹.1 w✝¹.2) t₂✝ ⇒ t'
Tactic:
exact ⟨_, .app₂ _ h₂⟩
State after:
no goals