We introduce LEAN 4 language (often typeset L∃∀N) with focus on Theoretical Computer Scientists. Basic knowledge of coding and proof techniques is assumed.

Resources

When searching the internet for examples and solutions keep in mind that the many resoruces are written in older, incompatible, version of the language LEAN 3. Currently, LEAN 4 is the latest version and there is no reason to learn the old version.

LEAN Community ↗ website is a good place to search for anything LEAN related.

Sources are listed at the bottom of the page.

Language syntax

The language contains everything you would expect but additionally supports theorem proving. This is possible due to the dependant type theory the language is built upon. We touch on theorem proving later.

Aside from the basic language syntax whenever one is expected to enter a term, then

It is important to know that LEAN has two different modes – normal (term) and tactics. Unless we jump to tactics mode the entire source code is in normal mode. Many online examples show solutions in tactics but learning the underlying normal methods is important to understand what is happening. We explain tactics mode separately in a later section.

Basic syntax

-- this is a comment
namespace MyLeanTests

-- function as: def <name> <parameters> : <return type> := <body>
def sampleFunction1 (x : Nat) (y : Nat) := x*y + 3

-- variable as: def <name> : <type> := <value>
def res := sampleFunction1 4000000000 (20+30)

-- newline & repetitions of white-spaces don't matter (except for tactics)
def sampleFunction2 (x : Nat) :=
  if x > 100 then
    2*x*x - x + 3
  else
    x*x

-- many types can be inferred from the context (x has no explicit type)
-- separate statements on the same line by a semicolon ;
def sampleFunction3 x := if x > 100 then let z := 2*x*x; z - x + 3 else x*x

-- show value
#eval sampleFunction2 2000
-- show type
#check sampleFunction2

-- function as a parameter
def twice (f : Nat -> Nat) (a : Nat) := f (f a)

-- a trivial proof by reflexivity
-- passing anonymous functions (lambdas)
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl

Enumerations

-- define enum
inductive DayPhase where
  | morning   : DayPhase
  | afternoon : DayPhase
  | evening   : DayPhase
  | night     : DayPhase

-- access an enum value
#check DayPhase.morning

-- expand namespace to allow accessing its elements directly
open DayPhase
#check morning

-- match for pattern matching
def preferences (d : DayPhase) : Nat :=
  match d with
  | afternoon => 3
  | evening   => 6
  | _         => 2

def DayPhase.next (d : DayPhase) : DayPhase :=
  match d with
  | morning   => afternoon
  | afternoon => evening
  | evening   => night
  | night     => morning

def DayPhase.previous : DayPhase -> DayPhase
  | morning   => afternoon
  | afternoon => evening
  | evening   => night
  | night     => morning

def isMorning : DayPhase → Bool :=
  fun -- idiom for lambda with a match
    | morning => true
    | _       => false

-- ToString is a generic class which contains a toString function
instance : ToString DayPhase where
  toString (d : DayPhase) : String :=
    match d with
    | morning   => "morning"
    | afternoon => "afternoon"
    | evening   => "evening"
    | night     => "night"

theorem DayPhase.nextOfPrevious (d : DayPhase) : next (previous d) = d :=
  sorry -- incomplete proof

Special symbols

The language adopts use of many special symbols. For example -> can be written as →, and fun as λ. To enter these symbols we usually write something like \to in the editor and press Tab. The particular method depends on your editor, but know that any symbol can be inspected in the editor to show how it is written (in VS code just hover over it with mouse).

We give a (non-exhaustive) table with such symbols and what they represent. All further examples use these symbols often.

Symbol Input Alternative Structure
λ \lam, \fun fun ?
→ \to -> ?
↔ \iff <-> Iff
∧ \and ? And
∨ \or ? Or
¬ \neg ? λ x → False
· \. ? ?
∘ \circ ? ?
⟨, ⟩ \<, \> ? X.intro

Proofs

…

Sources

This page paraphrases explanations and examples from various sources, you may find going through the original sources more preferable. The sources I used to create this page are: