# 4.16 Rewriting with Equivalences

# 4.16 Rewriting with Equivalences

Equalities are often too strict. In many developments you work with *equivalences* rather than literal equality. In Lean, these appear as logical equivalence `↔`, isomorphisms `≃`, or other structure-preserving relations. Rewriting with them requires conversion to equality or use of specialized lemmas.

## Logical equivalence `↔`

For propositions, `P ↔ Q` states that `P` and `Q` are interchangeable. You cannot directly use `rw` with `↔`. Instead, you extract directions:

```lean id="k9j2rm"
example (P Q : Prop) (h : P ↔ Q) :
  P -> Q := by
  intro hp
  exact h.mp hp
```

The projection `.mp` gives `P -> Q`, and `.mpr` gives `Q -> P`.

In goals, you can use `simp` with equivalences when appropriate:

```lean id="6q4c3x"
example (P Q : Prop) (h : P ↔ Q) :
  P = Q := by
  -- not definitional equality, but can be reasoned via iff
  admit
```

In practice, you avoid converting `↔` to `=` and instead reason directly with implications.

## Rewriting propositions

When the goal is itself a proposition, `simp` can rewrite using equivalences:

```lean id="t5m8df"
example (P Q : Prop) (h : P ↔ Q) :
  (P ∧ True) ↔ (Q ∧ True) := by
  simp [h]
```

Here `simp` uses `h` to replace `P` with `Q` inside a larger proposition.

## Type equivalences `≃`

For types, equivalences are expressed with structures such as `α ≃ β`. These contain forward and backward functions along with proofs of inverse behavior. To rewrite with them, apply the forward map:

```lean id="r3c8wz"
example (α β : Type) (e : α ≃ β) (x : α) :
  β := e x
```

To relate expressions, use the properties of the equivalence:

```lean id="w0f7yx"
example (α β : Type) (e : α ≃ β) (x : α) :
  e.symm (e x) = x :=
  e.left_inv x
```

Rewriting with `≃` typically involves applying `e`, `e.symm`, or their inverse laws rather than `rw`.

## Bridging equivalence and equality

Some equivalences induce equalities in specific contexts. For example, extensionality principles convert pointwise equivalence into equality:

```lean id="z4a9pk"
example (f g : Nat -> Nat)
  (h : ∀ x, f x = g x) :
  f = g := by
  funext x
  exact h x
```

This allows subsequent rewriting with `rw` on functions.

## Using `simp` with equivalences

Many equivalence lemmas are tagged for simplification. For example, logical identities:

```lean id="o6c2js"
example (P : Prop) :
  (P ∧ True) ↔ P := by
  simp
```

`simp` knows how to eliminate `True` and normalize the proposition.

You can extend this with custom equivalences:

```lean id="m7q1xb"
example (P Q : Prop) (h : P ↔ Q) :
  (¬ P) ↔ (¬ Q) := by
  simp [h]
```

The simplifier propagates the equivalence through logical structure.

## Practical guidance

* Use `.mp` and `.mpr` for directional reasoning with `↔`.
* Use `simp [h]` to propagate equivalences through propositions.
* Use `funext` to convert pointwise equality into function equality.
* Use equivalence maps (`e`, `e.symm`) for type-level transformations.
* Avoid forcing equivalences into equalities unless required.

## Summary

Equivalences generalize equality. They support rewriting at the level of logic and structure rather than syntax. By combining directional reasoning, simplification, and extensionality, you can integrate equivalences into standard rewriting workflows without losing precision.