A 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.

4#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

The result of squaring the integer 4573 and adding 3 is 20912332
#eval println! "The result of squaring the integer 4573 and adding 3 is {result1}"

The result of squaring the integer 4573 and adding 3 is 20912332

When needed, annotate the type of a parameter name using '(argument : type)'.

def sampleFunction2 (x : Nat) := 2*x*x - x + 3def result2 := sampleFunction2 (7 + 4)

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

The result of applying the 2nd sample function to (7 + 4) is 234

Conditionals use if/then/else

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

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

The result of applying sampleFunction3 to 2 is -27

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

14#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.

14#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.

Weekday.sunday : Weekday#check Weekday.sunday

Weekday.sunday : Weekday

Weekday.monday : Weekday#check Weekday.monday

Weekday.monday : Weekday

The open command opens a namespace, making all declarations in it accessible without qualification.

open WeekdayWeekday.sunday : Weekday#check sunday

Weekday.sunday : Weekday

Weekday.tuesday : Weekday#check tuesday

Weekday.tuesday : Weekday

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

3#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

true#eval isMonday monday

true

false#eval isMonday sunday

false

Lean has support for type classes and polymorphic methods. The toString method converts a value into a String.

"10"#eval toString 10

"10"

"(10, 20)"#eval toString (10, 20)

"(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"

"(Sunday, 10)"#eval toString (sunday, 10)

"(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

Thursday#eval Weekday.next Weekday.wednesday

Thursday

Since the Weekday namespace has already been opened, you can also write

Thursday#eval next wednesday

Thursday

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

Wednesday#eval next (previous wednesday)

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 := byd:Weekday⊢ d.previous.next = d
  cases dsunday⊢ sunday.previous.next = sundaymonday⊢ monday.previous.next = mondaytuesday⊢ tuesday.previous.next = tuesdaywednesday⊢ wednesday.previous.next = wednesdaythursday⊢ thursday.previous.next = thursdayfriday⊢ friday.previous.next = fridaysaturday⊢ saturday.previous.next = saturday       -- A proof by case distinction
  all_goals rflAll goals completed! 🐙  -- Each case is solved using `rfl`