.. _inductive_types: Inductive Types =============== We have seen that Lean's formal foundation includes basic types, ``Prop, Type 0, Type 1, Type 2, ...``, and allows for the formation of dependent function types, ``Π x : α, β``. 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: .. code-block:: text inductive foo : Sort u | 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 [Dybj94]_. 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. Enumerated Types ---------------- The simplest kind of inductive type is simply a type with a finite, enumerated list of elements. .. code-block:: lean 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. .. code-block:: lean 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 ``sunday``, ``monday``, :math:`\ldots`, ``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 a slight variant of ``weekday.rec``, ``weekday.rec_on`` (also generated automatically), which takes its arguments in a more convenient order. (Note that the shorter names ``rec`` and ``rec_on`` are not made available by default when we open the ``weekday`` namespace. This avoids clashes with the functions of the same names for other inductive types.) We can use ``weekday.rec_on`` to define a function from ``weekday`` to the natural numbers: .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday -- BEGIN def number_of_day (d : weekday) : ℕ := weekday.rec_on d 1 2 3 4 5 6 7 #reduce number_of_day weekday.sunday #reduce number_of_day weekday.monday #reduce 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. .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday -- BEGIN def number_of_day (d : weekday) : ℕ := 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`` and ``cases_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. .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday -- BEGIN namespace weekday @[reducible] private def cases_on := @weekday.cases_on def number_of_day (d : weekday) : nat := cases_on d 1 2 3 4 5 6 7 end weekday #reduce weekday.number_of_day weekday.sunday open weekday (renaming cases_on → cases_on) #reduce number_of_day sunday #check cases_on -- END We can define functions from ``weekday`` to ``weekday``: .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday -- BEGIN namespace weekday def next (d : weekday) : weekday := weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday def previous (d : weekday) : weekday := weekday.cases_on d saturday sunday monday tuesday wednesday thursday friday #reduce next (next tuesday) #reduce 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: .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday namespace weekday def next (d : weekday) : weekday := weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday def 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: .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday namespace weekday def next (d : weekday) : weekday := weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday def 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 Using a tactic proof, we can be even more concise: .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday namespace weekday def next (d : weekday) : weekday := weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday def 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 := by apply weekday.cases_on d; refl -- END end weekday :numref:`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 ``cases_on`` to prove theorems as well as define functions. In fact, we could equally well have used ``rec_on``: .. code-block:: lean inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday namespace weekday def next (d : weekday) : weekday := weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday def 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 := by apply weekday.rec_on d; refl -- END end weekday In other words, under the propositions-as-types correspondence, the proof by cases is a kind of definition by recursion, where what is being "defined" is a proof instead of a piece of data. Some fundamental data types in the Lean library are instances of enumerated types. .. code-block:: lean -- BEGIN namespace hidden inductive empty : Type inductive unit : Type | star : unit inductive bool : Type | ff : bool | tt : bool end hidden -- END (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.) The type ``empty`` is an inductive data type 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 you can define a binary operation like ``band`` using a case split: .. code-block:: lean namespace hidden -- BEGIN def band (b1 b2 : bool) : bool := bool.cases_on b1 ff b2 -- END end hidden Similarly, most identities can be proved by introducing suitable case splits, and then using ``rfl``. 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: .. code-block:: lean namespace hidden -- BEGIN universes u v inductive prod (α : Type u) (β : Type v) | mk : α → β → prod inductive sum (α : Type u) (β : Type v) | inl : α → sum | inr : β → sum -- END end hidden Notice that we do not include the types ``α`` and ``β`` in the target of the constructors. 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 α β``, 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``. .. code-block:: lean universes u v -- BEGIN def fst {α : Type u} {β : Type v} (p : α × β) : α := prod.rec_on p (λ a b, a) def snd {α : Type u} {β : Type v} (p : α × β) : β := prod.rec_on p (λ a b, b) -- END The function ``fst`` takes a pair, ``p``. Applying the recursor ``prod.rec_on p (λ 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``. Remember that you can enter the symbol for a product by typing ``\times``. Recall also from :numref:`dependent_types` that to give these definitions the greatest generality possible, we allow the types ``α`` and ``β`` to belong to any universe. Here is another example: .. code-block:: lean def prod_example (p : bool × ℕ) : ℕ := prod.rec_on p (λ b n, cond b (2 * n) (2 * n + 1)) #reduce prod_example (tt, 3) #reduce prod_example (ff, 3) The ``cond`` function is a boolean conditional: ``cond b t1 t2`` returns ``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 α β``, 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``. .. code-block:: lean -- BEGIN def sum_example (s : ℕ ⊕ ℕ) : ℕ := sum.cases_on s (λ n, 2 * n) (λ n, 2 * n + 1) #reduce sum_example (sum.inl 3) #reduce sum_example (sum.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``. You can enter the symbol for the sum by typing ``\oplus``. 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 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 α β`` 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: .. code-block:: lean namespace hidden -- BEGIN universes u v inductive prod (α : Type u) (β : Type v) | mk (fst : α) (snd : β) : prod inductive sum (α : Type u) (β : Type v) | inl {} (a : α) : sum | inr {} (b : β) : sum -- END end hidden The results of these definitions are essentially the same as the ones given earlier in this section. Note that in the definition of ``sum``, the annotation ``{}`` refers to the parameters, ``α`` and ``β``. As with function definitions, you can use curly braces to specify which arguments are meant to be left implicit. 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. .. code-block:: lean namespace hidden -- BEGIN structure prod (α β : Type*) := mk :: (fst : α) (snd : β) -- END end hidden This example simultaneously introduces the inductive type, ``prod``, its constructor, ``mk``, the usual eliminators (``rec`` and ``rec_on``), 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: .. code-block:: lean open nat -- BEGIN structure color := (red : nat) (green : nat) (blue : nat) def yellow := color.mk 255 255 0 #reduce 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: .. code-block:: lean universe u structure Semigroup := (carrier : Type u) (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 :numref:`Chapter %s `. We have already discussed sigma types, also known as the dependent product: .. code-block:: lean universes u v namespace hidden -- BEGIN inductive sigma {α : Type u} (β : α → Type v) | dpair : Π a : α, β a → sigma -- END end hidden Two more examples of inductive types in the library are the following: .. code-block:: lean namespace hidden -- BEGIN inductive option (α : Type*) | none {} : option | some : α → option inductive inhabited (α : Type*) | mk : α → inhabited -- END end hidden 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 Pi type ``Π x : α, β`` 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 the ``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. 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. .. code-block:: lean namespace hidden -- BEGIN inductive false : Prop inductive true : Prop | intro : true inductive and (a b : Prop) : Prop | intro : a → b → and inductive or (a b : Prop) : Prop | intro_left : a → or | intro_right : b → or -- END end hidden 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 the section on inductive families. Even the existential quantifier is inductively defined: .. code-block:: lean namespace hidden -- BEGIN inductive Exists {α : Type*} (q : α → Prop) : Prop | intro : ∀ (a : α), q a → Exists def exists.intro := @Exists.intro -- END end hidden Keep in mind that the notation ``∃ x : α, p`` is syntactic sugar for ``Exists (λ 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 : α, p``. This is a good place to mention another inductive type, denoted ``{x : α // p}``, which is sort of a hybrid between ``∃ x : α, P`` and ``Σ x : α, P``. .. code-block:: lean namespace hidden -- BEGIN inductive subtype {α : Type*} (p : α → Prop) | mk : Π x : α, p x → subtype -- END end hidden In fact, in Lean, ``subtype`` is defined using the structure command: .. code-block:: lean universe u namespace hidden -- BEGIN structure subtype {α : Sort u} (p : α → Prop) := (val : α) (property : p val) section variables {α : Type u} (p : α → Prop) #check subtype p #check { x : α // p x} end -- END end hidden The notation ``{x : α // p x}`` is syntactic sugar for ``subtype (λ 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``. 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: .. code-block:: lean namespace hidden -- BEGIN inductive nat : Type | zero : nat | succ : nat → nat -- END end hidden 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, .. code-block:: lean namespace hidden inductive nat : Type | zero : nat | succ : nat → nat -- BEGIN #check @nat.rec_on -- END end hidden we find the following: .. code-block:: text Π {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, since it describes the kind of object we wish to construct. 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)``. .. code-block:: lean namespace hidden inductive nat : Type | zero : nat | succ : nat → nat -- BEGIN namespace nat def add (m n : nat) : nat := nat.rec_on n m (λ n add_m_n, succ add_m_n) -- try it out #reduce add (succ zero) (succ (succ zero)) end nat -- END end hidden 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: .. code-block:: lean namespace hidden inductive nat : Type | zero : nat | succ : nat → nat namespace nat def add (m n : nat) : nat := nat.rec_on n m (fun n add_m_n, succ add_m_n) -- BEGIN instance : has_zero nat := has_zero.mk zero instance : has_add nat := has_add.mk 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 hidden We will explain how the ``instance`` command works in :numref:`Chapter %s `. In the examples below, we will henceforth use Lean's version of the natural numbers. 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)``. .. code-block:: lean namespace hidden open nat -- BEGIN theorem zero_add (n : ℕ) : 0 + n = n := nat.rec_on n (show 0 + 0 = 0, from rfl) (assume n, assume ih : 0 + n = n, show 0 + succ n = succ n, from calc 0 + succ n = succ (0 + n) : rfl ... = succ n : by rw ih) -- END end hidden Notice that, once again, when ``nat.rec_on`` is used in the context of a proof, it is really the induction principle in disguise. The ``rewrite`` and ``simp`` tactics tend to be very effective in proofs like these. In this case, each can be used to reduce the proof to a one-liner: .. code-block:: lean namespace hidden open nat -- BEGIN theorem zero_add (n : ℕ) : 0 + n = n := nat.rec_on n rfl (λ n ih, by rw [add_succ, ih]) theorem zero_add' (n : ℕ) : 0 + n = n := nat.rec_on n rfl (λ n ih, by simp only [add_succ, ih]) -- END end hidden The second example would be misleading without the ``only`` modifier, because ``zero_add`` is in fact declared to be a simplification rule in the standard library. Using ``only`` guarantees that ``simp`` only uses the identities listed. 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: .. code-block:: lean namespace hidden open nat -- BEGIN theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) := nat.rec_on k (show m + n + 0 = m + (n + 0), from rfl) (assume 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)) : by rw ih ... = m + succ (n + k) : rfl ... = m + (n + succ k) : rfl) -- END end hidden One again, there is a one-line proof: .. code-block:: lean namespace hidden open nat -- BEGIN theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) := nat.rec_on k rfl (λ k ih, by simp only [add_succ, ih]) -- END end hidden Suppose we try to prove the commutativity of addition. Choosing induction on the second argument, we might begin as follows: .. code-block:: lean namespace hidden open nat theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) := nat.rec_on k (show m + n + 0 = m + (n + 0), from rfl) (assume 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)) : by rw ih ... = m + succ (n + k) : rfl ... = m + (n + succ k) : rfl) -- BEGIN theorem add_comm (m n : nat) : m + n = n + m := nat.rec_on n (show m + 0 = 0 + m, by rw [nat.zero_add, nat.add_zero]) (assume n, assume ih : m + n = n + m, calc m + succ n = succ (m + n) : rfl ... = succ (n + m) : by rw ih ... = succ n + m : sorry) -- END end hidden 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``: .. code-block:: lean namespace hidden open nat theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) := nat.rec_on k (show m + n + 0 = m + (n + 0), from rfl) (assume 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)) : by rw ih ... = m + succ (n + k) : rfl ... = m + (n + succ k) : rfl) -- BEGIN theorem succ_add (m n : nat) : succ m + n = succ (m + n) := nat.rec_on n (show succ m + 0 = succ (m + 0), from rfl) (assume 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)) : by rw ih ... = succ (m + succ n) : rfl) -- END end hidden We can then replace the ``sorry`` in the previous proof with ``succ_add``. Yet again, the proofs can be compressed: .. code-block:: lean namespace hidden open nat theorem add_zero (m : nat) : m + 0 = m := rfl theorem zero_add (n : ℕ) : 0 + n = n := nat.rec_on n rfl (λ n ih, by rw [add_succ, ih]) -- BEGIN theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) := nat.rec_on k rfl (λ k ih, by simp only [add_succ, ih]) theorem succ_add (m n : nat) : succ m + n = succ (m + n) := nat.rec_on n rfl (λ n ih, by simp only [add_succ, ih]) theorem add_comm (m n : nat) : m + n = n + m := nat.rec_on n (by simp only [zero_add, add_zero]) (λ n ih, by simp only [add_succ, ih, succ_add]) -- END end hidden Other Recursive Data Types -------------------------- Let us consider some more examples of inductively defined types. For any type, ``α``, the type ``list α`` of lists of elements of ``α`` is defined in the library. .. code-block:: lean namespace hidden -- BEGIN inductive list (α : Type*) | nil {} : list | cons : α → list → list namespace list variable {α : Type*} notation (name := cons) h :: t := cons h t def append (s t : list α) : list α := list.rec t (λ x l u, x::u) s notation (name := append) s ++ t := append s t theorem nil_append (t : list α) : nil ++ t = t := rfl theorem cons_append (x : α) (s t : list α) : x::s ++ t = x::(s ++ t) := rfl end list -- END end hidden A list of elements of type ``α`` is either the empty list, ``nil``, or an element ``h : α`` followed by a list ``t : list α``. 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 α`` to specify the type ``α``. Lean allows us to define iterative notation for lists: .. code-block:: lean namespace hidden -- BEGIN inductive list (α : Type*) | nil {} : list | cons : α → list → list namespace list notation (name := list) `[` 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 int) end end list -- END end hidden In the first ``#check``, Lean assumes that ``[1, 2, 3, 4, 5]`` is a list of natural numbers. The ``(t : list int)`` expression forces Lean to interpret ``t`` as a list of integers. As an exercise, prove the following: .. code-block:: lean namespace hidden inductive list (α : Type*) | nil {} : list | cons : α → list → list namespace list notation (name := list) `[` l:(foldr `,` (h t, cons h t) nil) `]` := l variable {α : Type*} notation (name := cons) h :: t := cons h t def append (s t : list α) : list α := list.rec_on s t (λ x l u, x::u) notation (name := append) s ++ t := append s t theorem nil_append (t : list α) : nil ++ t = t := rfl theorem cons_append (x : α) (s t : list α) : x::s ++ t = x::(s ++ t) := rfl -- BEGIN theorem append_nil (t : list α) : t ++ nil = t := sorry theorem append_assoc (r s t : list α) : r ++ s ++ t = r ++ (s ++ t) := sorry -- END end list end hidden Try also defining the function ``length : Π {α : Type*}, list α → 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: .. code-block:: lean 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: .. code-block:: lean inductive cbtree | leaf : cbtree | sup : (ℕ → cbtree) → cbtree namespace cbtree def succ (t : cbtree) : cbtree := sup (λ n, t) def omega : cbtree := sup (λ n, nat.rec_on n leaf (λ n t, succ t)) end cbtree .. _tactics_for_inductive_types: Tactics for Inductive Types --------------------------- Given the fundamental importance of inductive types in Lean, it should not be surprising that there are a number of tactics designed to work with them effectively. We describe some of them here. The ``cases`` tactic works on elements of an inductively defined type, and does what the name suggests: it decomposes the element according to each of the possible constructors. In its most basic form, it is applied to an element ``x`` in the local context. It then reduces the goal to cases in which ``x`` is replaced by each of the constructions. .. code-block:: lean open nat variable p : ℕ → Prop example (hz : p 0) (hs : ∀ n, p (succ n)) : ∀ n, p n := begin intro n, cases n, { exact hz }, -- goal is p 0 apply hs -- goal is a : ℕ ⊢ p (succ a) end There are extra bells and whistles. For one thing, ``cases`` allows you to choose the names for the arguments to the constructors using a ``with`` clause. In the next example, for example, we choose the name ``m`` for the argument to ``succ``, so that the second case refers to ``succ m``. More importantly, the cases tactic will detect any items in the local context that depend on the target variable. It reverts these elements, does the split, and reintroduces them. In the example below, notice that the hypothesis ``h : n ≠ 0`` becomes ``h : 0 ≠ 0`` in the first branch, and ``h : succ m ≠ 0`` in the second. .. code-block:: lean open nat example (n : ℕ) (h : n ≠ 0) : succ (pred n) = n := begin cases n with m, -- first goal: h : 0 ≠ 0 ⊢ succ (pred 0) = 0 { apply (absurd rfl h) }, -- second goal: h : succ m ≠ 0 ⊢ succ (pred (succ m)) = succ m reflexivity end Notice that ``cases`` can be used to produce data as well as prove propositions. .. code-block:: lean def f (n : ℕ) : ℕ := begin cases n, exact 3, exact 7 end example : f 0 = 3 := rfl example : f 5 = 7 := rfl Once again, cases will revert, split, and then reintroduce dependencies in the context. .. code-block:: lean def tuple (α : Type*) (n : ℕ) := { l : list α // list.length l = n } variables {α : Type*} {n : ℕ} def f {n : ℕ} (t : tuple α n) : ℕ := begin cases n, exact 3, exact 7 end def my_tuple : tuple ℕ 3 := ⟨[0, 1, 2], rfl⟩ example : f my_tuple = 7 := rfl If there are multiple constructors with arguments, you can provide ``cases`` with a list of all the names, arranged sequentially: .. code-block:: lean inductive foo : Type | bar1 : ℕ → ℕ → foo | bar2 : ℕ → ℕ → ℕ → foo def silly (x : foo) : ℕ := begin cases x with a b c d e, exact b, -- a, b are in the context exact e -- c, d, e are in the context end The syntax of the ``with`` is unfortunate, in that we have to list the arguments to all the constructors sequentially, making it hard to remember what the constructors are, or what the arguments are supposed to be. For that reason, Lean provides a complementary ``case`` tactic, which allows one to assign variable names after the fact: .. code-block:: lean inductive foo : Type | bar1 : ℕ → ℕ → foo | bar2 : ℕ → ℕ → ℕ → foo open foo def silly (x : foo) : ℕ := begin cases x, case bar1 : a b { exact b }, case bar2 : c d e { exact e } end The ``case`` tactic is clever, in that it will match the constructor to the appropriate goal. For example, we can fill the goals above in the opposite order: .. code-block:: lean inductive foo : Type | bar1 : ℕ → ℕ → foo | bar2 : ℕ → ℕ → ℕ → foo open foo def silly (x : foo) : ℕ := begin cases x, case bar2 : c d e { exact e }, case bar1 : a b { exact b } end You can also use ``cases`` with an arbitrary expression. Assuming that expression occurs in the goal, the cases tactic will generalize over the expression, introduce the resulting universally quantified variable, and case on that. .. code-block:: lean open nat variable p : ℕ → Prop example (hz : p 0) (hs : ∀ n, p (succ n)) (m k : ℕ) : p (m + 3 * k) := begin cases (m + 3 * k), { exact hz }, -- goal is p 0 apply hs -- goal is a : ℕ ⊢ p (succ a) end Think of this as saying "split on cases as to whether ``m + 3 * k`` is zero or the successor of some number." The result is functionally equivalent to the following: .. code-block:: lean open nat variable p : ℕ → Prop -- BEGIN example (hz : p 0) (hs : ∀ n, p (succ n)) (m k : ℕ) : p (m + 3 * k) := begin generalize : m + 3 * k = n, cases n, { exact hz }, -- goal is p 0 apply hs -- goal is a : ℕ ⊢ p (succ a) end -- END Notice that the expression ``m + 3 * k`` is erased by generalize; all that matters is whether it is of the form ``0`` or ``succ a``. This form of ``cases`` will *not* revert any hypotheses that also mention the expression in equation (in this case, ``m + 3 * k``). If such a term appears in a hypothesis and you want to generalize over that as well, you need to ``revert`` it explicitly. If the expression you case on does not appear in the goal, the ``cases`` tactic uses ``have`` to put the type of the expression into the context. Here is an example: .. code-block:: lean example (p : Prop) (m n : ℕ) (h₁ : m < n → p) (h₂ : m ≥ n → p) : p := begin cases lt_or_ge m n with hlt hge, { exact h₁ hlt }, exact h₂ hge end The theorem ``lt_or_ge m n`` says ``m < n ∨ m ≥ n``, and it is natural to think of the proof above as splitting on these two cases. In the first branch, we have the hypothesis ``h₁ : m < n``, and in the second we have the hypothesis ``h₂ : m ≥ n``. The proof above is functionally equivalent to the following: .. code-block:: lean example (p : Prop) (m n : ℕ) (h₁ : m < n → p) (h₂ : m ≥ n → p) : p := begin have h : m < n ∨ m ≥ n, { exact lt_or_ge m n }, cases h with hlt hge, { exact h₁ hlt }, exact h₂ hge end After the first two lines, we have ``h : m < n ∨ m ≥ n`` as a hypothesis, and we simply do cases on that. Here is another example, where we use the decidability of equality on the natural numbers to split on the cases ``m = n`` and ``m ≠ n``. .. code-block:: lean #check nat.sub_self example (m n : ℕ) : m - n = 0 ∨ m ≠ n := begin cases decidable.em (m = n) with heq hne, { rw heq, left, exact nat.sub_self n }, right, exact hne end Remember that if you ``open classical``, you can use the law of the excluded middle for any proposition at all. But using type class inference (see :numref:`Chapter %s `), Lean can actually find the relevant decision procedure, which means that you can use the case split in a computable function. .. code-block:: lean def f (m k : ℕ) : ℕ := begin cases m - k, exact 3, exact 7 end example : f 5 7 = 3 := rfl example : f 10 2 = 7 := rfl Aspects of computability will be discussed in :numref:`Chapter %s `. Just as the ``cases`` tactic can be used to carry out proof by cases, the ``induction`` tactic can be used to carry out proofs by induction. The syntax is similar to that of ``cases``, except that the argument can only be a term in the local context. Here is an example: .. code-block:: lean namespace hidden open nat -- BEGIN theorem zero_add (n : ℕ) : 0 + n = n := begin induction n with n ih, refl, rw [add_succ, ih] end -- END end hidden As with ``cases``, we can use the ``case`` tactic instead to identify one case at a time and name the arguments: .. code-block:: lean namespace hidden open nat -- BEGIN theorem zero_add (n : ℕ) : 0 + n = n := begin induction n, case zero : { refl }, case succ : n ih { rw [add_succ, ih]} end theorem succ_add (m n : ℕ) : succ m + n = succ (m + n) := begin induction n, case zero : { refl }, case succ : n ih { rw [add_succ, add_succ, ih] } end theorem add_comm (m n : ℕ) : m + n = n + m := begin induction n, case zero : { rw zero_add, refl }, case succ : n ih { rw [add_succ, ih, succ_add] } end -- END end hidden The name before the colon corresponds to the constructor of the associated inductive type. The cases can appear in any order, and when there are no parameters to rename (for example, as in the ``zero`` cases above) the colon can be omitted. Once again, we can reduce the proofs of these, as well as the proof of associativity, to one-liners. .. code-block:: lean namespace hidden open nat theorem add_zero (m : nat) : m + 0 = m := rfl -- BEGIN theorem zero_add (n : ℕ) : 0 + n = n := by induction n; simp only [*, add_zero, add_succ] theorem succ_add (m n : ℕ) : succ m + n = succ (m + n) := by induction n; simp only [*, add_zero, add_succ] theorem add_comm (m n : ℕ) : m + n = n + m := by induction n; simp only [*, add_zero, add_succ, succ_add, zero_add] theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) := by induction k; simp only [*, add_zero, add_succ] -- END end hidden We close this section with one last tactic that is designed to facilitate working with inductive types, namely, the ``injection`` tactic. By design, the elements of an inductive type are freely generated, which is to say, the constructors are injective and have disjoint ranges. The ``injection`` tactic is designed to make use of this fact: .. code-block:: lean open nat example (m n k : ℕ) (h : succ (succ m) = succ (succ n)) : n + k = m + k := begin injection h with h', injection h' with h'', rw h'' end The first instance of the tactic adds ``h' : succ m = succ n`` to the context, and the second adds ``h'' : m = n``. The plural variant, ``injections``, applies ``injection`` to all hypotheses repeatedly. It still allows you to name the results using ``with``. .. code-block:: lean open nat -- BEGIN example (m n k : ℕ) (h : succ (succ m) = succ (succ n)) : n + k = m + k := begin injections with h' h'', rw h'' end example (m n k : ℕ) (h : succ (succ m) = succ (succ n)) : n + k = m + k := by injections; simp * -- END The ``injection`` and ``injections`` tactics will also detect contradictions that arise when different constructors are set equal to one another, and use them to close the goal. .. code-block:: lean open nat -- BEGIN example (m n : ℕ) (h : succ m = 0) : n = n + 7 := by injections example (m n : ℕ) (h : succ m = 0) : n = n + 7 := by contradiction example (h : 7 = 4) : false := by injections -- END As the second example shows, the ``contradiction`` tactic also detects contradictions of this form. But the ``contradiction`` tactic does not solve the third goal, while ``injections`` does. Inductive Families ------------------ We are almost done describing the full range of inductive definitions accepted by Lean. So far, you have seen that Lean allows you to introduce inductive types with any number of recursive constructors. In fact, a single inductive definition can introduce an indexed *family* of inductive types, in a manner we now describe. An inductive family is an indexed family of types defined by a simultaneous induction of the following form: .. code-block:: text inductive foo : ... → Sort u := | constructor₁ : ... → foo ... | constructor₂ : ... → foo ... ... | constructorₙ : ... → foo ... In contrast to ordinary inductive definition, which constructs an element of some ``Sort u``, the more general version constructs a function ``... → Sort u``, where "``...``" denotes a sequence of argument types, also known as *indices*. Each constructor then constructs an element of some member of the family. One example is the definition of ``vector α n``, the type of vectors of elements of ``α`` of length ``n``: .. code-block:: lean open nat universe u namespace hidden -- BEGIN inductive vector (α : Type u) : nat → Type u | nil {} : vector zero | cons {n : ℕ} (a : α) (v : vector n) : vector (succ n) -- END end hidden Notice that the ``cons`` constructor takes an element of ``vector α n`` and returns an element of ``vector α (succ n)``, thereby using an element of one member of the family to build an element of another. A more exotic example is given by the definition of the equality type in Lean: .. code-block:: lean universe u namespace hidden -- BEGIN inductive eq {α : Sort u} (a : α) : α → Prop | refl [] : eq a -- END end hidden For each fixed ``α : Sort u`` and ``a : α``, this definition constructs a family of types ``eq a x``, indexed by ``x : α``. Notably, however, there is only one constructor, ``refl``, which is an element of ``eq a a``, and the square brackets after the constructor tell Lean to make the argument to ``refl`` explicit. 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 is as follows: .. code-block:: lean universes u v #check (@eq.rec_on : Π {α : Sort u} {a : α} {C : α → Sort v} {b : α}, 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``. The definition of equality is atypical, however; see the discussion in the next section. The recursor ``eq.rec_on`` is also used to define substitution: .. code-block:: lean namespace hidden universe u inductive eq {α : Type u} (a : α) : α → Prop | refl [] : eq a -- BEGIN @[elab_as_eliminator] theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : eq a b) (h₂ : p a) : p b := eq.rec h₂ h₁ -- END end hidden 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. The definition of ``subst`` is marked with an elaboration hint, as described in :numref:`elaboration_hints`. 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). .. code-block:: lean namespace hidden universe u inductive eq {α : Type u} (a : α) : α → Prop | refl [] : eq a @[elab_as_eliminator] theorem subst {α : Type u} {a b : α} {P : α → Prop} (h₁ : eq a b) (h₂ : P a) : P b := eq.rec h₂ h₁ -- BEGIN theorem symm {α : Type u} {a b : α} (h : eq a b) : eq b a := subst h (eq.refl a) theorem trans {α : Type u} {a b c : α} (h₁ : eq a b) (h₂ : eq b c) : eq a c := sorry theorem congr {α β : Type u} {a b : α} (f : α → β) (h : eq a b) : eq (f a) (f b) := sorry -- END end hidden 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. Axiomatic Details ----------------- We have described inductive types and their syntax through examples. This section provides additional information for those interested in the axiomatic foundations. We have seen that the constructor to an inductive type takes *parameters* --- intuitively, the arguments that remain fixed throughout the inductive construction --- and *indices*, the arguments parameterizing the family of types that is simultaneously under construction. Each constructor should have a Pi type, where the argument types are built up from previously defined types, the parameter and index types, and the inductive family currently being defined. The requirement is that if the latter is present at all, it occurs only *strictly positively*. This means simply that any argument to the constructor in which it occurs is a Pi type in which the inductive type under definition occurs only as the resulting type, where the indices are given in terms of constants and previous arguments. Since an inductive type lives in ``Sort u`` for some ``u``, it is reasonable to ask *which* universe levels ``u`` can be instantiated to. Each constructor ``c`` in the definition of a family ``C`` of inductive types is of the form .. code-block:: text c : Π (a : α) (b : β[a]), C a p[a,b] where ``a`` is a sequence of data type 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. (Note that this description is somewhat misleading, in that the arguments to the constructor can appear in any order as long as the dependencies make sense.) The constraints on the universe level of ``C`` fall into two cases, depending on whether or not the inductive type is specified to land in ``Prop`` (that is, ``Sort 0``). Let us first consider the case where the inductive type is *not* specified to land in ``Prop``. Then the universe level ``u`` is constrained to satisfy the following: For each constructor ``c`` as above, and each ``βk[a]`` in the sequence ``β[a]``, if ``βk[a] : Sort v``, we have ``u`` ≥ ``v``. In other words, the universe level ``u`` 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 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``. There is an exception to this last rule: we are allowed to eliminate from an inductively defined ``Prop`` to an arbitrary ``Sort`` when there is only one constructor and each constructor argument is either in ``Prop`` or an index. The intuition is that in this case the elimination does not make use of any information that is not already given by the mere fact that the type of argument is inhabited. This special case is known as *singleton elimination*. We have already seen singleton elimination at play in applications of ``eq.rec``, the eliminator for the inductively defined equality type. We can use an element ``h : eq a b`` to cast an element ``t' : p a`` to ``p b`` even when ``p a`` and ``p b`` are arbitrary types, because the cast does not produce new data; it only reinterprets the data we already have. Singleton elimination is also used with heterogeneous equality and well-founded recursion, which will be discussed in a later chapter. .. _mutual_and_nested_inductive_types: Mutual and Nested Inductive Types --------------------------------- We now consider two generalizations of inductive types that are often useful, which Lean supports by "compiling" them down to the more primitive kinds of inductive types described above. In other words, Lean parses the more general definitions, defines auxiliary inductive types based on them, and then uses the auxiliary types to define the ones we really want. Lean's equation compiler, described in the next chapter, is needed to make use of these types effectively. Nonetheless, it makes sense to describe the declarations here, because they are straightforward variations on ordinary inductive definitions. 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(s). .. code-block:: lean mutual inductive even, odd with even : ℕ → Prop | even_zero : even 0 | even_succ : ∀ n, odd n → even (n + 1) with odd : ℕ → Prop | odd_succ : ∀ n, even n → odd (n + 1) In this example, two types are defined simultaneously: a natural number ``n`` is ``even`` if it is ``0`` or one more than an ``odd`` number, and ``odd`` if it is one more than an even number. Under the hood, this definition is compiled down to a single inductive type with an index ``i`` in a two-valued type (such as ``bool``), where ``i`` encodes which of ``even`` or ``odd`` is intended. In the exercises below, you are asked to spell out the details. A mutual inductive definition can also be used to define the notation of a finite tree with nodes labeled by elements of ``α``: .. code-block:: lean universe u mutual inductive tree, list_tree (α : Type u) with tree : Type u | node : α → list_tree → tree with list_tree : Type u | nil {} : list_tree | cons : tree → list_tree → list_tree With this definition, one can construct an element of ``tree α`` by giving an element of ``α`` together with a list of subtrees, possibly empty. The list of subtrees is represented by the type ``list_tree α``, which is defined to be either the empty list, ``nil``, or the ``cons`` of a tree and an element of ``list_tree α``. This definition is inconvenient to work with, however. It would be much nicer if the list of subtrees were given by the type ``list (tree α)``, especially since Lean's library contains a number of functions and theorems for working with lists. One can show that the type ``list_tree α`` is *isomorphic* to ``list (tree α)``, but translating results back and forth along this isomorphism is tedious. In fact, Lean allows us to define the inductive type we really want: .. code-block:: lean universe u -- BEGIN inductive tree (α : Type u) | mk : α → list tree → tree -- END This is known as a *nested* inductive type. It falls outside the strict specification of an inductive type given in the last section because ``tree`` does not occur strictly positively among the arguments to ``mk``, but, rather, nested inside the ``list`` type constructor. Under the hood, Lean compiles this down to the mutual inductive type described above, which, in turn, is compiled down to an ordinary inductive type. Lean then automatically builds the isomorphism between ``list_tree α`` and ``list (tree α)``, and defines the constructors for ``tree`` in terms of the isomorphism. The types of the constructors for mutual and nested inductive types can be read off from the definitions. Defining functions *from* such types is more complicated, because these also have to be compiled down to more basic operations, making use of the primitive recursors that are associated to the inductive types that are declared under the hood. Lean does its best to hide the details from users, allowing them to use the equation compiler, described in the next section, to define such functions in natural ways. Exercises --------- #. 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. Since many of these are already defined in Lean's core library, you should work within a namespace named ``hide``, or something like that, in order to avoid name clashes. #. Define some operations on lists, like a ``length`` function or the ``reverse`` function. Prove some properties, such as the following: a. ``length (s ++ t) = length s + length t`` b. ``length (reverse t) = length t`` c. ``reverse (reverse t) = t`` #. Define an inductive data type consisting of terms built up from the following constructors: - ``const n``, a constant denoting the natural number ``n`` - ``var n``, a variable, numbered ``n`` - ``plus s t``, denoting the sum of ``s`` and ``t`` - ``times s t``, denoting the product of ``s`` and ``t`` Recursively define a function that evaluates any such term with respect to an assignment of values to the variables. #. Similarly, define the type of propositional formulas, as well as functions on the type of such formulas: an evaluation function, functions that measure the complexity of a formula, and a function that substitutes another formula for a given variable. #. Simulate the mutual inductive definition of ``even`` and ``odd`` described in :numref:`mutual_and_nested_inductive_types` with an ordinary inductive type, using an index to encode the choice between them in the target type.