# 2.24 Simplification and Automation

Lean provides automation to reduce routine proof steps. The goal is to remove mechanical transformations while preserving the logical structure of the argument. The main tool is `simp`, supported by targeted tactics such as `dsimp`, `simp_all`, and lightweight automation like `aesop`.

## Problem

Manual rewriting becomes repetitive:

```lean
rw [Nat.add_zero]
rw [Nat.zero_add]
rw [Nat.add_comm]
```

This obscures the intent. You want Lean to perform standard reductions automatically while keeping control over nontrivial steps.

## The `simp` Tactic

`simp` applies a collection of rewrite rules tagged as simplification lemmas.

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

Lean uses lemmas such as `Nat.add_zero` automatically.

`simp` reduces expressions to a normal form using:

* arithmetic identities
* logical simplifications
* definitional equalities

## Using `simp` with Hypotheses

`simp` can use local equalities.

```lean
theorem simp_with_hyp
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  simp [hAB]
```

The list `[hAB]` adds custom rewrite rules.

## Simplifying Hypotheses

```lean
theorem simp_at_hyp
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 0 = 5) :
    b = 5 := by
  simp [hAB] at ha
  exact ha
```

`simp` rewrites inside `ha`.

## Simplifying Everything

```lean
theorem simp_all_example
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 0 = 5) :
    b = 5 := by
  simp_all
```

`simp_all` simplifies the goal and all hypotheses using all available information.

Use it when the context is small and stable.

## Controlled Simplification

`simp` accepts explicit rewrite rules.

```lean
theorem simp_controlled (a b : Nat) :
    a + b = b + a := by
  simp [Nat.add_comm]
```

Without the explicit rule, `simp` may not use commutativity.

## Avoiding Over-Simplification

`simp` may change expressions more than expected.

```lean
theorem simp_caution (a : Nat) :
    (a + 0) + 0 = a := by
  simp
```

This works, but the intermediate structure disappears. If the structure matters, use `rw` instead.

## The `dsimp` Tactic

`dsimp` performs definitional simplification only.

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

theorem dsimp_example (n : Nat) :
    double n = n + n := by
  dsimp [double]
```

`dsimp` does not use general rewrite lemmas. It unfolds definitions.

Use it when you want predictable, minimal changes.

## The `simp?` Helper

Lean can suggest simplifications.

```lean
simp?
```

This prints a suggested `simp` call with the lemmas it used.

Useful for learning which lemmas are relevant.

## The `simp` Normal Form

`simp` aims to reduce expressions to a canonical form.

Examples:

```lean
n + 0 → n
0 + n → n
n = n → True
True ∧ P → P
```

Understanding this helps predict results.

## Combining `simp` with Other Tactics

Typical pattern:

```lean
theorem simp_then_apply
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  simp [hAB]
```

Or:

```lean
theorem simp_then_exact
    (a : Nat) :
    a + 0 = a := by
  simp
```

Or mixed:

```lean
theorem mixed_simp_rw
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  simp
```

## Conditional Simplification

`simp` can use implications and conditions.

```lean
theorem simp_conditional
    (P : Prop)
    (h : P) :
    P ∧ True := by
  simp [h]
```

Lean simplifies `True` automatically.

## Using `simp` for Logical Goals

```lean
theorem simp_logic
    (P : Prop) :
    P ∧ True -> P := by
  intro h
  simpa using h
```

`simpa` runs `simp` and finishes the goal.

## The `simpa` Shortcut

`simpa` combines `simp` with `exact`.

```lean
theorem simpa_example
    (n : Nat) :
    n + 0 = n := by
  simpa
```

Or with hypotheses:

```lean
theorem simpa_with_hyp
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  simpa [hAB]
```

## Lightweight Automation: `aesop`

`aesop` is a general-purpose automation tactic.

```lean
theorem aesop_example
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  aesop
```

It combines introduction, elimination, and search.

Use it when the structure is routine.

Avoid it when teaching or when proof structure matters.

## When to Use Automation

Use `simp` when:

* rewriting follows standard rules
* the goal should reduce to normal form
* manual rewriting is repetitive

Use `dsimp` when:

* only definitions should be unfolded

Use `simpa` when:

* a simplified expression matches the goal

Use `aesop` when:

* the proof is routine and structure is not important

## When to Avoid Automation

Avoid automation when:

* the proof teaches a concept
* the structure matters
* debugging is needed
* the context is large and unstable

In these cases, explicit steps are clearer.

## Debugging `simp`

If `simp` fails:

* add relevant lemmas explicitly
* check if the expression is in normal form
* try `simp?` to see suggestions
* use `rw` to guide the transformation

Example:

```lean
theorem simp_needs_help (a b : Nat)
    (hAB : a = b) :
    a + b = b + b := by
  simp [hAB]
```

Without `[hAB]`, `simp` does not know how to replace `a`.

## Common Patterns

Basic simplification:

```lean
simp
```

With hypotheses:

```lean
simp [h]
```

At a hypothesis:

```lean
simp at h
```

Everywhere:

```lean
simp_all
```

Shortcut:

```lean
simpa
```

Definition-only:

```lean
dsimp [f]
```

## Common Pitfalls

Do not rely on `simp` without understanding what it does.

Do not expect `simp` to apply nontrivial lemmas like commutativity unless explicitly provided.

Do not use `simp_all` in large contexts without checking side effects.

Do not replace meaningful proof steps with automation when clarity matters.

Do not assume `simp` will preserve expression structure.

## Takeaway

Simplification and automation reduce routine proof work. The main tool is `simp`, which applies standard rewrite rules to reach a canonical form. Use it to eliminate boilerplate, but keep control over key logical steps. Effective proofs combine explicit reasoning with targeted automation.