The previous installment we gave an initial look at some basic Lean features:
 Propositions
 Proofs
 Tactics
Today we’re going to focus on two topics:
 creating data structures via inductive types
 using pattern matching to transform or consume inductive types.
Latest revision: Sep 4, 2022
Inductive types
Inductive types are the type theory version of what in functional programming is known as Algebraic Data Types.
1. Enumerations
The simplest kind: not parameterized, nor recursive.
Lean 4  Scala 3 


This definition creates 1) a type 2) a namespace 3) exactly 7 ways to construct values of type Weekday
.
Elements can be accessed like so
Weekday.sunday
alternatively the namespace can be opened:
Lean 4  Scala 3 


An important difference is that in Scala each constructor has its own type, whereas in Lean constructors are just functions (without arguments in this case).
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 index .
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:
Lean 4  Scala 3 


which is syntactic sugar for match expressions:
Lean 4  Scala 3 


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
.
In both cases Lean can verify that the recursive invocation is given a smaller data structure, and that the recursion will eventually terminate.
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
repeat { rfl }
1.2 Examples
Some important enumerations are defined in the std library:
 a type without inhabitants
inductive Empty: Type
 a proposition without inhabitants; that means that it's imposible 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
2. Structures
Structures in Lean are inductive definitions with only one case, and one or more fields.
Lean 4  Scala 3 


The keyword structure defines several things at once:
 A type (
Color
)  A constructor (
Color.mk
)  A getter function
Color > Nat
for each field (Color.red
,Color.green
,Color.blue
)
Lean provides a limited form of dot notation:
def yellow := Color.mk 255 255 0
example: yellow.red = 255 := rfl
example: yellow.green = 255 := rfl
example: yellow.blue = 0 := rfl
Structures can have parameters; for example here’s how the product of two types A
and B
is defined in the std library:
Lean 4  Scala 3 


3. Algebraic Data Types
Here’s a simplified version of Option
and Sum
as defined in the std library. They are good examples of simple ADTs.
Lean 4  Scala 3 


3.1 Recursive definitions
List
is different from Option
and Product
in that a list can contain other lists of the same type.
3.1.1 Lists
Lean 4  Scala 3 


notation
is not really an extension method, but rather something closer to a macro.
3.1.2 Natural numbers
The natural numbers (Nat
) are defined inductively in Lean.
(number literals are provided via type classes, which we’ll explore in the future).
inductive Nat
 zero
 succ (n: nat)
Unfortunately Nat
is not available in Scala’s std library but we could create one like so:
enum Nat:
case Zero()
case Succ[N <: Nat](n: N)
(This version carries both type and valuelevel information).
3.1.3 Addition
Addition of two natural numbers as just created can be defined via two transformation rules:
add l zero => l
add l (succ r) => succ (add l r)
Lean 4
def add (l: Nat): Nat > Nat
 zero => l
 succ r => succ (add l r)
Numbers are normally represented using literals like 0
, 1
, etc, so we can write:
def add (l: Nat): Nat > Nat
 0 => l
 r + 1 => (add l r) + 1
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, which we’ll discuss in the future.
4. Generalized Algebraic Data Types
GADTs are called inductive families in Lean.
Here are two examples:
4.1 A simple language
A tiny typed language of arithmetic expressions, that delegates its typing to the host language.
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:
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
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
is parameterized by a type A
and a natural number (a value).
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)
infixr:67 " :: " => Vec.cons
notation "[" "]" => Vec.nil
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.
def v: Vec Nat 2 := 1 :: 1 :: []
example: Vec.head v = 1 := rfl
example: Vec.add v v = (2 :: 2 :: [] : Vec Nat _) := rfl
 doesn't compile!
#check_failure Vec.head Vec.vnil
Scala 3
import compiletime.ops.int._
import compiletime.S
enum Vec[+A, n <: Int]:
case VNil extends Vec[Nothing, 0]
case Cons(a: A, v: Vec[A, n]) extends Vec[A, n + 1]
import Vec.*
extension [A, n <: Int] (a: A)
def :: (v: Vec[A, n]): Vec[A, n + 1] = Cons(a, v)
def head[A, n <: Int]: Vec[A, S[n]] => A =
case VNil => ??? // impossible
case Cons(a, _): 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)
Scala will correctly reject head(VNil)
, but will still complain if we don’t add 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.
Chapter 7: “Inductive types” 
Advanced Functional Programming, by Dr Anil Madhavapeddy, Dr Jeremy Yallop.

Scala 3 Reference manual.