# 1.25 Minimal Working Examples

A minimal working example is the smallest complete Lean fragment that demonstrates a definition, theorem, error, or technique. It should compile by itself inside a project, use only the imports it needs, and contain no unrelated code. Minimal examples are essential for learning, debugging, documentation, and reporting issues.

## Problem

You want to isolate a Lean idea in a short file that another person can run and understand immediately.

## Solution

Start with the smallest import set, write one or two declarations, and include a check or evaluation command.

```lean id="vpq6dm"
def double (n : Nat) : Nat :=
  n + n

#eval double 21
```

Expected output:

```text id="in3a5p"
42
```

This example is complete. It defines one function and shows one observable result.

## Minimal Proof Example

A proof example should include only the statement and the proof.

```lean id="q6tpaf"
theorem id_prop (P : Prop) : P -> P := by
  intro h
  exact h
```

This theorem needs no imports. It is minimal because it uses only core logical features.

A slightly richer example:

```lean id="xdq071"
theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left
```

This example demonstrates implication, conjunction, introduction, and field access on a conjunction proof.

## Minimal Import Example

If an example requires a library, include the import.

```lean id="r7j0dz"
import Std

#eval Std.HashMap.emptyWithCapacity
```

For mathlib examples, prefer narrow imports when you know them.

```lean id="j937no"
import Mathlib.Data.Nat.Basic

theorem add_zero_example (n : Nat) : n + 0 = n := by
  simp
```

A minimal example should not import a large library unless the behavior being demonstrated depends on it.

## Minimal Structure Example

```lean id="khk85x"
structure Point where
  x : Nat
  y : Nat
deriving Repr

def p : Point :=
  { x := 3, y := 4 }

#eval p.x + p.y
```

Expected output:

```text id="gu8tfg"
7
```

This example shows structure declaration, construction, projection, and evaluation.

## Minimal Inductive Example

```lean id="9jlhal"
inductive Color where
  | red
  | green
  | blue
deriving Repr, DecidableEq

def isRed : Color -> Bool
| Color.red => true
| _ => false

#eval isRed Color.red
#eval isRed Color.blue
```

Expected output:

```text id="0bwvhi"
true
false
```

This demonstrates constructors, pattern matching, and derived instances.

## Minimal Rewriting Example

```lean id="xecj61"
theorem rewrite_example (a b : Nat) (h : a = b) :
    a + 1 = b + 1 := by
  rw [h]
```

The example contains the needed equality as a hypothesis. Nothing else is required.

## Minimal Debugging Example

When reporting an error, remove everything not needed to reproduce it.

Bad example:

```lean id="pcf8tz"
import Mathlib

namespace LargeProject

-- hundreds of unrelated declarations

theorem broken (n : Nat) : n = n + 0 := by
  rfl

end LargeProject
```

Better example:

```lean id="pkurey"
theorem broken (n : Nat) : n = n + 0 := by
  rfl
```

This isolates the problem: `rfl` cannot prove the statement because `n` and `n + 0` are not definitionally equal.

A fixed version:

```lean id="oslsaz"
theorem fixed (n : Nat) : n = n + 0 := by
  simp
```

## Minimal Project Example

For examples involving imports or executables, include the project structure.

```text id="cx72sa"
hello/
├── lakefile.lean
├── lean-toolchain
├── Hello/
│   └── Basic.lean
└── Main.lean
```

`Hello/Basic.lean`:

```lean id="a23nqn"
namespace Hello

def message : String :=
  "hello"

end Hello
```

`Main.lean`:

```lean id="vumzx8"
import Hello.Basic

def main : IO Unit := do
  IO.println Hello.message
```

Run:

```sh id="qgm7cr"
lake exe hello
```

Expected output:

```text id="39ps98"
hello
```

This is minimal for demonstrating a Lake executable with a local module.

## What to Remove

When minimizing an example, remove:

| Remove               | Keep                                        |
| -------------------- | ------------------------------------------- |
| unrelated imports    | imports needed for the failing name         |
| unrelated namespaces | namespace only if it affects resolution     |
| unused variables     | variables used in the statement or proof    |
| long theorem chains  | the first theorem that reproduces the issue |
| automation noise     | the tactic that demonstrates the behavior   |

The goal is to preserve the behavior while reducing the context.

## What to Keep

Keep enough information for another person or tool to reproduce the result:

* Lean version, when version-sensitive
* required imports
* complete declaration
* exact error or expected output
* project context, if module resolution matters

For toolchain-sensitive issues, include the contents of `lean-toolchain`.

```text id="l67rm8"
leanprover/lean4:v4.12.0
```

## Recipe: Minimize a Failed Proof

Start with the failing theorem.

Replace the proof with a hole.

```lean id="bkx8qe"
theorem target (n : Nat) : n = n + 0 := by
  _
```

Inspect the goal.

Try the failing tactic.

```lean id="ks0ceg"
theorem target (n : Nat) : n = n + 0 := by
  rfl
```

If it still fails without surrounding code, you have a minimal example.

If it succeeds, restore only the nearest dependency until the failure returns.

## Recipe: Create a Teaching Example

A teaching example should demonstrate one idea.

For `rw`:

```lean id="q15p4z"
theorem rw_teaching (a b : Nat) (h : a = b) :
    a + a = b + b := by
  rw [h]
```

For `constructor`:

```lean id="f4wz38"
theorem constructor_teaching (P Q : Prop) (hp : P) (hq : Q) :
    P ∧ Q := by
  constructor
  · exact hp
  · exact hq
```

For `cases`:

```lean id="fgo1s9"
theorem cases_teaching (P Q : Prop) :
    P ∨ Q -> Q ∨ P := by
  intro h
  cases h with
  | inl hp =>
      right
      exact hp
  | inr hq =>
      left
      exact hq
```

Each example introduces one tactic in a clear setting.

## Common Pitfalls

If the example imports too much, the real dependency may be hidden.

If the example uses project-local names, include their definitions.

If the example depends on notation, include the notation declaration or use the underlying name.

If the example uses automation, make sure the imports explain why the automation works.

If the example is too small and no longer reproduces the issue, restore the last removed dependency.

## Takeaway

A minimal working example is a complete, small, reproducible Lean fragment. It is the main unit for debugging, teaching, and communication. Good examples keep only the declarations, imports, and context needed to demonstrate one behavior.