Module 2 · Lesson 1

rfl — Reflexivity

rfl proves that something equals itself. It's the most fundamental tactic and often the first you'll learn.

The Basic Idea

Every value equals itself. That's the reflexivity of equality:

lean

1-- Anything equals itself
2example : 5 = 5 := rfl
3example : "hello" = "hello" := rfl
4example : [1, 2, 3] = [1, 2, 3] := rfl

But rfl is more powerful than it looks. It works whenever Lean can compute both sides to the same value:

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    -- Computed: 7 = 7
5
6-- String operations too
7example : "hel" ++ "lo" = "hello" := rfl
8
9-- List operations
10example : [1, 2] ++ [3] = [1, 2, 3] := rfl

Key Takeaway

rfl works when both sides of an equalitycompute (or "reduce") to the same term. Lean evaluates as much as it can before comparing.

When rfl Works

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
7
8def double (n : Nat) : Nat := n * 2
9example : double 5 = 10 := rfl          -- User-defined function

When rfl Fails

rfl can't prove things that require reasoning beyond computation:

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
5
6-- example : n + 0 = n := rfl
7-- Fails for arbitrary n (even though true by definition for specific n)
8
9-- example : n * 1 = n := rfl
10-- Fails! Requires induction to prove for all n

⚠

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.

rfl as a Tactic vs Term

rfl can be used both as a proof term and as a tactic:

lean

1-- As a term (no 'by')
2example : 2 + 2 = 4 := rfl
3
4-- As a tactic (with 'by')
5example : 2 + 2 = 4 := by rfl
6
7-- They're equivalent, but the tactic version gives better error messages

Related: Eq.refl

rfl is notation for Eq.refl, which explicitly takes the value:

lean

1-- These are the same
2example : 5 = 5 := rfl
3example : 5 = 5 := Eq.refl 5
4
5-- Eq.refl has type: ∀ (a : α), a = a
6#check @Eq.refl  -- {α : Sort u} → (a : α) → a = a

Deep Dive: Definitional vs Propositional Equality

Lean has two notions of equality:

Definitional equality: Two terms compute to the same value. Checked automatically. rfl proves this.
Propositional equality: Two terms are provably equal via some chain of reasoning. Requires explicit proof.

For example, 2 + 2 and 4 are definitionally equal. But n + 0 and nare only propositionally equal (proven by the lemma Nat.add_zero).

Common Uses

Proving computed results

lean

1-- After computation, things equal themselves
2example : (3 + 4) * 2 = 14 := rfl
3example : "abc".length = 3 := rfl
4example : [1, 2, 3].reverse = [3, 2, 1] := rfl

Closing goals after rewriting

lean

1example (a b : Nat) (h : a = b) : b = a := by
2  rw [h]    -- Goal becomes: b = b
3  rfl       -- Trivially true

Showing function application

lean

1def f (x : Nat) : Nat := x + 1
2
3example : f 5 = 6 := rfl  -- f 5 computes to 5 + 1 = 6

The native_decide Alternative

For decidable propositions that take too long to compute with rfl, use native_decide:

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

The Proof State Next: rw — Rewriting