The Lean Theorem Prover | Homotopy Type Theory

The Lean Theorem Prover

Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development for the foreseeable future. The code is open source, and available on Github.

You can install it on Windows, OS X or Linux. It will come with a useful mode for Emacs, with syntax highlighting, on-the-fly syntax checking, autocompletion and many other features. There is also an online version of Lean which you can try in your browser. The on-line version is quite a bit slower than the native version and it takes a little while to load, but it is still useful to try out small code snippets. You are invited to test the code snippets in this post in the on-line version. You can run code by pressing shift+enter.

In this post I’ll first say more about the Lean proof assistant, and then talk about the considerations for the HoTT library of Lean (Lean has two libraries, the standard library and the HoTT library). I will also cover our approach to higher inductive types. Since Lean is not mature yet, things mentioned below can change in the future.

Update January 2017: the newest version of Lean currently doesn’t support HoTT, but there is a frozen version which does support HoTT. The newest version is available here, and the frozen version is available here. To use the frozen version, you will have to compile it from the source code yourself.

Examples

First let’s go through some examples. Don’t worry if you don’t fully understand these examples for now, I’ll go over the features in more detail below. You can use the commands check, print and eval to ask Lean for information. I will give the output as a comment, which is a double dash in Lean. check just gives the type of an expression.

This states that this sigma-type lives in the lowest universe in Lean (since ℕ and le live in the lowest universe). Unicode can be input (in both the browser version and the Emacs version) using a backslash. For example Σ is input by \Sigma or \S. In the browser version you have to hit space to convert it to Unicode.

check is useful to see the type of a theorem (the curly braces indicate that those arguments are implicit).

print can show definitions.

It prints which notation uses a particular symbol.

And it prints inductive definitions.

eval evaluates an expression.

The Kernel

Lean is a proof assistant with as logic dependent type theory with inductive types and universes, just as Coq and Agda. It has a small kernel, which implements only the following components:

• Dependent lambda calculus
• Universe polymorphism in a hierarchy of many universe levels
• Inductive types and inductive families of types, generating only the recursor for an inductive type.

In particular it does not contain

• A Termination checker
• Fixpoint operators
• Pattern matching
• Module management and overloading

Let’s discuss the above features in more detail. The function types are exactly as in the book with judgemental beta and eta rules. There are a lot of different notations for functions and function types, for example

Lean supports universe polymorphism. So if you define the identity function as follows

you actually get a function my_id.{u} for every universe u. You rarely have to write universes explicitly, but you can always give them explicitly if you want. For example:

The universes in Lean are not cumulative. However, with universe polymorphism universe cumulativity is rarely needed. In the cases where you would use universe cumulativity you can use the lift map explicitly. There are only a handful of definitions or theorems (less than 10) currently in the HoTT library where lifts are needed (if it is not proving something about lifts itself). Some examples:

• In the proof that univalence implies function extensionality;
• In the proof that Type.{u} is not a set, given that Type.{0} is not a set;
• In the Yoneda Lemma;
• In the characterization of equality in sum types (see below for the pattern matching notation):
  open sum

  definition sum.code.{u v} {A : Type.{u}}

  {B : Type.{v}} : A + B → A + B → Type.{max u v}

  | sum.code (inl a) (inl a') := lift (a = a')

  | sum.code (inr b) (inr b') := lift (b = b')

  | sum.code _ _              := lift empty

The first two examples only need lifts because we also decided that inductive types without parameters (empty, unit, bool, nat, etc.) should live in the lowest universe, instead of being universe polymorphic.

Lastly, the kernel contains inductive types. The syntax to declare them is very similar to Coq’s. For example, you can write

which defines the natural numbers. This gives the type my_nat with two constructors my_nat.zero and my_nat.succ, a dependent recursor my_nat.rec and two computation rules.

Lean also automatically defines a couple of other useful definitions, like the injectivity of the constructors, but this is done outside the kernel (for a full list you can execute print prefix my_nat if you’ve installed Lean). Lean supports inductive families and mutually defined inductive types, but not induction-induction or induction-recursion.

There is special support for structures – inductive types with only one constructor. For these the projections are automatically generated, and we can extend structures with additional fields. This is also implemented outside the kernel. In the following example we extend the structure of groups to the structure of abelian groups.

The result is a structure with all the fields of group, but with one additional field. Also, the coercion from abelian_group to group is automatically defined.

The Lean kernel can be instantiated in multiple ways. There is a standard mode where the lowest universe Prop is impredicative and has proof irrelevance. The standard mode also has built-in quotient types. Secondly, there is the HoTT mode without impredicative or proof irrelevant universes. The HoTT mode also has some support for HITs; see below.

Elaboration

On top of the kernel there is a powerful elaboration engine which

1. Infers implicit universe variables
2. Infers implicit arguments, using higher order unification
3. Supports overloaded notation or declarations
4. Inserts coercions
5. Infers implicit arguments using type classes
6. Convert readable proofs to proof terms
7. Constructs terms using tactics

It does most of these things simultaneously, for example it can use the term constructed by type classes to find out implicit arguments for functions.

Let’s run through the above list in more detail.

1. As said before, universe variables are rarely needed explicitly, usually only in cases where it would be ambiguous when you don’t give them (for example sum.code as defined above could also live in Type.{(max u v)+3} if the universe levels were not given explicitly).

2. As in Coq and Agda, we can use binders with curly braces {...} to indicate which arguments are left implicit. For example with the identity function above, if we write id (3 + 4) this will be interpreted as @id _ (3 + 4). Then the placeholder _ will be filled by the elaborator to get @id ℕ (3 + 4). Lean also supports higher order unification. This allows, for example, to leave the type family of a transport implicit. For example (▸ denotes transport):

Or the following lemma about transport in sigma-types:

Here the first transport is along the type family λa, Σ(b : B a), C a b. The second transport is along the type family B and the p ▸D is a dependent transport which is a map C a₁ b → C a₂ (p ▸ b). The check command shows these type families. Also in the proof we don’t have to give the type family of the inductions eq.rec and sigma.rec explicitly. However, for nested inductions higher-order unification becomes expensive quickly, and it is better to use pattern matching or the induction tactic, discussed below.

3&4 Lean supports overloading and coercions. Some examples:

In this example f is in the type of equivalences between A and B and is coerced into the function type. Also, ⁻¹ is overloaded to mean both function inverse and path inverse.

5. Lean has type classes, similar to Coq’s and Agda’s, but in Lean they are very tightly integrated into the elaboration process. We use type class inference for inverses of functions. We can write f⁻¹ for an equivalence f : A → B, and then Lean will automatically try to find an instance of type is_equiv f.

Here’s an example, where we prove that the type of natural transformations between two functors is a set.

In the proof we only have to show that the type of natural transformation is equivalent to a sigma-type (nat_trans.sigma_char) and that truncatedness respects equivalences (is_trunc_equiv_closed). The fact that the sigma-type is a set is then inferred by type class resolution.

The brackets [...] specify that that argument is inferred by type class inference.

6. There are multiple ways to write readable proofs in Lean, which are then converted to proof terms by the elaborator. One thing you can do is define functions using pattern matching. We already saw an example above with sum.code. In contrast to Coq and Agda, these expressions are not part of the kernel. Instead, they are ‘compiled down’ to basic recursors, keeping Lean’s kernel simple, safe, and, well, ‘lean.’ Here is a simple example. The print command shows how inv is defined internally.

Here are some neat examples with vectors.

You can use calculations in proofs, for example in the following construction of the composition of two natural transformations:

There are various notations for using forward reasoning. For example the following proof is from the standard library. In the proof below we use the notation `p > 0`, which is interpreted as the inhabitant of the type p > 0 in the current context. We also use the keyword this, which is the name term constructed by the previous unnamed have expression.

7. Lean has a tactic language, just as Coq. You can write

anywhere in a term to synthesize that subterm with tactics. You can also use by *tactic* to apply a single tactic (which we used in the above calculation proof). The type of the subterm you want to synthesize is the goal and you can use tactics to solve the goal or apply backwards reasoning on the goal. For example if the goal is f x = f y you can use the tactic apply ap f to reduce the goal to x = y. Another tactic is the exact tactic, which means you give the term explicitly.

The proof language offers various mechanisms to pass back and forth between the two modes. You can begin using tactics anywhere a proof term is expected, and, conversely, you can enter structured proof terms while in tactic mode using the exact tactic.

A very simple tactic proof is

which produces the proof term ap g (ap f p). In the Emacs mode of Lean you can see the intermediate goals by moving your cursor to the desired location and pressing Ctrl-C Ctrl-G

Lean has too many tactics to discuss here, although not as many as Coq. Here are some neat examples of tactics in Lean.

The cases tactic can be used to destruct a term of an inductive type. In the following examples, it destructs the path p to reflexivity. In the second example it uses that succ is injective, since it is the constructor of nat, so that it can still destruct p. It also doesn’t matter whether the free variable is on the left hand side or the right hand side of the equality. In the last example it uses that different constructors of an inductive type cannot be equal.

The rewrite tactic is useful for doing a lot of rewrite rules. It is modeled after the rewrite tactic in SSReflect. For example in the following proof of Eckmann-Hilton we rewrite the goal 4 times with theorems to solve the goal. The notation ▸* simplifies the goal similar to Coq’s simpl, and -H means to rewrite using H⁻¹.

The induction tactic performs induction. For example if the goal is P n for a natural number n (which need not be a variable), then you can use induction n to obtain the two goals P 0 and P (k + 1) assuming P k. What’s really neat is that it supports user-defined recursors. So you can define the recursor of a HIT, tag it with the [recursor] attribute, and then it can be used for the induction tactic. Even more: you can arrange it in such a way that it uses the nondependent recursion principle whenever possible, and otherwise the dependent recursion principle.

In the future there will be more tactics, providing powerful automation such as a simplifier and a tableaux theorem prover.

---

The HoTT Library

I’ve been extensively working this year on the HoTT library of Lean, with the help of Jakob von Raumer and Ulrik Buchholtz. The HoTT library is coming along nicely. We have most things from the first 7 chapters of the HoTT book, and some category theory. In this file there is a summary what is in the HoTT library sorted by where it appears in the HoTT book.

I’ve developed the library partly by porting it from the Coq-HoTT library, since Coq’s syntax is pretty close to Lean. Other things I’ve proven using the proof in the book, or just by proving it myself.

In the library we are heavily using the cubical ideas Dan Licata wrote about earlier this year. For example we have the type of pathovers, which are heterogenous paths lying over another path. These can be written as b =[p] b' (or pathover B b p b' if you want to give the fibration explicitly). These are used for the recursion principle of HITs

and for the equality in sigma’s

There are also squares and squareovers which are presentations of higher equalities. One neat example which shows the strength of these additional structures is the following example. I had the term and could fill every square in the diagram below. I wanted to rewrite this term to .

If every square is formulated as a path between compositions of paths, then this rewriting takes a lot of work. You have to rewrite any individual square (assuming it is formulated as “top equals composition of the other three sides”), then you have to perform a lot of associativity steps to be able to cancel the sides which you get in the middle of the diagram.
Or you can formulate and prove a dedicated lemma for this rewrite step, which also takes quite some work.

However, because I formulated these two-dimensional paths as squares, I could first horizontally compose the four squares. This gives a square with as top and as bottom . Then you can apply the theorem that the top of a square equals the composition of the other 3 sides, which gives exactly the desired rewrite rule. Similar simplifications by the use of pathovers and squares are occurring all over the library.

HITs

Lastly I want to talk about our way of handling HITs in Lean. In Coq and Agda the way to define a HIT is to make a type with the point constructors and then (inconsistently) assume that this type contains the right path constructors and the correct induction principle and computation rules. Then we forget we assumed something which was inconsistent. This is often called Dan Licata’s trick. This works well, but it’s not so clean since it assumes an inconsistency.

In Lean, we add two specific HITs as kernel extension. These HITs are the quotient and the -truncation. The formation rule, the constructors and the recursion principle are added as constants, and the computation rule on the points is added as a definitional equality to the kernel (the computation rule for paths is an axiom).

The quotient (not to be confused with a set-quotient) is the following HIT: (this is not Lean syntax)

So in a quotient we specify the type of points, and we can add any type of paths to the quotient.

In Lean we have the following constants for quotients. The computation rule for points, rec_class_of, is just defined as reflexivity, to illustrate that the reduction rule is added to the Lean kernel.

Using these HITs, we can define all HITs in Chapters 1-7 of the book. For example we can define the sequential colimit of a type family with functions by taking the quotient of the type with relation defined as an inductive family

In similar ways we can define pushouts, suspensions, spheres and so on. But you can define more HITs with quotients. In my previous blog post I wrote how to construct the propositional truncation using just quotients. In fact, Egbert Rijke and I are working on a generalization of this construction to construct all -truncations, which means we can even drop -truncations as a primitive HIT.

Quotients can even be used to construct HITs with 2-path constructors. I have formalized a way to construct quite general HITs with 2-constructors, as long as they are nonrecursive. The HIT I constructed has three constructors. The point constructor i and path constructor p are the same as for the quotient, but there is also a 2-path constructor, which can equate

• One path constructors
• Reflexivity
• ap i p where i is the point constructor and p is a path in A
• concatenations and/or inverses of such paths

Formally, the defintion of the HIT is as follows. Given a type and a binary (type-valued) relation on . Let be the “formal equivalence closure” of , i.e. the following inductive family:

Note that if we’re given a map we can extend it to a map by interpreting e.g. .

Now if you’re also given a “relation on ”, i.e. a family , then we can construct the following type just using quotients

This two_quotient allows to construct at least the following HITs:

• The torus (the formulation with two loops and a 2-constructor)
• The reduced suspension
• The groupoid quotient

So in conclusion, from quotients you can define the most commonly used HITs. You can (probably) not define every possible HIT, though, so for the other HITs you still have to use Dan Licata’s trick. I should note here that currently there is no private modifier in Lean yet, so we cannot do Dan Licata’s trick very well in Lean now.

These are all the topics I want to talk about in this blog post. I tried to cover as much of the functionalities of Lean, but there are still features I haven’t talked about. For more information, you can look at the Lean tutorial. Keep in mind that the tutorial is written for the standard library, not the HoTT library, and you might want to skip the first couple of chapters explaining dependent type theory. The Quick Reference chapter at the end of the tutorial (or in pdf format) is also very useful. Also feel free to ask any questions in the comments, in the lean-user google group or in an issue on Github. Finally, if you’re willing to help with the HoTT library, that would be very much appreciated!