Basic Syntax

This chapter introduces the foundational elements of Lean 4’s syntax. We will learn how to define variables, write functions, and work with types and expressions, the essential building blocks of Lean 4 programming. By the end, we will be able to read and write basic Lean 4 programs, preparing us for more advanced topics ahead.

The Lean 4 Working Environment in VS Code

When we start a Lean 4 project in VS Code, the working environment is laid out in a three-pane interface, with each panel serving a crucial function.

The File Explorer, located on the left, presents our project’s hierarchical structure, allowing you to navigate through the various .lean files. In the center, the Code Editor acts as the core of our writing. Here, we will enter the text for our program or proof and benefit from advanced features like syntax highlighting, which colors keywords and types for better readability. Finally, the right-hand panel, known as the Lean Infoview, is the most distinctive and powerful tool in this ecosystem. This panel is a real-time viewer of our code’s state, showing the proof state (the goal to prove and the available assumptions) line by line, allowing us to follow the evolution of our arguments. Additionally, the Infoview is where detailed error and warning messages appear, helping us diagnose type or syntax problems, and where we can inspect information about any definition by hovering over it.

The integration of these three panels creates an immediate and continuous feedback loop, optimizing the process of development and proof-writing in Lean.

To get started, we need to ask a fundamental question.

What is a type?

A type is a label or classification for data, defining what kind of values it can hold and what operations can be performed on it. Types are essential in both programming and theorem proving, ensuring correctness and structuring reasoning. In Lean 4, types act as a safety mechanism:

• A value of type Nat (natural number) can be 0, 1, 2, etc.
• A value of type String can be "hello", "Lean 4", etc.
• A function of type Nat → Nat takes a natural number as input and outputs another natural number.

By assigning types to values and functions, Lean 4 prevents errors like adding a number to a string or applying a function to incompatible data.

Next, we will explore some fundamental Lean 4 commands.

Comment code

In Lean 4, comments help make code more readable and serve as documentation. They are ignored by the compiler and do not affect execution. Here’s how to write comments in Lean:

• Single-line comments start with -- and apply to the rest of the line.
• Multi-line comments are enclosed between /- and -/.

comment.lean

-- This is a comment  

/-
This is a multi-line comment.
It can span multiple lines.
Useful for longer explanations. 
-/

check

We will begin with the #check command, a key tool for exploring Lean’s type system. The #check command allows us to inspect the type of an expression, definition, or theorem in Lean. It’s invaluable for understanding how Lean interprets our code and for troubleshooting type-related issues.

check.lean

#check true  
#check 42     
#check 'h'
#check ['h', 'e', 'l', 'l', 'o']
#check "hello"   
#check Nat     
#check Type

In these examples:

1. #check true outputs Bool.true : Bool which tells us that true is of type Bool (a boolean).

2. #check 42 outputs 42 : Nat which tells us that 42 is of type Nat (natural number).

3. #check 'h' outputs 'h' : Char which tells us that 'h' is of type Char (a character).

4. #check ['h', 'e', 'l', 'l', 'o'] outputs ['h', 'e', 'l', 'l', 'o'] : List Char which tells us that ['h', 'e', 'l', 'l', 'o'] is of type List Char (a list of characters).

5. #check "hello" outputs "hello" : String which tells us that "hello" is of type String (a string).

6. #check Nat outputs Nat : Type which tells us that Nat is of type Type (a type).

7. #check Type outputs Type : Type 1 which tells us that Type is of Type 1 (a type of level 1). Type 1 is a universe one level higher than Type. Universes are organized in a hierarchy: Type (also called Type 0), Type 1, Type 2, and so on. This reflects the hierarchical structure of universes in type theory, where each universe is contained in a higher-level universe to maintain logical consistency.

print

The #print command allows us to inspect the definition of a function, theorem, or other named entity in Lean. It provides detailed information, including the type, implementation, and any dependencies. This command is especially useful for understanding how Lean’s standard library works or for debugging our own code.

print.lean

#print Bool 
#print Nat
#print Char
#print List
#print String
-- We cannot #print Type because this is a built-in concept
#print Type -- returns an error

In these examples:

• #print Bool outputs

inductive Bool : Type
number of parameters: 0
constructors:
Bool.false : Bool
Bool.true : Bool

This tells us that Bool is an inductive type with no parameters and two constructors. Constructors are ways to provide elements of the given type—in this case, Bool.false represents the value false, and Bool.true represents the value true. Thus, an inductive type defines a new type by specifying a set of constructors that generate its elements. Each constructor may take arguments, including recursive references to the type itself. Inductive types are fundamental in Lean, serving as the basis for both data structures (such as natural numbers, lists, and trees) and logical propositions. We will delve into inductive types in greater detail later, but for now, note that constructors specify the possible values of a type, and Bool is a type with exactly two such values.

• #print Nat outputs

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

As we can see, Nat is also an inductive type representing natural numbers, which do not require parameters. It has two constructors:

• Nat.zero, which represents the number 0.
• Nat.succ, which represents the successor of a natural number (essentially adding 1).

This definition allows natural numbers to be constructed starting from 0 and adding 1 repeatedly. Another way of denoting natural numbers in Lean is using ℕ. To type this symbol, you can use the shortcut \N.

• #print Char outputs

structure Char : Type
number of parameters: 0
constructor:
Char.mk : (val : UInt32) → val.isValidChar → Char
fields:
val : UInt32
valid : self.val.isValidChar

Char is a structure representing a single character and does not have parameters. A structure in Lean is a way to define a type that groups together related data. The Char structure has a constructor called Char.mk, which takes:

• A UInt32 value (a 32-bit unsigned integer) representing the Unicode code point of the character.
• val.isValidChar, a proof that the value is a valid Unicode character.

Moreover, every element of type Char has two associated fields:

• val: This field returns the Unicode value of the character.
• valid: This field returns the proof that the code point is valid.

Thus, the Char structure combines the character value and its validity in a structured way. We will also explore structures in more detail in future chapters.

• #print List outputs

inductive List.{u} : Type u → Type u
number of parameters: 1
constructors:
List.nil : {α : Type u} → List α
List.cons : {α : Type u} → α → List α → List α

List is an inductive type that represents a sequence of elements of a type α, where α is a type of some universe u. This is the more general way of defining lists. The List type requires one parameter, α, where α is the type of elements in the list. For example, when we instantiate List with Nat, we get the type of lists of natural numbers (List Nat), and when instantiated with Char, we get the type of lists of characters (List Char). We can also instantiate it with Type, to get a list of types (List Type). The List type has two constructors:

• List.nil, which represents the empty list ([]).
• List.cons, which adds an element to the front of a list.

Thus, List allows us to work with ordered sequences of elements, either empty or with elements added recursively.

• #print String outputs

structure String : Type
number of parameters: 0
constructor:
String.mk : List Char → String
fields:
data : List Char

This indicates that String is a structure in Lean, with no parameters, that represents strings. The constructor for String is String.mk, which takes a List Char (a list of characters) as input and returns a String. Each element of type String has a field called data, which returns the list of characters that make up the string.

• #print Type outputs an error.

The reason is that Type is a fundamental, built-in concept within Lean’s logical framework, not a user-defined term or definition. In Lean, Type denotes the universe of all types, and it cannot be queried using #print because it is not a printable entity like user-defined terms.

def

The def keyword is used to define a function or a value in Lean. It is one of the most fundamental constructs, allowing us to create reusable code—whether for simple values, functions, or more complex computations.

def.lean

-- Definition of number pi
def pi : Float := 3.1415926

Definitions can have parameters.

def.lean

-- Definition of the sum of two natural numbers
def sum (a b : Nat) : Nat := a + b

fun

The fun keyword is used to define anonymous functions (also called lambda functions) in Lean. These are functions that do not have a name and are defined inline. The fun keyword is a core concept in functional programming. We can also use the λ (lambda) operator to define anonymous functions, which is written as \lambda in Lean.

fun.lean

-- Two anonymous ways of defining the sum of two natural numbers
#check fun (a b : Nat) => a + b
#check λ (a b : Nat) => a + b

The resulting type Nat → Nat → Nat represents a curried function, which is a fundamental concept in functional programming. This type can be understood as follows:

• Nat → Nat → Nat is a function that takes a Nat (first argument) and returns another function.
• The returned function then takes a Nat (second argument) and returns a Nat (final result).

This curried function type is equivalent to Nat → (Nat → Nat)—meaning a function that takes a Nat and returns a function from Nat to Nat. In Lean, function types are right-associative, so the parentheses are often omitted for clarity. Thus, Nat → Nat → Nat is interpreted as Nat → (Nat → Nat).

The function type

In general, if A and B are types, then A → B is a type representing all functions from type A to type B. This means that any value of type A → B is a mapping that takes an element of type A and returns an element of type B. In Lean, we use \to to type the arrow → when writing this in code. We will explore this type in more detail later.

function.lean

-- The type of all mappings from Nat to Nat
#check Nat → Nat 

-- An example of an element of the above type
#check sum 42

This new construction provides an alternative approach to defining the previous sum mapping. The goal is to construct an element of type Nat → Nat → Nat. There are several ways to achieve this: either by using the fun keyword, as previously demonstrated, or by explicitly introducing the variables and specifying the expression that the mapping should return.

The latter approach uses the keywords by, intro, and exact. These are used in interactive proof mode, where you construct definitions step by step using tactics.

• by: This keyword signals that the definition will be built interactively using tactics.
• intro: This tactic introduces the function’s arguments as hypotheses in the goal.
• exact: This tactic is used to provide the exact value that satisfies the goal.

sum.lean

-- This function has name
def sum2 : Nat → Nat → Nat := fun a b => a + b

-- This function has name and uses tactics
def sum3 : Nat → Nat → Nat := by
    intro a b 
    exact a + b

cases

The cases tactic splits the definition into branches based on the possible values of the input. We will use it to define the Negation function for Booleans.

BoolNot.lean

-- The negation function for Booleans using cases
def BoolNot : Bool → Bool := by
  intro b
  cases b
  -- b = false
  exact true
  -- b = true
  exact false

match

The match keyword is used for pattern matching. This is another way to handle different cases of the input.

BoolNot.lean

-- The negation function for Booleans using match
def BoolNot2 : Bool → Bool := by
  intro b
  match b with
    | false => exact true
    | true  => exact false

let

The let keyword is used to define local variables or terms within a proof or expression.

sphere.lean

-- The volume of a sphere as a function of its radius
def sphereVolume (r : Float) : Float :=
  let pi : Float := 3.1415926
  (4/3) * pi * r^3 

eval

The #eval command is used to evaluate an expression and display its result. It is one of the most commonly used commands for testing and debugging code, as it allows us to see the output of a computation directly.

eval.lean

#eval sum 3 4
#eval (sum 3) 4
#eval (fun (a b : Nat) => a + b) 3 4
#eval pi
#eval Nat.succ 4 
#eval UInt32.isValidChar 104
#eval 'h'.val
#eval String.mk ['h', 'e', 'l', 'l', 'o']
#eval "hello".data

The first evaluations result in 7 because they compute the sum 3 + 4. After that, the following evaluations make use of previously defined values. For example, #eval pi returns the value of pi that was defined earlier. #eval Nat.succ 4 evaluates the successor function for natural numbers, applied to 4, returning 5 as the result. #eval UInt32.isValidChar 104 returns true, indicating that 104 is a valid Unicode character. #eval 'h'.val shows that the character 'h' has the Unicode value 104. Additionally, #eval String.mk ['h', 'e', 'l', 'l', 'o'] transforms the list of characters ['h', 'e', 'l', 'l', 'o'] into a string, in this case "hello". Finally, #eval "hello".data returns the list of characters that make up the string "hello", in this case ['h', 'e', 'l', 'l', 'o'].

variable

The keyword variable is used to declare variables that can be used later in the code. These variables are implicitly available in the context of any theorem, definition, or proof that follows. They allow us to introduce general assumptions or placeholders for types or values without needing to explicitly define them at each step.

variable.lean

variable (m n : Nat)
#check m

namespaces

Namespaces in Lean are used to organize code, helping with structure and readability. We can define variables, functions, or theorems within a namespace, and these definitions are scoped to that namespace, meaning they are only accessible inside it. When we exit a namespace, the variables defined inside it are no longer recognized. To access a variable defined within a namespace, we must reference it using the namespace name.

namespace.lean

namespace WorkSpace

-- Define a natural number r with the value 27
def r : Nat := 27

-- The variable r is perfectly defined within the namespace
#eval r   

end WorkSpace

-- Evaluating r outside the namespace will result in an error
#eval r  -- Error: unknown identifier 'r'

-- To access r, we must reference it using its namespace
#eval WorkSpace.r  -- Output: 27

open

The open keyword is used in Lean to bring definitions, theorems, or namespaces into the current scope, allowing us to reference them without needing to use their full qualified names. This helps make our code more concise and easier to read by reducing the need for repetitive namespace prefixes.

open.lean

open Workspace
#eval r -- Output: 27