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:

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:

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:

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:

example (α β : Type) (e : α ≃ β) (x : α) :
  β := e x

To relate expressions, use the properties of the equivalence:

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:

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:

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:

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.