# 4.17 Rewriting in Structures and Records

# 4.17 Rewriting in Structures and Records

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:

```lean
structure Point where
  x : Nat
  y : Nat
```

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

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

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

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

Using it:

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

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

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

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

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

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

or more compactly when simp lemmas are available:

```lean
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.