Skip to content

4.17 Rewriting in Structures and Records

Structures package multiple fields into a single value.

lean proof-assistant type-theory functional-programming

Structures package multiple fields into a single value. Rewriting with them requires attention to projections, constructors, and extensionality. In Lean, most equalities between structures reduce to equalities between their fields.

Projection-based rewriting

Given a structure:

structure Point where
  x : Nat
  y : Nat

and a hypothesis h : p = q, rewriting propagates through projections:

example (p q : Point) (h : p = q) :
  p.x = q.x := by
  rw [h]

The same holds for any field. Congruence handles the projection automatically.

Constructor-based goals

When the goal is equality of structures, a direct rw is often insufficient. Instead, reduce the goal to field-wise equalities:

example (p q : Point)
  (hx : p.x = q.x) (hy : p.y = q.y) :
  p = q := by
  cases p
  cases q
  simp at hx hy
  simp [hx, hy]

A more systematic approach uses extensionality.

Extensionality lemmas

Extensionality states that two structures are equal if all corresponding fields are equal. Many structures have an ext lemma:

#check Point.ext
-- Point.ext : p.x = q.x -> p.y = q.y -> p = q

Using it:

example (p q : Point)
  (hx : p.x = q.x) (hy : p.y = q.y) :
  p = q := by
  apply Point.ext
  · exact hx
  · exact hy

The tactic ext automates this:

example (p q : Point)
  (hx : p.x = q.x) (hy : p.y = q.y) :
  p = q := by
  ext
  · exact hx
  · exact hy

This reduces the goal to field equalities.

Rewriting fields

When working with structures, it is common to rewrite fields independently:

example (p : Point) :
  { x := p.x + 0, y := p.y } = p := by
  ext
  · simp
  · rfl

Each field is handled separately. This aligns with the canonical forms enforced by simp.

Updating structures

Lean supports record update syntax:

example (p : Point) :
  { p with x := p.x } = p := by
  ext
  · rfl
  · rfl

Rewriting inside updates follows the same pattern: reduce to fields, then apply rewriting or simplification.

Nested structures

For nested structures, extensionality composes:

structure Box where
  pt : Point

example (b₁ b₂ : Box)
  (h : b₁.pt = b₂.pt) :
  b₁ = b₂ := by
  cases b₁
  cases b₂
  simp [h]

Alternatively, use ext twice if extensionality lemmas are available.

Interaction with simp

Many projection and update lemmas are tagged for simplification. This allows simp to normalize structures:

example (p : Point) :
  { x := p.x, y := p.y } = p := by
  ext <;> rfl

or more compactly when simp lemmas are available:

example (p : Point) :
  { p with } = p := by
  rfl

(depending on definitions and transparency).

Practical guidance

  • Use projection rewriting (rw [h]) for accessing fields.
  • Use ext to reduce structure equality to field equalities.
  • Normalize fields with simp before closing goals.
  • Prefer field-wise reasoning over whole-structure rewriting.
  • Keep structures shallow when frequent rewriting is required.

Summary

Rewriting with structures decomposes into rewriting their fields. Extensionality provides the bridge from field equalities to structure equality. By working at the level of projections and using ext, you maintain control and clarity in proofs involving records.