The Lean Theorem Prover

Many thanks to

• Cody Roux
• Georges Gonthier
• Grant Passmore
• Nikhil Swamy
• Assia Mahboubi
• Bas Spitters
• Steve Awodey
• Ulrik Buchholtz
• Tom Ball
• Parikshit Khanna

Introduction: Lean

• New open source theorem prover
• Platform for
  • Software verification & development
  • Formalized mathematics
  • Education (mathematics, logic, computer science)
  • Synthesis (proofs & programs)
• de Bruijn's Principle: small trusted kernel
• Expressive logic
• Partial constructions: automation fills the "holes"

Introduction: Lean

• It is an ongoing and long long term effort
• At CMU, it is already being used for formalizing
  • Homotopy Type Theory
  • Category Theory
  • Algebraic Hierarchy
  • Nonabelian Algebraic Topology
  • Number Theory
• Interactive theory proving course at CMU
• Haitao Zhang is formalizing Group Theory

Main Goal

Lean aims to bring two worlds together

• An interactive theorem prover with powerful automation
• An automated reasoning tool that
  • produces (detailed) proofs,
  • has a rich language,
  • can be used interactively, and
  • is built on a verified mathematical library

Secondary Goals

• Minimalist and high-performace kernel
• Experiment with different flavors of type theory
  • Proof irrelevant vs Proof relevant
  • Impredicative vs Predicative
  • Higher Inductive Types
  • Quotient Types
  • Observational Type Theory
• Education
  • Interactive courses
  • Proving should be as easy as programming
• Have Fun

Software verification and
Formalized Mathematics

• Some projects at Microsoft Research
  • Verifying the Microsoft Hyper-V Hypervisor using VCC
  • Ironclad: automated full-system verification
  • Automated Verification of a Type-Safe Operating System
  • Four-color theorem
  • Feit Thompson theorem
• Disclaimer: this projects were developed before Lean existed
• They used Boogie/Z3 and Coq.

Software verification and
Formalized Mathematics

• Similar problems
  • Proof stability
  • Scalability issues
  • Libraries are big
  • Finding existing functions/theorems

What is new?

• Poweful elaboration engine that can handle
  • Higher-order unification
  • Definitional reductions
  • Coercions
  • Ad-hoc polymorphism (aka overloading)
  • Type classes
  • Tactics

"By relieving the brain of all unnecessary work, a good notation sets it free to concentrate on more advanced problems, and in effect increases the mental power of the race." – A. N. Whitehead

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
  • It does not contain
    • Termination checker
    • Fixpoint operators
    • Pattern matching
    • Module management

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
  • Process theorems in parallel
  • Execute/try tactics (automation) in parallel

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
• Fast incremental compilation

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
• Fast incremental compilation
• Support for mixed declarative and tactic proof style

Dependent Type Theory

• Before we started Lean, we have studied different theorem provers: ACL2, Agda, Automath, Coq, HOL (family), Isabelle, Mizar, PVS
• Dependent type theory is really beautiful
• Some advantages
  • Bultin computational interpretation
  • Same data-structure for representing proofs and terms
  • Reduce code duplication, example:
    • We implemented a compiler for Haskell-like recursive equations, we can use it to construct proofs by induction
  • Mathematical structures (such as Groups and Rings) are first-class citizens
• Some references
  • In praise of dependent types (Mike Shulman)
  • Type inference in mathematics (Jeremy Avigad)

Dependent Type Theory

• Constants

• Function applications

• Lambda abstractions

• Function spaces

Dependent Type Theory

• What is the type of nat?

• What is the type of Type?

Is Lean inconsistent? NO

• Lean has a noncumulative universe hierarchy

• Supports universe polymorphism

• In ordinary situations you can ignore the universe parameters and simply write Type, leaving the "universe management" to Lean
• examples/ex1.lean

Propositions as types

• Propositions are types

• The inhabitants/elements of a proposition P are the proofs of P
• Prop is the type of all propositions

Architecture

Architecture

Architecture

Kernel

• Kernel is implemented in two layers for easy customization
• 1st layer, dependent lambda calculus + options:
  • Proof irrelevance
  • Impredicative Prop
  Π (x : nat), x = x -- is a Proposition ∀ (x : nat), x = x -- Alternative notation
• 2nd layer: Inductive families, Quotient types, HITs

Two official libraries

• Standard
  • Proof irrelevant and impredicative Prop
  • Smooth transition to classical logic
  • Inductive Families
  • Quotient Types
• HoTT
  • Proof relevant and no impredicative Prop
  • Univalence axiom
  • Inductive Families
  • HIT
• Easy to implement experimental versions, Example: Steve Awodey asked for proof relevant and impredicative universe

Implicit arguments

• Curly braces indicate that argument should be inferred rather than entered explicitly.

Implicit arguments

• Elaborator uses higher-order unification.

Example 2

• examples/ex2.lean

Agnostic Mathematics

• Support constructive and classical mathematics
• Constructive results are more informative
• Computation is important to mathematics
• Core parts of the standard library are constructive
• Separation of concerns:
  • Methods to write computer programs
  • Freedom to use a nonconstructive theories and methods to reason about them

Agnostic Mathematics

• Semi constructive axioms:
  • Function extensionality
  • Proposition extensionality
  • Quotient types (implies function extensionality)

• Computationally compatible axioms: proof irrelevant excluded middle, axiom of choice
• Anti constructive: Hilbert's choice (aka magic)
  • consequence: all propositions are decidable

Tracking anti constructive axioms

• We cannot generate code for anti constructive axioms such as Hilbert's choice
• Lean provides a mechanism for checking whether a definition depends on anti constructive axioms or not.

• It prevents anti constructive axioms from accidentally leaking inside definitions we want to compute with (generate code for).

Axioms in the standard library

• The standard library contains 3 axioms

• The first two axioms are semi-constructive.
• Most of the standard library does not use these axioms.

We use propext and quot.sound for defining sets, finite sets and bags.

• The choice axiom is used to define real division and to prove that the reals are Cauchy complete.
• The analysis library will also be classic.

Axioms in the standard library

Freedom to trust

• Option: type check imported modules.
• Macros: semantic attachments for speeding up type checking and evaluation.
• Macros can be eliminated (expanded into pure Lean code).
• Each macro provides a function for computing the type and evaluating an instance.
• Each macro can be assigned a trust level.
• Many applications: interface with the GNU multiprecision arithmetic (GMP) library.

Freedom to trust

• Relaxed mode
  • Trust the imported modules have not been tampered
  • Trust all macros
• Paranoid mode
  • Retype check all imported modules (someone may have changed the binaries)
  • Expand all macros (the developers may have made mistakes, GMP may be buggy)
• Stronger guarantee Retype check everything using Lean reference type checker
  • Daniel Selsam implemented a reference type checker in Haskell

Reference type checker

• Implemented by Daniel Selsam
• < 2000 lines of Haskell code
• Available at github
• Code is easy to read and understand
• It can type check the whole standard library (35K lines of Lean code) under 2 mins

Exporting libraries

• All Lean files can be exported in a very simple format
• Documentation is available on github
• Communicate with other tools
• Interface with the Lean reference type checker

Inductive families

Inductive families

• examples/ex3.lean

Inductive families

Inductive families

• It is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, function spaces, and inductive types; everything else follows from those.

Inductive families: auxiliary definitions

• Lean automatically generates several auxiliary definitions whenever a new inductive family is declared.
• examples/ex4.lean

Recursive equations

• Recursors are inconvenient to use.
• Compiler from recursive equations to recursors.
• Two compilation strategies: structural and well-founded recursion

Recursive equations

• Proofs by induction

• examples/ex5.lean

Recursive equations

• Dependent pattern matching

Definitional Reductions

• Elaborator must respect the computational interpretation of terms

Coercions

• In Lean, we can associate attributes to definitions.
• Coercion is one of the available attributes.

Namespaces

• We can group definitions, metadata (e.g., notation declarations and attributes) into namespaces.
• We can open namespaces

Ad-hoc polymorphism

• We can use namespaces to avoid unwanted ambiguity.
• We can override overloading

Human-readable proofs

Human-readable proofs

Human-readable proofs

• have x : T, from P, C is notation for (λ x : T, C) P
• have T, from P, C is notation for have this : T, from P, C
• take x : T, C, is notation for λ x : T, C
• assume x : T, C, is notation for λ x : T, C
• suppose T, C, is notation for λ this : T, C
• obtain w hw, from ex, C is notation for
  exists.rec (λ h hw, C) ex
• obtain supports any inductive datatype with a single constructor
• show T, from P is notation for (P : T)
• `p` is notation for show p, by assumption

Type classes

• Synthesis procedure
• It can be viewed as a lambda-Prolog interpreter
• Big picture
  • Mark some inductive families as classes
  • Mark some definitions as (generators of) instances
  • Indicate that some implicit arguments must be synthesized using type classes
• Instances are treated as Horn clauses

Inhabited Type Class

• examples/ex6.lean

Decidable Type Class

• An element of Prop is said to be

decidable if we can decide whether it is true or false.

• Having an element t : decidable p is stronger than having an element t : p ∨ ¬p
• The expression if c then t else e contains an implicit argument [d : decidable c].
• If Hilbert's choice is imported, then all propositions are decidable (smooth transition to classical reasoning).

Decidable Type Class

• examples/ex7.lean

Tactics

• Automation such as rewrite engined, simplifiers and decision procedures are integrated into the system as tactics.
• A placeholder/hole can be viewed as a goal
• A proof state is a sequence of goals, substitution (already solved holes), and postponed constraints.
• A tactic is a function from proof state to a lazy stream of proof states (very similar to Isabelle).
• Tacticals are tactic combinadors: andthen, orelse, par, …

Tactics

• We can switch to tactic mode using begin … end or by …

• examples/ex8.lean

Structures

• Special kind of inductive datatype (only one constructor)
• Projections are generated automatically
• "Inheritance"
• Extensively used to formalize the algebraic hierarchy
• We can view them as parametric modules

Structures

Structures (additional instances)

Structures (concrete instances)

• Is int a add_group? Yes

Quotients

• Let A be any type, and let R be an equivalence relation on A. It is mathematically common to form the "quotient" A / R, that is, the type of elements of A "modulo" R.
• Set theoretically, one can view A / R as the set of equivalence classes of A modulo R.
• If f : A → B is any function that respects the equivalence relation in the sense that for every x y : A, R x y implies f x = f y, then f "lifts" to a function f' : A / R → B defined on each equivalence class [x] by f' [x] = f x.

Quotients

The quotient package consists of the following constructors:

Quotients

• Quotients are used to prove function extensionality
• They are used to define finite sets and bags in the standard library

Sylow theorem

• Developed by Haitao Zhang
• Available in the standard library

Bundled structures

Category Theory

• Developed by Floris van Doorn and Jakob von Raumer
• In the HoTT library

Lua interface

• Lua is an efficient embedded programming language
• It is very popular in the computer gaming industry
• Lean provides a Lua API
• We can access terms, create definitions and tactics, type check terms etc
• Lua scripts can be embedded in Lean files
• examples/lua.lean

Javascript

• Lean has been compiled as a Javascript library
• We have used this library to implement the interactive tutorial
• We can use it to write other applications (e.g., a fancier web IDE)
• examples/ex.html

Future work

• Auto tactic based on equational reasoning, matching, heuristic instantiation, …
• Decision procedures for arithmetic
• Efficient evaluator
• Better support for proof by reflection
• Better libraries (ongoing work)
• Machine learning

Thank you

• Website: http://leanprover.github.io/
• Source code: https://github.com/leanprover/lean
• Theorem proving in Lean: https://leanprover.github.io/tutorial/index.html