rfl - A deeper dive - Lean Notes

Source: Gemini 3.5 prompt: Lean4: Describe in detail the rfl tactic and prove five examples in increasing complexity. --- The `**rfl**` tactic (short for _reflexivity_) is a workhorse in Lean 4. It discharges equality goals of the form a = b whenever a and b can be simplified or evaluated to be under Lean's computation rules. ### 1. Mathematical and Logical Foundation In Dependent Type Theory—specifically the **Calculus of Inductive Constructions (CIC)** on which Lean 4 is built—equality comes in two distinct flavors: #### Definitional Equality ($\equiv$) Two expressions are **definitionally equal** if they evaluate to the exact same normal form under computational reduction rules: - $\beta$-reduction: $(\lambda x, e) \ v \rightsquigarrow e[x \mapsto v]$ (function application) - $\delta$-reduction:** replacing a defined constant/identifier with its definition - $\iota$-reduction:** pattern matching on inductive types (e.g., structural recursion on `Nat`) - $\zeta$-reduction expanding `let`-bindings - $\eta$-reduction: $(\lambda x, f\ x) \rightsquigarrow f$ when x is not free in f Definitional equality is a meta-theoretic judgments: if a $\equiv$ b, the Lean kernel treats them as inter-exchangeable without requiring a explicit proof object. #### Propositional Equality (=) **Propositional equality** is a type/proposition represented by the datatype `Eq a b` (written a = b). It has a single constructor: $\text{Eq.refl} : \forall \{A : \text{Sort } u\} (a : A), a = a$ Mathematically, `rfl` works by bridging the gap between definitional equality and propositional equality: > If two terms a and b are **definitionally equal** $(a \equiv b)$, then by replacing b with its definitionally equivalent term a, the goal becomes a = a. This immediately satisfies the constructor $\text{Eq.refl }$ a. ### 2. Lean 4 Implementation Details In Lean 4, `rfl` is not just a hardcoded kernel rule; it is extensible and tied to the type class mechanism as well as core macro expansions. ``` ┌─────────────────────────────┐ │ Goal State: a = b │ └──────────────┬──────────────┘ │ [ Macro / Syntax Expansion ] │ ▼ ┌─────────────────────────────┐ │ Is it standard Eq? │ └──────┬───────────────┬──────┘ Yes │ │ No ▼ ▼ ┌───────────────────┐ ┌───────────────────────────┐ │ Synthesize │ │ Search for `@[refl]` │ │ `Eq.refl a` proof │ │ theorem in environment │ └─────────┬─────────┘ └─────────────┬─────────────┘ │ │ └─────────────┬─────────────┘ │ ▼ ┌─────────────────────────────┐ │ Kernel DefEq Check (a ≡ b) │ └─────────────────────────────┘ ``` #### Syntax and Macro Expansion At the tactic level, invoking `rfl` expands to calling `evalRefl` or applying a generalized relation. 1. **Standard Propositional Equality (`Eq`):** When the target goal is a = b, `rfl` emits the kernel term `Eq.refl a`. The typechecker then attempts to unify a and b by checking if $a \equiv b.$ 2. **Generalized Reflexivity (`@[refl]`):** Lean 4 extends `rfl` to work for user-defined reflexive relations (like $\le, ~~\equiv, ~~or ~~\leftrightarrow$). When `rfl` encounters a goal like $a \sim b,$ it searches the environment for a theorem marked with the `@[refl]` attribute (such as `Nat.le_refl`). #### Kernel DefEq Checking & Reduction Hierarchy When Lean attempts to unify a and b, the elaborator and kernel perform reductions in stages: 1. **DefEq Unification:** It attempts to unfold constants ($\delta$-reduction), substitute variables ($\zeta$-reduction), and compute recursive pattern matches ($\iota$-reduction). 2. **Whnf (Weak Head Normal Form):** Lean reduces both sides to WHNF to inspect their outer constructors. 3. **Transparency Settings:** By default, tactics run under `default` transparency (unfolding non-irreducible definitions). The kernel checks the resulting proof term under strict kernel transparency. If a and b fail to reduce to identical syntactic forms, the `rfl` tactic throws a unification error: `type mismatch, term Eq.refl a has type a = a but is expected to have type a = b`. ### 3. Five Examples in Increasing Complexity #### Example 1: Syntactic Identity (Trivial) The simplest case where both sides of the equality are identical expressions without requiring any computation. ```lean theorem ex1 (x : Nat) : x = x := by rfl ``` - **Mechanism:** x and x are already syntactically identical. Lean directly applies `Eq.refl x`. #### Example 2: Definitional Unfolding ($\delta$-reduction) Equality where one side uses a defined constant or alias that needs to be expanded. ```lean def double (n : Nat) : Nat := n + n theorem ex2 (n : Nat) : double n = n + n := by rfl ``` - **Mechanism:** The identifier `double` is unfolded ($\delta$-reduction) to `fun n => n + n`. Then function application ($\beta$-reduction) yields `n + n = n + n`. #### Example 3: Computational Evaluation ($\iota$-reduction on Nat) Equality relying on recursive computation over structural definitions (like natural number addition). ```lean theorem ex3 : 2 + 3 = 5 := by rfl ``` - **Mechanism:** In Lean, `Nat` addition is defined recursively on the second argument: $n + 0 = n\\\\ n + (m + 1) = (n + m) + 1 $ Lean unfolds `2 + 3` into `Nat.succ (2 + 2)` $\rightarrow$ `Nat.succ (Nat.succ (2 + 1))` $\dots$ down to `5`. Both sides evaluate to `Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))`, matching definitionally. #### Example 4: Higher-Order Functions ($\beta$, $\zeta$, and $\eta$ Reductions) Equality involving anonymous functions, `let`-bindings, and tuple projections. ```lean theorem ex4 (f : Nat → Nat) : (let g := fun x => f (x + 1); g 4) = f 5 := by rfl ``` - **Mechanism:** 1. $\zeta$-reduction expands the `let g := ...` binding. 2. The target becomes `(fun x => f (x + 1)) 4 = f 5`. 3. $\beta$-reduction substitutes `4` for `x`: `f (4 + 1) = f 5`. 4. $\iota$-reduction simplifies `4 + 1` to `5`, yielding `f 5 = f 5`. #### Example 5: Type-Level Computation (Dependent Types & Decidable Props) Equality involving type-level evaluation, structures, and proofs embedded inside values. ```lean -- A proof that a boolean statement is true via Decidable computation theorem ex5 : (if 10 < 20 then "yes" else "no") = "yes" := by rfl ``` - **Mechanism:** 1. The condition `10 < 20` is evaluated using the `Decidable (10 < 20)` instance (`Decidable.isTrue ...`). 2. The `if ... then ... else ...` construct evaluates its branch based on the synthesized decidability proof object. 3. The expression reduces to `"yes" = "yes"` entirely at compile-time/type-checking time.