Skip to content

1.23 Interactive Development Workflow

Lean development is interactive.

lean proof-assistant type-theory functional-programming

Lean development is interactive. You usually do not write a complete proof or definition in one pass. You write a statement, inspect the goal, add a small step, inspect again, and continue until the file checks. This workflow is central to productive Lean use.

Problem

You want a reliable workflow for building definitions and proofs without guessing what Lean expects.

Solution

Work inside a Lake project, keep the editor goal view open, and develop one checked step at a time.

A typical proof starts with a statement and a hole:

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

Lean shows the goal:

P Q : Prop
⊢ P ∧ Q -> Q ∧ P

Introduce the hypothesis:

theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  _

Now the goal becomes:

P Q : Prop
h : P ∧ Q
⊢ Q ∧ P

Construct the conjunction:

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

The Basic Loop

The usual loop is:

  1. Write the expected type.
  2. Insert a hole.
  3. Read the goal.
  4. Apply one small step.
  5. Repeat.

For definitions:

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

The goal is:

n : Nat
⊢ Nat

Fill it:

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

For proofs, the same method applies. The only difference is that the expected type is a proposition.

Use #check Before Guessing

When using a function, theorem, or tactic input, inspect its type.

#check And.intro
#check And.left
#check And.right

Typical output:

And.intro : P -> Q -> P ∧ Q
And.left : P ∧ Q -> P
And.right : P ∧ Q -> Q

Then use it deliberately:

theorem and_swap_term (P Q : Prop) : P ∧ Q -> Q ∧ P :=
  fun h => And.intro h.right h.left

Use #eval for Computation

For executable definitions, evaluate small examples near the definition.

def normalizeName (s : String) : String :=
  s.trim.toLower

#eval normalizeName "  LEAN  "

Expected output:

"lean"

This confirms behavior before the function is used elsewhere.

Keep Examples Small

Small examples help isolate mistakes.

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

#eval double 0
#eval double 7

Expected output:

0
14

Avoid debugging a large theorem and a large definition at the same time. Confirm the computational part first, then prove properties about it.

Build Proofs by Naming Steps

Use have to name intermediate facts.

theorem chain (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 style makes the proof inspectable. If the proof fails, the failing line is usually clear.

Replace Automation with Explicit Steps

If simp, aesop, or another automated tactic fails, reduce the proof to explicit steps.

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

If the automation does not do what you expect, inspect the theorem you need:

#check Nat.add_zero

Then write:

theorem add_zero_example_rw (n : Nat) : n + 0 = n := by
  rw [Nat.add_zero]

Explicit proofs are often better while learning. Automation can be reintroduced after the structure is clear.

Keep Imports Local and Minimal

Start with the smallest imports that support the file.

import Std

For mathlib projects, avoid importing everything in every file unless you need it.

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

Smaller imports make build failures and name origins easier to diagnose.

Use Sections for Local Context

A section lets you share variables across related declarations.

section

variable (P Q R : Prop)

theorem imp_refl : P -> P := by
  intro h
  exact h

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

end

After the section closes, variables are generalized into parameters of the declarations.

Use Namespaces for Organization

Namespaces keep names stable and prevent collisions.

namespace Cookbook

def inc (n : Nat) : Nat :=
  n + 1

theorem inc_zero : inc 0 = 1 := by
  rfl

end Cookbook

Use qualified names from outside:

#check Cookbook.inc
#check Cookbook.inc_zero

Check Often

Lean rewards frequent checking. A good rhythm is to keep every file compiling after each small change.

Useful commands:

lake build

and inside Lean files:

#check name
#eval expression

The earlier an error appears, the smaller the search space.

Minimize Before Refactoring

Before changing a large proof, isolate the failing part.

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  constructor
  · exact h.right
  · exact h.left

Once the example works, move the pattern back into the larger proof.

Common Pitfalls

If you write too much before checking, errors become harder to localize.

If you rely on transitive imports, later edits may break unrelated files.

If you overuse automation early, you may not understand why the proof succeeds or fails.

If you leave holes in committed code, the project will not compile.

If you ignore goal state, you will guess instead of using Lean’s feedback.

Takeaway

The Lean workflow is incremental: state the target, inspect the goal, make one precise move, and repeat. #check, #eval, holes, local examples, and frequent builds turn Lean development into a controlled feedback loop.