aesop - Automated Proof Search

aesop is a proof search tactic from Mathlib. It explores small proof steps such as introductions, case splits, simplifications, and lemma applications to close goals automatically.

Basic Usage

Use aesop as a finishing tactic after you introduce variables or simplify the goal. It is most effective when the necessary facts are already in the local context.

1import Mathlib.Tactic
2
3example (P Q R : Prop) (hP : P) (hPQ : P -> Q) (hQR : Q -> R) : R := by
4  aesop
5
6example (P Q R : Prop) : (P -> Q) -> (Q -> R) -> P -> R := by
7  intro hPQ hQR hP
8  aesop
9
10example (P Q : Prop) (h : P \/ Q) (hp : P -> Q) : Q := by
11  aesop

When aesop Works Best

Think of aesop as a searcher for small logical steps. It performs best when a short chain of applications and simplifications can finish the goal.

• The goal is propositional and does not require heavy computation.
• The context already contains the lemmas or hypotheses you need.
• The remaining proof is a short chain of introductions and applications.

What aesop Tries

At a high level, aesop builds a search tree. It introduces hypotheses, splits cases, runs simplification, and applies lemmas it considers safe. If a branch fails, it backtracks and tries a different path until the goal is solved or the search budget runs out.

1import Mathlib.Tactic
2
3example (n : Nat) : n + 0 = n := by
4  aesop
5
6example (h : P /\ Q) : Q := by
7  aesop

Common Workflows

Finish After Setup

Open the goal with a few explicit steps, then let aesopclose the remaining details.

1import Mathlib.Tactic
2
3example (P Q R : Prop) : (P -> Q) -> (Q -> R) -> P -> R := by
4  intro hPQ hQR hP
5  aesop

Split and Solve

If you already know the main case split, do it yourself and letaesop finish each branch.

1import Mathlib.Tactic
2
3example (P Q R : Prop) (h : P \/ Q) (hP : P -> R) (hQ : Q -> R) : R := by
4  cases h with
5  | inl hp => aesop
6  | inr hq => aesop

Guiding the Search

If aesop does not solve the goal, simplify first, add the missing lemma to the context, or break the goal into smaller parts. The clearer the proof state, the easier the search.

1import Mathlib.Tactic
2
3example (n : Nat) (h : n = 3) : n + 1 = 4 := by
4  simp [h]
5  aesop

Registering aesop Rules

If you use a lemma frequently, register it so aesopcan apply it automatically.

1import Mathlib.Tactic
2
3def Even (n : Nat) : Prop := Exists fun k => n = 2 * k
4
5@[aesop]
6lemma even_zero : Even 0 := by
7  exact Exists.intro 0 (by simp)
8
9example : Even 0 := by
10  aesop

aesop? for Proof Scripts

Use aesop? when you want a concrete proof script. It runs the same search and prints a suggestion you can paste into your file.

1import Mathlib.Tactic
2
3example (P Q R : Prop) (hP : P) (hPQ : P -> Q) (hQR : Q -> R) : R := by
4  aesop?
5  -- The messages window shows a suggested tactic script.

1import Mathlib.Tactic
2
3example (P Q R : Prop) (hP : P) (hPQ : P → Q) (hQR : Q → R) : R := by
4  aesop