a very incomplete formalization of simply-typed lambda calculus in Lean

STLC.lean

/- Base types -/
variable (τ : Type)

/- Base type inhabitants -/
variable (ν : τ → Type)

def Name := String
    deriving DecidableEq

inductive Term :=
    | lit (t : τ) (v : ν t) : Term
    | binop (t₁ t₂ u : τ) (op : ν t₁ → ν t₂ → ν u) (x y : Term) : Term
    | app (f x : Term) : Term
    | lam (x : Name) (v : Term) : Term
    | var (x : Name) : Term

inductive Ty :=
    | base : τ → Ty
    | fn   : Ty → Ty → Ty

open Term

/- From here on out, these should be implicit -/
variable {τ : Type} {ν : τ → Type}

def subst (t : Term τ ν) (x : Name) (v : Term τ ν) :=
    match t with
    | lit _ _ => t
    | binop t₁ t₂ u op a b =>
      binop t₁ t₂ u op (subst a x v) (subst b x v)
    | app f a => app (subst f x v) (subst a x v)
    | lam x' a =>
        if x = x' then
            t
        else
            lam x' (subst a x v)
    | var x' => if x = x' then v else t

inductive Val : Term τ ν → Prop :=
    | lit (t : τ) (v : ν t)
        : Val (lit t v)
    | lam (x : Name) (v : Term τ ν)
        : Val (lam x v)

inductive Step : Term τ ν → Term τ ν → Prop :=
    | binop (t₁ t₂ u : τ) (op : ν t₁ → ν t₂ → ν u)
                 (x : ν t₁) (y : ν t₂)
        : Step (binop t₁ t₂ u op (lit t₁ x) (lit t₂ y))
               (lit u (op x y))
    | app1 (f f' x : Term τ ν)
        : Step f f'
        → Step (app f x) (app f' x)
    | app2 (f x x' : Term τ ν)
        : Val f
        → Step x x'
        → Step (app f x) (app f x')
    | app_subst (a : Name) (x v : Term τ ν)
        : Val x
        → Step (app (lam a v) x) (subst v a x)

infix:50 " ⟹ " => Step

-- XXX is there a reflexive-transitive closure somewhere in the stdlib?
-- should I pull-in mathlib for something like this?
-- maybe lean/batteries?
inductive Steps : Term τ ν → Term τ ν → Prop :=
    | refl (x : Term τ ν)
        : Steps x x
    | step (x y z : Term τ ν)
        : x ⟹ y
        → Steps y z
        → Steps x z

infix:50 " ⤳ " => Steps

section fun_upd
    variable [DecidableEq α]

    def fun_upd (f : α → Option β) (x : α) (v : β) :=
        λ a => if a = x then some v else f a

    notation:max f "[" x " := " v:0 "]" => fun_upd f x v

    variable {f : α → Option β}

    @[simp] theorem fun_upd_this : f[x := a] x = some a := by
        unfold fun_upd
        split -- XXX how do i simplify if {true thing} then _ else _
        · rfl
        · contradiction

    @[simp] theorem fun_upd_other (h : x ≠ y) : f[x := a] y = f y := by
        unfold fun_upd
        split
        · subst y; contradiction
        · rfl

    @[simp] theorem fun_upd_same :
        f[x := a][x := b] = f[x := b]
    := by
        funext y
        unfold fun_upd
        split <;> rfl

    theorem fun_upd_comm (h : x ≠ y):
        f[x := a][y := b] = f[y := b][x := a]
    := by
        funext z
        unfold fun_upd
        split <;> split <;> try rfl
        subst z y; contradiction
end fun_upd

abbrev Ctx τ := Name → Option (Ty τ)

def Γ₀ : Ctx τ := λ _ => none

inductive HasType : Ctx τ → Term τ ν → Ty τ → Prop :=
    | lit Γ t v
        : HasType Γ (lit t v) (Ty.base t)
    | op Γ t₁ t₂ u op x y
        : HasType Γ x (Ty.base t₁)
        → HasType Γ y (Ty.base t₂)
        → HasType Γ (binop t₁ t₂ u op x y) (Ty.base u)
    | app Γ f x t u
        : HasType Γ f (Ty.fn t u)
        → HasType Γ x t
        → HasType Γ (app f x) u
    | lam {Γ x v t u}
        : HasType Γ[x := t] v u
        → HasType Γ (lam x v) (Ty.fn t u)
    | var Γ x t
        : Γ x = some t
        → HasType Γ (var x) t

theorem subst_ty :
    HasType Γ₀ a u →
    HasType Γ[x := u] b t →
    HasType Γ (subst b x a) t
:= by
    generalize h : Γ[x := u] = Γ'
    intros ha hb
    induction hb generalizing Γ <;> clear Γ' <;> unfold subst
    case lit => constructor
    case op hsubx hsuby =>
        constructor
        · apply hsubx h
        · apply hsuby h
    case app hsubf hsubx =>
        constructor
        · apply hsubf h
        · apply hsubx h
    case lam Γ' x' v t₁ t₂ hv hsubv =>
        subst Γ'
        split
        · subst x'
          simp at hv
          constructor
          assumption
        · refine (HasType.lam $ hsubv (fun_upd_comm ?_))
          intro; subst x; contradiction -- XXX this would just be `congruence` in Coq
    case var Γ' x' t' hΓ =>
        subst Γ'
        split
        · subst x'
          simp at hΓ
          subst t'
          sorry -- XXX this needs a lemma I don't feel like proving right now
        · constructor
          rw [fun_upd_other sorry] at hΓ
          exact hΓ