inductive Expr : Type where
  | var (name : String) : Expr
  | number (num : Nat) : Expr
  | plus : Expr → Expr → Expr

inductive Ty where
  | number

inductive Typing : Expr → Ty → Type where
  | var (name : String) : Typing (Expr.var name) Ty.number
  | number (num : Nat) : Typing (Expr.number num) Ty.number
  | plus {e₁ e₂ : Expr} : Typing e₁ Ty.number → Typing e₂ Ty.number → Typing (Expr.plus e₁ e₂) Ty.number

inductive Value : {e : Expr} → {τ : Ty} → (Typing e τ) → Type where
  | number {num : Nat} : Value (Typing.number num)

mutual

inductive Normal : {e : Expr} → {τ : Ty} → (Typing e τ) → Type where
  | neutral {e : Expr} {τ : Ty} {t : Typing e τ} : Neutral t → Normal t
  | number (num : Nat) : Normal (Typing.number num)

inductive Neutral : {e : Expr} → {τ : Ty} → (Typing e τ) → Type where
  | var (name : String) : Neutral (Typing.var name)
  | plus₁ {e₁ e₂ : Expr} {t₁ : Typing e₁ Ty.number} {t₂ : Typing e₂ Ty.number} : Neutral t₁ → Normal t₂ → Neutral (Typing.plus t₁ t₂)
  | plus₂ {e₁ e₂ : Expr} {t₁ : Typing e₁ Ty.number} {t₂ : Typing e₂ Ty.number} : Value t₁ → Neutral t₂ → Neutral (Typing.plus t₁ t₂)

end

inductive Transition : {e₁ e₂ : Expr} → {τ : Ty} → (Typing e₁ τ) → (Typing e₂ τ) → Type where
  | ξ_plus₁
      {e₁ e₁' e₂ : Expr} {t₁ : Typing e₁ Ty.number} {t₁' : Typing e₁' Ty.number} {t₂ : Typing e₂ Ty.number} :
      Transition t₁ t₁' →
      Transition (Typing.plus t₁ t₂) (Typing.plus t₁' t₂)

  | ξ_plus₂
      {e₁ e₂ e₂' : Expr} {t₁ : Typing e₁ Ty.number} {t₂ : Typing e₂ Ty.number} {t₂' : Typing e₂' Ty.number} :
      Normal t₁ →
      Transition t₂ t₂' →
      Transition (Typing.plus t₁ t₂) (Typing.plus t₁ t₂')

  | β_plus
      {num₁ num₂ : Nat} :
      Normal (Typing.number num₁) →
      Normal (Typing.number num₂) →
      Transition (Typing.plus (Typing.number num₁) (Typing.number num₂)) (Typing.number (num₁ + num₂))

def Value.does_not_reduce
  {e₁ e₂ : Expr} {τ : Ty} {t₁ : Typing e₁ τ} {t₂ : Typing e₂ τ} :
  Value t₁ → Transition t₁ t₂ → Empty
  | .number, tr => nomatch tr

mutual

private theorem normal_does_not_reduce
  {e₁ e₂ : Expr} {τ : Ty} {t₁ : Typing e₁ τ} {t₂ : Typing e₂ τ} :
  Normal t₁ → Transition t₁ t₂ → Empty
  | .neutral neut, tr => neutral_does_not_reduce neut tr

private theorem neutral_does_not_reduce
  {e₁ e₂ : Expr} {τ : Ty} {t₁ : Typing e₁ τ} {t₂ : Typing e₂ τ} :
  Neutral t₁ → Transition t₁ t₂ → Empty
  | .plus₁ neut₁ _, .ξ_plus₁ tr₁ => neutral_does_not_reduce neut₁ tr₁
  | .plus₁ _ norm₂, .ξ_plus₂ _ tr₂ => normal_does_not_reduce norm₂ tr₂
  | .plus₂ v₁ neut₂, .ξ_plus₁ tr₁ => v₁.does_not_reduce tr₁
  | .plus₂ v₁ neut₂, .ξ_plus₂ norm₁ tr₂ => neutral_does_not_reduce neut₂ tr₂

end