Simply typed lambda calculus in Lean 4

stlc.lean

/- Everybody's Got To Be Somewhere. Conor McBride.
https://arxiv.org/abs/1807.04085 -/
inductive Cover : (x y z : List α) -> Type u
  | done  : Cover [] [] []
  | left  : Cover x y z -> Cover (t :: x) y (t :: z)
  | right : Cover x y z -> Cover x (t :: y) (t :: z)
  | both  : Cover x y z -> Cover (t :: x) (t :: y) (t :: z)

inductive HList {α : Type u} (β : α -> Type v) : List α -> Type (max u v)
  | term : HList β []
  | cons : β x -> HList β xs -> HList β (x :: xs)

namespace Cover
  def partition : Cover Γ₁ Γ₂ Γ -> HList β Γ -> HList β Γ₁ × HList β Γ₂
    | .done, .term => (.term, .term)
    | .left  c, .cons v xs => let (l, r) := partition c xs; (.cons v l, r)
    | .right c, .cons v xs => let (l, r) := partition c xs; (l, .cons v r)
    | .both  c, .cons v xs => let (l, r) := partition c xs; (.cons v l, .cons v r)
end Cover

/- A Cosmology of Datatypes. Pierre- ́Evariste Dagand.
https://www.irif.fr/~dagand/stuffs/thesis-2011-phd/thesis.pdf -/
inductive Desc
  | unit
  | prod (a b : Desc)
  | func (a b : Desc)

namespace Desc
  @[reducible] def denote : Desc -> Type
    | .unit => Unit
    | .prod a b => a.denote × b.denote
    | .func a b => a.denote -> b.denote
end Desc

/- Correct by Construction Language Implementations. Rouvoet, A.J
https://repository.tudelft.nl/islandora/object/uuid:f0312839-3444-41ee-9313-b07b21b59c11 -/
inductive Stlc : Desc -> List Desc -> Type
  | const : Stlc .unit []
  | var : Stlc t [t]
  | lam : Stlc b (a :: Γ) -> Stlc (.func a b) Γ
  | app : Stlc (.func a b) Γ₁ -> Stlc a Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc b Γ
  | prod : Stlc a Γ₁ -> Stlc b Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc (.prod a b) Γ

namespace Stlc
  @[simp] def denote : Stlc ty Γ -> HList Desc.denote Γ -> ty.denote
    | .const, .term => ()
    | .var, .cons x .term => x
    | .lam f, xs => fun x => f.denote (.cons x xs)
    | .app f x c, xs => let (l, r) := c.partition xs; f.denote l (x.denote r)
    | .prod a b c, xs => let (l, r) := c.partition xs; (a.denote l, b.denote r) 
end Stlc

example : Stlc.denote .const .term = () := rfl
example : Stlc.denote .var (.cons x .term) = x := rfl
example : Stlc.denote (.lam .var) .term x = x := rfl
example : Stlc.denote (.app (.lam .var) .var (.right .done)) (.cons x .term) = x := rfl
example : Stlc.denote (.prod .const .const .done) .term = ((), ()) := rfl
example : Stlc.denote (.prod .var .var (.both .done)) (.cons x .term) = (x, x) := rfl