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:

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.

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:

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.

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:

hp : P
hq : Q
⊢ P ∧ Q

You can introduce several assumptions at once:

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.

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:

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.

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.

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.

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.

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

After clear hq, the context is smaller:

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.

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:

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.

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

Before revert hp:

hp : P
hPQ : P -> Q
⊢ Q

After revert hp:

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.

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

This introduces:

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.

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:

hp : P
⊢ R

or:

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.

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:

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:

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

Also readable:

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:

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.

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:

intro hp hq

Add a local fact:

have hq : Q := hPQ hp

State a sufficient intermediate goal:

suffices hq : Q from hQR hq

Remove unused context:

clear h

Rename generated names:

rename_i hp hq

Move a hypothesis back to the goal:

revert hp

Unpack compound context:

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.