Skip to content

1.20 Holes and Goals

Lean development is driven by goals.

lean proof-assistant type-theory functional-programming

Lean development is driven by goals. A goal is the type of the term that Lean expects you to produce. A hole is a placeholder for a missing term. Together, they provide an interactive way to construct definitions and proofs incrementally.

Problem

You want to write incomplete code, inspect what Lean expects at each step, and refine it until the program or proof is complete.

Solution

Use _ to create a hole. Lean reports the expected type and the local context.

def addOne (n : Nat) : Nat :=
  _

Lean shows a goal:

⊢ Nat

This means the hole must be filled with a term of type Nat.

Inspecting Context

In proofs, holes reveal both the goal and available assumptions.

theorem hole_example (P : Prop) (h : P) : P := by
  _

Lean shows:

P : Prop
h : P
⊢ P

This tells you that h can solve the goal.

theorem hole_example (P : Prop) (h : P) : P := by
  exact h

Named Holes

You can name holes for reuse.

def pairSame (n : Nat) : Nat × Nat :=
  (?x, ?x)

Lean introduces a goal named ?x:

?x : Nat

You must supply a value for ?x. Once filled, both occurrences are replaced.

Incremental Construction

Start with a hole, then refine step by step.

def double (n : Nat) : Nat :=
  _

Check the goal, then fill it:

def double (n : Nat) : Nat :=
  n + n

For proofs:

theorem and_intro (P Q : Prop) : P -> Q -> P ∧ Q := by
  _

Lean shows:

⊢ P -> Q -> P ∧ Q

Introduce assumptions:

theorem and_intro (P Q : Prop) : P -> Q -> P ∧ Q := by
  intro hp hq
  _

Now the goal is:

hp : P
hq : Q
⊢ P ∧ Q

Fill it:

theorem and_intro (P Q : Prop) : P -> Q -> P ∧ Q := by
  intro hp hq
  exact And.intro hp hq

Using Holes in Terms

Holes also work in term mode.

def addTwo (n : Nat) : Nat :=
  (n + _) + _

Lean produces two goals:

⊢ Nat
⊢ Nat

Each hole must be filled with a term of type Nat.

This is useful for building expressions piece by piece.

Holes and Tactics

Inside tactic mode, _ creates a goal but does not provide structure. Prefer tactic commands when you know the next step.

theorem example (P : Prop) (h : P) : P := by
  _

Better:

theorem example (P : Prop) (h : P) : P := by
  exact h

Use holes when exploring, not as a final style.

Goal Inspection

Lean continuously shows:

  • the local context
  • the current goal

Example:

theorem chain (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R := by
  intro hp
  _

Goal:

P Q R : Prop
hpq : P -> Q
hqr : Q -> R
hp : P
⊢ R

From this, you can plan:

  • get Q using hpq hp
  • then get R using hqr

Complete:

theorem chain (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R := by
  intro hp
  exact hqr (hpq hp)

Multiple Goals

Some tactics produce multiple goals.

theorem and_intro2 (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor

Lean shows two goals:

⊢ P
⊢ Q

Each must be solved.

theorem and_intro2 (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq

Goal Order

Goals are solved in order. Lean focuses on one goal at a time.

You can structure proofs to keep goals small and clear. Avoid leaving many unsolved goals open at once.

Debugging with Holes

When a proof fails, replace part of it with a hole.

theorem debug_example (P : Prop) (h : P) : P := by
  _

Inspect the goal, then rebuild the proof.

This isolates the problem and avoids guessing.

Holes in Definitions vs Proofs

In definitions:

  • holes must produce data

In proofs:

  • holes must produce proofs

Example:

def badDef : Nat :=
  _

Goal:

⊢ Nat

Example:

theorem badThm : True := by
  _

Goal:

⊢ True

The mechanism is the same, but the interpretation differs.

Common Pitfalls

If a hole remains, Lean reports an incomplete definition.

If a hole appears in compiled code, the file does not typecheck.

If many holes appear, focus on one and fill it before proceeding.

If the goal is unclear, simplify it using tactics like intro, simp, or cases.

If the context is large, look for the minimal data needed to solve the goal.

Recipe: Develop with Holes

Start with the type:

theorem ex (P Q : Prop) : P -> Q -> P := by
  _

Inspect:

⊢ P -> Q -> P

Introduce:

  intro hp hq

Inspect:

hp : P
hq : Q
⊢ P

Finish:

  exact hp

This process scales to larger proofs.

Takeaway

Holes expose goals. Goals describe exactly what Lean expects. By iteratively inspecting goals and filling holes, you can construct definitions and proofs with precise guidance. This interactive loop replaces guesswork with structured development.