4.18 Rewriting of Functions and Extensionality

Equality between functions requires a different treatment than equality between values. In Lean, two functions are equal when they produce equal outputs for all inputs. This principle is formalized by function extensionality.

Function extensionality

The core lemma is:

funext : (∀ x, f x = g x) → f = g

It reduces function equality to pointwise equality. To prove f = g, introduce an arbitrary argument and prove f x = g x.

example (f g : Nat -> Nat)
  (h : ∀ x, f x = g x) :
  f = g := by
  funext x
  exact h x

The tactic funext performs this transformation automatically.

Rewriting functions

Direct rewriting between functions rarely works because functions are opaque until applied. Instead, rewrite after applying the function or after reducing equality to pointwise form.

example (f : Nat -> Nat) (a b : Nat)
  (h : a = b) :
  f a = f b := by
  rw [h]

Here rewriting succeeds because the functions are applied.

For equality between functions:

example (a b : Nat) (h : a = b) :
  (fun x => x + a) = (fun x => x + b) := by
  funext x
  rw [h]

The binder is opened, exposing the occurrence of a.

Higher-order rewriting

When functions take functions as arguments, rewriting proceeds similarly by isolating the application point:

example (F : (Nat -> Nat) -> Nat)
  (f g : Nat -> Nat)
  (h : ∀ x, f x = g x) :
  F f = F g := by
  -- requires equality of functions
  have hf : f = g := by
    funext x
    exact h x
  rw [hf]

First establish equality of functions, then rewrite.

Composition and rewriting

Function composition often appears in rewriting:

example (f g : Nat -> Nat) (a b : Nat)
  (h : a = b) :
  (f ∘ g) a = (f ∘ g) b := by
  rw [h]

After expansion, this reduces to f (g a) = f (g b).

When functions are nested, congruence applies:

example (f g : Nat -> Nat)
  (h : f = g) (x : Nat) :
  f x = g x := by
  rw [h]

Rewriting with dependent functions

For dependent functions (x : α) -> β x, extensionality still applies, but rewriting may affect types:

example (f g : (n : Nat) -> Nat)
  (h : ∀ n, f n = g n) :
  f = g := by
  funext n
  exact h n

Once reduced to pointwise equality, standard rewriting applies.

Interaction with simp

simp can use extensionality implicitly in some contexts, but explicit use of funext is often clearer. After reducing to pointwise equality, simp can normalize expressions:

example (a : Nat) :
  (fun x => x + a + 0) = (fun x => x + a) := by
  funext x
  simp

Practical guidance

• Reduce function equality to pointwise equality using funext.
• Rewrite after applying functions or after introducing arguments.
• Use congruence when functions are nested inside larger expressions.
• Keep function bodies simple to enable rewriting and simplification.
• Combine funext with simp for normalization.

Summary

Function equality is extensional. Rewriting proceeds by exposing arguments, applying equalities pointwise, and then reconstructing the function. This pattern is essential whenever functions appear as first-class values in proofs.