# 1.20 Holes and Goals

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.

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

Lean shows a goal:

```text
⊢ 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.

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

Lean shows:

```text
P : Prop
h : P
⊢ P
```

This tells you that `h` can solve the goal.

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

## Named Holes

You can name holes for reuse.

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

Lean introduces a goal named `?x`:

```text
?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.

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

Check the goal, then fill it:

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

For proofs:

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

Lean shows:

```text
⊢ P -> Q -> P ∧ Q
```

Introduce assumptions:

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

Now the goal is:

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

Fill it:

```lean
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.

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

Lean produces two goals:

```text
⊢ 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.

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

Better:

```lean
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:

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

Goal:

```text
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:

```lean
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.

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

Lean shows two goals:

```text
⊢ P
⊢ Q
```

Each must be solved.

```lean
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.

```lean
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:

```lean
def badDef : Nat :=
  _
```

Goal:

```text
⊢ Nat
```

Example:

```lean
theorem badThm : True := by
  _
```

Goal:

```text
⊢ 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:

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

Inspect:

```text
⊢ P -> Q -> P
```

Introduce:

```lean
  intro hp hq
```

Inspect:

```text
hp : P
hq : Q
⊢ P
```

Finish:

```lean
  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.