# 2.19 Local Context Management

The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof. Most Lean proofs are won or lost by keeping this context small enough to read and rich enough to solve the current goal.

## Problem

You want to control which assumptions are available, how they are named, and when they should be introduced, removed, or generalized.

A typical proof state looks like this:

```lean
P Q R : Prop
hPQ : P -> Q
hQR : Q -> R
hp : P
⊢ R
```

The lines above the turnstile are the local context. The line below the turnstile is the current goal.

## Solution

Introduce assumptions deliberately, name important facts, remove irrelevant hypotheses when they add noise, and generalize variables when a proof has become too specific.

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

Here the context grows by one useful fact:

```lean
hq : Q
```

The final step then has the exact input required by `hQR`.

## Introducing Context

The `intro` tactic moves assumptions from the goal into the local context.

```lean
theorem intro_context
    (P Q : Prop) :
    P -> Q -> P ∧ Q := by
  intro hp
  intro hq
  constructor
  · exact hp
  · exact hq
```

After the introductions, the context contains:

```lean
hp : P
hq : Q
⊢ P ∧ Q
```

You can introduce several assumptions at once:

```lean
theorem intro_context_short
    (P Q : Prop) :
    P -> Q -> P ∧ Q := by
  intro hp hq
  exact ⟨hp, hq⟩
```

Use the short form when the assumptions are simple. Use separate lines when you want the proof state to be easier to inspect.

## Naming Introduced Assumptions

Names should match their types.

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

The context becomes:

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

This reads directly. Avoid generic names when the context has more than one nontrivial hypothesis.

## Adding Local Facts with `have`

The command `have` adds a local theorem.

```lean
theorem have_context
    (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 is useful when an intermediate result has meaning, or when a proof becomes easier after naming it.

You can also prove a `have` by a nested tactic block.

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

## Replacing the Goal with `suffices`

The command `suffices` adds a local claim and asks you to prove it later.

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

This is useful when the final goal follows from a simpler intermediate statement.

## Clearing Unused Hypotheses

The `clear` tactic removes a hypothesis from the local context.

```lean
theorem clear_context
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P := by
  clear hq
  exact hp
```

After `clear hq`, the context is smaller:

```lean
hp : P
⊢ P
```

Clearing is mostly useful in large proofs where unused hypotheses obscure the relevant ones.

You cannot clear a variable that is used by another hypothesis or by the goal.

## Renaming Hypotheses

The `rename_i` tactic names automatically introduced variables.

```lean
theorem rename_context
    (P Q : Prop) :
    P ∧ Q -> Q ∧ P := by
  intro h
  cases h
  rename_i hp hq
  exact ⟨hq, hp⟩
```

After `cases h`, Lean may introduce unnamed or automatically named variables. `rename_i` lets you assign readable names.

A more explicit form avoids the need for `rename_i`:

```lean
theorem rename_avoided
    (P Q : Prop) :
    P ∧ Q -> Q ∧ P := by
  intro h
  rcases h with ⟨hp, hq⟩
  exact ⟨hq, hp⟩
```

Prefer explicit destructuring when it keeps the proof clear.

## Reverting Context Back into the Goal

The `revert` tactic moves a local variable or hypothesis back into the goal.

```lean
theorem revert_context
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  revert hp
  intro hp'
  exact hPQ hp'
```

Before `revert hp`:

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

After `revert hp`:

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

Then `intro hp'` reintroduces the assumption.

This example is artificial, but `revert` is useful before induction or when a proof needs a more general statement.

## Generalizing Values

Sometimes a proof is too specific because a term appears in the goal in a fixed form. The `generalize` tactic replaces a term by a fresh variable and records an equality.

```lean
theorem generalize_context
    (n : Nat) :
    n + 0 = n := by
  generalize h : n + 0 = m
  rw [Nat.add_zero] at h
  rw [← h]
```

This introduces:

```lean
m : Nat
h : n + 0 = m
```

Generalization should be used sparingly. It changes the shape of the proof state and may make the proof harder to read. It is most useful when preparing for induction or when isolating a repeated expression.

## Managing Context in Case Analysis

Case analysis replaces a compound hypothesis with the data carried by its constructor.

```lean
theorem cases_context
    (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
```

Each branch has its own local context:

```lean
hp : P
⊢ R
```

or:

```lean
hq : Q
⊢ R
```

Do not assume facts from one branch are available in another branch.

## Managing Context in Existentials

Unpacking an existential adds a witness and a proof about that witness.

```lean
theorem exists_context
    (P : Nat -> Prop)
    (h : ∃ n : Nat, P n) :
    ∃ m : Nat, P m := by
  rcases h with ⟨n, hn⟩
  use n
  exact hn
```

After `rcases`, the context contains:

```lean
n : Nat
hn : P n
```

The existential has been converted into ordinary local data.

## Avoiding Context Pollution

A context can become hard to read if every small fact receives a name. Name facts that will be reused or that explain the proof. Inline facts that are used once and are easy to read.

Readable:

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

Also readable:

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

Less useful:

```lean
theorem context_over_named
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  have h1 : P := hp
  have h2 : Q := hPQ h1
  have h3 : R := hQR h2
  exact h3
```

The extra names do not add meaning.

## Localizing Automation

Automation works better when the context contains only relevant facts.

```lean
theorem automation_context
    (P Q R : Prop)
    (hp : P)
    (hq : Q)
    (hR : R) :
    P ∧ R := by
  clear hq
  constructor
  · exact hp
  · exact hR
```

In larger proofs, clearing irrelevant facts can make automation faster and error messages clearer.

## Common Patterns

Introduce assumptions:

```lean
intro hp hq
```

Add a local fact:

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

State a sufficient intermediate goal:

```lean
suffices hq : Q from hQR hq
```

Remove unused context:

```lean
clear h
```

Rename generated names:

```lean
rename_i hp hq
```

Move a hypothesis back to the goal:

```lean
revert hp
```

Unpack compound context:

```lean
rcases h with ⟨x, hx⟩
```

## Common Pitfalls

Do not introduce all variables too early before induction if the induction hypothesis needs to remain general.

Do not clear a hypothesis that later automation needs.

Do not overuse `generalize`; it can hide the original expression that gave the proof its meaning.

Do not let automatically generated names remain in a proof that will be maintained.

Do not add intermediate facts whose names do not clarify the argument.

## Takeaway

The local context is the working memory of a Lean proof. Manage it deliberately. Introduce assumptions when needed, unpack compound hypotheses, name meaningful intermediate facts, clear noise in large proofs, and generalize only when the proof requires a broader statement.