# 2.18 Naming Conventions

Names in Lean carry meaning. They determine how easily a proof can be read, refactored, and extended. Good naming makes the structure of the argument visible without inspecting every term.

## Problem

You want names that reflect the role of each hypothesis and intermediate result, instead of relying on generic placeholders like `h`, `h1`, `h2`.

## Principles

Use names that encode:

* the proposition or structure being described
* the direction of implication
* the relationship between objects

Prefer short but meaningful identifiers over long descriptive phrases.

## Naming Hypotheses

For implications, include both source and target.

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

The name `hPQ` indicates a map from `P` to `Q`. This avoids confusion in longer chains.

Bad:

```lean
(h1 : P -> Q) (h2 : Q -> R)
```

Good:

```lean
(hPQ : P -> Q) (hQR : Q -> R)
```

## Naming Proofs of Propositions

Use the prefix `h` for hypotheses, followed by the proposition or role.

```lean
hp  : P
hq  : Q
hnp : ¬ P
hpq : P ∧ Q
```

For conjunctions:

```lean
rcases hpq with ⟨hp, hq⟩
```

The names match the components.

## Naming Equalities

Use names that describe the relation.

```lean
hAB : a = b
hBC : b = c
```

Then:

```lean
rw [hAB, hBC]
```

reads naturally as a chain.

For properties:

```lean
hzero : n = 0
hsucc : n = k + 1
```

Avoid ambiguous names like `h1`, which do not indicate what is being rewritten.

## Naming Existential Witnesses

For existentials, use a base name for the witness and a related name for its property.

```lean
rcases h with ⟨n, hn⟩
```

For multiple properties:

```lean
rcases h with ⟨n, hn₁, hn₂⟩
```

Or more descriptive:

```lean
rcases h with ⟨n, hn_eq, hn_bound⟩
```

The suffix indicates the meaning of each proof.

## Naming in Case Analysis

Name each branch variable to reflect its origin.

```lean
cases h with
| inl hp =>
  ...
| inr hq =>
  ...
```

For natural numbers:

```lean
cases n with
| zero =>
  ...
| succ k =>
  ...
```

The name `k` indicates the predecessor.

## Naming Intermediate Results

Use `have` with meaningful names.

```lean
have hq : Q := hPQ hp
have hr : R := hQR hq
```

The name should reflect the type. Avoid:

```lean
have h1 : Q := ...
```

unless the context is extremely small.

## Naming Functions and Predicates

Use uppercase letters for propositions and predicates:

```lean
P Q R : Prop
P : α -> Prop
```

Use lowercase for values:

```lean
x y z : α
n m k : Nat
```

For functions:

```lean
f g : α -> β
```

When a function has a role, encode it:

```lean
next : Nat -> Nat
pred : Nat -> Nat
```

## Naming with Indices

When several similar objects appear, use indexed names.

```lean
h₁ h₂ h₃
```

or:

```lean
hPQ₁ hPQ₂
```

Unicode subscripts are often clearer than numeric suffixes.

```lean
hp₁ hp₂
```

is preferable to:

```lean
hp1 hp2
```

## Naming in Chains

For equality chains, maintain consistent naming.

```lean
hAB : a = b
hBC : b = c
hCD : c = d
```

This makes both `rw` and `calc` readable.

```lean
calc
  a = b := hAB
  _ = c := hBC
  _ = d := hCD
```

## Naming Avoids Errors

Good naming prevents mistakes.

Bad:

```lean
rw [h1, h2]
```

You must inspect `h1` and `h2` to know what they do.

Good:

```lean
rw [hAB, hBC]
```

The direction and meaning are visible.

## Naming and Refactoring

When proofs grow, names allow local changes.

```lean
have hq : Q := hPQ hp
```

If the proof of `Q` changes, only this line needs modification. The rest of the proof remains stable.

Unnamed intermediate expressions force you to rewrite multiple lines.

## Naming for Readability

Compare:

```lean
exact h3 (h2 (h1 hp))
```

versus:

```lean
have hq : Q := hPQ hp
have hr : R := hQR hq
exact hRS hr
```

The second version is longer but explains the argument.

## Naming for Patterns

Use consistent names across similar proofs.

For implication chains:

```lean
hPQ : P -> Q
hQR : Q -> R
```

For conjunction:

```lean
hp : P
hq : Q
```

For disjunction:

```lean
hp : P
hq : Q
```

For existentials:

```lean
x  : α
hx : P x
```

Consistency reduces cognitive load.

## Naming Exceptions

Short names are acceptable when:

* the proof is one or two lines
* the meaning is obvious from context
* the variable is used once

Example:

```lean
intro h
exact h
```

Here `h` is sufficient.

## Common Patterns

Implication:

```lean
hPQ : P -> Q
hp  : P
```

Conjunction:

```lean
hpq : P ∧ Q
⟨hp, hq⟩
```

Disjunction:

```lean
cases h with
| inl hp => ...
| inr hq => ...
```

Existential:

```lean
⟨x, hx⟩
```

Equality:

```lean
hAB : a = b
```

## Common Pitfalls

Do not reuse the same name for different meanings in the same scope.

Do not use names that conflict with Lean keywords or standard library identifiers.

Do not overuse single-letter names in long proofs.

Do not encode too much information into a name. `hPQ_to_R_via_trans` is harder to read than `hPR`.

Do not change naming conventions within the same file.

## Takeaway

Names encode structure. Use them to reflect the logical role of each term: source and target for implications, components for conjunctions, branches for disjunctions, witnesses for existentials, and chains for equalities. Consistent naming turns a proof into a readable argument.