Lean for Scala programmers - Part 2

In the previous installment we took a first look at some basic Lean features:

• Propositions and proofs
• Dependent function types
• Tactics, and a first proof by induction

Today we're going to focus on two topics:

• creating data structures via inductive types
• using pattern matching to transform or consume inductive types.

Inductive types are the type theory version of what in functional programming is known as Algebraic Data Types.

Scala version used: 3.9.0
Lean 4 version: 4.31.0
Latest revision: Sep 23, 2026

1. Enumerations

The simplest kind: not parameterized, nor recursive.

inductive Weekday
  | sunday
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday

enum Weekday:
  case Sunday
  case Monday
  case Tuesday
  case Wednesday
  case Thursday
  case Friday
  case Saturday

This definition creates 1) a type 2) a namespace 3) exactly 7 ways to construct values of type Weekday. (Lean also generates a few auxiliary definitions, such as the recursor Weekday.rec; pattern matching is ultimately translated into it.)

Elements can be accessed like so

Weekday.sunday

alternatively the namespace can be opened:

open Weekday

import Weekday.*

An important difference is that in Scala each case also defines a type (Weekday.Sunday.type, or Option.Some[A] for a case with parameters), which is a subtype of the enum. Lean has no subtyping: constructors are just functions (without arguments in this case) that return a Weekday.

This has a consequence: if we want to define operations that only work on some constructors, we need to come up with a way to distinguish them in the type system, perhaps using another type as an index. We'll see how in section 4.

1.1 Pattern matching

There are several ways to pattern match on inductive types.

A common approach is to use a function defined by cases:

def next: Weekday -> Weekday
  | sunday    => monday
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

val next: Weekday => Weekday =
  case Sunday    => Monday
  case Monday    => Tuesday
  case Tuesday   => Wednesday
  case Wednesday => Thursday
  case Thursday  => Friday
  case Friday    => Saturday
  case Saturday  => Sunday

which is syntactic sugar for match expressions:

def next' (d: Weekday) : Weekday :=
  match d with
  | sunday    => monday
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

def next2(d: Weekday): Weekday =
  d match
    case Sunday    => Monday
    case Monday    => Tuesday
    case Tuesday   => Wednesday
    case Wednesday => Thursday
    case Thursday  => Friday
    case Friday    => Saturday
    case Saturday  => Sunday

Let's prove that applying next 7 times is the identity function.

First we need a way to iterate a function a number of times:

def iter (f: A -> A): Nat -> (A -> A)
  | 0     => id
  | n + 1 => f ∘ (iter f n)


example: iter next 0 = id                 := rfl
example: iter next 1 = next               := rfl
example: iter next 2 = next ∘ next        := rfl
example: iter next 3 = next ∘ next ∘ next := rfl

id is the identity function fun x => x. The composition operator ∘ can be entered as \circ.

Observe how we're using n + 1 as a pattern, allowing us to extract n and pass it to the next iter call. This is similar to deconstructing a list as h :: t. (As we'll see in section 3.1.2, n + 1 in a pattern stands for the constructor Nat.succ n.)

In both cases Lean can verify that the recursive invocation is given a smaller data structure, and that the recursion will eventually terminate. This is called structural recursion.

Now we can state and prove the proposition:

for all weekdays, the function next has period 7

example: ∀ (w: Weekday), (iter next 7) w = w := by
  intro w
  cases w <;> rfl

Step by step:

• intro w introduces an arbitrary weekday w. The goal becomes (iter next 7) w = w.
• cases w splits the goal into seven goals, one for each constructor: (iter next 7) sunday = sunday, and so on.
• <;> rfl runs rfl on each of the seven goals. With a concrete weekday, the type checker can compute iter next 7 step by step, so both sides reduce to the same value.

For an arbitrary w, rfl alone doesn't work: next w can't reduce until Lean knows which constructor w is. Case analysis gives it that information.

1.2 Examples

Some important enumerations are defined in Lean's core library. We wrap them in a Hidden namespace so the definitions don't clash with the identically-named types in Lean's prelude:

namespace Hidden

-- a type without inhabitants

inductive Empty: Type

-- a proposition without inhabitants; that means that it's impossible to prove.
-- This is taken as the definition of False.

inductive False : Prop

-- a proposition with only one way to prove it: True.intro

inductive True : Prop where
  | intro : True

end Hidden

Empty and False have the same shape (no constructors at all); they only differ in where they live: Type or Prop. False is the one that logic uses. In Part 1 we said that a proposition p is false when we can prove ¬p, which is a function p → False. Since False has no constructors, such a function shows that p can't have a proof: otherwise we could apply the function to it and obtain a proof of False.

2. Structures

Structures in Lean are inductive definitions with only one constructor, and zero or more fields.

structure Color where
  red  : Nat
  green: Nat
  blue : Nat

case class Color(
  red  : Int,
  green: Int,
  blue : Int
)

The keyword structure defines several things at once:

1. A type (Color)
2. A constructor (Color.mk)
3. A getter function Color -> Nat for each field (Color.red, Color.green, Color.blue)

Lean provides dot notation, just like Scala:

def yellow := Color.mk 255 255 0

example: yellow.red   = 255 := rfl
example: yellow.green = 255 := rfl
example: yellow.blue  = 0   := rfl

Dot notation is not limited to fields. If x has type T, then x.f means T.f x for any function f in the namespace T:

def Weekday.isWeekend: Weekday -> Bool
  | saturday | sunday => true
  | _                 => false

example: sunday.isWeekend = true := rfl

This works a lot like a Scala extension method. We'll use it again in section 4.

Besides Color.mk, there are two shorter ways to build a structure:

example: (⟨255, 255, 0⟩ : Color) = yellow := rfl

example: { red := 255, green := 255, blue := 0 : Color } = yellow := rfl

The first one is the anonymous constructor (you type ⟨ and ⟩ as \< and \>). The second one names the fields, like Color(red = 255, green = 255, blue = 0) in Scala.

Structures can have parameters; for example here's a simplified version of the product of two types A and B, as defined in Lean's core library:

namespace Hidden

structure Prod (A B: Type) where
  fst: A
  snd: B

def t := Prod.mk 1 "one"

end Hidden

case class Prod[A, B](
  fst: A,
  snd: B
)
val t = Prod(1, "one")

3. Algebraic Data Types

Here's a simplified version of Option and Sum as defined in Lean's core library. They are good examples of simple ADTs.

namespace Hidden

inductive Option (A: Type)
  | none
  | some (a: A)

inductive Sum (A B: Type)
  | inl (a: A)
  | inr (b: B)

end Hidden

enum Option[+A]:
  case None
  case Some(a: A)

enum Sum[+A, +B]:
  case Inl(a: A)
  case Inr(b: B)

Scala needs variance annotations (+A) because it has subtyping: Option.None must be an Option[Int], an Option[String], and so on. Lean has no subtyping, so it has no variance annotations either: Option.none simply takes the type A as an (implicit) argument.

3.1 Recursive definitions

List is different from Option and Sum because it is recursive: the constructor cons takes another List T as an argument (the tail).

3.1.1 Lists

namespace Hidden

inductive List (T: Type)
  | nil
  | cons (head: T) (tail: List T)

scoped infixr:67 " :: " => List.cons
scoped notation "[" "]" => List.nil

def lst : List Nat := 1 :: 2 :: []

end Hidden

enum List[+T]:
  case Nil
  case Cons(head: T, tail: List[T])

extension [T] (h: T)
  def :: (t: List[T]) = List.Cons(h,t)


val lst = 1 :: 2 :: List.Nil

infixr and notation are not functions or extension methods: they are macros that add new syntax to Lean's parser. We mark them scoped so that they are active only inside the Hidden namespace. Otherwise they would stay active in the whole file, as extra meanings for Lean's own :: and [].

3.1.2 Natural numbers

The natural numbers (Nat) are defined inductively in Lean:

namespace Hidden

inductive Nat
  | zero
  | succ (n: Nat)

end Hidden

Number literals such as 3 are provided via the OfNat type class; we'll explore type classes in Part 3. (Although Nat is defined in this unary way, Lean's kernel and compiler use efficient binary numbers for it.)

Unfortunately Nat is not available in Scala's standard library, but we could create one like so:

enum Nat:
  case Zero()
  case Succ[N <: Nat](n: N)

(This version carries both type and value-level information.)

3.1.3 Addition

Addition of two natural numbers can be defined via two transformation rules:

1. add l zero => l
2. add l (succ r) => succ (add l r)

From here on we use the built-in Nat again:

Lean 4

def add (l: Nat): Nat -> Nat
  | .zero   => l
  | .succ r => .succ (add l r)

.zero and .succ are short for Nat.zero and Nat.succ: Lean takes the namespace from the expected type.

Numbers are normally represented using literals like 0, 1, etc., so we can also write:

def add' (l: Nat): Nat -> Nat
  | 0     => l
  | r + 1 => (add' l r) + 1

In the pattern, r + 1 is notation for Nat.succ r. Both definitions compute the same function; the examples below use add:

example: add 1 2 = 3 := rfl

-- by definition of add:

theorem add_zero (l: Nat) : add l 0 = l := by rfl

theorem add_succ (l r: Nat): add l (r + 1) = (add l r) + 1 := by rfl

Proving add 0 m = m, on the other hand, requires a proof by induction on m: rfl fails, because add 0 m can't reduce while m is unknown. We saw a first proof by induction in Part 1, and Part 4 proves the same result for Lean's built-in + (as zero_add).

4. Generalized Algebraic Data Types

GADTs are called inductive families in Lean.

The key difference from ordinary inductive types is the distinction between parameters and indices. A parameter (written before the colon) is the same in every constructor, like A in Option A. An index (written after the colon, as part of the type) can be different in each constructor. That's what lets each constructor refine the type, just like extends Expr[Int] does in a Scala GADT.

Here are two examples:

4.1 A simple language

A tiny typed language of arithmetic expressions, that delegates its typing to the host language. Expr has no parameters and one index of type Type:

Lean 4

inductive Expr : Type -> Type
  | num (n: Nat)          : Expr Nat
  | bool (b: Bool)        : Expr Bool
  | add (e1 e2: Expr Nat) : Expr Nat
  | mul (e1 e2: Expr Nat) : Expr Nat

Scala 3

enum Expr[A]:
  case Num(n: Int) extends Expr[Int]
  case Bool(b: Boolean) extends Expr[Boolean]
  case Add(e1: Expr[Int], e2: Expr[Int]) extends Expr[Int]
  case Mul(e1: Expr[Int], e2: Expr[Int]) extends Expr[Int]

Here's an interpreter for this language:

Lean 4

def Expr.eval: Expr A -> A
  | num n => n
  | bool b => b
  | add e1 e2 => e1.eval + e2.eval
  | mul e1 e2 => e1.eval * e2.eval

Inside def Expr.eval the namespace Expr is open, so we can write num instead of Expr.num, and e1.eval is dot notation for Expr.eval e1.

Scala 3

import Expr.*

def eval[A]: Expr[A] => A =
  case Num(n) => n
  case Bool(b) => b
  case Add(e1, e2) => eval(e1) + eval(e2)
  case Mul(e1, e2) => eval(e1) * eval(e2)

4.2 Vectors

Each Vec has a type parameter A and an index of type Nat (a value): the length of the vector.

Lean 4

inductive Vec (A: Type) : Nat -> Type
  | vnil : Vec A 0
  | cons {n: Nat} (a: A) (v: Vec A n) : Vec A (n + 1)

namespace Vec
scoped infixr:67 " :: " => Vec.cons
scoped notation "[" "]" => Vec.vnil
end Vec

open Vec

def Vec.head: Vec A (n + 1) -> A
  | h :: _ => h

def Vec.add: Vec Nat n -> Vec Nat n -> Vec Nat n
  | [],       []       => vnil
  | h1 :: t1, h2 :: t2 => (h1 + h2) :: (add t1 t2)

head takes a vector of length n + 1. Lean can infer that there's no need to handle the vnil case: vnil has type Vec A 0, and 0 can never match n + 1, because they are built with different constructors of Nat (zero and succ).

def v: Vec Nat 2 := 1 :: 1 :: []

example: Vec.head v = 1 := rfl
example: Vec.add v v = (2 :: 2 :: [] : Vec Nat _) := rfl

-- `#check_failure` succeeds only if the expression does NOT type-check:
#check_failure Vec.head Vec.vnil

Scala 3

import compiletime.ops.int.S

enum Vec[+A, n <: Int]:
  case VNil extends Vec[Nothing, 0]
  case Cons(a: A, v: Vec[A, n]) extends Vec[A, S[n]]

import Vec.*

extension [A, n <: Int] (a: A)
  def :: (v: Vec[A, n]): Vec[A, S[n]] = Cons(a, v)

def head[A, n <: Int]: Vec[A, S[n]] => A =
  case VNil       => ??? // impossible
  case Cons(a, _) => a

def add[n <: Int]: (Vec[Int, n], Vec[Int, n]) => Vec[Int, n] =
  case (VNil, VNil)                 => VNil
  case (Cons(h1, t1), Cons(h2, t2)) => (h1 + h2) :: add(t1, t2)

We use S[n] (the successor of n, from scala.compiletime.ops.int) rather than n + 1. For a concrete n the two reduce to the same number, but Scala can infer n only from S[n]: with n + 1 in the type of head, the call head(v) fails, because Scala can't solve n + 1 = 2 for n.

Scala will correctly reject head(VNil), but it still warns that the match may not be exhaustive if we leave out the useless case VNil => ???.

val v = 1 :: 1 :: VNil

assert( head(v) == 1 )
assert( add(v, v) == 2 :: 2 :: VNil )

// Doesn't even compile:
// head(VNil)

In the next episode of this series we'll discuss dependent types at length, getting us closer to our goal of being able to prove some properties of our code.

Resources

• Theorem Proving in Lean 4.

  Inductive Types

• Advanced Functional Programming, by Dr Anil Madhavapeddy and Dr Jeremy Yallop.

  Chapter 9: "Programming with GADTs"

• Scala 3 Reference.

  Algebraic Data Types

  Match Types and Dependent Typing