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.

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

#eval double 21

Expected output:

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.

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:

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.

import Std

#eval Std.HashMap.emptyWithCapacity

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

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

structure Point where
  x : Nat
  y : Nat
deriving Repr

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

#eval p.x + p.y

Expected output:

7

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

Minimal Inductive Example

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:

true
false

This demonstrates constructors, pattern matching, and derived instances.

Minimal Rewriting Example

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:

import Mathlib

namespace LargeProject

-- hundreds of unrelated declarations

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

end LargeProject

Better example:

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:

theorem fixed (n : Nat) : n = n + 0 := by
  simp

Minimal Project Example

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

hello/
├── lakefile.lean
├── lean-toolchain
├── Hello/
│   └── Basic.lean
└── Main.lean

Hello/Basic.lean:

namespace Hello

def message : String :=
  "hello"

end Hello

Main.lean:

import Hello.Basic

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

Run:

lake exe hello

Expected output:

hello

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

What to Remove

When minimizing an example, remove:

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.

leanprover/lean4:v4.12.0

Recipe: Minimize a Failed Proof

Start with the failing theorem.

Replace the proof with a hole.

theorem target (n : Nat) : n = n + 0 := by
  _

Inspect the goal.

Try the failing tactic.

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:

theorem rw_teaching (a b : Nat) (h : a = b) :
    a + a = b + b := by
  rw [h]

For constructor:

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

For cases:

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.