Module 2 · Lesson 1

rfl — Reflexivity

rflproves that something equals itself. It's the most fundamental tactic in Lean 4 and often the first you'll learn. Despite its simplicity, understanding when and why it works is essential for mastering proof writing.

The Basic Idea

Every value equals itself. This is the reflexivity property of equality—one of the most basic axioms in mathematics. In Lean, rfl(short for "reflexivity") is how you prove that two expressions are equal when they compute to the same value:

lean

1-- Anything equals itself
2example : 5 = 5 := rfl
3example : "hello" = "hello" := rfl
4example : [1, 2, 3] = [1, 2, 3] := rfl
5
6-- Works for any type
7example : true = true := rfl
8example : () = () := rfl  -- Unit type

But rfl is more powerful than it looks. It works whenever Lean can computeboth sides to the same value. This means you can prove equalities that don't look identical at first glance:

lean

1-- These compute to the same value
2example : 2 + 2 = 4 := rfl        -- 2 + 2 computes to 4
3example : 10 - 3 = 7 := rfl       -- 10 - 3 computes to 7
4example : 2 * 3 + 1 = 7 := rfl    -- 2 * 3 + 1 → 6 + 1 → 7
5
6-- String operations
7example : "hel" ++ "lo" = "hello" := rfl
8
9-- List operations
10example : [1, 2] ++ [3] = [1, 2, 3] := rfl
11example : [1, 2, 3].head? = some 1 := rfl

Key Takeaway

rfl works when both sides of an equality compute(or "reduce") to the same term. Lean evaluates as much as it can before comparing. This is called definitional equality.

When to Use rfl

Reach for rfl in these situations:

Closing trivial goals: When both sides of an equality are identical or compute to the same thing
After rewriting: When rw transforms the goal to x = x
Verifying function definitions: To confirm that a function produces the expected output for specific inputs
Testing computed values: To validate that complex expressions evaluate correctly

lean

1-- Definitional equality: both sides compute to the same thing
2example : (fun x => x + 1) 5 = 6 := rfl  -- Function application
3
4example : [1, 2, 3].length = 3 := rfl   -- Method call
5
6example : (if true then 1 else 2) = 1 := rfl  -- Conditional evaluation
7
8def double (n : Nat) : Nat := n * 2
9example : double 5 = 10 := rfl          -- User-defined function
10
11-- Pattern matching computes
12def isZero : Nat → Bool
13  | 0 => true
14  | _ => false
15example : isZero 0 = true := rfl
16example : isZero 7 = false := rfl

When rfl Fails

rflcan't prove things that require reasoning beyond computation. If Lean can't directly evaluate both sides to the exact same term, rfl will fail:

lean

1-- These require actual reasoning, not just computation
2
3-- example (a b : Nat) : a + b = b + a := rfl
4-- ❌ Fails: nothing can reduce until a and b are known
5
6-- example (n : Nat) : 0 + n = n := rfl
7-- ❌ Fails: Nat.add recurses on its SECOND argument, so 0 + n is stuck
8
9-- example (n : Nat) : n * 1 = n := rfl
10-- ❌ Fails: n * 1 reduces to 0 + n, which is stuck (see above)
11
12-- example (xs : List Nat) : xs.reverse.reverse = xs := rfl
13-- ❌ Fails: can't compute without knowing xs
14
15-- But note that this one DOES work, which surprises people:
16example (n : Nat) : n + 0 = n := rfl   -- ✓

When rfl fails, you need other tactics:

simp — for simplification using known lemmas
rw — to rewrite using equalities
ring — for algebraic identities
omega — for linear arithmetic

⚠

rfl only works for definitional equality—when things compute to the same value. For propositionalequality (things that are equal but don't directly compute), you need other tactics.

Common Mistakes

Here are pitfalls beginners often encounter with rfl:

Mistake 1: Expecting rfl to prove algebraic identities

lean

1-- ❌ Wrong: rfl cannot prove commutativity - nothing reduces
2-- example (a b : Nat) : a + b = b + a := rfl
3
4-- ✓ Correct: use the lemma, or a decision procedure
5example (a b : Nat) : a + b = b + a := Nat.add_comm a b
6example (a b : Nat) : a + b = b + a := by omega

Mistake 2: Confusing similar-looking expressions

lean

1-- These look the same but aren't definitionally equal!
2-- example (xs : List Nat) : xs ++ [] = xs := rfl  -- ❌ Fails
3
4-- The definition of ++ recurses on the first list
5-- so xs ++ [] doesn't simplify without knowing xs
6example (xs : List Nat) : xs ++ [] = xs := by simp  -- ✓ Works

Mistake 3: Forgetting which side reduction happens on

This is the single most confusing thing about rfl, and it comes entirely from how Nat.add is defined:

lean

1-- Nat.add recurses on its SECOND argument:
2--   n + 0     = n
3--   n + (m+1) = (n + m) + 1
4
5-- So a literal on the RIGHT can be consumed step by step:
6example (n : Nat) : n + 0 = n := rfl        -- ✓ one step
7example (n : Nat) : n + 2 = n + 1 + 1 := rfl  -- ✓ two steps
8
9-- But a variable on the RIGHT blocks everything:
10-- example (n : Nat) : 0 + n = n := rfl     -- ❌ stuck immediately
11example (n : Nat) : 0 + n = n := Nat.zero_add n   -- ✓ needs the theorem
12
13-- Same story for multiplication (also recursive on the right):
14example (n : Nat) : n * 0 = 0 := rfl        -- ✓
15-- example (n : Nat) : n * 1 = n := rfl     -- ❌ reduces to 0 + n, stuck
16-- example (n : Nat) : 1 * n = n := rfl     -- ❌ stuck immediately

💡

The rule of thumb: reduction eats the right-hand argument. If the thing you want to disappear is on the right and is a literal, try rfl. If it is on the left, or is a variable, you need Nat.zero_add, simp, omega, or induction.

rfl as a Tactic vs Term

rfl can be used both as a proof term and as a tactic. Both are correct, but they behave slightly differently:

lean

1-- As a term (no 'by') - direct proof term
2example : 2 + 2 = 4 := rfl
3
4-- As a tactic (with 'by') - enters tactic mode first
5example : 2 + 2 = 4 := by rfl
6
7-- The tactic version gives better error messages when it fails
8-- It also allows you to add other tactics before it if needed
9example : 2 + 2 = 4 := by
10  -- could add 'show 4 = 4' or other tactics here
11  rfl

Related: Eq.refl and @rfl

rfl is actually notation for Eq.refl _, where Lean infers the value. Understanding this helps when you need more control:

lean

1-- These are all equivalent
2example : 5 = 5 := rfl
3example : 5 = 5 := Eq.refl 5
4example : 5 = 5 := @rfl Nat 5
5
6-- Eq.refl has type: ∀ (a : α), a = a
7#check @Eq.refl  -- {α : Sort u} → (a : α) → a = a
8
9-- Sometimes you need @rfl to help type inference
10example : ([] : List Nat) = [] := @rfl (List Nat) []

Deep Dive: Definitional vs Propositional Equality

Lean has two notions of equality, and understanding the difference is crucial:

Definitional equality:Two terms compute to the same value. Checked automatically by Lean's kernel. rfl proves this.
Propositional equality: Two terms are provably equal via some chain of reasoning. Requires explicit proof with tactics or lemmas.

For example:

2 + 2 and 4 are definitionally equal
n + 0 and n are definitionally equal — Nat.add_zeroexists as a named lemma, but its proof is literally rfl
0 + n and n are only propositionally equal — Nat.zero_addis proved by induction on n
a + b and b + a are only propositionally equal(proven by Nat.add_comm)

Definitional equality is "built-in" and checked automatically. Propositional equality requires you to prove it explicitly.

Real-World Examples

Validating data transformations

lean

1-- Verify JSON-like value transformations
2def Config := List (String × Nat)
3
4def defaultConfig : Config := [("timeout", 30), ("retries", 3)]
5
6example : defaultConfig.length = 2 := rfl
7example : (defaultConfig.lookup "timeout") = some 30 := rfl

Testing parsing functions

lean

1-- Quick unit tests using rfl
2def parseDigit : Char → Option Nat
3  | '0' => some 0
4  | '1' => some 1
5  | '2' => some 2
6  | _ => none
7
8example : parseDigit '1' = some 1 := rfl
9example : parseDigit 'a' = none := rfl

Closing goals after rewriting

lean

1-- rw already tries rfl for you, so usually you write just:
2example (a b : Nat) (h : a = b) : b = a := by
3  rw [h]       -- goal becomes b = b, and rw closes it
4
5example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by
6  rw [h1, h2]  -- goal becomes z = z, closed
7
8-- Adding an explicit rfl after these gives "No goals to be solved".
9-- You only need rfl when the rewrite leaves a goal that is definitionally
10-- true but not SYNTACTICALLY identical:
11example (n : Nat) (h : n = 3) : n + 0 = 3 := by
12  rw [h]       -- goal: 3 + 0 = 3, which rw's rfl also handles

When Computation Gets Expensive

rflruns inside Lean's kernel. For Nat arithmetic that is fine — the kernel has special GMP-backed support for it — but for anything the kernel must unfold step by step, it can become slow.

lean

1-- Perfectly fast: the kernel special-cases Nat arithmetic
2example : 123456 + 789012 = 912468 := by rfl
3example : 2 ^ 64 = 18446744073709551616 := by rfl
4
5-- decide: for decidable propositions that are not equations
6example : (5 : Nat) < 10 ∧ (3 : Nat) ≠ 4 := by decide
7
8-- native_decide: compiles the check to machine code and trusts the result
9-- example : someHugeComputation = expected := by native_decide

⚠

native_decide is a genuine escape hatch, not just a faster decide. It adds Lean.ofReduceBoolto your trusted base — meaning you are now trusting the Lean compiler, your C compiler, and the hardware, rather than only the ~5000-line kernel. Check for it with #print axioms, and reach for it only when decide genuinely cannot finish.

Summary

Situation	Use rfl?
Goal is `x = x`	✅ Yes
Both sides compute to same value	✅ Yes
Variable with a literal on the right (`n + 0 = n`)	✅ Yes — this one reduces
Variable on the right (`0 + n = n`)	❌ No, use `simp` or `Nat.zero_add`
Algebraic identity (like `a + b = b + a`)	❌ No, use `ring` or lemma

Exercise 1: Basic Computation

Close the goal using computation and rfl.

lean

1example : (3 * 4) + 2 = 14 := by
2  rfl

Exercise 2: Function Verification

Verify that this function works correctly for the given input.

lean

1def greet (name : String) : String := "Hello, " ++ name ++ "!"
2
3example : greet "World" = "Hello, World!" := by
4  rfl

Exercise 3: Why Does This Fail?

This proof fails with rfl. Can you explain why and fix it with the right tactic?

lean

1-- This does NOT work:
2-- example (n : Nat) : 0 + n = n := rfl
3-- Why? Nat.add recurses on its second argument, so with n unknown
4-- there is nothing to reduce.
5
6-- Fix it, three ways:
7example (n : Nat) : 0 + n = n := by simp
8example (n : Nat) : 0 + n = n := Nat.zero_add n
9example (n : Nat) : 0 + n = n := by omega
10
11-- Meanwhile, its mirror image needs no tactic at all:
12example (n : Nat) : n + 0 = n := rfl

Proof Workflow Next: rw — Rewriting