7.1. Enumerated Types🔗

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

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

Weekday.sunday : Weekday

Weekday.monday : Weekday

Weekday.sunday : Weekday

Weekday.monday : Weekday

You can omit : Weekday when declaring the Weekday inductive type.

Think of sunday, monday, ... , saturday as being distinct elements of Weekday, with no other distinguishing properties. The elimination principle, Weekday.rec, is defined along with 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 the match expression to define a function from Weekday to the natural numbers:

1

2

3

When using Lean's logic, the match expression is compiled using the recursor Weekday.rec generated when you declare the inductive type. This ensures that the resulting term is well-defined in the type theory. For compiled code, match is compiled as in other functional programming languages.

def numberOfDay : (d : Weekday) → Nat :=
fun (d : Weekday) =>
  numberOfDay.match_1.{1} (fun (d : Weekday) => Nat) d
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 5) (instOfNatNat (nat_lit 5)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 6) (instOfNatNat (nat_lit 6))) fun (_ : Unit) =>
    @OfNat.ofNat.{0} Nat (nat_lit 7) (instOfNatNat (nat_lit 7))

@[instance_reducible] def numberOfDay.match_1.{u_1} : (motive : Weekday → Sort u_1) →
  (d : Weekday) →
    (h_1 : (_ : Unit) → motive Weekday.sunday) →
      (h_2 : (_ : Unit) → motive Weekday.monday) →
        (h_3 : (_ : Unit) → motive Weekday.tuesday) →
          (h_4 : (_ : Unit) → motive Weekday.wednesday) →
            (h_5 : (_ : Unit) → motive Weekday.thursday) →
              (h_6 : (_ : Unit) → motive Weekday.friday) → (h_7 : (_ : Unit) → motive Weekday.saturday) → motive d :=
fun (motive : Weekday → Sort u_1) (d : Weekday) (h_1 : (_ : Unit) → motive Weekday.sunday)
    (h_2 : (_ : Unit) → motive Weekday.monday) (h_3 : (_ : Unit) → motive Weekday.tuesday)
    (h_4 : (_ : Unit) → motive Weekday.wednesday) (h_5 : (_ : Unit) → motive Weekday.thursday)
    (h_6 : (_ : Unit) → motive Weekday.friday) (h_7 : (_ : Unit) → motive Weekday.saturday) =>
  @Weekday.casesOn.{u_1} (fun (x : Weekday) => motive x) d (h_1 Unit.unit) (h_2 Unit.unit) (h_3 Unit.unit)
    (h_4 Unit.unit) (h_5 Unit.unit) (h_6 Unit.unit) (h_7 Unit.unit)

@[reducible] def Weekday.casesOn.{u} : {motive : (t : Weekday) → Sort u} →
  (t : Weekday) →
    (sunday : motive Weekday.sunday) →
      (monday : motive Weekday.monday) →
        (tuesday : motive Weekday.tuesday) →
          (wednesday : motive Weekday.wednesday) →
            (thursday : motive Weekday.thursday) →
              (friday : motive Weekday.friday) → (saturday : motive Weekday.saturday) → motive t :=
fun {motive : (t : Weekday) → Sort u} (t : Weekday) (sunday : motive Weekday.sunday) (monday : motive Weekday.monday)
    (tuesday : motive Weekday.tuesday) (wednesday : motive Weekday.wednesday) (thursday : motive Weekday.thursday)
    (friday : motive Weekday.friday) (saturday : motive Weekday.saturday) =>
  @Weekday.rec.{u} motive sunday monday tuesday wednesday thursday friday saturday t

@Weekday.rec.{u_1} : {motive : (t : Weekday) → Sort u_1} →
  (sunday : motive Weekday.sunday) →
    (monday : motive Weekday.monday) →
      (tuesday : motive Weekday.tuesday) →
        (wednesday : motive Weekday.wednesday) →
          (thursday : motive Weekday.thursday) →
            (friday : motive Weekday.friday) → (saturday : motive Weekday.saturday) → (t : Weekday) → motive t

When declaring an inductive datatype, you can use deriving Repr to instruct Lean to generate a function that converts Weekday objects into text. This function is used by the #eval command to display Weekday objects. If no Repr exists, #eval attempts to derive one on the spot.

Weekday.tuesday

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 numberOfDay function in the Weekday namespace. We are then allowed to use the shorter name when we open the namespace.

We can define functions from Weekday to Weekday:

Weekday.thursday

Weekday.tuesday

How can we prove the general theorem that next (previous d) = d for any Weekday d? You can use match to provide a proof of the claim for each constructor:

Using a tactic proof, we can be even more concise:

Tactics for Inductive Types below will introduce additional tactics that are specifically designed to make use of inductive types.

Notice that, under the propositions-as-types correspondence, we can use match to prove theorems as well as define functions. In other words, under the propositions-as-types correspondence, the proof by cases is a kind of definition by cases, where what is being “defined” is a proof instead of a piece of data.

The Bool type in the Lean library is an instance of enumerated type.

(To run these examples, we put them in a namespace called Hidden, 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 when the system is started.)

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 and, or, not on the Bool type, and verifying common identities. Note that you can define a binary operation like and using match:

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

7.2. Constructors with Arguments🔗

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:

Consider 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 α β, 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 α × β for Prod α β and (a, b) for Prod.mk a b.

The function fst takes a pair, p. The match interprets p as a pair, Prod.mk a b. Recall also from Dependent Type Theory that to give these definitions the greatest generality possible, we allow the types α and β to belong to any universe.

Here is another example where we use the recursor Prod.casesOn instead of match.

6

7

The argument motive is used to specify the type of the object you want to construct, and it is a function because it may depend on the pair. The cond function is a boolean conditional: cond b t1 t2 returns t1 if b is true, and t2 otherwise. 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 α β, 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.

6

7

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.

Notice that the product type depends on parameters α β : 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 or the return type, and makes them implicit in that case.

In Defining the Natural Numbers 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 each constructor relies only on previously specified types.

Notice that a type with multiple constructors is disjunctive: an element of Sum α β 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 α β 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.

As with function definitions, Lean's inductive definition syntax will let you put named arguments to the constructors before the colon:

The results of these definitions are essentially the same as the ones given earlier in this section.

A type, like Prod, that has 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, the keyword structure can be used to define such an inductive type as well as its projections, at the same time.

This example simultaneously introduces the inductive type, Prod, its constructor, mk, the usual eliminators (rec and recOn), as well as the projections, fst and snd, 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:

255

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:

We will see more examples in the chapter on structures and records.

We have already discussed the dependent product type Sigma:

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

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

An element of Inhabited α is simply a witness to the fact that there is an element of α. 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 α to β and β to γ, 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.

7.3. Inductively Defined Propositions🔗

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.

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 hp : p carries no data. There is a small exception to this rule, however, which we will discuss below, in Inductive Families.

Even the existential quantifier is inductively defined:

Keep in mind that the notation ∃ x : α, p is syntactic sugar for Exists (fun x : α => 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 u for some u. In a similar way, ∃ x : α, p is a Prop-valued variant of Σ x : α, β.

This is a good place to mention another inductive type, denoted {x : α // p}, which is sort of a hybrid between ∃ x : α, p and Σ x : α, β.

In fact, in Lean, Subtype is defined using the structure command:

The notation {x : α // p x} is syntactic sugar for Subtype (fun x : α => p x). It is modeled after subset notation in set theory: the idea is that {x : α // p x} denotes the collection of elements of α that have property p.

7.4. Defining the Natural Numbers🔗

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:

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) → motive n for some motive : Nat → Sort u. 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, you find the following:

The implicit argument, motive, is the codomain of the function being defined. In type theory it is common to say motive is the motive for the elimination/recursion, since it describes the kind of object we wish to construct. The next two arguments specify how to compute the zero and successor cases, as described above. They are also known as the minor premises. Finally, the t : Nat is the input to the function. It is also known as the major premise.

The Nat.recOn is similar to Nat.rec but the major premise occurs before 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).

Hidden.Nat.succ (Hidden.Nat.succ (Hidden.Nat.succ (Hidden.Nat.zero)))

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:

We will explain how the instance command works in the Type Classes chapter. In the examples below, we will use Lean's version of the natural numbers.

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

Notice that, once again, when Nat.recOn is used in the context of a proof, it is really the induction principle in disguise. The rw and simp tactics tend to be very effective in proofs like these. In this case, each can be used to reduce the proof to: