# 2.17 Proof Structuring Patterns

A Lean proof should expose the shape of the argument. The goal is not merely to make the theorem compile. The goal is to make the proof local, stable, and readable when the surrounding file changes.

## Problem

You have a theorem that can be proved in several ways, but the proof becomes hard to read because assumptions, intermediate facts, and final construction steps are mixed together.

## Solution

Use a simple proof structure:

1. Introduce assumptions
2. Destructure compound hypotheses
3. Prove intermediate facts with `have`
4. Build the final goal
5. Use automation only where the intended step is clear

For example:

```lean
theorem structured_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  exact hr
```

This proof names each logical step. It is longer than necessary, but it is easy to inspect.

## Compact Version

The same theorem can be proved in one line:

```lean
theorem compact_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  exact hQR (hPQ hp)
```

This version is fine when the composition is obvious. Prefer the structured version when the intermediate terms carry mathematical meaning or when the proof is likely to grow.

## Introduce First

For theorems with implication or universal quantification, introduce the variables and assumptions before doing serious work.

```lean
theorem introduce_first
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ
  intro hQR
  intro hp
  exact hQR (hPQ hp)
```

A shorter form is also common:

```lean
theorem introduce_first_short
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ hQR hp
  exact hQR (hPQ hp)
```

Use one name per logical object. Avoid names such as `h`, `h1`, and `h2` when the proof is longer than a few lines.

## Destructure Early

If a hypothesis contains a conjunction or existential, unpack it near the beginning of the proof.

```lean
theorem destructure_early
    (P Q R : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R) :
    P ∧ R := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  exact ⟨hp, hr⟩
```

This makes the available facts explicit:

```lean
hp : P
hq : Q
hr : R
```

The final construction then reads directly.

## Keep Case Branches Symmetric

When using a disjunction, each branch should have a similar shape.

```lean
theorem branch_structure
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    exact hPR hp
  | inr hq =>
    exact hQR hq
```

The branch names indicate what evidence is available. Each branch proves the same goal `R`.

For nested case splits, avoid excessive nesting when possible. Extract helper lemmas if the branches become long.

## Use `have` for Named Intermediate Facts

The `have` command adds a local theorem to the context.

```lean
theorem have_example
    (P Q R S : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hRS : R -> S)
    (hp : P) :
    S := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  have hs : S := hRS hr
  exact hs
```

A good `have` statement should have a type that explains why it exists. If the type is obscure, the proof will be obscure.

## Use Anonymous `have` Sparingly

Lean allows unnamed intermediate facts:

```lean
theorem anonymous_have
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  have : Q := hPQ hp
  exact hQR this
```

This is acceptable when there is only one unnamed fact in scope. In longer proofs, named facts are safer.

## Use `suffices` to State the Missing Step

The `suffices` command changes the proof into a named subgoal that is enough to prove the target.

```lean
theorem suffices_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  suffices hq : Q from hQR hq
  exact hPQ hp
```

This reads as: it is enough to prove `Q`, because `Q` implies `R`.

Use `suffices` when the intermediate claim is conceptually prior to the final conclusion.

## Use `show` to Clarify the Current Goal

The `show` command states what the current goal should be.

```lean
theorem show_example
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · show P
    exact hp
  · show Q
    exact hq
```

This is useful when the goal has been simplified or rewritten and is no longer visually obvious.

## Separate Proof Search from Proof Shape

Automation is useful, but it should not hide the main argument.

```lean
theorem automation_local
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · exact hp
  · exact hq
```

This proof is better than:

```lean
theorem automation_too_much
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  aesop
```

The `aesop` version is shorter, but it hides the introduction rule for conjunction. Use broad automation when the logical structure is routine or irrelevant to the section.

## Structure Rewriting Proofs

For equality proofs, prefer a `calc` block when the chain matters.

```lean
theorem calc_structure
    (a b c d : Nat)
    (hAB : a = b)
    (hBC : b = c)
    (hCD : c = d) :
    a = d := by
  calc
    a = b := hAB
    _ = c := hBC
    _ = d := hCD
```

Use `rw` when the rewrite is local and obvious.

```lean
theorem rw_structure
    (a b : Nat)
    (h : a = b) :
    a + 1 = b + 1 := by
  rw [h]
```

## Use Helper Lemmas

If a proof repeats the same local pattern, extract a lemma.

```lean
theorem imp_trans
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R) :
    P -> R := by
  intro hp
  exact hQR (hPQ hp)
```

Then use it:

```lean
theorem helper_lemma_example
    (P Q R S : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hRS : R -> S)
    (hp : P) :
    S := by
  exact hRS (imp_trans P Q R hPQ hQR hp)
```

The helper lemma gives a reusable name to a common reasoning step.

## Prefer Stable Proofs

A proof is stable if small changes to definitions do not break unrelated parts.

Stable proofs usually:

* name important intermediate facts
* avoid relying on fragile context order
* keep automation local
* use explicit rewrite rules
* avoid unnecessary unfolding

For example:

```lean
theorem stable_rewrite
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  simp
```

This says exactly which equality is used, then lets `simp` handle the standard arithmetic cleanup.

## Common Patterns

Use this skeleton for implication-heavy proofs:

```lean
theorem skeleton
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ hQR hp
  have hq : Q := hPQ hp
  exact hQR hq
```

Use this skeleton for conjunction-heavy proofs:

```lean
theorem conjunction_skeleton
    (P Q R : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R) :
    P ∧ R := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  exact ⟨hp, hr⟩
```

Use this skeleton for disjunction-heavy proofs:

```lean
theorem disjunction_skeleton
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    exact hPR hp
  | inr hq =>
    exact hQR hq
```

## Common Pitfalls

Do not compress a proof before it is understood. First write the explicit proof, then shorten only the parts that remain obvious.

Do not leave important intermediate claims unnamed. If a fact has mathematical meaning, give it a name.

Do not use broad automation to hide the connective being introduced or eliminated in a beginner proof.

Do not destructure hypotheses far away from where they are introduced unless delaying the destructuring improves readability.

Do not let branch proofs drift into different styles unless the cases are genuinely different.

## Takeaway

Proof structure is part of the proof. Introduce assumptions first, unpack compound data early, name important intermediate facts, and build the final goal explicitly. Use compact terms and automation only where they preserve the shape of the argument.