# 4.18 Rewriting of Functions and Extensionality

# 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:

```lean id="2g3s9w"
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`.

```lean id="3p8k1m"
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.

```lean id="6u1r0c"
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:

```lean id="0l9d4v"
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:

```lean id="j2m5t8"
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:

```lean id="4t0q2s"
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:

```lean id="8x9n3k"
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:

```lean id="5k1p7d"
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:

```lean id="7v4l9q"
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.