Module 2 · Lesson 1

rfl — Reflexivity

rfl proves 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 compute both 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

rfl can'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 = b + a := rfl  
4-- ❌ Fails! Lean doesn't know what a and b are, can't compute
5
6-- example : n + 0 = n := rfl
7-- ❌ Fails for arbitrary n (works for specific n like 5)
8
9-- example : n * 1 = n := rfl
10-- ❌ Fails! Requires induction to prove for all n
11
12-- example : List.reverse (List.reverse xs) = xs := rfl
13-- ❌ Fails! Can't compute without knowing xs

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 propositional equality (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 can't prove this
2-- example (n : Nat) : n + 0 = n := rfl
3
4-- ✓ Correct: use simp or the specific lemma
5example (n : Nat) : n + 0 = n := by simp
6example (n : Nat) : n + 0 = n := Nat.add_zero n

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 order matters for some operations

lean

1-- 0 + n and n + 0 behave differently!
2example (n : Nat) : 0 + n = n := rfl  -- ✓ Works! (by definition of +)
3-- example (n : Nat) : n + 0 = n := rfl  -- ❌ Fails (requires lemma)

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 only propositionally equal(proven by the lemma Nat.add_zero)
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-- Common pattern: rewrite then close with rfl
2example (a b : Nat) (h : a = b) : b = a := by
3  rw [h]    -- Goal becomes: b = b
4  rfl       -- Now trivially true
5
6example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by
7  rw [h1, h2]  -- Goal becomes: z = z
8  rfl

Performance: native_decide

For decidable propositions with large computations, rfl can be slow because it runs in Lean's type checker. For better performance, usenative_decide which compiles to native code:

lean

1-- This might be slow with rfl for large numbers
2example : 123456 + 789012 = 912468 := by native_decide
3
4-- native_decide uses compiled code, which is much faster
5-- Useful for large computations you want to verify

Summary

Situation	Use rfl?
Goal is `x = x`	✅ Yes
Both sides compute to same value	✅ Yes
Involves variables (like `n + 0 = n`)	❌ No, use `simp`
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 doesn't work:
2-- example (n : Nat) : n + 0 = n := rfl
3
4-- Fix it:
5example (n : Nat) : n + 0 = n := by
6  simp  -- or: exact Nat.add_zero n

The Proof State Next: rw — Rewriting