# 4.14 Dependent Rewriting and Transport

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

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

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

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

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

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

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

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