Skip to content

1.16 Inductive Types Introduction

Inductive types define data by listing its constructors.

lean proof-assistant type-theory functional-programming

Inductive types define data by listing its constructors. Each constructor describes one way to build an element of the type. Once Lean knows the constructors, it automatically provides the principles needed to define functions by recursion and prove theorems by induction.

Problem

You want to define your own data types, construct values of those types, pattern match on them, and prove simple facts about them.

Solution

Use inductive to declare a type and its constructors.

inductive Color where
  | red
  | green
  | blue
deriving Repr

This declares a type named Color with three constructors:

#check Color
#check Color.red
#check Color.green
#check Color.blue

Typical output:

Color : Type
Color.red : Color
Color.green : Color
Color.blue : Color

The clause deriving Repr tells Lean how to print values of Color.

#eval Color.red

Expected output:

Color.red

Constructors

A constructor is a function that builds an element of an inductive type.

For an enumeration, constructors take no arguments.

inductive Direction where
  | north
  | south
  | east
  | west
deriving Repr

Each constructor is a value:

#check Direction.north

Output:

Direction.north : Direction

For a type with data, constructors take arguments.

inductive Shape where
  | circle (radius : Nat)
  | rectangle (width height : Nat)
deriving Repr

Now the constructors are functions:

#check Shape.circle
#check Shape.rectangle

Typical output:

Shape.circle : Nat -> Shape
Shape.rectangle : Nat -> Nat -> Shape

Use them to build values:

#eval Shape.circle 10
#eval Shape.rectangle 3 4

Pattern Matching on Inductive Types

Define functions by matching on constructors.

def isPrimary : Color -> Bool
| Color.red   => true
| Color.green => true
| Color.blue  => true

A more useful example:

inductive TrafficLight where
  | red
  | yellow
  | green
deriving Repr

def canGo : TrafficLight -> Bool
| TrafficLight.red    => false
| TrafficLight.yellow => false
| TrafficLight.green  => true

#eval canGo TrafficLight.green
#eval canGo TrafficLight.red

Expected output:

true
false

Pattern matching covers all constructors. If a constructor is missing, Lean reports an incomplete match.

Recursive Inductive Types

An inductive type may refer to itself in constructor arguments.

inductive NatList where
  | nil
  | cons (head : Nat) (tail : NatList)
deriving Repr

This is a simple list type specialized to natural numbers.

Values are built recursively:

def xs : NatList :=
  NatList.cons 1 (NatList.cons 2 (NatList.cons 3 NatList.nil))

#eval xs

A recursive function over NatList follows the same structure.

def NatList.length : NatList -> Nat
| NatList.nil => 0
| NatList.cons _ tail => NatList.length tail + 1

#eval NatList.length xs

Expected output:

3

The recursive call is made on tail, a structurally smaller part of the input, so Lean accepts the definition.

Polymorphic Inductive Types

An inductive type can take a type parameter.

inductive Box (α : Type) where
  | mk (value : α)
deriving Repr

Use it with different element types:

#check Box Nat
#check Box String
#eval Box.mk 5
#eval Box.mk "Lean"

A more familiar example is an optional value type:

inductive Maybe (α : Type) where
  | none
  | some (value : α)
deriving Repr

This resembles Lean’s built-in Option.

#eval Maybe.some 10
#eval (Maybe.none : Maybe Nat)

The type annotation is needed for Maybe.none because there is no value from which Lean can infer α.

Namespaces from Inductive Types

An inductive declaration creates a namespace for its constructors.

#check Maybe.none
#check Maybe.some

You may open the namespace:

open Maybe

#check none
#check some

In larger files, qualified names are often clearer.

Inductive Propositions

Inductive types also define propositions. A constructor of an inductive proposition is an introduction rule.

inductive Even : Nat -> Prop where
  | zero : Even 0
  | step {n : Nat} : Even n -> Even (n + 2)

This defines a proposition Even n.

#check Even
#check Even.zero
#check Even.step

Typical output:

Even : Nat -> Prop
Even.zero : Even 0
Even.step : Even n -> Even (n + 2)

A proof that 4 is even:

theorem even_four : Even 4 := by
  exact Even.step (Even.step Even.zero)

The same constructor mechanism builds both data and proofs.

Induction Principles

For every inductive type, Lean generates an induction principle.

#check Color.rec
#check NatList.rec

For recursive types, the induction principle includes one case per constructor. For NatList, proving a property for all lists requires:

  • a proof for nil
  • a proof that the property is preserved by cons

This mirrors recursive function definitions.

Proving by Cases

For a finite inductive type, proofs often use cases.

theorem canGo_false_or_true (t : TrafficLight) :
    canGo t = true ∨ canGo t = false := by
  cases t with
  | red =>
      right
      rfl
  | yellow =>
      right
      rfl
  | green =>
      left
      rfl

Each case corresponds to one constructor.

Deriving Instances

The deriving clause asks Lean to generate standard instances.

inductive Status where
  | pending
  | done
  | failed
deriving Repr, DecidableEq

Now Lean can print values and decide equality.

#eval Status.pending == Status.done
#eval Status.done == Status.done

Expected output:

false
true

Common derivable instances include Repr, DecidableEq, and others depending on the type.

Common Pitfalls

If Lean cannot print a value, add deriving Repr.

If Lean cannot compare values with ==, add deriving DecidableEq.

If a match is incomplete, add a case for every constructor.

If a recursive function is rejected, check that every recursive call uses structurally smaller data.

If a constructor like none is ambiguous, add a type annotation.

Recipe: Define a Small Inductive Type

Start with the possible cases.

inductive Result where
  | ok (value : Nat)
  | error (message : String)
deriving Repr

Then define behavior by cases.

def Result.isOk : Result -> Bool
| Result.ok _ => true
| Result.error _ => false

Test examples.

#eval Result.isOk (Result.ok 10)
#eval Result.isOk (Result.error "bad input")

Expected output:

true
false

This is the basic cycle: declare constructors, build values, match on values, and test behavior.

Takeaway

An inductive type is defined by its constructors. Pattern matching consumes values by considering those constructors, recursion follows the recursive structure of the type, and induction proves properties by the same cases. This single mechanism underlies data types, logical propositions, and many proof patterns in Lean.