What is Lean

Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.

Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.

-- Defines a function that takes a name and produces a greeting.
def getGreeting (name : String) := s!"Hello, {name}! Isn't Lean great?"

-- The `main` function is the entry point of your program.
-- Its type is `IO Unit` because it can perform `IO` operations (side effects).
def main : IO Unit :=
  -- Define a list of names
  let names := ["Sebastian", "Leo", "Daniel"]

  -- Map each name to a greeting
  let greetings := names.map getGreeting

  -- Print the list of greetings
  for greeting in greetings do
    IO.println greeting

Lean has numerous features, including:

• Type inference
• First-class functions
• Powerful data types
• Pattern matching
• Type classes
• Monads
• Extensible syntax
• Hygienic macros
• Dependent types
• Metaprogramming
• Multithreading
• Verification: you can prove properties of your functions using Lean itself

Tour of Lean

The best way to learn about Lean is to read and write Lean code. This article will act as a tour through some of the key features of the Lean language and give you some code snippets that you can execute on your machine. To learn about setting up a development environment, check out Setting Up Lean.

There are two primary concepts in Lean: functions and types. This tour will emphasize features of the language which fall into these two concepts.

Functions and Namespaces

The most fundamental pieces of any Lean program are functions organized into namespaces. Functions perform work on inputs to produce outputs, and they are organized under namespaces, which are the primary way you group things in Lean. They are defined using the def command, which give the function a name and define its arguments.

namespace BasicFunctions

-- The `#eval` command evaluates an expression on the fly and prints the result.
#eval 2+2

-- You use 'def' to define a function. This one accepts a natural number
-- and returns a natural number.
-- Parentheses are optional for function arguments, except for when
-- you use an explicit type annotation.
-- Lean can often infer the type of the function's arguments.
def sampleFunction1 x := x*x + 3

-- Apply the function, naming the function return result using 'def'.
-- The variable type is inferred from the function return type.
def result1 := sampleFunction1 4573

-- This line uses an interpolated string to print the result. Expressions inside
-- braces `{}` are converted into strings using the polymorphic method `toString`
#eval println! "The result of squaring the integer 4573 and adding 3 is {result1}"

-- When needed, annotate the type of a parameter name using '(argument : type)'.
def sampleFunction2 (x : Nat) := 2*x*x - x + 3

def result2 := sampleFunction2 (7 + 4)

#eval println! "The result of applying the 2nd sample function to (7 + 4) is {result2}"

-- Conditionals use if/then/else
def sampleFunction3 (x : Int) :=
  if x > 100 then
    2*x*x - x + 3
  else
    2*x*x + x - 37

#eval println! "The result of applying sampleFunction3 to 2 is {sampleFunction3 2}"

end BasicFunctions

-- Lean has first-class functions.
-- `twice` takes two arguments `f` and `a` where
-- `f` is a function from natural numbers to natural numbers, and
-- `a` is a natural number.
def twice (f : Nat → Nat) (a : Nat) :=
  f (f a)

-- `fun` is used to declare anonymous functions
#eval twice (fun x => x + 2) 10

-- You can prove theorems about your functions.
-- The following theorem states that for any natural number `a`,
-- adding 2 twice produces a value equal to `a + 4`.
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
  -- The proof is by reflexivity. Lean "symbolically" reduces both sides of the equality
  -- until they are identical.
  rfl

-- `(· + 2)` is syntax sugar for `(fun x => x + 2)`. The parentheses + `·` notation
-- is useful for defining simple anonymous functions.
#eval twice (· + 2) 10

-- Enumerated types are a special case of inductive types in Lean,
-- which we will learn about later.
-- The following command creates a new type `Weekday`.
inductive Weekday where
  | sunday    : Weekday
  | monday    : Weekday
  | tuesday   : Weekday
  | wednesday : Weekday
  | thursday  : Weekday
  | friday    : Weekday
  | saturday  : Weekday

-- `Weekday` has 7 constructors/elements.
-- The constructors live in the `Weekday` namespace.
-- Think of `sunday`, `monday`, …, `saturday` as being distinct elements of `Weekday`,
-- with no other distinguishing properties.
-- The command `#check` prints the type of a term in Lean.
#check Weekday.sunday
#check Weekday.monday

-- The `open` command opens a namespace, making all declarations in it accessible without
-- qualification.
open Weekday
#check sunday
#check tuesday

-- You can define functions by pattern matching.
-- The following function converts a `Weekday` into a natural number.
def natOfWeekday (d : Weekday) : Nat :=
  match d with
  | sunday    => 1
  | monday    => 2
  | tuesday   => 3
  | wednesday => 4
  | thursday  => 5
  | friday    => 6
  | saturday  => 7

#eval natOfWeekday tuesday

def isMonday : Weekday → Bool :=
  -- `fun` + `match`  is a common idiom.
  -- The following expression is syntax sugar for
  -- `fun d => match d with | monday => true | _ => false`.
  fun
    | monday => true
    | _      => false

#eval isMonday monday
#eval isMonday sunday

-- Lean has support for type classes and polymorphic methods.
-- The `toString` method converts a value into a `String`.
#eval toString 10
#eval toString (10, 20)

-- The method `toString` converts values of any type that implements
-- the class `ToString`.
-- You can implement instances of `ToString` for your own types.
instance : ToString Weekday where
  toString (d : Weekday) : String :=
    match d with
    | sunday    => "Sunday"
    | monday    => "Monday"
    | tuesday   => "Tuesday"
    | wednesday => "Wednesday"
    | thursday  => "Thursday"
    | friday    => "Friday"
    | saturday  => "Saturday"

#eval toString (sunday, 10)

def Weekday.next (d : Weekday) : Weekday :=
  match d with
  | sunday    => monday
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

#eval Weekday.next Weekday.wednesday
-- Since the `Weekday` namespace has already been opened, you can also write
#eval next wednesday

-- Matching on a parameter like in the previous definition
-- is so common that Lean provides syntax sugar for it. The following
-- function uses it.
def Weekday.previous : Weekday -> Weekday
  | sunday    => saturday
  | monday    => sunday
  | tuesday   => monday
  | wednesday => tuesday
  | thursday  => wednesday
  | friday    => thursday
  | saturday  => friday

#eval next (previous wednesday)

-- We can prove that for any `Weekday` `d`, `next (previous d) = d`
theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d :=
  match d with
  | sunday    => rfl
  | monday    => rfl
  | tuesday   => rfl
  | wednesday => rfl
  | thursday  => rfl
  | friday    => rfl
  | saturday  => rfl

-- You can automate definitions such as `Weekday.nextOfPrevious`
-- using metaprogramming (or "tactics").
theorem Weekday.nextOfPrevious' (d : Weekday) : next (previous d) = d := by
  cases d       -- A proof by case distinction
  all_goals rfl  -- Each case is solved using `rfl`

Quickstart

These instructions will walk you through setting up Lean 4 together with VS Code as an editor for Lean 4. See Setup for supported platforms and other ways to set up Lean 4.

1. Install VS Code.

2. Launch VS Code and install the lean4 extension by clicking on the "Extensions" sidebar entry and searching for "lean4".

   

3. Open the Lean 4 setup guide by creating a new text file using "File > New Text File" (Ctrl+N), clicking on the ∀-symbol in the top right and selecting "Documentation… > Setup: Show Setup Guide".

   

4. Follow the Lean 4 setup guide. It will walk you through learning resources for Lean 4, teach you how to set up Lean's dependencies on your platform, install Lean 4 for you at the click of a button and help you set up your first project.

   

Supported Platforms

Tier 1

Platforms built & tested by our CI, available as binary releases via elan (see below)

• x86-64 Linux with glibc 2.27+
• x86-64 macOS 10.15+
• x86-64 Windows 10+

Tier 2

Platforms cross-compiled but not tested by our CI, available as binary releases

Releases may be silently broken due to the lack of automated testing. Issue reports and fixes are welcome.

• aarch64 Linux with glibc 2.27+
• aarch64 (Apple Silicon) macOS
• x86 (32-bit) Linux
• Emscripten Web Assembly

Setting Up Lean

See also the quickstart instructions for a standard setup with VS Code as the editor.

Release builds for all supported platforms are available at https://github.com/leanprover/lean4/releases. Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager elan instead:

$ elan self update  # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable

lake

Lean 4 comes with a package manager named lake. Use lake init foo to initialize a Lean package foo in the current directory, and lake build to typecheck and build it as well as all its dependencies. Use lake help to learn about further commands. The general directory structure of a package foo is

lakefile.lean  # package configuration
lean-toolchain # specifies the lean version to use
Foo.lean       # main file, import via `import Foo`
Foo/
  A.lean       # further files, import via e.g. `import Foo.A`
  A/...        # further nesting
.lake/         # `lake` build output directory

After running lake build you will see a binary named ./.lake/build/bin/foo and when you run it you should see the output:

Hello, world!

Editing

Lean implements the Language Server Protocol that can be used for interactive development in Emacs, VS Code, and possibly other editors.

Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).

Theorem Proving in Lean

We strongly encourage you to read the book Theorem Proving in Lean. Many Lean users consider it to be the Lean Bible.

Functional Programming in Lean

The goal of this book is to be an accessible introduction to using Lean 4 as a programming language. It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming. It does not assume any background with functional programming, though it's probably not a good first book on programming in general. New content will be added once per month until it's done.

Examples

• Palindromes
• Binary Search Trees
• A Certified Type Checker
• The Well-Typed Interpreter
• Dependent de Bruijn Indices
• Parametric Higher-Order Abstract Syntax

Palindromes

Palindromes are lists that read the same from left to right and from right to left. For example, [a, b, b, a] and [a, h, a] are palindromes.

We use an inductive predicate to specify whether a list is a palindrome or not. Recall that inductive predicates, or inductively defined propositions, are a convenient way to specify functions of type ... → Prop.

This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification".

inductive 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α → 
Prop: Type
Prop where
  | 
nil: ∀ {α : Type u_1}, Palindrome []
nil      : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
[]: List ?m.17
[]
  | 
single: ∀ {α : Type u_1} (a : α), Palindrome [a]
single   : (
a: α
a : 
α: Type u_1
α) → 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome [
a: α
a]
  | 
sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
sandwich : (
a: α
a : 
α: Type u_1
α) → 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List α
as → 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome ([
a: α
a] ++ 
as: List α
as ++ [
a: α
a])

The definition distinguishes three cases: (1) [] is a palindrome; (2) for any element a, the singleton list [a] is a palindrome; (3) for any element a and any palindrome [b₁, . . ., bₙ], the list [a, b₁, . . ., bₙ, a] is a palindrome.

We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate h : Palindrome as.

theorem 
palindrome_reverse: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverse
palindrome_reverse (
h: Palindrome as
h : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.394
as) : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.394
as.
reverse: {α : Type u_1} → List α → List α
reverse := by
Goals accomplished! 🐙
  induction 
h: Palindrome as
h with
α✝: Type u_1
as: List α✝
h: Palindrome as
Palindrome as.reverse
  | 
nil: ∀ {α : Type u_1}, Palindrome []
nil =>
α✝: Type u_1
as: List α✝
nil
Palindrome [].reverse exact 
Palindrome.nil: ∀ {α : Type u_1}, Palindrome []
Palindrome.nil
Goals accomplished! 🐙
  | 
single: ∀ {α : Type u_1} (a : α), Palindrome [a]
single 
a: α✝
a =>
α✝: Type u_1
as: List α✝
a: α✝
single
Palindrome [a].reverse exact 
Palindrome.single: ∀ {α : Type u_1} (a : α), Palindrome [a]
Palindrome.single 
a: α✝
a
Goals accomplished! 🐙
  | 
sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
sandwich 
a: α✝
a 
h: Palindrome as✝
h 
ih: Palindrome as✝.reverse
ih =>
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome as✝.reverse
sandwich
Palindrome ([a] ++ as✝ ++ [a]).reverse simp
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome as✝.reverse
sandwich
Palindrome (a :: (as✝.reverse ++ [a])); exact 
Palindrome.sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
Palindrome.sandwich 
_: α✝
_ 
ih: Palindrome as✝.reverse
ih
Goals accomplished! 🐙

If a list as is a palindrome, then the reverse of as is equal to itself.

theorem 
reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → as.reverse = as
reverse_eq_of_palindrome (
h: Palindrome as
h : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.661
as) : 
as: List ?m.661
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List ?m.661
as := by
Goals accomplished! 🐙
  induction 
h: Palindrome as
h with
α✝: Type u_1
as: List α✝
h: Palindrome as
as.reverse = as
  | 
nil: ∀ {α : Type u_1}, Palindrome []
nil =>
α✝: Type u_1
as: List α✝
nil
[].reverse = [] rfl
Goals accomplished! 🐙
  | 
single: ∀ {α : Type u_1} (a : α), Palindrome [a]
single 
a: α✝
a =>
α✝: Type u_1
as: List α✝
a: α✝
single
[a].reverse = [a] rfl
Goals accomplished! 🐙
  | 
sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
sandwich 
a: α✝
a
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: as✝.reverse = as✝
sandwich
([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] 
h: Palindrome as✝
h
Warning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: as✝.reverse = as✝
sandwich
([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] 
ih: as✝.reverse = as✝
ih: as✝.reverse = as✝
ih =>
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: as✝.reverse = as✝
sandwich
([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] simp [
ih: as✝.reverse = as✝
ih]
Goals accomplished! 🐙

Note that you can also easily prove palindrome_reverse using reverse_eq_of_palindrome.

example: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverse
example (
h: Palindrome as
h : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.903
as) : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.903
as.
reverse: {α : Type u_1} → List α → List α
reverse := by
Goals accomplished! 🐙
  simp [
reverse_eq_of_palindrome: ∀ {α : Type ?u.899} {as : List α}, Palindrome as → as.reverse = as
reverse_eq_of_palindrome 
h: Palindrome as
h, 
h: Palindrome as
h]
Goals accomplished! 🐙

Given a nonempty list, the function List.last returns its element. Note that we use (by simp) to prove that a₂ :: as ≠ [] in the recursive application.

def 
List.last: {α : Type u_1} → (as : List α) → as ≠ [] → α
List.last : (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) → 
as: List α
as ≠ 
[]: List α
[] → 
α: Type u_1
α
  | [
a: α
a],         _ => 
a: α
a
  | _::
a₂: α
a₂:: 
as: List α
as, _ => (
a₂: α
a₂::
as: List α
as).
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last (by
Goals accomplished! 🐙 simp
Goals accomplished! 🐙)

We use the function List.last to prove the following theorem that says that if a list as is not empty, then removing the last element from as and appending it back is equal to as. We use the attribute @[simp] to instruct the simp tactic to use this theorem as a simplification rule.

@[simp] theorem 
List.dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), as.dropLast ++ [as.last h] = as
List.dropLast_append_last (
h: as ≠ []
h : 
as: List ?m.1443
as ≠ 
[]: List ?m.1443
[]) : 
as: List ?m.1443
as.
dropLast: {α : Type u_1} → List α → List α
dropLast ++ [
as: List ?m.1443
as.
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last 
h: as ≠ []
h] = 
as: List ?m.1443
as := by
Goals accomplished! 🐙
  match 
as: List α✝
as with
α✝: Type u_1
as: List α✝
h: as ≠ []
as.dropLast ++ [as.last h] = as
  | [] =>
α✝: Type u_1
as: List α✝
h: [] ≠ []
[].dropLast ++ [[].last h] = [] contradiction
Goals accomplished! 🐙
  | [
a: α✝
a] =>
α✝: Type u_1
as: List α✝
a: α✝
h: [a] ≠ []
[a].dropLast ++ [[a].last h] = [a] simp_all [
last: {α : Type ?u.1743} → (as : List α) → as ≠ [] → α
last, 
dropLast: {α : Type ?u.2176} → List α → List α
dropLast]
Goals accomplished! 🐙
  | 
a₁: α✝
a₁ :: 
a₂: α✝
a₂ :: 
as: List α✝
as =>
α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []
(a₁ :: a₂ :: as).dropLast ++ [(a₁ :: a₂ :: as).last h] = a₁ :: a₂ :: as
    simp [
last: {α : Type ?u.2254} → (as : List α) → as ≠ [] → α
last, 
dropLast: {α : Type ?u.2272} → List α → List α
dropLast]
α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []
(a₂ :: as).dropLast ++ [(a₂ :: as).last ⋯] = a₂ :: as
    exact 
dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), as.dropLast ++ [as.last h] = as
dropLast_append_last (as := 
a₂: α✝
a₂ :: 
as: List α✝
as) (
α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []
(a₂ :: as).dropLast ++ [(a₂ :: as).last ⋯] = a₂ :: asby
Goals accomplished! 🐙 simp
Goals accomplished! 🐙)
Goals accomplished! 🐙

We now define the following auxiliary induction principle for lists using well-founded recursion on as.length. We can read it as follows, to prove motive as, it suffices to show that: (1) motive []; (2) motive [a] for any a; (3) if motive as holds, then motive ([a] ++ as ++ [b]) also holds for any a, b, and as. Note that the structure of this induction principle is very similar to the Palindrome inductive predicate.

theorem 
List.palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
  motive [] →
    (∀ (a : α), motive [a]) →
      (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive as
List.palindrome_ind (
motive: List α → Prop
motive : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α → 
Prop: Type
Prop)
    (
h₁: motive []
h₁ : 
motive: List α → Prop
motive 
[]: List α
[])
    (
h₂: ∀ (a : α), motive [a]
h₂ : (
a: α
a : 
α: Type u_1
α) → 
motive: List α → Prop
motive [
a: α
a])
    (
h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])
h₃ : (
a: α
a 
b: α
b : 
α: Type u_1
α) → (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) → 
motive: List α → Prop
motive 
as: List α
as → 
motive: List α → Prop
motive ([
a: α
a] ++ 
as: List α
as ++ [
b: α
b]))
    (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α)
    : 
motive: List α → Prop
motive 
as: List α
as :=
  match 
as: List α
as with
  | []  => 
h₁: motive []
h₁
  | [
a: α
a] => 
h₂: ∀ (a : α), motive [a]
h₂ 
a: α
a
  | 
a₁: α
a₁::
a₂: α
a₂::
as': List α
as' =>
    have 
ih: motive (a₂ :: as').dropLast
ih := 
palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
  motive [] →
    (∀ (a : α), motive [a]) →
      (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive as
palindrome_ind 
motive: List α → Prop
motive 
h₁: motive []
h₁ 
h₂: ∀ (a : α), motive [a]
h₂ 
h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])
h₃ (
a₂: α
a₂::
as': List α
as').
dropLast: {α : Type u_1} → List α → List α
dropLast
    have : [
a₁: α
a₁] ++ (
a₂: α
a₂::
as': List α
as').
dropLast: {α : Type u_1} → List α → List α
dropLast ++ [(
a₂: α
a₂::
as': List α
as').
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last (by
Goals accomplished! 🐙 simp
Goals accomplished! 🐙)] = 
a₁: α
a₁::
a₂: α
a₂::
as': List α
as' := by
Goals accomplished! 🐙 simp
Goals accomplished! 🐙
    
this: [a₁] ++ (a₂ :: as').dropLast ++ [(a₂ :: as').last ⋯] = a₁ :: a₂ :: as'
this ▸ 
h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])
h₃ 
_: α
_ 
_: α
_ 
_: List α
_ 
ih: motive (a₂ :: as').dropLast
ih
termination_by 
as: List α
as.
length: {α : Type u_1} → List α → Nat
length

We use our new induction principle to prove that if as.reverse = as, then Palindrome as holds. Note that we use the using modifier to instruct the induction tactic to use this induction principle instead of the default one for lists.

theorem 
List.palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, as.reverse = as → Palindrome as
List.palindrome_of_eq_reverse (
h: as.reverse = as
h : 
as: List ?m.5450
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List ?m.5450
as) : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.5450
as := by
Goals accomplished! 🐙
  induction 
as: List α✝
as using 
palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
  motive [] →
    (∀ (a : α), motive [a]) →
      (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive as
palindrome_ind
α✝: Type u_1
h: [].reverse = []
h₁
Palindrome []
α✝: Type u_1
a✝: α✝
h: [a✝].reverse = [a✝]
h₂
Palindrome [a✝]
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: as✝.reverse = as✝ → Palindrome as✝
h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]
h₃
Palindrome ([a✝¹] ++ as✝ ++ [b✝])
  next   =>
α✝: Type u_1
h: [].reverse = []
h₁
Palindrome []
α✝: Type u_1
a✝: α✝
h: [a✝].reverse = [a✝]
h₂
Palindrome [a✝]
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: as✝.reverse = as✝ → Palindrome as✝
h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]
h₃
Palindrome ([a✝¹] ++ as✝ ++ [b✝]) exact 
Palindrome.nil: ∀ {α : Type u_1}, Palindrome []
Palindrome.nil
Goals accomplished! 🐙
  next 
a: α✝
a =>
α✝: Type u_1
a✝: α✝
h: [a✝].reverse = [a✝]
h₂
Palindrome [a✝]
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: as✝.reverse = as✝ → Palindrome as✝
h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]
h₃
Palindrome ([a✝¹] ++ as✝ ++ [b✝]) exact 
Palindrome.single: ∀ {α : Type u_1} (a : α), Palindrome [a]
Palindrome.single 
a: α✝
a
Goals accomplished! 🐙
  next 
a: α✝
a 
b: α✝
b 
as: List α✝
as 
ih: as.reverse = as → Palindrome as
ih =>
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: as✝.reverse = as✝ → Palindrome as✝
h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]
h₃
Palindrome ([a✝¹] ++ as✝ ++ [b✝])
    have : 
a: α✝
a = 
b: α✝
b :=
α✝: Type u_1
a, b: α✝
as: List α✝
ih: as.reverse = as → Palindrome as
h: ([a] ++ as ++ [b]).reverse = [a] ++ as ++ [b]
Palindrome ([a] ++ as ++ [b]) by
Goals accomplished! 🐙 simp_all
Goals accomplished! 🐙
    subst 
this: a = b
this
α✝: Type u_1
a: α✝
as: List α✝
ih: as.reverse = as → Palindrome as
h: ([a] ++ as ++ [a]).reverse = [a] ++ as ++ [a]
Palindrome ([a] ++ as ++ [a])
    have : 
as: List α✝
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List α✝
as :=
α✝: Type u_1
a: α✝
as: List α✝
ih: as.reverse = as → Palindrome as
h: ([a] ++ as ++ [a]).reverse = [a] ++ as ++ [a]
Palindrome ([a] ++ as ++ [a]) by
Goals accomplished! 🐙 simp_all
Goals accomplished! 🐙
    exact 
Palindrome.sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
Palindrome.sandwich 
a: α✝
a (
ih: as.reverse = as → Palindrome as
ih 
this: as.reverse = as
this)
Goals accomplished! 🐙

We now define a function that returns true iff as is a palindrome. The function assumes that the type α has decidable equality. We need this assumption because we need to compare the list elements.

def 
List.isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → Bool
List.isPalindrome [
DecidableEq: Type u_1 → Type u_1
DecidableEq 
α: Type u_1
α] (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) : 
Bool: Type
Bool :=
    
as: List α
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List α
as

It is straightforward to prove that isPalindrome is correct using the previously proved theorems.

theorem 
List.isPalindrome_correct: ∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), as.isPalindrome = true ↔ Palindrome as
List.isPalindrome_correct [
DecidableEq: Type u_1 → Type u_1
DecidableEq 
α: Type u_1
α] (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) : 
as: List α
as.
isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → Bool
isPalindrome ↔ 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List α
as := by
Goals accomplished! 🐙
  simp [
isPalindrome: {α : Type ?u.6472} → [inst : DecidableEq α] → List α → Bool
isPalindrome]
α: Type u_1
inst✝: DecidableEq α
as: List α
as.reverse = as ↔ Palindrome as
  exact 
Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.intro (fun 
h: as.reverse = as
h => 
palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, as.reverse = as → Palindrome as
palindrome_of_eq_reverse 
h: as.reverse = as
h) (fun 
h: Palindrome as
h => 
reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → as.reverse = as
reverse_eq_of_palindrome 
h: Palindrome as
h)
Goals accomplished! 🐙

#eval
true
 [
1: Nat
1, 
2: Nat
2, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
#eval
false
 [
1: Nat
1, 
2: Nat
2, 
3: Nat
3, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome

example: [1, 2, 1].isPalindrome = true
example : [
1: Nat
1, 
2: Nat
2, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome := 
rfl: ∀ {α : Type} {a : α}, a = a
rfl
example: [1, 2, 2, 1].isPalindrome = true
example : [
1: Nat
1, 
2: Nat
2, 
2: Nat
2, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome := 
rfl: ∀ {α : Type} {a : α}, a = a
rfl
example: (![1, 2, 3, 1].isPalindrome) = true
example : ![
1: Nat
1, 
2: Nat
2, 
3: Nat
3, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome := 
rfl: ∀ {α : Type} {a : α}, a = a
rfl

Binary Search Trees

If the type of keys can be totally ordered -- that is, it supports a well-behaved ≤ comparison -- then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.

This example is based on a similar example found in the "Software Foundations" book (volume 3).

We use Nat as the key type in our implementation of BSTs, since it has a convenient total order with lots of theorems and automation available. We leave as an exercise to the reader the generalization to arbitrary types.

inductive 
Tree: Type v → Type v
Tree (
β: Type v
β : 
Type v: Type (v + 1)
Type v) where
  | 
leaf: {β : Type v} → Tree β
leaf
  | 
node: {β : Type v} → Tree β → Nat → β → Tree β → Tree β
node (
left: Tree β
left : 
Tree: Type v → Type v
Tree 
β: Type v
β) (
key: Nat
key : 
Nat: Type
Nat) (
value: β
value : 
β: Type v
β) (
right: Tree β
right : 
Tree: Type v → Type v
Tree 
β: Type v
β)
  deriving 
Repr: Type u → Type u
Repr

The function contains returns true iff the given tree contains the key k.

def 
Tree.contains: {β : Type u_1} → Tree β → Nat → Bool
Tree.contains (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) : 
Bool: Type
Bool :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.1317} → Tree β
leaf => 
false: Bool
false
  | 
node: {β : Type ?u.1326} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value
Warning: unused variable `value`
note: this linter can be disabled with `set_option linter.unusedVariables false` 
right: Tree β
right =>
    if 
k: Nat
k < 
key: Nat
key then
      
left: Tree β
left.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains 
k: Nat
k
    else if 
key: Nat
key < 
k: Nat
k then
      
right: Tree β
right.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains 
k: Nat
k
    else
      
true: Bool
true

t.find? k returns some v if v is the value bound to key k in the tree t. It returns none otherwise.

def 
Tree.find?: {β : Type u_1} → Tree β → Nat → Option β
Tree.find? (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) : 
Option: Type u_1 → Type u_1
Option 
β: Type u_1
β :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.1656} → Tree β
leaf => 
none: {α : Type u_1} → Option α
none
  | 
node: {β : Type ?u.1668} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value 
right: Tree β
right =>
    if 
k: Nat
k < 
key: Nat
key then
      
left: Tree β
left.
find?: {β : Type u_1} → Tree β → Nat → Option β
find? 
k: Nat
k
    else if 
key: Nat
key < 
k: Nat
k then
      
right: Tree β
right.
find?: {β : Type u_1} → Tree β → Nat → Option β
find? 
k: Nat
k
    else
      
some: {α : Type u_1} → α → Option α
some 
value: β
value

t.insert k v is the map containing all the bindings of t along with a binding of k to v.

def 
Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) (
v: β
v : 
β: Type u_1
β) : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.2003} → Tree β
leaf => 
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node 
leaf: {β : Type u_1} → Tree β
leaf 
k: Nat
k 
v: β
v 
leaf: {β : Type u_1} → Tree β
leaf
  | 
node: {β : Type ?u.2018} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value 
right: Tree β
right =>
    if 
k: Nat
k < 
key: Nat
key then
      
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node (
left: Tree β
left.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
k: Nat
k 
v: β
v) 
key: Nat
key 
value: β
value 
right: Tree β
right
    else if 
key: Nat
key < 
k: Nat
k then
      
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value (
right: Tree β
right.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
k: Nat
k 
v: β
v)
    else
      
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
k: Nat
k 
v: β
v 
right: Tree β
right

Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs. If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list. Here's a function that does so with an in-order traversal of the tree.

def 
Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toList (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β) :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.2370} → Tree β
leaf => 
[]: List (Nat × β)
[]
  | 
node: {β : Type ?u.2382} → Tree β → Nat → β → Tree β → Tree β
node 
l: Tree β
l 
k: Nat
k 
v: β
v 
r: Tree β
r => 
l: Tree β
l.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList ++ [(
k: Nat
k, 
v: β
v)] ++ 
r: Tree β
r.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList

#eval
Tree.node (Tree.node (Tree.leaf) 1 "one" (Tree.leaf)) 2 "two" (Tree.node (Tree.leaf) 3 "three" (Tree.leaf))
 
Tree.leaf: {β : Type} → Tree β
Tree.leaf.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
2: Nat
2 
"two": String
"two"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
3: Nat
3 
"three": String
"three"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
1: Nat
1 
"one": String
"one"

#eval
[(1, "one"), (2, "two"), (3, "three")]
 
Tree.leaf: {β : Type} → Tree β
Tree.leaf.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
2: Nat
2 
"two": String
"two"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
3: Nat
3 
"three": String
"three"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
1: Nat
1 
"one": String
"one"
      |>.
toList: {β : Type} → Tree β → List (Nat × β)
toList

The implementation of Tree.toList is inefficient because of how it uses the ++ operator. On a balanced tree its running time is linearithmic, because it does a linear number of concatenations at each level of the tree. On an unbalanced tree it's quadratic time. Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:

def 
Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toListTR (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β) :=
  
go: Tree β → List (Nat × β) → List (Nat × β)
go 
t: Tree β
t 
[]: List (Nat × β)
[]
where
  
go: Tree β → List (Nat × β) → List (Nat × β)
go (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
acc: List (Nat × β)
acc : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β)) : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β) :=
    match 
t: Tree β
t with
    | 
leaf: {β : Type ?u.2878} → Tree β
leaf => 
acc: List (Nat × β)
acc
    | 
node: {β : Type ?u.2888} → Tree β → Nat → β → Tree β → Tree β
node 
l: Tree β
l 
k: Nat
k 
v: β
v 
r: Tree β
r => 
go: Tree β → List (Nat × β) → List (Nat × β)
go 
l: Tree β
l ((
k: Nat
k, 
v: β
v) :: 
go: Tree β → List (Nat × β) → List (Nat × β)
go 
r: Tree β
r 
acc: List (Nat × β)
acc)

We now prove that t.toList and t.toListTR return the same list. The proof is on induction, and as we used the auxiliary function go to define Tree.toListTR, we use the auxiliary theorem go to prove the theorem.

The proof of the auxiliary theorem is by induction on t. The generalizing acc modifier instructs Lean to revert acc, apply the induction theorem for Trees, and then reintroduce acc in each case. By using generalizing, we obtain the more general induction hypotheses

• left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc

• right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc

Recall that the combinator tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'. In this theorem, we use it to apply simp and close each subgoal produced by the induction tactic.

The simp parameters toListTR.go and toList instruct the simplifier to try to reduce and/or apply auto generated equation theorems for these two functions. The parameter * instructs the simplifier to use any equation in a goal as rewriting rules. In this particular case, simp uses the induction hypotheses as rewriting rules. Finally, the parameter List.append_assoc instructs the simplifier to use the List.append_assoc theorem as a rewriting rule.

theorem 
Tree.toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), t.toList = t.toListTR
Tree.toList_eq_toListTR (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β)
        : 
t: Tree β
t.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList = 
t: Tree β
t.
toListTR: {β : Type u_1} → Tree β → List (Nat × β)
toListTR := by
Goals accomplished! 🐙
  simp [
toListTR: {β : Type ?u.3907} → Tree β → List (Nat × β)
toListTR, 
go: ∀ (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = t.toList ++ acc
go 
t: Tree β
t 
[]: List (Nat × β)
[]]
Goals accomplished! 🐙
where
  
go: ∀ {β : Type u_1} (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = t.toList ++ acc
go (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
acc: List (Nat × β)
acc : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β))
     : 
toListTR.go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)
toListTR.go 
t: Tree β
t 
acc: List (Nat × β)
acc = 
t: Tree β
t.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList ++ 
acc: List (Nat × β)
acc := by
Goals accomplished! 🐙
    induction 
t: Tree β
t generalizing 
acc: List (Nat × β)
acc
β: Type u_1
t: Tree β
acc: List (Nat × β)
leaf
toListTR.go leaf acc = leaf.toList ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = left✝.toList ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = right✝.toList ++ acc
acc: List (Nat × β)
node
toListTR.go (left✝.node key✝ value✝ right✝) acc = (left✝.node key✝ value✝ right✝).toList ++ acc <;>
β: Type u_1
t: Tree β
acc: List (Nat × β)
leaf
toListTR.go leaf acc = leaf.toList ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = left✝.toList ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = right✝.toList ++ acc
acc: List (Nat × β)
node
toListTR.go (left✝.node key✝ value✝ right✝) acc = (left✝.node key✝ value✝ right✝).toList ++ acc
      simp [
toListTR.go: {β : Type ?u.3766} → Tree β → List (Nat × β) → List (Nat × β)
toListTR.go, 
toList: {β : Type ?u.3572} → Tree β → List (Nat × β)
toList, *, 
List.append_assoc: ∀ {α : Type ?u.3798} (as bs cs : List α), as ++ bs ++ cs = as ++ (bs ++ cs)
List.append_assoc]
Goals accomplished! 🐙