Source: [rfl Tactic in Lean 4: Proof by Reflexivity](https://lean4.dev/tactics/core/rfl) --- ## rfl — Reflexivity `rfl` proves that something equals itself. It is usually the first tactic people learn. It is also worth understanding exactly when it works and when it does not, which is what this page covers. ## 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: ``` -- Anything equals itself example : 5 = 5 := rfl example : "hello" = "hello" := rfl example : [1, 2, 3] = [1, 2, 3] := rfl -- Works for any type example : true = true := rfl example : () = () := rfl -- Unit type ``` But `rfl` does more than it seems to. 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: ``` -- These compute to the same value example : 2 + 2 = 4 := rfl -- 2 + 2 computes to 4 example : 10 - 3 = 7 := rfl -- 10 - 3 computes to 7 example : 2 * 3 + 1 = 7 := rfl -- 2 * 3 + 1 → 6 + 1 → 7 -- String operations example : "hel" ++ "lo" = "hello" := rfl -- List operations example : [1, 2] ++ [3] = [1, 2, 3] := rfl example : [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 ``` -- Definitional equality: both sides compute to the same thing example : (fun x => x + 1) 5 = 6 := rfl -- Function application example : [1, 2, 3].length = 3 := rfl -- Method call example : (if true then 1 else 2) = 1 := rfl -- Conditional evaluation def double (n : Nat) : Nat := n * 2 example : double 5 = 10 := rfl -- User-defined function -- Pattern matching computes def isZero : Nat → Bool | 0 => true | _ => false example : isZero 0 = true := rfl example : 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: ``` -- These require actual reasoning, not just computation -- example (a b : Nat) : a + b = b + a := rfl -- ❌ Fails: nothing can reduce until a and b are known -- example (n : Nat) : 0 + n = n := rfl -- ❌ Fails: Nat.add recurses on its SECOND argument, so 0 + n is stuck -- example (n : Nat) : n * 1 = n := rfl -- ❌ Fails: n * 1 reduces to 0 + n, which is stuck (see above) -- example (xs : List Nat) : xs.reverse.reverse = xs := rfl -- ❌ Fails: can't compute without knowing xs -- But note that this one DOES work, which surprises people: example (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 *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 ``` -- ❌ Wrong: rfl cannot prove commutativity - nothing reduces -- example (a b : Nat) : a + b = b + a := rfl -- ✓ Correct: use the lemma, or a decision procedure example (a b : Nat) : a + b = b + a := Nat.add_comm a b example (a b : Nat) : a + b = b + a := by omega ``` ### Mistake 2: Confusing similar-looking expressions ``` -- These look the same but aren't definitionally equal! -- example (xs : List Nat) : xs ++ [] = xs := rfl -- ❌ Fails -- The definition of ++ recurses on the first list -- so xs ++ [] doesn't simplify without knowing xs example (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: ``` -- Nat.add recurses on its SECOND argument: -- n + 0 = n -- n + (m+1) = (n + m) + 1 -- So a literal on the RIGHT can be consumed step by step: example (n : Nat) : n + 0 = n := rfl -- ✓ one step example (n : Nat) : n + 2 = n + 1 + 1 := rfl -- ✓ two steps -- But a variable on the RIGHT blocks everything: -- example (n : Nat) : 0 + n = n := rfl -- ❌ stuck immediately example (n : Nat) : 0 + n = n := Nat.zero_add n -- ✓ needs the theorem -- Same story for multiplication (also recursive on the right): example (n : Nat) : n * 0 = 0 := rfl -- ✓ -- example (n : Nat) : n * 1 = n := rfl -- ❌ reduces to 0 + n, stuck -- 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: ``` -- As a term (no 'by') - direct proof term example : 2 + 2 = 4 := rfl -- As a tactic (with 'by') - enters tactic mode first example : 2 + 2 = 4 := by rfl -- The tactic version gives better error messages when it fails -- It also allows you to add other tactics before it if needed example : 2 + 2 = 4 := by -- could add 'show 4 = 4' or other tactics here 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: ``` -- These are all equivalent example : 5 = 5 := rfl example : 5 = 5 := Eq.refl 5 example : 5 = 5 := @rfl Nat 5 -- Eq.refl has type: ∀ (a : α), a = a #check @Eq.refl -- {α : Sort u} → (a : α) → a = a -- Sometimes you need @rfl to help type inference example : ([] : List Nat) = [] := @rfl (List Nat) [] ``` Deep Dive: Definitional vs Propositional Equality Lean has two notions of equality, and the difference decides whether `rfl` works: - **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_zero` exists as a named lemma, but its proof is literally `rfl` - `0 + n` and `n` are only **propositionally equal** — `Nat.zero_add` is 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 ``` -- Verify JSON-like value transformations def Config := List (String × Nat) def defaultConfig : Config := [("timeout", 30), ("retries", 3)] example : defaultConfig.length = 2 := rfl example : (defaultConfig.lookup "timeout") = some 30 := rfl ``` ### Testing parsing functions ``` -- Quick unit tests using rfl def parseDigit : Char → Option Nat | '0' => some 0 | '1' => some 1 | '2' => some 2 | _ => none example : parseDigit '1' = some 1 := rfl example : parseDigit 'a' = none := rfl ``` ### Closing goals after rewriting ``` -- rw already tries rfl for you, so usually you write just: example (a b : Nat) (h : a = b) : b = a := by rw [h] -- goal becomes b = b, and rw closes it example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by rw [h1, h2] -- goal becomes z = z, closed -- Adding an explicit rfl after these gives "No goals to be solved". -- You only need rfl when the rewrite leaves a goal that is definitionally -- true but not SYNTACTICALLY identical: example (n : Nat) (h : n = 3) : n + 0 = 3 := by rw [h] -- goal: 3 + 0 = 3, which rw's rfl also handles ``` ## When Computation Gets Expensive `rfl` runs 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. ``` -- Perfectly fast: the kernel special-cases Nat arithmetic example : 123456 + 789012 = 912468 := by rfl example : 2 ^ 64 = 18446744073709551616 := by rfl -- decide: for decidable propositions that are not equations example : (5 : Nat) < 10 ∧ (3 : Nat) ≠ 4 := by decide -- native_decide: compiles the check to machine code and trusts the result -- example : someHugeComputation = expected := by native_decide ``` ⚠ `native_decide` is a genuine escape hatch, not just a faster ` decide`. It adds `Lean.ofReduceBool` to 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 | Close the goal using computation and `rfl`. ``` example : (3 * 4) + 2 = 14 := by rfl ``` Verify that this function works correctly for the given input. ``` def greet (name : String) : String := "Hello, " ++ name ++ "!" example : greet "World" = "Hello, World!" := by rfl ``` Exercise 3: Why Does This Fail? This proof fails with `rfl`. Can you explain why and fix it with the right tactic? ``` -- This does NOT work: -- example (n : Nat) : 0 + n = n := rfl -- Why? Nat.add recurses on its second argument, so with n unknown -- there is nothing to reduce. -- Fix it, three ways: example (n : Nat) : 0 + n = n := by simp example (n : Nat) : 0 + n = n := Nat.zero_add n example (n : Nat) : 0 + n = n := by omega -- Meanwhile, its mirror image needs no tactic at all: example (n : Nat) : n + 0 = n := rfl ```