# 1.23 Interactive Development Workflow

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:

```lean id="w4q5is"
theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  _
```

Lean shows the goal:

```text id="fgpf40"
P Q : Prop
⊢ P ∧ Q -> Q ∧ P
```

Introduce the hypothesis:

```lean id="m3yp1l"
theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  _
```

Now the goal becomes:

```text id="z2x9cg"
P Q : Prop
h : P ∧ Q
⊢ Q ∧ P
```

Construct the conjunction:

```lean id="i24j49"
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:

```lean id="k1hwd2"
def addTwo (n : Nat) : Nat :=
  _
```

The goal is:

```text id="bcy0ri"
n : Nat
⊢ Nat
```

Fill it:

```lean id="h5tls8"
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.

```lean id="xrvuls"
#check And.intro
#check And.left
#check And.right
```

Typical output:

```text id="tuk7al"
And.intro : P -> Q -> P ∧ Q
And.left : P ∧ Q -> P
And.right : P ∧ Q -> Q
```

Then use it deliberately:

```lean id="bqx2gq"
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.

```lean id="q9t99a"
def normalizeName (s : String) : String :=
  s.trim.toLower

#eval normalizeName "  LEAN  "
```

Expected output:

```text id="jnr04i"
"lean"
```

This confirms behavior before the function is used elsewhere.

## Keep Examples Small

Small examples help isolate mistakes.

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

#eval double 0
#eval double 7
```

Expected output:

```text id="k0rnf6"
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.

```lean id="ukogns"
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.

```lean id="zsp9k1"
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:

```lean id="jt7wfe"
#check Nat.add_zero
```

Then write:

```lean id="6y6c4h"
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.

```lean id="q49oxu"
import Std
```

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

```lean id="tvvd2n"
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.

```lean id="olggl0"
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.

```lean id="pk1itz"
namespace Cookbook

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

theorem inc_zero : inc 0 = 1 := by
  rfl

end Cookbook
```

Use qualified names from outside:

```lean id="a8urky"
#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:

```sh id="vkd8po"
lake build
```

and inside Lean files:

```lean id="m9dbba"
#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.

```lean id="ovzjwp"
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.