We have seen that Lean’s formal foundation includes basic types, Prop, Type.{1}, Type.{2}, ..., and allows for the formation of dependent function types, Π x : A. B. In the examples, we have also made use of additional types like bool, nat, and int, and type constructors, like list, and product, ×. In fact, in Lean’s library, every concrete type other than the universes and every type constructor other than Pi is an instance of a general family of type constructions known as inductive types. It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, Pi types, and inductive types; everything else follows from those.

Intuitively, an inductive type is built up from a specified list of constructors. In Lean, the syntax for specifying such a type is as follows:

inductive foo : Type :=
| constructor₁ : ... → foo
| constructor₂ : ... → foo
...
| constructorₙ : ... → foo

The intuition is that each constructor specifies a way of building new objects of foo, possibly from previously constructed values. The type foo consists of nothing more than the objects that are constructed in this way. The first character | in an inductive declaration is optional. We can also separate constructors using a comma instead of |.

We will see below that the arguments to the constructors can include objects of type foo, subject to a certain “positivity” constraint, which guarantees that elements of foo are built from the bottom up. Roughly speaking, each ... can be any Pi type constructed from foo and previously defined types, in which foo appears, if at all, only as the “target” of the Pi type. For more details, see \cite{dybjer:94}.

We will provide a number of examples of inductive types. We will also consider slight generalizations of the scheme above, to mutually defined inductive types, and so-called inductive families.

As with the logical connectives, every inductive type comes with introduction rules, which show how to construct an element of the type, and elimination rules, which show how to “use” an element of the type in another construction. The analogy to the logical connectives should not come as a surprise; as we will see below, they, too, are examples of inductive type constructions. You have already seen the introduction rules for an inductive type: they are just the constructors that are specified in the definition of the type. The elimination rules provide for a principle of recursion on the type, which includes, as a special case, a principle of induction as well.

In the next chapter, we will describe Lean’s function definition package, which provides even more convenient ways to define functions on inductive types and carry out inductive proofs. But because the notion of an inductive type is so fundamental, we feel it is important to start with a low-level, hands-on understanding. We will start with some basic examples of inductive types, and work our way up to more elaborate and complex examples.

The simplest kind of inductive type is simply a type with a finite, enumerated list of elements.

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

The inductive command creates a new type, weekday. The constructors all live in the weekday namespace.

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

-- BEGIN
check weekday.sunday
check weekday.monday

open weekday

check sunday
check monday
-- END

Think of the sunday, monday, … as being distinct elements of weekday, with no other distinguishing properties. The elimination principle, weekday.rec, is defined at the same time as the type weekday and its constructors. It is also known as a recursor, and it is what makes the type “inductive”: it allows us to define a function on weekday by assigning values corresponding to each constructor. The intuition is that an inductive type is exhaustively generated by the constructors, and has no elements beyond those they construct.

We will use a slight (automatically generated) variant, weekday.rec_on, which takes its arguments in a more convenient order. Note that the shorter versions of names like weekday.rec and weekday.rec_on are not made available by default when we open the weekday namespace, to avoid clashes. If we import nat, we can use rec_on to define a function from weekday to the natural numbers:

import data.nat
open nat

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

-- BEGIN
definition number_of_day (d : weekday) : nat :=
weekday.rec_on d 1 2 3 4 5 6 7

eval number_of_day weekday.sunday
eval number_of_day weekday.monday
eval number_of_day weekday.tuesday
-- END

The first (explicit) argument to rec_on is the element being “analyzed.” The next seven arguments are the values corresponding to the seven constructors. Note that number_of_day weekday.sunday evaluates to 1: the computation rule for rec_on recognizes that sunday is a constructor, and returns the appropriate argument.

Below we will encounter a more restricted variant of rec_on, namely, cases_on. When it comes to enumerated types, rec_on and cases_on are the same. You may prefer to use the label cases_on, because it emphasizes that the definition is really a definition by cases.

import data.nat
open nat

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

-- BEGIN
definition number_of_day (d : weekday) : nat :=
weekday.cases_on d 1 2 3 4 5 6 7
-- END

It is often useful to group definitions and theorems related to a structure in a namespace with the same name. For example, we can put the number_of_day function in the weekday namespace. We are then allowed to use the shorter name when we open the namespace.

The names rec_on, cases_on, induction_on, and so on are generated automatically. As noted above, they are protected to avoid name clashes. In other words, they are not provided by default when the namespace is opened. However, you can explicitly declare abbreviations for them using the renaming option when you open a namespace.

import data.nat
open nat

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

-- BEGIN
namespace weekday
  local abbreviation cases_on := @weekday.cases_on

  definition number_of_day (d : weekday) : nat :=
  cases_on d 1 2 3 4 5 6 7
end weekday

eval weekday.number_of_day weekday.sunday

open weekday (renaming cases_on → cases_on)

eval number_of_day sunday
check cases_on
-- END

We can define functions from weekday to weekday:

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

-- BEGIN
namespace weekday
  definition next (d : weekday) : weekday :=
  weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday

  definition previous (d : weekday) : weekday :=
  weekday.cases_on d saturday sunday monday tuesday wednesday thursday friday

  eval next (next tuesday)
  eval next (previous tuesday)

  example : next (previous tuesday) = tuesday := rfl
end weekday
-- END

How can we prove the general theorem that next (previous d) = d for any weekday d? The induction principle parallels the recursion principle: we simply have to provide a proof of the claim for each constructor:

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

namespace weekday
  definition next (d : weekday) : weekday :=
  weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday

  definition previous (d : weekday) : weekday :=
  weekday.cases_on d saturday sunday monday tuesday wednesday thursday friday

-- BEGIN
  theorem next_previous (d: weekday) : next (previous d) = d :=
  weekday.induction_on d
    (show next (previous sunday) = sunday, from rfl)
    (show next (previous monday) = monday, from rfl)
    (show next (previous tuesday) = tuesday, from rfl)
    (show next (previous wednesday) = wednesday, from rfl)
    (show next (previous thursday) = thursday, from rfl)
    (show next (previous friday) = friday, from rfl)
    (show next (previous saturday) = saturday, from rfl)
-- END
end weekday

In fact, induction_on is just a special case of rec_on where the target type is an element of Prop. In other words, under the propositions-as-types correspondence, the principle of induction is a type of definition by recursion, where what is being “defined” is a proof instead of a piece of data. We could equally well have used cases_on:

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

namespace weekday
  definition next (d : weekday) : weekday :=
  weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday

  definition previous (d : weekday) : weekday :=
  weekday.cases_on d saturday sunday monday tuesday wednesday thursday friday

-- BEGIN
  theorem next_previous (d: weekday) : next (previous d) = d :=
  weekday.cases_on d
    (show next (previous sunday) = sunday, from rfl)
    (show next (previous monday) = monday, from rfl)
    (show next (previous tuesday) = tuesday, from rfl)
    (show next (previous wednesday) = wednesday, from rfl)
    (show next (previous thursday) = thursday, from rfl)
    (show next (previous friday) = friday, from rfl)
    (show next (previous saturday) = saturday, from rfl)
-- END
end weekday

While the show commands make the proof clearer and more readable, they are not necessary:

inductive weekday : Type :=
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

namespace weekday
  definition next (d : weekday) : weekday :=
  weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday

  definition previous (d : weekday) : weekday :=
  weekday.cases_on d saturday sunday monday tuesday wednesday thursday friday

-- BEGIN
  theorem next_previous (d: weekday) : next (previous d) = d :=
  weekday.cases_on d rfl rfl rfl rfl rfl rfl rfl
-- END
end weekday

Some fundamental data types in the Lean library are instances of enumerated types.

import standard

namespace hide

-- BEGIN
inductive empty : Type

inductive unit : Type :=
star : unit

inductive bool : Type :=
| ff : bool
| tt : bool
-- END

end hide

(To run these examples, we put them in a namespace called hide, so that a name like bool does not conflict with the bool in the standard library. This is necessary because these types are part of the Lean “prelude” that is automatically imported with the system is started.)

The type empty is an inductive datatype with no constructors. The type unit has a single element, star, and the type bool represents the familiar boolean values. As an exercise, you should think about what the introduction and elimination rules for these types do. As a further exercise, we suggest defining boolean operations band, bor, bnot on the boolean, and verifying common identities. Note that defining a binary operation like band will require nested cases splits:

import data.bool
open bool

namespace hide

-- BEGIN
definition band (b1 b2 : bool) : bool :=
bool.cases_on b1
  ff
  (bool.cases_on b2 ff tt)
-- END

end hide

Similarly, most identities can be proved by introducing suitable case splits, and then using rfl.

Enumerated types are a very special case of inductive types, in which the constructors take no arguments at all. In general, a “construction” can depend on data, which is then represented in the constructed argument. Consider the definitions of the product type and sum type in the library:

namespace hide

-- BEGIN
inductive prod (A B : Type) :=
mk : A → B → prod A B

inductive sum (A B : Type) : Type :=
| inl {} : A → sum A B
| inr {} : B → sum A B
-- END

end hide

For the moment, ignore the annotation {} after the constructors inl and inr; we will explain that below. In the meanwhile, think about what is going on in these examples. The product type has one constructor, prod.mk, which takes two arguments. To define a function on prod A B, we can assume the input is of the form prod.mk a b, and we have to specify the output, in terms of a and b. We can use this to define the two projections for prod; remember that the standard library defines notation A × B for prod A B and (a, b) for prod.mk a b.

import data.prod
open prod

namespace hide

-- BEGIN
definition pr1 {A B : Type} (p : A × B) : A :=
prod.rec_on p (λ a b, a)

definition pr2 {A B : Type} (p : A × B) : B :=
prod.rec_on p (λ a b, b)
-- END

end hide

The function pr1 takes a pair, p. Applying the recursor prod.rec_on p (fun a b, a) interprets p as a pair, prod.mk a b, and then uses the second argument to determine what to do with a and b.

Here is another example:

import data.bool data.prod data.nat data.prod data.sum
open prod sum nat bool
-- BEGIN
definition prod_example (p : bool × ℕ) : ℕ :=
prod.rec_on p (λ b n, cond b (2 * n) (2 * n + 1))

eval prod_example (tt, 3)
eval prod_example (ff, 3)
-- END

The cond function is a boolean conditional: cond b t1 t2 return t1 if b is true, and t2 otherwise. (It has the same effect as bool.rec_on b t2 t1.) The function prod_example takes a pair consisting of a boolean, b, and a number, n, and returns either 2 * n or 2 * n + 1 according to whether b is true or false.

In contrast, the sum type has two constructors, inl and inr (for “insert left” and “insert right”), each of which takes one (explicit) argument. To define a function on sum A B, we have to handle two cases: either the input is of the form inl a, in which case we have to specify an output value in terms of a, or the input is of the form inr b, in which case we have to specify an output value in terms of b.

import data.bool data.prod data.nat data.prod data.sum
open prod sum nat bool

-- BEGIN
definition sum_example (s : ℕ + ℕ) : ℕ :=
sum.cases_on s (λ n, 2 * n) (λ n, 2 * n + 1)

eval sum_example (inl 3)
eval sum_example (inr 3)
-- END

This example is similar to the previous one, but now an input to sum_example is implicitly either of the form inl n or inr n. In the first case, the function returns 2 * n, and the second case, it returns 2 * n + 1.

In the section after next we will see what happens when the constructor of an inductive type takes arguments from the inductive type itself. What characterizes the examples we consider in this section is that this is not the case: each constructor relies only on previously specified types.

Notice that a type with multiple constructors is disjunctive: an element of sum A B is either of the form inl a or of the form inl b. A constructor with multiple arguments introduces conjunctive information: from an element prod.mk a b of prod A B we can extract a and b. An arbitrary inductive type can include both features, by having any number of constructors, each of which takes any number of arguments.

A type, like prod, with only one constructor is purely conjunctive: the constructor simply packs the list of arguments into a single piece of data, essentially a tuple where the type of subsequent arguments can depend on the type of the initial argument. We can also think of such a type as a “record” or a “structure”. In Lean, these two words are synonymous, and provide alternative syntax for inductive types with a single constructor.

namespace hide

-- BEGIN
structure prod (A B : Type) :=
mk :: (pr1 : A) (pr2 : B)
-- END

end hide

The structure command simultaneously introduces the inductive type, prod, its constructor, mk, the usual eliminators (rec, rec_on), as well as the projections, pr1 and pr2, as defined above.

If you do not name the constructor, Lean uses mk as a default. For example, the following defines a record to store a color as a triple of RGB values:

open nat

-- BEGIN
record color := (red : nat) (green : nat) (blue : nat)
definition yellow := color.mk 255 255 0
eval color.red yellow
-- END

The definition of yellow forms the record with the three values shown, and the projection color.red returns the red component. The structure command is especially useful for defining algebraic structures, and Lean provides substantial infrastructure to support working with them. Here, for example, is the definition of a semigroup:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c))

We will see more examples in Chapter Structures and Records.

Notice that the product type depends on parameters A B : Type which are arguments to the constructors as well as prod. Lean detects when these arguments can be inferred from later arguments to a constructor, and makes them implicit in that case. Sometimes an argument can only be inferred from the return type, which means that it could not be inferred by parsing the expression from bottom up, but may be inferrable from context. In that case, Lean does not make the argument implicit by default, but will do so if we add the annotation {} after the constructor. We used that option, for example, in the definition of sum:

namespace hide

-- BEGIN
inductive sum (A B : Type) : Type :=
| inl {} : A → sum A B
| inr {} : B → sum A B
-- END

end hide

As a result, the argument A to inl and the argument B to inr are left implicit.

We have already discussed sigma types, also known as the dependent product:

namespace hide

-- BEGIN
inductive sigma {A : Type} (B : A → Type) :=
dpair : Π a : A, B a → sigma B
-- END

end hide

Two more examples of inductive types in the library are the following:

namespace hide

-- BEGIN
inductive option (A : Type) : Type :=
| none {} : option A
| some    : A → option A

inductive inhabited (A : Type) : Type :=
mk : A → inhabited A
-- END

end hide

In the semantics of dependent type theory, there is no built-in notion of a partial function. Every element of a function type A → B or a Pi type Π x : A, B is assumed to have a value at every input. The option type provides a way of representing partial functions. An element of option B is either none or of the form some b, for some value b : B. Thus we can think of an element f of the type A → option B as being a partial function from A to B: for every a : A, f a either returns none, indicating the f a is “undefined”, or some b.

An element of inhabited A is simply a witness to the fact that there is an element of A. Later, we will see that inhabited is an example of a type class in Lean: Lean can be instructed that suitable base types are inhabited, and can automatically infer that other constructed types are inhabited on that basis.

As exercises, we encourage you to develop a notion of composition for partial functions from A to B and B to C, and show that it behaves as expected. We also encourage you to show that bool and nat are inhabited, that the product of two inhabited types is inhabited, and that the type of functions to an inhabited type is inhabited.

Inductively defined types can live in any type universe, including the bottom-most one, Prop. In fact, this is exactly how the logical connectives are defined.

namespace hide

-- BEGIN
inductive false : Prop

inductive true : Prop :=
intro : true

inductive and (a b : Prop) : Prop :=
intro : a → b → and a b

inductive or (a b : Prop) : Prop :=
| intro_left  : a → or a b
| intro_right : b → or a b
-- END

end hide

You should think about how these give rise to the introduction and elimination rules that you have already seen. There are rules that govern what the eliminator of an inductive type can eliminate to, that is, what kinds of types can be the target of a recursor. Roughly speaking, what characterizes inductive types in Prop is that one can only eliminate to other types in Prop. This is consistent with the understanding that if P : Prop, an element p : P carries no data. There is a small exception to this rule, however, which we will discuss below, in the section on inductive families.

Even the existential quantifier is inductively defined:

namespace hide

-- BEGIN
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P

definition exists.intro := @Exists.intro
-- END

end hide

Keep in mind that the notation ∃ x : A, P is syntactic sugar for Exists (λ x : A, P).

The definitions of false, true, and, and or are perfectly analogous to the definitions of empty, unit, prod, and sum. The difference is that the first group yields elements of Prop, and the second yields elements of Type.{i} for i greater than 0. In a similar way, ∃ x : A, P is a Prop-valued variant of Σ x : A, P.

This is a good place to mention another inductive type, denoted {x : A | P}, which is sort of a hybrid between ∃ x : A, P and Σ x : A, P.

namespace hide

-- BEGIN
inductive subtype {A : Type} (P : A → Prop) : Type :=
tag : Π x : A, P x → subtype P
-- END

end hide

The notation {x : A | P} is syntactic sugar for subtype (λ x : A, P). It is modeled after subset notation in set theory: the idea is that {x : A | P} denotes the collection of elements of A that have property P.

The inductively defined types we have seen so far are “flat”: constructors wrap data and insert it into a type, and the corresponding recursor unpacks the data and acts on it. Things get much more interesting when the constructors act on elements of the very type being defined. A canonical example is the type nat of natural numbers:

namespace hide

-- BEGIN
inductive nat : Type :=
| zero : nat
| succ : nat → nat
-- END

end hide

There are two constructors. We start with zero : nat; it takes no arguments, so we have it from the start. In contrast, the constructor succ can only be applied to a previously constructed nat. Applying it to zero yields succ zero : nat. Applying it again yields succ (succ zero) : nat, and so on. Intuitively, nat is the “smallest” type with these constructors, meaning that it is exhaustively (and freely) generated by starting with zero and applying succ repeatedly.

As before, the recursor for nat is designed to define a dependent function f from nat to any domain, that is, an element f of Π n : nat, C n for some C : nat → Type. It has to handle two cases: the case where the input is zero, and the case where the input is of the form succ n for some n : nat. In the first case, we simply specify a target value with the appropriate type, as before. In the second case, however, the recursor can assume that a value of f at n has already been computed. As a result, the next argument to the recursor specifies a value for f (succ n) in terms of n and f n. If we check the type of the recursor,

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat
-- BEGIN
check @nat.rec_on
-- END

end hide

we find the following:

Π {C : nat → Type} (n : nat),
  C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n

The implicit argument, C, is the codomain of the function being defined. In type theory it is common to say C is the motive for the elimination/recursion. The next argument, n : nat, is the input to the function. It is also known as the major premise. Finally, the two arguments after specify how to compute the zero and successor cases, as described above. They are also known as the minor premises.

Consider, for example, the addition function add m n on the natural numbers. Fixing m, we can define addition by recursion on n. In the base case, we set add m zero to m. In the successor step, assuming the value add m n is already determined, we define add m (succ n) to be succ (add m n).

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat
-- BEGIN
namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (λ n add_m_n, succ add_m_n)

-- try it out
eval add (succ zero) (succ (succ zero))

end nat
-- END

end hide

It is useful to put such definitions into a namespace, nat. We can then go on to define familiar notation in that namespace. The two defining equations for addition now hold definitionally:

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat

namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)
-- BEGIN
notation 0 := zero
infix `+` := add

theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl
-- END
end nat

end hide

Proving a fact like 0 + m = m, however, requires a proof by induction. As observed above, the induction principle is just a special case of the recursion principle, when the codomain C n is an element of Prop. It represents the familiar pattern of an inductive proof: to prove ∀ n, C n, first prove C 0, and then, for arbitrary n, assume IH : C n and prove C (succ n).

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat

namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)

notation 0 := zero
infix `+` := add

theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl
-- BEGIN
local abbreviation induction_on := @nat.induction_on

theorem zero_add (n : nat) : 0 + n = n :=
induction_on n
  (show 0 + 0 = 0, from rfl)
  (take n,
    assume IH : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
          ... = succ n : IH)
-- END
end nat

end hide

In the example above, we encourage you to replace induction_on with rec_on and observe that the theorem is still accepted by Lean. As we have seen above, induction_on is just a special case of rec_on.

For another example, let us prove the associativity of addition, ∀ m n k, m + n + k = m + (n + k). (The notation +, as we have defined it, associates to the left, so m + n + k is really (m + n) + k.) The hardest part is figuring out which variable to do the induction on. Since addition is defined by recursion on the second argument, k is a good guess, and once we make that choice the proof almost writes itself:

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat

namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)

notation 0 := zero
infix `+` := add

theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl

local abbreviation induction_on := @nat.induction_on

theorem zero_add (n : nat) : 0 + n = n :=
induction_on n
  (show 0 + 0 = 0, from rfl)
  (take n,
    assume IH : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
          ... = succ n : IH)

-- BEGIN
theorem add_assoc (m n k : nat) : m + n + k = m + (n + k) :=
induction_on k
  (show m + n + 0 = m + (n + 0), from rfl)
  (take k,
    assume IH : m + n + k = m + (n + k),
    show m + n + succ k = m + (n + succ k), from
      calc
        m + n + succ k = succ (m + n + k) : rfl
          ... = succ (m + (n + k)) : IH
          ... = m + succ (n + k) : rfl
          ... = m + (n + succ k) : rfl)
-- END
end nat

end hide

For another example, suppose we try to prove the commutativity of addition. Choosing induction on the second argument, we might begin as follows:

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat

namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)

notation 0 := zero
infix `+` := add

theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl

local abbreviation induction_on := @nat.induction_on

theorem zero_add (n : nat) : 0 + n = n :=
induction_on n
  (show 0 + 0 = 0, from rfl)
  (take n,
    assume IH : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
          ... = succ n : IH)

attribute add [reducible]
theorem add_assoc (m n k : nat) : m + n + k = m + (n + k) :=
induction_on k rfl (fun k IH, eq.subst IH rfl)

-- BEGIN
theorem add_comm (m n : nat) : m + n = n + m :=
induction_on n
  (show m + 0 = 0 + m, from eq.symm (zero_add m))
  (take n,
    assume IH : m + n = n + m,
    calc
      m + succ n = succ (m + n) : rfl
        ... = succ (n + m) : IH
        ... = succ n + m : sorry)
-- END
end nat

end hide

At this point, we see that we need another supporting fact, namely, that succ (n + m) = succ n + m. We can prove this by induction on m:

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat

namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)

notation 0 := zero
infix `+` := add

theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl

local abbreviation induction_on := @nat.induction_on

theorem zero_add (n : nat) : 0 + n = n :=
induction_on n
  (show 0 + 0 = 0, from rfl)
  (take n,
    assume IH : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
          ... = succ n : IH)

attribute add [reducible]
theorem add_assoc (m n k : nat) : m + n + k = m + (n + k) :=
induction_on k rfl (take k IH, eq.subst IH rfl)

-- BEGIN
theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
induction_on n
  (show succ m + 0 = succ (m + 0), from rfl)
  (take n,
    assume IH : succ m + n = succ (m + n),
    show succ m + succ n = succ (m + succ n), from
      calc
        succ m + succ n = succ (succ m + n) : rfl
          ... = succ (succ (m + n)) : IH
          ... = succ (m + succ n) : rfl)
-- END
end nat

end hide

We can then replace the sorry in the previous proof with succ_add.

As an exercise, try defining other operations on the natural numbers, such as multiplication, the predecessor function (with pred 0 = 0), truncated subtraction (with n - m = 0 when m is greater than or equal to n), and exponentiation. Then try proving some of their basic properties, building on the theorems we have already proved.

namespace hide

inductive nat : Type :=
| zero : nat
| succ : nat → nat

namespace nat

definition add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)

notation 0 := zero
infix `+` := add

theorem add_zero (m : nat) : m + 0 = m := rfl

theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl

local abbreviation induction_on := @nat.induction_on

theorem zero_add (n : nat) : 0 + n = n :=
induction_on n
  (show 0 + 0 = 0, from rfl)
  (take n,
    assume IH : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
          ... = succ n : IH)

attribute add [reducible]
theorem add_assoc (m n k : nat) : m + n + k = m + (n + k) :=
induction_on k rfl (take k IH, eq.subst IH rfl)

theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
induction_on n
  (show succ m + 0 = succ (m + 0), from rfl)
  (take n,
    assume IH : succ m + n = succ (m + n),
    show succ m + succ n = succ (m + succ n), from
      calc
        succ m + succ n = succ (succ m + n) : rfl
          ... = succ (succ (m + n)) : IH
          ... = succ (m + succ n) : rfl)

theorem add_comm (m n : nat) : m + n = n + m :=
induction_on n
  (show m + 0 = 0 + m, from eq.symm (zero_add m))
  (take n,
    assume IH : m + n = n + m,
    calc
      m + succ n = succ (m + n) : rfl
        ... = succ (n + m) : IH
        ... = succ n + m : succ_add)

-- BEGIN
-- define mul by recursion on the second argument
definition mul (m n : nat) : nat := sorry

infix `*` := mul

-- these should be proved by rfl
theorem mul_zero (m : nat) : m * 0 = 0 := sorry
theorem mul_succ (m n : nat) : m * (succ n) = m * n + m := sorry

theorem zero_mul (n : nat) : 0 * n = 0 := sorry

theorem mul_distrib (m n k : nat) : m * (n + k) = m * n + m * k := sorry

theorem mul_assoc (m n k : nat) : m * n * k = m * (n * k) := sorry

-- hint: you will need to prove an auxiliary statement
theorem mul_comm (m n : nat) : m * n = n * m := sorry

definition pred (n : nat) : nat := nat.cases_on n zero (fun n, n)

theorem pred_succ (n : nat) : pred (succ n) = n := sorry

theorem succ_pred (n : nat) : n ≠ 0 → succ (pred n) = n := sorry
-- END
end nat

end hide

Let us consider some more examples of inductively defined types. For any type, A, the type list A of lists of elements of A is defined in the library.

namespace hide
-- BEGIN
inductive list (A : Type) : Type :=
| nil {} : list A
| cons : A → list A → list A

namespace list

variable {A : Type}

notation h :: t  := cons h t

definition append (s t : list A) : list A :=
list.rec t (λ x l u, x::u) s

notation s ++ t := append s t

theorem nil_append (t : list A) : nil ++ t = t := rfl

theorem cons_append (x : A) (s t : list A) : x::s ++ t = x::(s ++ t) := rfl

end list
-- END
end hide

A list of elements of type A is either the empty list, nil, or an element h : A followed by a list t : list A. We define the notation h :: t to represent the latter. The first element, h, is commonly known as the “head” of the list, and the remainder, t, is known as the “tail.” Recall that the notation {} in the definition of the inductive type ensures that the argument to nil is implicit. In most cases, it can be inferred from context. When it cannot, we have to write @nil A to specify the type A.

Lean allows us to define iterative notation for lists:

namespace hide

-- BEGIN
inductive list (A : Type) : Type :=
| nil {} : list A
| cons : A → list A → list A

namespace list

notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l

section
  open nat
  check [1, 2, 3, 4, 5]
  check ([1, 2, 3, 4, 5] : list ℕ)
end

end list
-- END

end hide

In the first check, Lean assumes that [1, 2, 3, 4, 5] is merely a list of numerals. The (t : list ℕ) expression forces Lean to interpret t as a list of natural numbers.

As an exercise, prove the following:

namespace hide

inductive list (A : Type) : Type :=
| nil {} : list A
| cons : A → list A → list A

namespace list

notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l

variable {A : Type}

notation h :: t  := cons h t

definition append (s t : list A) : list A :=
list.rec_on s t (λ x l u, x::u)

notation s ++ t := append s t

theorem nil_append (t : list A) : nil ++ t = t := rfl

theorem cons_append (x : A) (s t : list A) : x::s ++ t = x::(s ++ t) := rfl

-- BEGIN
theorem append_nil (t : list A) : t ++ nil = t := sorry

theorem append_assoc (r s t : list A) : r ++ s ++ t = r ++ (s ++ t) := sorry
-- END

end list

end hide

Try also defining the function length : Π A : Type, list A → nat that returns the length of a list, and prove that it behaves as expected (for example, length (s ++ t) = length s + length t).

For another example, we can define the type of binary trees:

inductive binary_tree :=
| leaf : binary_tree
| node : binary_tree → binary_tree → binary_tree

In fact, we can even define the type of countably branching trees:

import data.nat
open nat

inductive cbtree :=
| leaf : cbtree
| sup : (ℕ → cbtree) → cbtree

namespace cbtree

definition succ (t : cbtree) : cbtree :=
sup (λ n, t)

definition omega : cbtree :=
sup (nat.rec leaf (λ n t, succ t))

end cbtree

We now consider two generalizations of inductive types that are sometimes useful. First, Lean supports mutually defined inductive types. The idea is that we can define two (or more) inductive types at the same time, where each one refers to the other.

inductive tree (A : Type) : Type :=
| node : A → forest A → tree A
with forest : Type :=
| nil  : forest A
| cons : tree A → forest A → forest A

In this example, a tree with elements labeled from A is of the form node a f, where a is an element of A (the label), and f a forest. At the same time, a forest of trees with elements labeled from A is essentially defined to be a list of trees.

A more powerful generalization is given by the possibility of defining inductive type families. There are indexed families of types defined by a simultaneous induction of the following form:

inductive foo : ... → Type :=
| constructor₁ : ... → foo ...
| constructor₂ : ... → foo ...
...
| constructorₙ : ... → foo ...

In contrast to ordinary inductive definition, which construct an element of Type, the more general version constructs a function ... → Type, where ”...” denotes a sequence of argument types, also known as indices. Each constructor then constructs an element of some type in the family. One example is the definition of vector A n, the type of vectors of elements of A of length n:

open nat
namespace hide

-- BEGIN
inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero
| cons   : Π {n}, A → vector A n → vector A (succ n)
-- END

end hide

Notice that the cons constructor takes an element of vector A n, and returns an element of vector A (succ n), thereby using an element of one member of the family to build an element of another.

Another example is given by the family of types fin n. For each n, fin n is supposed to denote a generic type of n elements:

namespace hide

-- BEGIN
inductive fin : nat → Type :=
| fz : Π n, fin (nat.succ n)
| fs : Π {n}, fin n → fin (nat.succ n)
-- END

end hide

This example may be hard to understand, so you should take the time to think about how it works.

Yet another example is given by the definition of the equality type in the library:

namespace hide

-- BEGIN
inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a
-- END

end hide

For each fixed A : Type and a : A, this definition constructs a family of types eq a x, indexed by x : A. Notably, however, there is only one constructor, refl, which is an element of eq a a. Intuitively, the only way to construct a proof of eq a x is to use reflexivity, in the case where x is a. Note that eq a a is the only inhabited type in the family of types eq a x. The elimination principle generated by Lean says that eq is the least reflexive relation on A. The eliminator/recursor for eq is of the following form:

eq.rec_on : Π {A : Type} {a : A} {C : A → Type} {b : A}, a = b → C a → C b

It is a remarkable fact that all the basic axioms for equality follow from the constructor, refl, and the eliminator, eq.rec_on.

This eliminator illustrates the exception to the fact that inductive definitions living in Prop can only eliminate to Prop. Because there is only one constructor to eq, it carries no information, other than the type is inhabited, and Lean’s internal logic allows us to eliminate to an arbitrary Type. This is how we define a cast operation that casts an element from type A into B when a proof p : eq A B is provided:

namespace hide

inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a

-- BEGIN
theorem cast {A B : Type} (p : eq A B) (a : A) : B :=
eq.rec_on p a
-- END

end hide

The recursor eq.rec_on is also used to define substitution:

namespace hide

inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a

-- BEGIN
theorem subst {A : Type} {a b : A} {P : A → Prop}
  (H₁ : eq a b) (H₂ : P a) : P b :=
eq.rec H₂ H₁
-- END

end hide

Using the recursor with H₁ : a = b, we may assume a and b are the same, in which case, P b and P a are the same.

It is not hard to prove that eq is symmetric and transitive. In the following example, we prove symm and leave as exercise the theorems trans and congr (congruence).

namespace hide

inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a

theorem subst {A : Type} {a b : A} {P : A → Prop}
  (H₁ : eq a b) (H₂ : P a) : P b :=
eq.rec H₂ H₁

-- BEGIN
theorem symm {A : Type} {a b : A} (H : eq a b) : eq b a :=
subst H (eq.refl a)

theorem trans {A : Type} {a b c : A} (H₁ : eq a b) (H₂ : eq b c) : eq a c :=
sorry

theorem congr {A B : Type} {a b : A} (f : A → B) (H : eq a b) : eq (f a) (f b) :=
sorry
-- END

end hide

In the type theory literature, there are further generalizations of inductive definitions, for example, the principles of induction-recursion and induction-induction. These are not supported by Lean.

Given A : Type and B : A → Type, suppose we want to generalize the congruence theorem congr in the previous example to dependent functions f : Π x : A, B x. Roughly speaking, we would like to have a theorem that, says that if a = b, then f a = f b. The first obstacle is stating the theorem: the term eq (f a) (f b) is not type correct since f a has type B a, f b has type B b, and the equality predicate eq expects both arguments to have the same type. Notice that f a has type B a, so the term eq.rec_on H (f a) has type B b. You should think of eq.rec_on H (f a) as ”f a, viewed as an element of B b.” We can then write eq (eq.rec_on H (f a)) (f b) to express that f a and f b are equal, modulo the difference between their types. Here is a proof of the generalized congruence theorem, with this approach:

namespace hide

inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a

-- BEGIN
theorem hcongr {A : Type} {B : A → Type} {a b : A} (f : Π x : A, B x)
               (H : eq a b) : eq (eq.rec_on H (f a)) (f b) :=
have h₁ : ∀ h : eq a a, eq (eq.rec_on h (f a)) (f a), from
  assume h : eq a a, eq.refl (eq.rec_on h (f a)),
have h₂ : ∀ h : eq a b, eq (eq.rec_on h (f a)) (f b), from
  eq.rec_on H h₁,
show eq (eq.rec_on H (f a)) (f b), from
  h₂ H
-- END

end hide

Another option is to define a heterogeneous equality heq that can equate terms of different types, so that we can write heq (f a) (f b) instead of eq (eq.rec_on H (f a)) (f b). It is straightforward to define such an equality in Lean:

namespace hide

-- BEGIN
inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
refl : heq a a
-- END

end hide

Moreover, given a b : A, we can prove heq a b → eq a b using proof irrelevance. This theorem is called heq.to_eq in the Lean standard library. We can now state and prove hcongr using heterogeneous equality. Note the proof is also more compact and easier to understand.

namespace hide

inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a

inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
refl : heq a a

-- BEGIN
theorem hcongr {A : Type} {B : A → Type} {a b : A} (f : Π x : A, B x)
               (H : eq a b) : heq (f a) (f b) :=
eq.rec_on H (heq.refl (f a))
-- END

end hide

Heterogeneous equality, which gives elements of different types the illusion that they can be considered equal, is sometimes called John Major equality. (The name is a bit of political humor, due to Conor McBride.)

In the previous sections, we have seen that whenever we declare an inductive datatype I, the Lean kernel automatically declares its constructors (aka introduction rules), and generates and declares the eliminator/recursor I.rec. The eliminator expresses a principle of definition by recursion, as well as the principle of proof by induction. The kernel also associates a computational rule which determines how these definitions are eliminated when terms and proofs are normalized.

Consider, for example, the natural numbers. Given the motive C : nat → Type, and minor premises fz : C zero and fs : Π (n : nat), C n → C (succ n), we have the following two computational rules: nat.rec fz fs zero reduces to fz, and nat.rec fz fs (succ a) reduces to fs a (nat.rec fz fs a).

open nat

variable C  : nat → Type
variable fz : C zero
variable fs : Π (n : nat), C n → C (succ n)

eval nat.rec fz fs zero
-- nat.rec_on is defined from nat.rec
eval nat.rec_on zero fz fs

example : nat.rec fz fs zero = fz :=
rfl

variable a : nat

eval nat.rec fz fs (succ a)
eval nat.rec_on (succ a) fz fs

example (a : nat) : nat.rec fz fs (succ a) = fs a (nat.rec fz fs a) :=
rfl

The source code that validates an inductive declaration and generates the eliminator/recursor and computational rules is part of the Lean kernel. The kernel is also known as the trusted code base, because a bug in the kernel may compromise the soundness of the whole system.

When you define an inductive datatype, Lean automatically generates a number of useful definitions. We have already seen some of them: rec_on, induction_on, and cases_on. The module M that generates these definitions is not part of the trusted code base. A bug in M does not compromise the soundness of the whole system, since the kernel will catch such errors when type checking any incorrectly generated definition produced by M.

As described before, rec_on just uses its arguments in a more convenient order than rec. In rec_on, the major premise is provided before the minor premises. Constructions using rec_on are often easier to read and understand than the equivalent ones using rec.

open nat

print definition nat.rec_on

definition rec_on {C : nat → Type} (n : nat)
                  (fz : C zero) (fs : Π a, C a → C (succ a)) : C n :=
nat.rec fz fs n

Moreover, induction_on is just a special case of rec_on where the motive C is a proposition. Finally, cases_on is a special case of rec_on where the inductive/recursive hypotheses are omitted in the minor premises. For example, in nat.cases_on the minor premise fs has type Π (n : nat), C (succ n) instead of Π (n : nat), C n → C (succ n). Note that the inductive/recursive hypothesis C n has been omitted.

namespace hide
-- BEGIN
open nat

print definition nat.induction_on
print definition nat.cases_on

definition induction_on {C : nat → Prop} (n : nat)
                        (fz : C zero) (fs : Π a, C a → C (succ a)) : C n :=
nat.rec_on n fz fs

definition cases_on {C : nat → Prop} (n : nat)
                    (fz : C zero) (fs : Π a, C (succ a)) : C n :=
nat.rec_on n fz (fun (a : nat) (r : C a), fs a)
-- END
end hide

For any inductive datatype that is not a proposition, we can show that its constructors are injective and disjoint. For example, on nat, we can show that succ a = succ b → a = b (injectivity), and succ a ≠ zero (disjointness). Both proofs can be performed using the automatically generated definition nat.no_confusion. More generally, for any inductive datatype I that is not a proposition, Lean automatically generates a definition of I.no_confusion. Given a motive C and an equality h : c₁ t = c₂ s, where c₁ and c₂ are two distinct I constructors, I.no_confusion constructs an inhabitant of C. This is essentially the principle of explosion, that is, the fact that anything follows from a contradiction. On the other hand, given a proof of c t = c s with the same constructor on both sides and a proof of t = s → C, I.no_confusion returns an inhabitant of C.

Let us illustrate by considering the constructions for the type nat. The type of no_confusion is based on the auxiliary definition no_confusion_type:

open nat

check @nat.no_confusion
-- Π {P : Type} {v1 v2 : ℕ}, v1 = v2 → nat.no_confusion_type P v1 v2

check nat.no_confusion_type
-- Type → ℕ → ℕ → Type

Note that the motive is an implicit argument in no_confusion. The constructions work as follows:

open nat
-- BEGIN
variable C : Type
variables a b : nat

eval nat.no_confusion_type C zero     (succ a)
-- C
eval nat.no_confusion_type C (succ a) zero
-- C
eval nat.no_confusion_type C zero     zero
-- C → C
eval nat.no_confusion_type C (succ a) (succ b)
-- (a = b → C) → C
-- END

In other words, from a proof of zero = succ a or succ a = 0, we obtain an element of any type C at will. On the other hand, a proof of zero = zero provides no help in constructing an element of type C, whereas a proof of succ a = succ b reduces the task of constructing an element of type C to the task of constructing such an element under the additional hypothesis a = b.

It is not hard to prove that constructors are injective and disjoint using no_confusion. In the following example, we prove these two properties for nat and leave as exercise the equivalent proofs for trees.

open nat

theorem succ_ne_zero (a : nat) (h : succ a = zero) : false :=
nat.no_confusion h

theorem succ.inj (a b : nat) (h : succ a = succ b) : a = b :=
nat.no_confusion h (fun e : a = b, e)

inductive tree (A : Type) : Type :=
| leaf : A → tree A
| node : tree A → tree A → tree A

open tree

variable {A : Type}

theorem leaf_ne_node {a : A} {l r : tree A}
                     (h : leaf a = node l r) : false :=
sorry

theorem leaf_inj {a b : A} (h : leaf a = leaf b) : a = b :=
sorry

theorem node_inj_left {l1 r1 l2 r2 : tree A}
                      (h : node l1 r1 = node l2 r2) : l1 = l2 :=
sorry

theorem node_inj_right {l1 r1 l2 r2 : tree A}
                       (h : node l1 r1 = node l2 r2) : r1 = r2 :=
sorry

If a constructor contains dependent arguments (such as sigma.mk), the generated no_confusion uses heterogeneous equality to equate arguments of different types:

variables (A : Type) (B : A → Type)
variables (a1 a2 : A) (b1 : B a1) (b2 : B a2)
variable  (C : Type)

-- Remark: b1 and b2 have different types

eval sigma.no_confusion_type C (sigma.mk a1 b1) (sigma.mk a2 b2)
-- (a1 = a2 → b1 == b2 → C) → C

Lean also generates the predicate transformer below and the recursor brec_on. It is unlikely that you will ever need to use these constructions directly; they are auxiliary definitions used by the recursive equation compiler we will describe in the next chapter, and we will not discuss them further here.

Since an inductive type lives in Type.{i} for some i, it is reasonable to ask which universe levels i can be instantiated to. The goal of this section is to explain the relevant constraints.

In the standard library, there are two cases, depending on whether the inductive type is specified to land in Prop. Let us first consider the case where the inductive type is not specified to land in Prop, which is the only case that arises in the homotopy type theory instantiation of the kernel. Recall that each constructor c in the definition of a family C of inductive types is of the form

c : Π (a : A) (b : B[a]), C a p[a,b]

where a is a sequence of datatype parameters, b is the sequence of arguments to the constructors, and p[a, b] are the indices, which determine which element of the inductive family the construction inhabits. Then the universe level i of C is constrained to satisfy the following:

For each constructor c as above, and each Bk[a] in the sequence B[a], if Bk[a] : Type.{j}, we have i ≥ j.

In other words, the universe level i is required to be at least as large as the universe level of each type that represents an argument to a constructor.

When the inductive type C is specified to land in Prop, there are no constraints on the universe levels of the constructor arguments. But these universe levels do have a bearing on the elimination rule. Generally speaking, for an inductive type in Prop, the motive of the elimination rule is required to be in Prop. The exception we alluded to in the discussion of equality above is this: we are allowed to eliminate to an arbitrary Type when there is only one constructor, and each constructor argument is either in Prop or an index. This exception, which makes it possible to treat ordinary equality and heterogeneous equality as inductive types, can be justified by the fact that the elimination rule cannot take advantage of any “hidden” information.

Because inductive types can be polymorphic over universe levels, whether an inductive definition lands in Prop could, in principle, depend on how the universe levels are instantiated. To simplify the generation of the recursors, Lean adopts a convention that rules out this ambiguity: if you do not specify that the inductive type is an element of Prop, Lean requires the universe level to be at least one. Hence, a type specified by single inductive definition is either always in Prop or never in Prop. For example, if A and B are elements of Prop, A × B is assumed to have universe level at least one, representing a datatype rather than a proposition. The analogous definition of A × B, where A and B are restricted to Prop and the resulting type is declared to be an element of Prop instead of Type, is exactly the definition of A ∧ B.