path: root/plt/lean.md

---
layout: plt
title: An Unofficial Lean Reference
---

# imperative programming in lean

[Lean](https://lean-lang.org/) is a combination programming language and theorem prover. It's a pretty neat language!

I found it hard to get started with, however. This guide is an attempt at remedying that.

## table of contents

- [Documentation](#documentation)
- [Prelude](#prelude)
- Evaluation
- Assignment
- Data Types
  - [Structural Types](#structural-types)
  - [Products](#products)
  - Inductive Types
  - [Sums](#sums)
  - [Booleans](#booleans)
  - [Numbers](#numbers)
  - [Lists](#lists)
  - [Strings](#strings)
- Classes
  - Coersion
- Monads
  - IO
  - Errors
  - [Iteration](#iteration)
- Modules
- Macros
- Proof
  - Dependent Types
  - Tactics

## Documentation

First: where is the documentation?

The primary source of documentation is the [Lean source code documentation][Main Docs]. Despite the URL, it covers more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, but these docs are as close as it gets.

The secondary source of documentation is the [Lean Zulip]. Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and very knowledgeable people: with both channels for compiler development and new-to-Lean questions alike.

There is additionally the [official documentation page](https://lean-lang.org/documentation/) and the [unofficial documentation page](https://leanprover-community.github.io/learn.html), which together catalogue most all of the other learning resources available for Lean.
There are also several books written for Lean. Depending on what you want to do, *[Functional Programming in Lean]* or *[Theorem Proving in Lean]* are alternately recommended. There are a good deal more, which I have not read:
- *[Mathematics in Lean]*
- *[The Mechanics of Proof]*
- *[The Hitchhiker's Guide to Logical Verification]*
- *[Metaprogramming in Lean]*

Finally, there is [the Lean manual][Lean Manual]. It is *very* much a work in progress and contains plenty of blank pages. But, I've found some sections helpful on occasion.

[Main Docs]: https://leanprover-community.github.io/mathlib4_docs/
[Lean Zulip]: https://leanprover.zulipchat.com/
[Theorem Proving in Lean]: https://leanprover.github.io/theorem_proving_in_lean4/introduction.html
[Functional Programming in Lean]: https://leanprover.github.io/functional_programming_in_lean/introduction.html
[Mathematics in Lean]: https://leanprover-community.github.io/mathematics_in_lean/
[The Mechanics of Proof]: https://hrmacbeth.github.io/math2001/
[The Hitchhiker's Guide to Logical Verification]: https://browncs1951x.github.io/static/files/hitchhikersguide.pdf
[Metaprogramming in Lean]: https://leanprover-community.github.io/lean4-metaprogramming-book/
[Lean Manual]: https://lean-lang.org/lean4/doc/

## Prelude

Second: what is *in* the language, really? Is there a syntactic reference?

The short answer is no, there is not a syntax reference, and if there existed one it wouldn't be very helpful. Lean has an extremely powerful metaprogramming system: and the majority of *syntax* in Lean is user-defined.

However. To my best understanding, the syntactic forms are as follows:
- types: `:`
  - [`structure`] [`inductive`] <span title="Coinductive types do not actually exist yet.">`coinductive`</span> [`class`] `instance`
  - `where` `instance` `extends` `deriving`
- values:
  - `""` `''` `«»` `[]` `#[]` `{}` `()` `fun` `λ`
  - `--` `/- -/` `/-- -/` `/-! -/`
  - `×` `⊕`
  - numbers `0b` `0x` ...
- assignment: `:=`
  - `def` `abbrev`
  - `let` `let rec` `let mut`
- control flow: `if`/`then`/`else` `match`/`with`
- iteration:
  - `for`/`in`/`do` `while`/`do` `repeat`
  - `return` `continue` `break`
- exceptions: `try` `catch` `finally`
- monads: `<-` [`do`] (also `failure` `pure`)
- modules:
  - `namespace`/`end` `section`/`end`
  - `open`/`in` `import`
  - `hiding` `renaming` `exposing`
  - `export` `private` `protected` ...
- modifiers: `@[...]` `partial` `noncomputable` `nonrec`
- macros:
  - `macro` `macro_rules` `notation` `syntax`
  - `infix` `infixl` `infixr` `postfix` `prefix`
- debugging: `assert!` `dbg_trace`
- proof:
  - `axiom` `theorem` `lemma`
  - `show` `from` `have` `by` `at` `this`
  - `suffices` `calc` `admit`
- holes: `sorry` `stop`
- evaluation: `#eval` `#check` `#check_failure` `#reduce` `#print`

[`structure`]: https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html
[`inductive`]: https://leanprover.github.io/functional_programming_in_lean/getting-to-know/datatypes-and-patterns.html
[`class`]: https://leanprover.github.io/functional_programming_in_lean/type-classes/polymorphism.html

[`do`]: https://lean-lang.org/lean4/doc/do.html

This list is unlikely to be comprehensive.

The standard data types included in core Lean are the following:
- unit: [`Unit`]
- booleans: [`Bool`]
- numbers: [`Nat`] [`Int`] [`Fin n`]
  - [`USize`] [`UInt8`] [`UInt16`] [`UInt32`] [`UInt64`] [`BitVec w`]
- strings: [`Char`] [`String`] [`Substring`]
- lists: [`List α`] [`Array α`] [`Subarray`]
  - [`ByteArray`] [`FloatArray`]
  - (see also: [`Batteries.Vector α n`])
- errors: [`Option α`] [`Except ε α`]
- data: [`Prod α β`] [`Sum α β`]
  - (see also: `structure` `inductive`)
- types: [`Empty`] [`Nonempty`] [`Type`/`Prop`/`Type u`/`Sort u`]
- proof:
  - [`And α β`] [`Or α β`] [`Iff α β`] [`True`] [`False`]
  - [`Eq α β`] [`Equivalence`]
  - [`Exists`] (where is `Forall`?)

[`Unit`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Unit
[`Bool`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Bool
[`Nat`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat
[`Int`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/Int/Basic.html
[`Fin n`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Fin
[`USize`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#USize
[`UInt8`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt8
[`UInt16`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt16
[`UInt32`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt32
[`UInt64`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt64
[`BitVec w`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/BitVec/Basic.html
[`Char`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Char
[`String`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#String
[`Substring`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Substring
[`List α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#List
[`Array α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Array
[`Subarray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Subarray
[`Batteries.Vector α n`]: https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/Vector/Basic.html
[`ByteArray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/ByteArray/Basic.html
[`FloatArray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/FloatArray/Basic.html
[`Option α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Option
[`Except ε α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Except
[`Prod α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Prod
[`Sum α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Sum
[`Empty`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Empty
[`Nonempty`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nonempty
[`Type`/`Prop`/`Type u`/`Sort u`]: https://leanprover-community.github.io/mathlib4_docs/foundational_types.html
[`And α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#And
[`Or α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Or
[`Iff α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff
[`True`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#True
[`False`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#False
[`Eq α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Eq
[`Equivalence`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Equivalence
[`Exists`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Exists

The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*.

(If you are not writing Lean in VS Code, by the way, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.)

## Evaluation

## Assignment

## Data Types

### Structural Types

The `structure` type is analogous to structs in other languages. It behaves much as one would expect.

```lean
structure Header where
  (width height : Nat)
  alpha : Bool
  linear := false

let header : Header := {
  width := 1920
  height := 1080
  alpha := true
}

def increment_height (header : Header) : Header :=
  let {width, height, alpha, linear} := header
  let height := height + 1
  {width, height, alpha, linear}
```

Structures may be declared with the `structure ... where` syntax. Just like functions, multiple fields of the same type may be grouped together, and default values are supported. An individual field with a default value may be omitted in the constructor. A field of a function may or may not be wrapped in parentheses, but parentheses are required for multiple fields of the same type.

Structures may be constructed with braces. The braces are syntactic sugar for an underlying `Name.mk` constructor. Their fields take the form `field := value`, separated either by newlines or by commas. If `value` is a variable of the same name as `field`, the `field :=` portion may be omitted. The brace constructors are *structural*: the order in which fields are declared does not matter, only their name does.

Structures may be destructured either by pattern matching or with dot notation for field access. Pattern matching may be done via `match` or inline via `let` with the `{}` syntax.

They cannot be mutated: Lean is functional and so there is no explicit syntax for updating a field. `header.width ← ...` does nothing, even if `header` is declared to be mutable. Instead, the entire `header` structure must be updated at once. This can be a pain on large structures, so Lean provides the `with` keyword for succiently (re-)constructing a structure with only a few fields changed. The `increment_height` function above can thus be compactly declared as the following:
```lean
def increment_height (header : Header) : Header :=
  { header with height := header.height + 1 }
```

Structures may *extend* one another. A structure inherits all the fields of the structures it extends (which must not conflict), and can declare new fields. Default values may be redefined but fields may not be. As a type may not be referenced before its declaration, cyclic extensions cannot be formed.
```lean
structure Point where
  (x y : Int)

structure Color where
  (r g b a : UInt8)

structure Pixel extends Point, Color
  -- implicit fields:
  -- (x y : Int)
  -- (r g b a : UInt8)
```

Structures may also parametrize over terms or other types. todo

Be warned - the `where` in a `structure` declaration is mandatory. Leaving off the `where` will result in a (valid!) structure with *zero* fields, that is instead *parametrized* over what were intended to be the fields. This can lead to strange type errors.


See also: [FPIL:Structures](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html), [FPIL:Structures and Inheritance](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad/inheritance.html), [Manual:Structures](https://lean-lang.org/lean4/doc/struct.html)

### Products

Sometimes, it is convenient to not need to bother with naming structures or their fields. Whether inline within the definition of a more complex type, or as the return type of a helper function, it can be the case that having explicit names is more trouble than it is worth.

Lean provides a type for *anonymous structures*, that behave in a very similar fashion to *tuples* in other languages. This is called `Prod` on analogy with `Sum` (which we will see later) and is defined as follows:
```lean
structure Prod (α : Type) (β : Type) where
  fst : α
  snd : β

abbrev Image := (Header × Array Pixel)
let image : Image := (header, #[])

#check (image.fst : Header)
```

Lean also provides the compact `α × β` notation as syntactic sugar for `Prod α β`. With Lean's rules around function application, tuples of arbitrary arity can be written `α × β × γ × ...`, which is equivalent to `α × (β × (γ × ...))` (and `Prod α Prod β Prod γ ...`).

While products can be constructed with `Prod.mk a b` or `{ fst := a, snd := b }`, there is also provides tuple-like notation for constructing them: `(a, b, ...)`. This is overloaded to function for products of arbitrary arity. Similar to tuples elsewhere, the `.fst` and `.snd` destructors have aliases to `.1` and `.2`, respectively - however, there do not exist aliases for the rest of the natural numbers.

The name `Prod` comes from type theory (and category theory more broadly). Structures are a special case of what is more generally called a "product": a vast generalization of the idea of taking a "pair" of something. The design of the `Prod` type aligns significantly closer to the specific formal notion of a "product type" in type theory than `structure` does, making it additionally quite useful for mathematicians.

See also: [FPIL:Polymorphism#Prod](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/polymorphism.html#prod)

### Inductive Types

### Sums

Similarly to [products](#products), it is sometimes convenient to not need to bother with naming inductives or their variants.

The `Sum` type provides for this. It is defined as follows:
```lean
inductive Sum (α : Type) (β : Type) where
  | inl (val : α)
  | inr (val : β)
```

Lean provides the compact `α ⊕ β` notation as syntactic sugar for `Sum α β`. This generalizes to sums of arbitrary length: `α ⊕ β ⊕ γ ⊕ ...`. There is no syntactic sugar for `Sum.inl` and `Sum.inr`: sums must be explicitly constructed. There is also no syntactic sugar for destructuring: `match` must be used.

See also: [FPIL/Polymorphism#Sum](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#sum)

### Booleans

Lean provides a `Bool` type, defined as an inductive data type:
```lean
inductive Bool where
  | false
  | true
```

The `true` and `false` terms are exported in the Prelude and do not need to be prefixed with `Bool`. Standard `if`/`else` destructors are also provided. `else if` is special cased in the parser to behave nicely.

`if` is also overloaded to function with `let` to provide a compact alternative to a `match` statement.
```lean
let a := Chunk.rgb 1 2 3
if let {r, g, b} := a then
  IO.println s!"red: {r}, green: {g}, blue: {b}"

### Numbers

Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], and [`Fin n`].

`Nat` is an arbitrary-sized number type. It is defined as the following:
```lean
-- Zero is a natural number.
-- The successor of a natural number is a natural number.
inductive Nat where
  | zero
  | succ (n : Nat)
```

Lean recognizes numeric literals (`0`, `1`, `2`...) as numeric constructors, equivalent to their `Nat.succ (Nat.succ ...)` counterparts. Special compiler support allows for representing `Nats` in a reasonable / efficient fashion: numbers smaller than `2^63` are stored directly, while numbers larger than `2^63 - 1` use an arbitrary precision BigInt library.

It should be noted that Lean treats operations on `Nat` that would produce a negative number **as producing zero**. For example, `#check 4 - 5` prints `4 - 5 : Nat`, and `#eval 4 - 5` prints `0`.

[`Int`] is an extension of `Nat` to also represent negative numbers. It is similarly special-cased by the compiler. Lean recognizes (..., `-2`, `-1`) as equivalent to their `Int.negSucc n` counterparts, and will also implicitly cast (`0`, `1`, `2`...) to `Int` as required.
```lean
-- A natural number is an integer.
-- The negation of the *successor* of a natural number is an integer.
-- (the above is enforced by compiler magic)
inductive Int where
  | ofNat (n : Nat)   -- [0 : ∞)
  | negSucc (n : Nat) -- (-∞ : -1]
```

[`Fin n`] is a natural number guaranteed to be *smaller* than `n`: i.e. `i ∈ ℕ : 0 ≤ i < n`. The underlying representation is `val : Nat` and a proof that the `val < n`.
```lean
-- If i : Fin n, then i.val : Nat is the described number.
-- It can also be written as i.1 or just i when the target type is known.
-- If i : Fin n, then i.isLt is a proof that i.val < n.
structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n
```

Lean supports the following fixed-width integers: [`UInt8`], [`UInt16`], [`UInt32`], [`UInt64`], [`USize`]. They behave as one would expect. `USize` takes the size of a pointer on its appropriate platforms. Lean also supports *arbitrary* fixed-width integers with [`BitVec w`]. They are treated internally as `Fin (2 ^ w)`, and gain all the special support for math that `Fin n` and subsequently `Nat` has.

Lean is good at typechecking numbers. For example, the following code compiles:
```lean
abbrev UInt6 := BitVec 6
structure Pixel where
  (r g b a : UInt8)

def hash (pixel : Pixel) : UInt6 :=
  -- Lean recognizes the resulting value cannot be larger than 2^6 - 1 or 6 bits, via % 64.
  (pixel.r.val * 3 + pixel.g.val * 5 + pixel.b.val * 7 + pixel.a.val * 11) % 64
```

The expected basic mathematical operations are defined on all numbers. Their semantics differ depending on the specific numeric type.
- arithmetic: `+`, `-`, `*`, `/`, `%`, `∣`
- comparison: `<`, `>`, `<=`/`≤`, `>=`/`≥`
- bitwise: `&&&`, `|||`, `^^^`, `~~~`
- shifts: `<<<` and `>>>`

Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods.

### Lists

Lean provides for several representations of list-like data structures.

[`List α`] is the standard representation. It is represented as a linked list, and defined as the following:
```lean
inductive List (α : Type u) where
  | nil
  | cons (head : α) (tail : List α)
```

`List.nil` or more commonly `[]` represents the empty list. `List.cons a l` or `a :: l` (for some `a : α`, `l : List α`) are used for list concatenation. `[a, b, c, ...]` syntax can also be used for construction of lists. Various functions and classes are defined for and on lists.

[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. `Arrays` are significantly more performant than `Lists`: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", all updates will be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages.

You usually want to use `Array`. However: currently `Arrays` are represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays.

`Array` has a different syntax for its constructor: `#[a, b, c]`. It does overload `a :: l`.

The [`Batteries.Vector α n`] type is not in `Std`, but worth a mention. It is a *statically sized array*: represented under the hood by `Array`, but guaranteed to not change size throughout its existence.

All lists provide postfix `foo[i]` syntax for accessing arbitrary array elements. There are three variations:
- `foo[i]` takes an `i : Fin n`, where `n < foo.size`. If this cannot be proven it fails to compile.
- `foo[i]?` returns an `Option α`.
- `foo[i]!` returns an `α` or panics.

See also: [FPIL:Polymorphism#Linked Lists](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#linked-lists), [Manual:Arrays](https://lean-lang.org/lean4/doc/array.html)

### Strings

The [`String`] type represents a UTF-8 encoded string. It is treated as a `List Char`, but represented as a packed `ByteArray`. Strings are constructed via `""`.

The [`Char`] type represents a "Unicode scalar value": that is, a codepoint. The underlying value is represented (presumably) in UTF-32 as a `UInt32`. Chars are constructed via `''`.

String manipulation can be inefficient. The [`Substring`] type provides an immutable *view* into some subslice of a `String`.

## Classes

### Coersion


## Monads

The [Functional Programming in Lean] book contains extensive information on monads in Lean: [FPIL:Monads](https://leanprover.github.io/functional_programming_in_lean/monads.html), [FPIL:Functors, Applicative Functors, and Monads](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad.html), [FPIL:Monad Transformers](https://leanprover.github.io/functional_programming_in_lean/monad-transformers.html).

Those interested in theory and the intricate details may look there. I intend to present a purely-workable overview of the language features implemented *atop* monads.

### IO

### Errors

Lean encodes errors as monads. The [`Option α`] type is by far the most used.

An `Option α` is the following type:
```lean
inductive Option (α : Type) where
  | none
  | some (val : α)
```

There are other forms of errors. The [`Except ε α`] type allows for encoding a specific error type:
```lean
inductive Except (ε : Type) (α : Type) where
  | error (err : ε)
  | ok (val : α)
```

### Iteration

Lean has three main syntactic constructs for iteration: `for`, `while`, and `repeat`. They all function pretty much as you would expect and ultimately desugar to lambdas and (tail) recursion.

However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of side effects. And `for`/`while`/`repeat` return only the Unit value, providing no information.

Iteration is thus *useless* in the pure context! We can iterate, for sure, but there may never be any *observable* changes. As such, Lean does not allow `for`/`while`/`repeat` within pure functions. This can be the cause of some strange type errors. Ensure you are only iterating in a monadic `do` context.

It should be noted that the `do` in `for/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.

### implementing iterators: `ForIn` and `Stream`

`for` desugars to an appliction of the `ForIn.forIn` method, so that data structures can implement individually what exactly iteration means for them.

The iteration implemented by `ForIn` is called "internal iteration", which means it is a higher order function where you give the body of the loop to it to run on the elements yielded by the iterator in order. This is in contrast to "external iteration" (in the style of ex. Rust), where the iterator has a function returning the next value of the iterator.

One reason to prefer internal iteration is that it is easier to verify termination. This is something Lean cares very much about. But, internal iteration is a less flexible model than external iteration. You can't quite just convert an internal iterator to an external iterator. So there are some downsides.

Lean also has an external iteration typeclass, called `Stream`, but it is not used as much. `Stream α` provides a `.next?` method that returns an `Option (α × Stream α)`: however, because Lean is purely functional, the burden is on the user to use this new `Stream α`.

It is perhaps possible to do external iteration via the State monad. I would like to try this out.

## Modules

## Macros

The standard reference is [Metaprogramming in Lean](https://leanprover-community.github.io/lean4-metaprogramming-book/).

I will make no attempt to describe Lean's system in detail: but I do plan to provide a high-level overview.

## Proof

A text for type theorists is [Theorem Proving in Lean].
A text for mathematicians is [Mathematics in Lean].
A text for those new to mathematics is [The Mechanics of Proof].