Lean for Scala programmers - Part 4

Over the past few articles we've talked about inductive types, dependent functions, propositions as types, type classes, etc.

While this machinery is not strictly needed to start writing simple proofs (as witnessed by the amazing Natural Number Game), it certainly is when one is ready to move beyond carefully crafted pedagogical examples.

Today we're finally in a position to discuss in much more detail how to create proofs in Lean; in particular we'll analyze examples introduced previously.

Lean 4 version: 4.31.0
Latest revision: Sep 23, 2026

1. Two styles of proofs

Lean offers two ways to write a proof. Lean's documentation calls them term mode and tactic mode; here we'll use the names from The Hitchhiker's Guide to Logical Verification: forward and backward proofs.

1.1 Forward Proofs

A "forward" or "functional" proof (a term-mode proof) is just a regular function that uses standard functional programming constructs such as function application, pattern matching, variable assignment, etc. to construct a value of a given type.

1.1.1 Example 1

As a first example let's analyze the following statement:

Let $p, q$ be two arbitrary propositions.

Then

$$p \land q \implies q \land p$$

($\land$ is the logical And combinator)

This can be written in Lean as (we'll give it a name once it's finished)

example (p q: Prop) (h: p ∧ q): q ∧ p :=
  sorry

(∧ is entered with \and; ∨ with \or)

This declaration takes 3 arguments:

• Two propositions p, q
• A value h of type p ∧ q. In other words, h is a proof of the proposition p ∧ q.

The function itself corresponds to a logical implication; in order to prove it we have to create a value of type q ∧ p.

Looking at the definition of the And combinator we notice it is a structure with one constructor:

namespace Hidden

structure And (a b: Prop): Prop where
  intro ::
  left : a
  right : b

end Hidden

Note on syntax: intro :: changes the default constructor's name (mk), so that values can be created with And.intro a b. We put the definition in a Hidden namespace so it doesn't clash with the And already in Lean's prelude.

This means that we can use And.intro to introduce (i.e. create) conjunctions, and we can use And.left and And.right to eliminate (i.e. consume, or extract components of) conjunctions.

The symbol ∧ is infix notation for the type And. Lean's prelude declares it with infixr (an infix operator that associates to the right, with precedence 35). Here is the same declaration for our Hidden.And; scoped keeps it inside the Hidden namespace, so that it doesn't give the real ∧ a second meaning:

namespace Hidden

scoped infixr:35 " ∧ " => And

end Hidden

With this information let's finish the proof of and_is_comm:

theorem and_is_comm (p q: Prop) (h: p ∧ q): q ∧ p :=
  And.intro h.right h.left

With the anonymous constructor from Part 2, the same proof is even shorter:

example (p q: Prop) (h: p ∧ q): q ∧ p := ⟨h.right, h.left⟩

For a Scala programmer this proof should look familiar. Replace ∧ with a tuple, and it is the function that swaps the two components of a pair:

def andIsComm[P, Q](h: (P, Q)): (Q, P) = (h._2, h._1)

And plays the role of the tuple type (P, Q), And.intro of the tuple constructor, and .left / .right of ._1 / ._2. This is the Curry-Howard correspondence again: a proof of $p \land q \implies q \land p$ is a program that swaps a pair.

1.2 Backward Proofs

A second way to build proofs is using tactics (Lean calls this tactic mode). Tactics are meta programs that provide a layer of automation on top of the normal "forward" style. In many cases they are more convenient for interactive use:

theorem and_is_comm' (p q: Prop) (h: p ∧ q): q ∧ p := by
  apply And.intro
  exact h.right
  exact h.left

Tactic mode is entered with the keyword by.

Before describing each tactic we need to talk about the local context and the proof goal.

The local context can be seen in the Lean Infoview of VS Code. If you place the cursor at the end of the by line above you should see this (blocks like this one show the Infoview; they are not Lean code):

p q : Prop
h : p ∧ q
⊢ q ∧ p

The symbol ⊢ (turnstile) is used in logic to indicate that the right-hand side (q ∧ p) can be proved, or follows logically from the left-hand side.

The general form is:

Context ⊢ Goal

• The context is a list of hypotheses: names together with their types.
• The goal is a type; in many cases a proposition.

It is common to use the letter Gamma to represent the context:

Γ ⊢ Goal

When proving things in Lean our objective is to create a term of the type specified by the goal; or alternatively simplify the goal into something that is logically equivalent.

Returning to our proof:

• apply And.intro uses the constructor And.intro to generate two (sub) goals, named after the fields of And:

case left
p q : Prop
h : p ∧ q
⊢ q

case right
p q : Prop
h : p ∧ q
⊢ p

Intuitively, in order to prove q ∧ p it suffices to prove q and p separately, since we can use And.intro afterwards.

• exact h.right uses the function And.right to select the q component of h, and tries to close the subgoal q with it.
• exact h.left does the same for the second subgoal

After this there are no more goals left so this concludes the proof.

Notice how the context is just the scope of the function that represents the proof.

2. Induction and Natural Numbers

2.1 Example 2

Let's start with this proposition:

Addition of natural numbers is defined in Lean's core library as Nat.add (the + notation uses it), essentially like this:

def add: Nat -> Nat -> Nat
  | a, 0     => a
  | a, b + 1 => (add a b) + 1

and so the proposition is true basically "by definition" (it is the first case | a, 0 => a above; Part 3 explains why rfl works here)

theorem add_zero' (n: Nat): n + 0 = n := by rfl

This theorem is available in the core library as Nat.add_zero.

2.2 Example 3

On the other hand:

needs a real proof: rfl fails here, because 0 + n can't reduce while n is unknown.

We'll use mathematical induction over the input argument n. Here is the skeleton of the proof, with sorry in both cases:

example (n: Nat): 0 + n = n := by
  induction n with
  | zero =>
    -- base case:
    sorry
  | succ d hd =>
    -- inductive step:
    sorry

The induction tactic operates on the goal, which has to be a proposition that depends on a given variable n: Nat. In the succ case, d is the predecessor of n (so n is d + 1), and hd is the induction hypothesis: a proof of the statement for d. The names d and hd are our choice.

induction creates two subgoals, the base case and the inductive step:

case zero
⊢ 0 + 0 = 0

case succ
d : Nat
hd : 0 + d = d
⊢ 0 + (d + 1) = d + 1

The first subgoal can be completed with rfl:

example (n: Nat): 0 + n = n := by
  induction n with
  | zero => rfl
  | succ d hd => -- inductive step:
    sorry

For the second subgoal we'll use the tactic rw to rewrite it towards something that can be proved by rfl:

The rewrite tactic rw takes a value h of type a = b and uses it to replace all occurrences of a by b in the goal. After the rewrite, it tries to close the goal with rfl.

We're going to use the core library theorem Nat.add_succ:

Nat.add_succ (n m : Nat) : n + m.succ = (n + m).succ

(m.succ is dot notation for Nat.succ m, which is equal to m + 1 by definition.)

In particular

#check Nat.add_succ 0
-- Nat.add_succ 0 : ∀ (m : Nat), 0 + m.succ = (0 + m).succ

so that

rw [Nat.add_succ 0 d]

will transform

⊢ 0 + (d + 1) = d + 1

into

⊢ (0 + d).succ = d + 1

Similarly, rw [hd] will replace 0 + d by d. That gives d.succ = d + 1, which rw then closes with rfl.

Putting all the pieces together:

theorem zero_add (n: Nat): 0 + n = n := by
  induction n with
  | zero => rfl
  | succ d hd =>
    rw [Nat.add_succ 0 d]
    rw [hd]

-- Goals accomplished 🎉

The line rw [Nat.add_succ 0 d] can be also written as rw [Nat.add_succ], as Lean can infer the arguments 0 and d.

Before moving on let's show a different approach that can produce more compact proofs:

theorem zero_add': ∀ (n: Nat), 0 + n = n
  | 0     => rfl
  | d + 1 => by rw [Nat.add_succ, zero_add' d]

We are pattern matching on the structure of n: Nat and returning two proofs, and Lean is using them to assemble the full inductive proof.

• consecutive rw lines can be collapsed into a single rw [...]
• in the case d + 1, the recursive call zero_add' d is the inductive hypothesis, just like the recursive call in map_length in Part 1. The Infoview doesn't list zero_add' in the context, but we can call it on the smaller number d.
• this proof also mixes the two styles: the pattern match is term mode, and each case can switch to tactic mode with by.

3. Structural Induction

Induction over the natural numbers (mathematical induction) is a special case of Structural Induction, which can be used in Lean to prove properties of inductively defined data types.

3.1 Example 4

Let's analyze the map_length example we mentioned back in the first part of this series.

Given the following definitions of length and map on Lists:

def length: List A -> Nat
  | []     => 0
  | _ :: t => 1 + length t

def map (f: A -> B): List A -> List B
  | []     => []
  | h :: t => f h :: map f t

we'll prove that applying map doesn't change the length of the resulting List.

length (map f l) = length l

The idea is the same as in induction over the natural numbers: we consider all constructors for the given data type and provide proofs of all cases. Lean will assemble all the pieces into a proof that is valid for all inhabitants of the given type:

theorem map_length (f: A -> B):
  ∀ (l: List A), length (map f l) = length l
  | []     => by rfl
  | h :: t => by rw [length, map, length, map_length f t]

The base case is trivially true (provable by rfl) so let's focus on the inductive step.

This is the initial proof state:

A : Type u_1
B : Type u_2
f : A → B
h : A
t : List A
⊢ length (map f (h :: t)) = length (h :: t)

(A and B are auto-bound implicit arguments, which we saw in Part 1. As with zero_add', the recursive map_length is available, but the Infoview doesn't list it.)

We're going to manipulate the goal until we get something "obvious" that can be proved by rfl:

In this case we've used rw with a definition as an argument (instead of an equation). rw [length] rewrites with the equations that Lean generates from the definition of length, so it "unfolds" the definition one step at a time.

rw works on the syntax of the goal: it rewrites the first place where an equation matches. That's why the first rw [length] changes the right-hand side. On the left, map f (h :: t) doesn't have the form _ :: _ yet, so only length (h :: t) matches. After rw [map], the left side has that form, and the second rw [length] can unfold it.

The last step has the form a = a: after rw [map_length f t] the goal is 1 + length t = 1 + length t, and rw closes it with rfl automatically.

This is a good moment to mention the tactic simp

simp [h₁, h₂, ..., hₙ] uses the provided expressions, and other theorems tagged with the attribute [simp], to simplify the main goal.

We could have proved the inductive step like this:

  | h :: t => by simp [length, map, map_length]

3.2 A very low level proof

As a comparison here's a different proof (in functional style), showing all the gory details:

theorem map_length' (f: A -> B):
  ∀ (l: List A), length (map f l) = length l
  | []     => rfl
  | h :: t =>
    -- show that:  length (map f (h :: t)) = length (h :: t)
    let l1:     length (map f t) =     length t             := map_length' f t -- by induction hypothesis
    let l2: 1 + length (map f t) = 1 + length t             := congrArg _ l1    -- adding 1 on both sides
    let d1: 1 + length (map f t) = length (f h :: map f t)  := rfl       -- by definition of length
    let d2:       f h :: map f t = map f (h :: t)           := rfl       -- by definition of map
    let l3:         1 + length t = length (f h :: map f t)  := l2 ▸ d1   -- substitution (l2 in d1)
    let l4:         1 + length t = length (map f (h :: t))  := d2 ▸ l3   -- substitution (d2 in l3)
    let d3:         1 + length t = length (h :: t)          := rfl       -- by definition of length again

    let goal: length (map f (h :: t)) = length (h :: t) :=  l4 ▸ d3       -- substitution (l4 in d3)
    goal

• h ▸ e, where h : a = b, rewrites the type of e with h: it replaces a by b (or b by a, whichever makes the result fit the expected type). It serves the same purpose as rw in tactic mode.

If you look carefully at lines 9 and 12:

let d2:       f h :: map f t = map f (h :: t)           := rfl
let d3:         1 + length t = length (h :: t)          := rfl

you'll notice that we're creating proofs of something that is not literally of the form a = a.

d2 follows from the definition of map and d3 from the definition of length.

This shows that we can use rfl (or by rfl) to prove that two things are identical or equal "by definition".

Tactic-mode proofs are very handy for interactive use, since it's easy to inspect the state of the proof. On the other hand the state itself is not captured in the source code, which can make the proof harder to read.

It is good to remember that term mode and tactic mode can be mixed as needed: zero_add' and map_length above do exactly that.

Resources

• Theorem Proving in Lean 4:
  • Tactics
  • Induction and Recursion
• The Hitchhiker's Guide to Logical Verification (2023 edition, for Lean 4)
• Natural Number Game