# 3. Lean as a Programming Language

## 3.1. About Lean

*Lean 4* is a new programming language and interactive proof assistant.
It is currently used to formalize mathematics, to verify hardware and software,
and to explore applications of machine learning to mathematical reasoning.
Though the system is still new and under active development,
in many ways it is an ideal system for working with logical syntax
and putting logic to use.

You can learn more about Lean on the Lean home page, on the Lean community home page, and by asking questions on the Lean Zulip chat, which you are heartily encouraged to join. Lean has a very large mathematical library, known as mathlib, which you can learn more about on the Lean community pages.

The following documentation is available:

As a functional programming language, Lean bears some similarity to Haskell and OCaml. If you are new to functional programming, you might also find it helpful to consult an introduction to functional programming in Haskell. Lean 4 has a number of interesting features, and it is designed for implementing powerful logic-based systems, as evidenced by the fact that most of Lean 4 is implemented in Lean 4 itself.

The goal of this section is to give you a better sense of what Lean is, how it can possibly be a programming language and proof assistant at the same time, and why that makes sense. The rest of this section will give you a quick tour of some of its features, and we will learn more about them as the course progresses.

At the core, Lean is an implementation of a formal logical foundation known as *type theory*.
More specifically, it is an implementation of *dependent type theory*, and even
more specifically than that, it implements a version of the *Calculus of Inductive Constructions*.
Saying that it implements a formal logic foundation means that there is a precise
grammar for writing expressions, and precise rules for using them.
In Lean, every well-formed expression has a type.

```
#check 2 + 2
#check -5
#check [1, 2, 3]
#check #[1, 2, 3]
#check (1, 2, 3)
#check "hello world"
#check true
#check fun x => x + 1
#check fun x => if x = 1 then "yes" else "no"
```

You can find this example in the file using_lean_as_a_programming_language/examples1.lean in the
LAMR/Examples folder of the course repository.
We strongly recommend copying that entire folder into the `User`

folder,
so you can edit the files and try examples of your own.
That way, you can always find the original file in the folder `LAMR/Examples`

,
which you should not edit.
It will also make it easier to update your copy when we make changes.

If you hover over the `#check`

statements or move your cursor to one
of these lines and check the information window,
Lean reports the result of the command.
It tells you that `2 + 2`

has type `Nat`

, `-5`

has type `Int`

, and so on.
In fact, in the formal foundation, types are expressions as well.
The types of all the expressions above are listed below:

```
#check Nat
#check Int
#check List Nat
#check Array Nat
#check Nat × Nat × Nat
#check String
#check Bool
#check Nat → Nat
#check Nat → String
```

Now Lean tells you each of these has type `Type`

, indicating that they are
all data types. If you know the type of an expression, you can ask Lean to confirm it:

```
#check (2 + 2 : Nat)
#check ([1, 2, 3] : List Nat)
```

Lean will report an error if it cannot construe the expression as having the indicated type.

In Lean, you can define new objects with the `def`

command.
The new definition becomes part of the *environment*: the defined expression
is associated with the identifier that appears after the word `def`

.

```
def four : Nat := 2 + 2
def isOne (x : Nat) : String := if x = 1 then "yes" else "no"
#check four
#print four
#check isOne
#print isOne
```

The type annotations indicate the intended types of the arguments and the result, but they can be omitted when Lean can infer them from the context:

```
def four' := 2 + 2
def isOne' x := if x = 1 then "yes" else "no"
```

So far, so good: in Lean, we can define expressions and check their types.
What makes Lean into a programming language is that the logical foundation has
a computational semantics, under which expressions can be *evaluated*.

```
#eval four
#eval isOne 3
#eval isOne 1
```

The `#eval`

command evaluates the expression and then
displays the return value.
Evaluation can also have *side effects*,
which are generally related to system IO.
For example, displaying the string “Hello, world!”
is a side effect of the following evaluation:

```
#eval IO.println "Hello, world!"
```

Theoretical computer scientists are used to thinking about programs as expressions and identifying the act of running the program with the act of evaluating the expression. In Lean, this view is made manifest, and the expressions are defined in a formal system with a precise specification.

But what makes Lean into a proof assistant? To start with, some expressions in the proof system express propositions:

```
#check 2 + 2 = 4
#check 2 + 2 < 5
#check isOne 3 = "no"
#check 2 + 2 < 5 ∧ isOne 3 = "no"
```

Lean confirms that each of these is a proposition
by reporting that each of them has type `Prop`

.
Notice that they do not all express *true* propositions;
theorem proving is about certifying the ones that are.
But the language of Lean is flexible enough to express just about
any meaningful mathematical statement at all. For example,
here is the statement of Fermat’s last theorem:

```
def Fermat_statement : Prop :=
∀ a b c n : Nat, a * b * c ≠ 0 ∧ n > 2 → a^n + b^n ≠ c^n
```

In Lean’s formal system, data types are expressions of type `Type`

,
and if `T`

is a type, an expression of type `T`

denotes an object
of that type. We have also seen that propositions are expressions
of type `Prop`

. In the formal system, if `P`

is a proposition,
a proof of `P`

is just an expression of type `P`

.
This is the final piece of the puzzle:
we use Lean as a proof assistant by writing down a proposition `P`

,
writing down an expression `p`

, and asking Lean to confirm that
`p`

has type `P`

. The fact that 2 + 2 = 4 has an easy proof,
that we will explain later:

```
theorem two_plus_two_is_four : 2 + 2 = 4 := rfl
```

In contrast, proving Fermat’s last theorem is considerably harder.

```
theorem Fermat_last_theorem : Fermat_statement := sorry
```

Lean knows that `sorry`

is not a real proof, and it flags a warning there.
If you manage to replace `sorry`

by a real Lean expression, please let us know.
We will be very impressed.

So, in Lean, one can write programs and execute them, and one can state
propositions and prove them.
In fact, one can state propositions about programs and then prove those
statements as well.
This is known as *software verification*; it is a means of obtaining
a strong guarantee that
a computer program behaves as intended, something that is important,
say, if you are using the software to control a nuclear reactor or
fly an airplane.

This course is not about software verification. We will be using Lean 4 primarily as a programming language, one in which we can easily define logical expressions and manipulate them. To a small extent, we will also write some simple proofs in Lean. This will help us think about proof systems and rules, and understand how they work. Taken together, these two activities embody the general vision that animates this course: knowing how to work with formally specified expressions and rules opens up a world of opportunity. It is the key to unlocking the secrets of the universe.

## 3.2. Using Lean as a functional programming language

The fact that Lean is a functional programming language means
that instead of presenting a program as a list of instructions,
you simply *define* functions and ask Lean to evaluate them.

```
def foo n := 3 * n + 7
#eval foo 3
#eval foo (foo 3)
def bar n := foo (foo n) + 3
#eval bar 3
#eval bar (bar 3)
```

There is no global state: any value a function can act on is passed as an explicit argument and is never changed. For that reason, functional programming languages are amenable to parallelization.

Nonetheless, Lean can do handle system IO using the *IO monad*,
and can accommodate an imperative style of programming using *do notation*.

```
def printExample : IO Unit:= do
IO.println "hello"
IO.println "world"
#eval printExample
```

Recursive definitions are built into Lean.

```
def factorial : Nat → Nat
| 0 => 1
| (n + 1) => (n + 1) * factorial n
#eval factorial 10
#eval factorial 100
```

Here is a solution to the Towers of Hanoi problem:

```
def hanoi (numDisks start finish aux : Nat) : IO Unit :=
match numDisks with
| 0 => pure ()
| n + 1 => do
hanoi n start aux finish
IO.println s!"Move disk {n + 1} from peg {start} to peg {finish}"
hanoi n aux finish start
#eval hanoi 7 1 2 3
```

You can also define things by recursion on lists:

```
def addNums : List Nat → Nat
| [] => 0
| a::as => a + addNums as
#eval addNums [0, 1, 2, 3, 4, 5, 6]
```

In fact, there are a number of useful functions built
into Lean’s library. The function `List.range n`

returns the list
`[0, 1, ..., n-1]`

, and the functions `List.map`

and `List.foldl`

and `List.foldr`

implement the usual map and fold functions for lists.
By opening the `List`

namespace, we can refer to these as `range`

, `map`

,
`foldl`

, and `foldr`

. In the examples below,
the operation `<|`

has the same effect as putting parentheses around
everything that appears afterward.

```
#eval List.range 7
section
open List
#eval range 7
#eval addNums <| range 7
#eval map (fun x => x + 3) <| range 7
#eval foldl (. + .) 0 <| range 7
end
```

The scope of the `open`

command is limited to the section,
and the cryptic inscription `(. + .)`

is notation for the
addition function. Lean also supports projection notation
that is useful when the corresponding namespace is not open:

```
def myRange := List.range 7
#eval myRange.map fun x => x + 3
```

Because `myRange`

has type `List Nat`

, Lean interprets
`myrange.map fun x => x + 3`

as `List.map (fun x => x + 3) myrange`

.
In other words, it automatically interprets `map`

as being
in the `List`

namespace,
and then it interprets `myrange`

as the first `List`

argument.

This course assumes you have some familiarity with functional programming. One way to cope with the fact that there is not yet much documentation for Lean is to nose around the Lean code base itself. If you ctrl-click on the name of a function in the Lean library, the editor will jump to the definition, and you can look around and see what else is there. Another strategy is simply to ask us, ask each other, or ask questions on the Lean Zulip chat. We are all in this together.

When working with a functional programming language,
there are often clever tricks for doing things that you
may be more comfortable doing in an imperative programming language.
For example, as explained in Section 2.3,
here are Lean’s definitions of the `reverse`

and `append`

functions for lists:

```
namespace hidden
def reverseAux : List α → List α → List α
| [], r => r
| a::l, r => reverseAux l (a::r)
def reverse (as : List α) :List α :=
reverseAux as []
protected def append (as bs : List α) : List α :=
reverseAux as.reverse bs
end hidden
```

The function `reverseAux l r`

reverses the elements of list `l`

and adds them to the front of `r`

. When called from `reverse l`

,
the argument `r`

acts as an *accumulator*, storing the partial result.
Because `reverseAux`

is tail recursive, Lean’s compiler
can implement it efficiently as a loop rather than a recursive function.
We have defined these functions in a namespace named `hidden`

so that they don’t conflict with the ones in Lean’s library
if you open the `List`

namespace.

In Lean’s foundation, every function is totally defined.
In particular, every function that Lean computes has to
terminates (in principle) on every input.
Lean 4 will eventually support arbitrary recursive definitions in which
the arguments in a recursive call decrease by some measure,
but some work is needed to justify these calls in the underlying
foundation. In the meanwhile, we can always cheat by using the `partial`

keyword,
which will let us perform arbitrary recursive calls.

```
partial def gcd m n :=
if n = 0 then m else gcd n (m % n)
#eval gcd 45 30
#eval gcd 37252 49824
```

Using `partial`

takes us outside the formal foundation; Lean
will not let us prove anything about `gcd`

when we define it this way.
Using `partial`

also makes it easy for us to shoot ourselves in the foot:

```
partial def bad (n : Nat) : Nat := bad (n + 1)
```

On homework exercises, you should try to use structural recursion
when you can,
but don’t hesitate to use `partial`

whenever Lean complains
about a recursive definition.
We will not penalize you for it.

The following definition of the Fibonacci numbers does not require
the `partial`

keyword:

```
def fib' : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fib' (n + 1) + fib' n
```

But it is inefficient; you should convince yourself that the natural evaluation strategy requires exponential time. The following definition avoids that.

```
def fibAux : Nat → Nat × Nat
| 0 => (0, 1)
| n + 1 => let p := fibAux n
(p.2, p.1 + p.2)
def fib n := (fibAux n).1
#eval (List.range 20).map fib
```

Producing a *list* of Fibonacci numbers, however, as we have done here
is inefficient; you should convince yourself that the running
time is quadratic.
In the exercises, we ask you to define a function that computes
a list of Fibonacci values with running time linear in the
length of the list.

## 3.3. Inductive data types in Lean

One reason that computer scientists and logicians tend to like functional programming languages is that they often provide good support for defining inductive data types and then using structural recursion on such types. For example, here is a Lean definition of the extended binary trees that we defined in mathematical terms in Section 2.3:

```
inductive BinTree
| empty : BinTree
| node : BinTree → BinTree → BinTree
deriving Repr, DecidableEq, Inhabited
open BinTree
```

The command `import Init`

imports a part of the initial library for us to use.
The command `open BinTree`

allows us to write `empty`

and `node`

instead of
`BinTree.empty`

and `BinTree.node`

.
Note the Lean convention of capitalizing the names of data types.

The last line of the definition, the one that begins with the word `deriving`

,
is boilerplate.
It tells Lean to automatically generate a few additional functions that are
useful. The directive `deriving Repr`

tells Lean to define an internal function
that can be used to represent any `BinTree`

as a string.
This is the string that is printed out by any `#eval`

command whose argument
evaluates to a `BinTree`

.
Adding `DecidableEq`

defines a function that tests whether two `BinTrees`

are equal,
and adding `Inhabited`

defines an arbitrary value of the data type to serve as
a default value for function that need one. The following illustrates their use.

```
#eval node empty (node empty empty)
#eval empty == node empty empty -- evaluates to false
#eval (default : BinTree) -- BinTree.empty
```

We can now define the functions `size`

and `depth`

by structural recursion:

```
def size : BinTree → Nat
| empty => 0
| node a b => 1 + size a + size b
def depth : BinTree → Nat
| empty => 0
| node a b => 1 + Nat.max (depth a) (depth b)
def example_tree := node (node empty empty) (node empty (node empty empty))
#eval size example_tree
#eval depth example_tree
```

Lean also supports `match`

syntax.

```
def foo (b : BinTree) : Nat :=
match b with
| empty => 0
| node _ _ => 1
#eval foo (node empty empty)
```

In fact, the `List`

data type is also inductively defined.

```
#print List
```

You should try writing the inductive definition on your own. Call
it `MyList`

, and then try `#print MyList`

to see how it compares.

`Option`

types are commonly used in functional programming to
represent functions that might fail to return a value.
For any type `α`

, and element of type `Option α`

is either
of the form `some a`

, where `a`

is an element of `α`

, or `none`

.
You can use a `match`

to determine which case we are in.

```
#print Option
def bar (n? : Option Nat) : Nat :=
match n? with
| some n => n
| none => 0
#eval bar (some 5)
#eval bar none
```

It is a Lean convention to use variable names like `n?`

to range over an option type.
Similarly, functions that return an element of an option type
usually have names that end with a question mark.
The function `Option.getD`

can be used to return a default
value in case the input is none.

```
#eval (some 5).getD 0
#eval none.getD 0
```

## 3.4. Using Lean as an imperative programming language

The fact that Lean is a functional programming language means that there
is no global notion of *state*.
Functions take values as input and return values as output;
there are no global or even local variables that are changed by
the result of a function call.

But one of the interesting features of Lean is a functional programming language is
that it incorporates features that make it *feel* like an imperative programming
language. The following example shows how to print out, for each value \(i\)
less than 100, the the sum of the numbers up to \(i\).

```
def showSums : IO Unit := do
let mut sum := 0
for i in [0:100] do
sum := sum + i
IO.println s!"i: {i}, sum: {sum}"
#eval showSums
```

You can use a loop not just to print values, but also to compute values. The following is a boolean test for primality:

```
def isPrime (n : Nat) : Bool := Id.run do
if n < 2 then false else
for i in [2:n] do
if n % i = 0 then
return false
if i * i > n then
return true
true
```

You can use such a function with the list primitives to construct a list of the first 10,000 prime numbers.

Note that in both cases, the program begins with the special
identifier `do`

,
which invokes notation that makes sense when the return type is what
is known as a *monad*.
In the first case, the return value is in the `IO`

monad.
You can think of the fact that `showSums`

has type `IO Unit`

as saying that it doesn’t return any data but has *side effects*, namely, sending output to the standard output channel.
In the second case, `Bool`

is not a monad, but Lean allows us
to treat it as one by inserting the prefix `Id.run`

.
Technically, it is reinterpreting `Bool`

as `Id Bool`

,
where `Id`

is the *identity monad*.
Don’t worry about the details, though.
For the most part, you can treat `do`

notation as a magical black box.

```
#eval (List.range 10000).filter isPrime
```

Within a `do`

block, there is nice syntax for handling option types.

```
def bar (n? : Option Nat) : IO Unit := do
let some n := n? |
IO.println "oops"
IO.println n
#eval bar (some 2)
#eval bar none
```

You can also combine `do`

blocks with Lean’s support for *arrays*.
Within the formal foundation these are modeled as lists,
but the compiler implements them as dynamic arrays, and for efficiency
it will modify values rather than copy them whenever the old value is
not referred to by another part of an expression.

```
def primes (n : Nat) : Array Nat := Id.run do
let mut result := #[]
for i in [2:n] do
if isPrime i then
result := result.push i
result
#eval (primes 10000).size
```

Notice the notation: `#[]`

denotes a fresh array (Lean infers the type from context),
and the `Array.push`

function adds a new element at the end of the array.

The following example shows how to compute a two-dimensional array, a ten by ten multiplication table.

```
def mulTable : Array (Array Nat) := Id.run do
let mut table := #[]
for i in [:10] do
let mut row := #[]
for j in [:10] do
row := row.push ((i + 1) * (j + 1))
table := table.push row
table
#eval mulTable
```

Alternatively, you can use the function `Array.mkArray`

to initialize an array
(in this case, to the values 0), and then use the `Array.set!`

function
to replace the elements later one.

```
def mulTable' : Array (Array Nat) := Id.run do
let mut s : Array (Array Nat) := mkArray 10 (mkArray 10 0)
for i in [:10] do
for j in [:10] do
s := s.set! i <| s[i]!.set! j ((i + 1) * (j + 1))
s
```

Here we replace the ith row by the previous ith row, with the jth column updated.
The notation `s[i]!`

asks Lean’s type checker to trust that the array access is
within bounds. If it isn’t, Lean will throw an error at runtime.
Lean also provides mechanisms by which we can provide a *static* guarantee
that the array access is in bounds by providing a proof. But talking about how to do that
now would take us too far afield.

The following snippet prints out the table. The idiom `show T from t`

is a way of telling Lean that term `t`

should have type `T`

.
Writing `@id T t`

has a similar effect, as does writing `(t : T)`

.
(A difference is that the first two expressions have type `T`

exactly,
whereas `(t : T)`

only ensures that `t`

has a type that Lean recognizes as being
equivalent to `T`

.)

```
#eval show IO Unit from do
for i in [:10] do
for j in [:10] do
let numstr := toString mulTable[i]![j]!
-- print 1-3 spaces
IO.print <| " ".pushn ' ' (3 - numstr.length)
IO.print numstr
IO.println ""
```

## 3.5. Exercises

Using operations on

`List`

, write a Lean function that for every \(n\) returns the list of all the divisors of \(n\) that are less than \(n\).A natural number \(n\) is

*perfect*if it is equal to the sum of the divisors less than \(n.\) Write a Lean function (with return type Bool) that determines whether a number \(n\) is perfect. Use it to find all the perfect numbers less than 1,000.Define a recursive function \(\fn{sublists}(\ell)\) that, for every list \(\ell\), returns a list of all the sublists of \(\ell\). For example, given the list \([1, 2, 3]\), it should compute the list

\[[ [], [1], [2], [3], [1,2], [1,3], [2, 3], [1, 2, 3] ].\]The elements need not be listed in that same order.

Prove in Lean that the length of \(\fn{sublists}(\ell)\) is \(2^{\fn{length}(\ell)}\).

Define a function \(\fn{permutations}(\ell)\) that returns a list of all the permutations of \(\ell\).

Prove in Lean that the length of \(\fn{permutations}(\ell)\) is \(\fn{factorial}(\fn{length}(\ell))\).

Define in Lean a function that, assuming \(\ell\) is a list of lists representing an \(n \times n\) array, returns a list of lists representing the transpose of that array.

Write a program that solves the Tower of Hanoi problem with \(n\) disks on the assumption that disks can only be moved to an

*adjacent*peg. (See Section 2.5.)Write a program that solves the Tower of Hanoi problem with \(n\) disks on the assumption that disks can only be moved clockwise. (See Section 2.5.)

Define a Lean data type of binary trees in which every node is numbered by a label. Define a Lean function to compute the sum of the nodes in such a tree. Also write functions to list the elements in a preorder, postorder, and inorder traversal.

Write a Lean function

`pascal`

which, on input`n`

, outputs the first`n`

rows of Pascal’s triangle.