2.2.1. Days of the Week (Enumerated Types)🔗

Let's start with a very simple example. The following declaration tells Lean to give a name to a set of data values, i.e., to define a type.

The new type is called Day, and its members are monday, tuesday, etc. These are also called the constructors of the Day type. We often call this sort of inductive type an enumerated type since the values belonging to the type are explicitly enumerated in its definition.

Having defined Day, we can write Lean functions that operate on days.

Note that the argument and result types of this function are explicitly declared on its first line. As in most functional programming languages, Lean can often figure out these types for itself when they are not given explicitly — i.e., it can do type inference — but we'll generally include them to make reading easier.

The match on the second line is Lean's keyword for pattern matching, the functional programming way of examining and making decisions on data. To evaluate match d with..., Lean will examine the structure of d to see which case to execute; if d is Day.monday, for example, it will evaluate the first case of the match statement; if d is Day.friday, it will evaluate the fifth case. (There is much more to say about pattern matching! We'll introduce more of its features as the need arises.)

You may notice that we qualified Day's constructors when using them, writing Day.monday instead of just monday, for example. Lean places all constructors into a namespace associated with their type, and generally requires those constructors to be prefixed with their namespace when they are used, though we will see later that this requirement can sometimes be relaxed.

If you ever need to know the type of any pattern, object, or function, you can hover over it with your mouse, either in VS Code or in the HTML version of the chapter.

Having defined a function, we should check that it works on some examples. There are a few different ways to do this in Lean. One is to use the #eval command to evaluate a compound expression involving nextWorkingDay.

Day.monday

Day.tuesday

We can also record what we expect the result of calling a function to be in the form of a Lean example:

This declaration asserts that the second working day after saturday is tuesday. Having made the assertion, we can also ask Lean to verify it. The by rfl can be read as "The assertion we've just made can be proved by observing that both sides of the equality evaluate to the same term."

Here, rfl is pronounced "reflexivity," the principle that any value is equal to itself. After evaluation, both sides of the equality are the same value, so the assertion is true by reflexivity. If we had made a different assertion, such as

then Lean would not be able to verify it and would instead signal an error.

(The sf_expect_failure_in annotation tells Lean that there is intended to be an error in the following expression and it should not mark the whole file as broken.)

2.2.2. Aside: Using the VS Code Lean Extension🔗

If you have not already done so, this would be an excellent moment to fire up VS Code with the Lean Extension and load this file, Basics.lean, from the book's Lean sources. Locate the above example and observe its result in the Lean InfoView panel.

This panel displays the results of commands like #eval (click on a particular #eval to see), as well as the current goal state when you are working on proofs. The InfoView content always follows your cursor.

On Windows and Linux, Ctrl-click a type or variable name to navigate to its definition. On macOS, Command-click instead. Try this with the mention of nextWorkingDay in the above #eval.

You can also hover over expressions in the source code to see their types. Try this with mentions of nextWorkingDay and Day.saturday in the above #eval. If you hover over the #eval command itself, you will see the popup that contains its output (at the top). Sometimes we show Lean's responses to commands in the text below them; by hovering over the command, you can check against that text.

Experiment with adding your own #eval commands to test other inputs. Lean typechecks the file as you edit it, so you can see the results of your changes immediately.

2.2.3. Booleans🔗

Following the pattern of the days of the week above, we can define the standard type Bool of booleans by enumerating its members true and false. We define our own MyBool to teach the concept of building booleans from scratch. Our definition of MyBool is equivalent to Lean's built-in Bool, which we'll switch to later. We call it MyBool to avoid clashing with the built-in name. Later in the chapter, we will show a different way of avoiding such clashes: we will place our custom natural numbers in a fresh NatPlayground namespace, where they can be called Nat without clashing with Lean's built-in Nat.

We next invoke a couple of Lean directives to help control formatting. Exactly what these directives mean is not important for present purposes — you can understand everything in the rest of the book without knowing — so we will mark these commands — and similar bits later on — with THE FOLLOWING DETAILS CAN BE SKIPPED comments in .lean files, and with folded-up segments in the HTML presentation. Feel free to have a peek if you want (click on the triangle in the HTML to unfold it), or just jump down to the following material and keep going.

The next command opens the namespace associated with the MyBool type, so subsequent definitions will be part of the MyBool namespace. In Lean, functions on a type are typically defined in that type's namespace, which avoids name clashes with functions of the same name elsewhere (e.g., functions on the built-in Bool type). We give a full treatment of namespaces below.

Functions over booleans can be defined in the same way as functions over days of the week.

The and and or definitions illustrate Lean's syntax for multi-argument functions. The corresponding multi-argument function-application syntax is illustrated by the following tests, which effectively constitute a complete specification — a truth table — for the or function:

Lean also allows us to define symbolic notations for these functions.

The technical details of how these symbolic notations work are not something you need to understand until quite a bit later in your Lean journey.

2.3.1. Aside: Unicode in Lean🔗

Note that ∀ and ⊢ are Unicode symbols, not plain ASCII characters. The Lean Extension for VS Code provides convenient shortcuts for entering such symbols. Simply type \ (backslash) followed by the name of the symbol (its "shortcode"), and the extension will automatically replace it with the actual symbol. For example, typing either \all or \forall will produce ∀, and \-> or \to will produce →. To find out what backslash sequence produces a Unicode symbol that you can see on the screen, just hover over it. To see a list of all of the Unicode shortcodes, open the Command Palette (Ctrl+Shift+P on Windows/Linux or Cmd+Shift+P on macOS), type "Lean 4: Show Unicode Input Abbreviations", and press Enter.

2.3.2. Types🔗

Every expression in Lean has a type describing what sort of value it computes. The #check command asks Lean to print the type of an expression.

Bool.true : Bool

If the expression after #check is followed by a colon and a type, Lean will verify that the type of the expression matches the given type and signal an error if not.

true : Bool

!true : Bool

Functions like Bool.not are themselves ordinary values, just like Bool.true and Bool.false. Their types are called function types, and they are written with arrows.

The type of Bool.not, written Bool → Bool and pronounced "Bool arrow Bool," can be read, "Given an input of type Bool, this function produces an output of type Bool." Similarly, the type of Bool.and, written Bool → Bool → Bool, can be read, "Given two inputs, each of type Bool, this function produces an output of type Bool."

2.3.3. New Types from Old🔗

The enumerated types we have seen so far are so named because their definitions explicitly enumerate a finite set of elements: their constructors. Here is a more interesting inductive type definition, Color, where one of the constructors takes an argument:

Constructor expressions are formed by applying a constructor to zero or more other constructors or constructor expressions, obeying the declared number and types of the constructor arguments. E.g., these are valid constructor expressions...

• RGB.red

• Bool.true

• Color.primary RGB.red

...but these are not:

• RGB.red Color.primary

• Bool.true RGB.red

• Color.primary (Color.primary RGB.red)

We can define functions on colors using pattern matching, just as we did for Day and MyBool.

Since the primary constructor takes an argument, a pattern that matches .primary should include a variable, a constant of appropriate type, or _. Lean's convention is to use a _ (called a wildcard) when the argument to a constructor doesn't matter. In the definition of monochrome, we don't use the argument to Color.primary, so a more idiomatic definition would be:

We can use a constant argument to Color.primary to match a specific primary color:

The pattern Color.primary RGB.red will match only when c is Color.primary with the argument RGB.red. The pattern Color.primary _ matches every Color.primary color, but because patterns are checked in order, the Color.primary _ case will never be reached if the color is RGB.red.

An alternative way to write the same function would be to explicitly nest match statements:

This isRed' function produces the same result as isRed. It also illustrates the use of a pattern variable in the corresponding branch.

The Color.primary r pattern stores the RGB argument into variable r, and then pattern matches on that argument to produce the final result.

2.3.4. Namespaces🔗

This chapter has already used Lean's system of namespaces for managing potentially conflicting names in a few places. Now we have seen enough that we can look more closely at how it works.

When we enclose a collection of declarations in namespace X ... end X, references from outside this collection to names declared within it are referred to with prefix X., like X.foo instead of just foo. In large Lean developments, namespaces are used to organize definitions and theorems similarly to how modules are used in other programming languages.

myFoo : Bool

Playground.myFoo : RGB

Namespaces can be closed and later reopened, as often as you like, to add new definitions and access old ones more conveniently. When inside a namespace, definitions from that namespace can be referenced without prefixes.

Playground.myBar : RGB

Lean gives each constructor of an inductive type a name prefixed by the type's name, such as RGB.blue. When we enter the RGB namespace, we can use its constructors without the RGB prefix. For example, we can write just blue below.

Top-level definitions can also be prefixed by a namespace, which opens the namespace temporarily for the body of the definition.

RGB.myBlue : RGB

RGB.myOtherBlue : RGB

Unknown identifier `myBlue`

Similarly, we could rewrite the definition of nextWorkingDay inside the Day namespace like so:

We can also use open to bring the definitions of a namespace into the current scope; after that, we can refer to any of the namespace's definitions without a prefix.

MyNamespace.myDef : Bool

If we only want to bring some, rather than all, of the definitions of a namespace into the current scope, we can use the open (...) form:

MyOtherNamespace.myVisibleDef : Bool

But myHiddenDef, which we did not include in the open, still needs to be qualified:

Unknown identifier `myHiddenDef`

You might be wondering why we can use constructors like true and false and functions like not without qualifying them with Bool, and without explicitly opening the Bool namespace. Lean provides a way to export unprefixed names from a namespace, with the same effect as selectively opening that namespace downstream, and the Lean prelude does that for commonly used names from the standard library. We don't explain this mechanism here because it's rarely used.

Bool.true : Bool

Bool.true : Bool

Finally, Lean can often use an expression's expected type to fill in the missing prefix of a name that begins with .. So, instead of the fully qualified style Day.monday, we can write just .monday.

For example, when the expected type is Day, Lean interprets .monday as Day.monday. If the context does not determine an expected type, Lean reports an error.

So, for example, we can also write nextWorkingDay like this, using the shorter style for both the value being matched and the value being returned:

Here, both the type of d and the return type of the function are declared to be Days. When we use the .monday style in the function body, Lean can figure out that we must mean Day.monday. However, in the example below, there is no expected type, so Lean cannot determine which declaration named .true is intended. In this case, it raises an error:

Invalid dotted identifier notation: The expected type of `.true` could not be determined

Hint: Using one of these would be unambiguous:
  [apply] `true`
  [apply] `MyBool.true`
  [apply] `Lake.Toml.true`
  [apply] `Lean.LBool.true`
  [apply] `Std.Do.ExceptConds.true`
  [apply] `Lean.Meta.Grind.Filter.true`

But in the following example, because Bool.not takes a Bool argument, Lean knows that .true must here be a Bool:

!true : Bool

#check .black           -- Write your prediction here.
#check Color.black      -- Write your prediction here.
#check RGB              -- Write your prediction here.
#check Playground.myFoo -- Write your prediction here.

2.3.5. Constructors with Multiple Parameters (Tuple Types)🔗

A constructor of an inductive type can have multiple parameters, not just zero or one. This feature lets us define tuple types in Lean.

As an example, consider representing the four bits in a nibble (half a byte). We first define a datatype Bit that resembles Bool (using the constructors b1 and b0 for the two possible bit values) and then define the datatype Nibble, which is a tuple of four bits.

Nibble.bits Bit.b1 Bit.b0 Bit.b1 Bit.b0 : Nibble

The bits constructor illustrates a convenience feature of multi-parameter declarations, both for constructors and for functions: instead of writing (x0 : Bit) (x1 : Bit) ..., we write (x0 x1 ... : Bit) since all of the variables have the same type. We could have done the same with the function definition MyBool.or above, writing or (b1 b2 : MyBool) rather than or (b1 : MyBool) (b2 : MyBool).

The bits constructor acts as a wrapper for its contents. Unwrapping happens during pattern matching, as in the allZero function below, which tests a Nibble to see if all its bits are b0.

{ x0 := Playground.Bit.b0, x1 := Playground.Bit.b0, x2 := Playground.Bit.b0, x3 := Playground.Bit.b0 } : NibbleStruct

2.3.6. Natural Numbers🔗

We put this portion of the chapter in a namespace so that our definition of numbers does not interfere with the one from the standard library. Our definition matches the standard one, which we will use in the rest of the book.

All the types we have defined so far — both enumerated types such as Day, MyBool, and Playground.Bit, and tuple types such as Playground.Nibble built from them — are finite. The natural numbers, on the other hand, are an infinite set, so we'll need to use a slightly richer form of inductive type declaration to represent them: recursive inductive types.

While the need for recursion is unequivocal, there are many recursively defined representations of numbers to choose from. You are certainly familiar with decimal notation (base 10), using the digits 0 through 9, for example, to form the number 123. You have likely also encountered hexadecimal notation (base 16), in which the same number is represented as 7B, or octal (base 8), where it is 173, or binary (base 2), where it is 1111011. Using an enumerated type to represent digits, we could use any of these as our representation of natural numbers.

There are circumstances in which each of these choices is useful. The binary representation is valuable in computer hardware because the digits can be represented with just two distinct voltage levels, resulting in simple circuitry.

Here we choose an even simpler unary (base 1) representation, for the sake of streamlining proofs. As a Lean datatype, it uses two constructors. The zero constructor represents the number zero. The succ constructor can be applied to the representation of the natural number n, yielding the representation of n + 1, where succ stands for "successor." The number n is then represented by n applications of succ to zero.

Here is the complete datatype definition:

With a little Lean magic, we can also arrange that ordinary numerals such as 0, 1, and 2 will be interpreted as values of our new Nat type whenever this is sensible in context. The technical details are not important.

We'll define some shorthands for numbers, putting them in the Nat namespace so we don't need to use . notation everywhere.

We can also write functions on Nat.

Look at the types of succ, pred, and minusTwo:

succ : Nat → Nat

pred : Nat → Nat

minusTwo : Nat → Nat

These are all things that can be applied to a number to yield a number. But there is a difference between succ and the other two.

Functions like pred and minusTwo are defined by giving computation rules — e.g., the definition of pred says that pred (succ (succ zero)) can be simplified to succ zero — while the definition of succ has no such behavior attached. Although it is like a function in the sense that it can be applied to an argument, it does not do anything at all! It is just the way we write down numbers.

We can also define recursive functions: functions that call themselves repeatedly down to a base case. Recursion is the essence of repeated computation in functional programming; in this course, we will make extensive use of recursive functions.

We first define a simple recursive function, even, then a slightly more sophisticated recursive function, add.

We could define odd by a similar recursive declaration, but here is a simpler way:

This function takes multiple parameters, recursing on the second:

NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.zero)))

We can also define infix notation for our add function.

NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.zero)))

2.4.1. Proving Properties about Functions in Lean🔗

Being recursive on a Nat and returning a Nat as well, add is the first example of a more sophisticated class of functions. In this chapter and beyond, we will prove properties about recursive functions like add over inductive datatypes like Nat, using simplification rules, also known as characterizing lemmas, about their behavior.

Here is a simplification rule about add:

• n + zero = n

In Lean, this rule looks like this:

NatPlayground.Nat.add_zero (n : Nat) : n + zero = n

Using our simplification rule add_zero, we can carry out a simple proof about natural numbers.

We'll walk through this proof in the next section.

2.4.2. Proof State and Tactics🔗

The rewrite tactic in the proof of add_zero_zero is used to transform the goal of the proof according to an equality. The add_zero in brackets is an argument to the rewrite tactic.

Let's walk through the theorem again in detail.

Give this proof a try (it's similar):

2.4.3. The rewrite tactic🔗

The rewrite tactic tells Lean to rewrite (part of) a goal or hypothesis based on a rule (or rules), given in square brackets. For example, given the rule add_zero, which states that n + zero is equal to n for any n, we can replace any n + zero in our proof with n via rewrite [add_zero].

2.4.4. The rfl tactic🔗

The rfl tactic closes a goal of the shape a = a, for any a. It checks that both sides of the equality are definitionally equal — that is, that they reduce to the same term. (So, in particular, a term is always definitionally equal to itself.)

2.4.5. A New add Rule🔗

Here is another fundamental rule about addition:

n + (succ m) = succ (n + m).

This is the rule we need to push succ around.

Here it is in Lean: