4.14 Dependent Rewriting and Transport

When types depend on values, rewriting affects both terms and their types. In Lean, this is handled by transport: moving a term across an equality in an indexed family. Ordinary rw works when the dependency is shallow; deeper dependencies require explicit alignment of indices or use of transport-oriented combinators.

Consider a dependent predicate P : Nat -> Prop. Given h : a = b and Ha : P a, you can obtain P b by transporting along h:

example (a b : Nat) (h : a = b)
  (P : Nat -> Prop) (Ha : P a) :
  P b := by
  rw [← h]
  exact Ha

The rewrite changes the goal from P b to P a, which matches the hypothesis. Choosing the correct direction is essential; transport is directional.

For data, the same principle applies. With f : Nat -> Nat:

example (a b : Nat) (h : a = b) :
  f a = f b := by
  exact congrArg f h

Here congrArg performs transport through a non-dependent context. In dependent contexts, Lean uses a more general mechanism based on substitution in types.

A canonical transport operator is Eq.rec (also known as Eq.recOn). It has the shape:

-- Eq.rec : (motive : α → Sort u) → motive a → a = b → motive b

You rarely write it explicitly, but it explains how Lean moves terms across equalities. The rw tactic invokes this mechanism internally when needed.

Dependent pattern matching often exposes transport implicitly:

example (a b : Nat) (h : a = b)
  (P : Nat -> Prop) :
  P a -> P b := by
  intro Ha
  cases h
  exact Ha

The step cases h replaces b by a everywhere, including in types. This is transport specialized to equality.

Transport becomes more visible with indexed types. Suppose you have a vector type indexed by length:

-- conceptual example
structure Vec (α : Type) (n : Nat) where
  data : List α

If you know h : n = m, then a value of type Vec α n can be viewed as a value of type Vec α m via transport. In practice, you either rewrite the index or use a helper lemma that performs the conversion.

Rewriting under dependencies can fail when indices are not aligned. A typical pattern is to rewrite the goal so that indices match a hypothesis:

example (a b : Nat) (h : a = b)
  (P : Nat -> Prop) (Hb : P b) :
  P a := by
  rw [h] at Hb
  exact Hb

Here the hypothesis is rewritten instead of the goal. This often avoids complex transport in the goal.

For functions returning dependent types, extensionality may be required before rewriting:

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

If the dependency is deeper, introduce arguments to expose the structure.

A practical workflow for dependent rewriting:

1. Identify where the dependency occurs (in the goal or in a hypothesis).
2. Choose the direction that aligns indices with available data.
3. Rewrite the goal or the hypothesis to match.
4. Apply the desired lemma or finish by reflexivity.

Avoid mixing multiple dependent rewrites in a single step. Break them into small, verifiable transformations.

In summary, dependent rewriting generalizes ordinary rewriting to indexed families. Transport is the underlying mechanism. By controlling direction and location, you can align types and terms so that proofs remain straightforward.