# 1.16 Inductive Types Introduction

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.

```lean id="jrt18j"
inductive Color where
  | red
  | green
  | blue
deriving Repr
```

This declares a type named `Color` with three constructors:

```lean id="x4pnrw"
#check Color
#check Color.red
#check Color.green
#check Color.blue
```

Typical output:

```text id="kc26fm"
Color : Type
Color.red : Color
Color.green : Color
Color.blue : Color
```

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

```lean id="gpqr4c"
#eval Color.red
```

Expected output:

```text id="oh0m70"
Color.red
```

## Constructors

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

For an enumeration, constructors take no arguments.

```lean id="yqemwe"
inductive Direction where
  | north
  | south
  | east
  | west
deriving Repr
```

Each constructor is a value:

```lean id="u9f6ol"
#check Direction.north
```

Output:

```text id="cyyx7t"
Direction.north : Direction
```

For a type with data, constructors take arguments.

```lean id="1zvvop"
inductive Shape where
  | circle (radius : Nat)
  | rectangle (width height : Nat)
deriving Repr
```

Now the constructors are functions:

```lean id="8hu0ab"
#check Shape.circle
#check Shape.rectangle
```

Typical output:

```text id="pj5tzx"
Shape.circle : Nat -> Shape
Shape.rectangle : Nat -> Nat -> Shape
```

Use them to build values:

```lean id="z4intq"
#eval Shape.circle 10
#eval Shape.rectangle 3 4
```

## Pattern Matching on Inductive Types

Define functions by matching on constructors.

```lean id="oqkkiw"
def isPrimary : Color -> Bool
| Color.red   => true
| Color.green => true
| Color.blue  => true
```

A more useful example:

```lean id="2zdm1q"
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:

```text id="xwsndm"
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.

```lean id="0uw8u7"
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:

```lean id="8eoioe"
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.

```lean id="o8as55"
def NatList.length : NatList -> Nat
| NatList.nil => 0
| NatList.cons _ tail => NatList.length tail + 1

#eval NatList.length xs
```

Expected output:

```text id="bo2cuv"
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.

```lean id="8f6nxf"
inductive Box (α : Type) where
  | mk (value : α)
deriving Repr
```

Use it with different element types:

```lean id="v7s7vb"
#check Box Nat
#check Box String
#eval Box.mk 5
#eval Box.mk "Lean"
```

A more familiar example is an optional value type:

```lean id="gsltmf"
inductive Maybe (α : Type) where
  | none
  | some (value : α)
deriving Repr
```

This resembles Lean's built-in `Option`.

```lean id="6qs1vc"
#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.

```lean id="45et5z"
#check Maybe.none
#check Maybe.some
```

You may open the namespace:

```lean id="7w7agi"
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.

```lean id="nb42i9"
inductive Even : Nat -> Prop where
  | zero : Even 0
  | step {n : Nat} : Even n -> Even (n + 2)
```

This defines a proposition `Even n`.

```lean id="zb6wj9"
#check Even
#check Even.zero
#check Even.step
```

Typical output:

```text id="obd4sv"
Even : Nat -> Prop
Even.zero : Even 0
Even.step : Even n -> Even (n + 2)
```

A proof that `4` is even:

```lean id="vxm37f"
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.

```lean id="70skba"
#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`.

```lean id="4msb6r"
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.

```lean id="f7nyfl"
inductive Status where
  | pending
  | done
  | failed
deriving Repr, DecidableEq
```

Now Lean can print values and decide equality.

```lean id="g9a6sr"
#eval Status.pending == Status.done
#eval Status.done == Status.done
```

Expected output:

```text id="nbm8oh"
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.

```lean id="e2nbzc"
inductive Result where
  | ok (value : Nat)
  | error (message : String)
deriving Repr
```

Then define behavior by cases.

```lean id="itqn95"
def Result.isOk : Result -> Bool
| Result.ok _ => true
| Result.error _ => false
```

Test examples.

```lean id="95fab5"
#eval Result.isOk (Result.ok 10)
#eval Result.isOk (Result.error "bad input")
```

Expected output:

```text id="zb9d1s"
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.