Aesop

Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic for Lean 4. It is broadly similar to Isabelle's auto. In essence, Aesop works like this:

• As with simp, you tag a (large) collection of definitions with the @[aesop] attribute, registering them as Aesop rules. Rules can be arbitrary tactics. We provide convenient ways to create common types of rules, e.g. rules which apply a lemma.
• Aesop takes these rules and tries to apply each of them to the initial goal. If a rule succeeds and generates subgoals, Aesop recursively applies the rules to these subgoals, building a search tree.
• The search tree is explored in a best-first manner. You can mark rules as more or less likely to be useful. Based on this information, Aesop prioritises the goals in the search tree, visiting more promising goals before less promising ones.
• Before any rules are applied to a goal, it is normalised, using a special (customisable) set of normalisation rules. An important built-in normalisation rule runs simp_all, so your @[simp] lemmas are taken into account by Aesop.
• Rules can be marked as safe to optimise Aesop's performance. A safe rule is applied eagerly and is never backtracked. For example, Aesop's built-in rules safely split a goal P ∧ Q into goals for P and Q. After this split, the original goal P ∧ Q is never revisited.
• Aesop provides a set of built-in rules which perform logical operations (e.g. case-split on hypotheses P ∨ Q) and some other straightforward deductions.
• Aesop uses indexing methods similar to those of simp and other Lean tactics. This means it should remain reasonably fast even with a large rule set.
• When called as aesop?, Aesop prints a tactic script that proves the goal, similar to simp?. This way you can avoid the performance penalty of running Aesop all the time. However, the script generation is currently not fully reliable, so you may have to adjust the generated script.

Aesop is suitable for two main use cases:

• General-purpose automation, where Aesop is used to dispatch 'trivial' goals. By registering enough lemmas as Aesop rules, you can turn Aesop into a much more powerful simp.
• Special-purpose automation, where specific Aesop rule sets are built to address a certain class of goals. Mathlib tactics such as measurability and continuity are implemented by Aesop.

I only occasionally update this README, so details may be out of date. If you have questions, please create an issue or ping me (Jannis Limperg) on the Lean Zulip. Pull requests are very welcome!

There's also a paper about Aesop which covers many of the topics discussed here, sometimes in more detail.

Building

With elan installed, lake build should suffice.

Adding Aesop to Your Project

To use Aesop in a Lean 4 project, first add this package as a dependency. In your lakefile.lean, add

require aesop from git "https://github.com/JLimperg/aesop"

You also need to make sure that your lean-toolchain file contains the same version of Lean 4 as Aesop's, and that your versions of Aesop's dependencies (currently only std4) match. We unfortunately can't support version ranges at the moment.

Now the following test file should compile:

import Aesop

example : α → α :=
  by aesop

Quickstart

To get you started, I'll explain Aesop's major concepts with a series of examples. A more thorough, reference-style discussion follows in the next section.

We first define our own version of lists (so as not to clash with the standard library) and an append function:

inductive MyList (α : Type _)
  | nil
  | cons (hd : α) (tl : MyList α)

namespace MyList

protected def append : (_ _ : MyList α) → MyList α
  | nil, ys => ys
  | cons x xs, ys => cons x (MyList.append xs ys)

instance : Append (MyList α) :=
  ⟨MyList.append⟩

We also tell simp to unfold applications of append:

@[simp]
theorem nil_append : nil ++ xs = xs := rfl

@[simp]
theorem cons_append : cons x xs ++ ys = cons x (xs ++ ys) := rfl

When Aesop first encounters a goal, it normalises it by running a customisable set of normalisation rules. One such normalisation rule effectively runs simp_all, so Aesop automatically takes simp lemmas into account.

Now we define the NonEmpty predicate on MyList:

@[aesop safe [constructors, cases]]
inductive NonEmpty : MyList α → Prop
  | cons : NonEmpty (cons x xs)

Here we see the first proper Aesop feature: we use the @[aesop] attribute to construct two Aesop rules related to the NonEmpty type. These rules are added to a global rule set. When Aesop searches for a proof, it systematically applies each available rule, then recursively searches for proofs of the subgoals generated by the rule, and so on, building a search tree. A goal is proved when Aesop applies a rule that generates no subgoals.

In general, rules can be arbitrary tactics. But since you probably don't want to write a tactic for every rule, the aesop attribute provides several rule builders which construct common sorts of rules. In our example, we construct:

• A constructors rule. This rule tries to apply each constructor of NonEmpty whenever a goal has target NonEmpty _.
• A cases rule. This rule searches for hypotheses h : NonEmpty _ and performs case analysis on them (like the cases tactic).

Both rules above are added as safe rules. When a safe rule succeeds on a goal encountered during the proof search, it is applied and the goal is never visited again. In other words, the search does not backtrack safe rules. We will later see unsafe rules, which can backtrack.

With these rules, we can prove a theorem about NonEmpty and append:

@[aesop unsafe 50% apply]
theorem nonEmpty_append₁ {xs : MyList α} ys :
    NonEmpty xs → NonEmpty (xs ++ ys) := by
  aesop

Aesop finds this proof in four steps:

• A built-in rule introduces the hypothesis h : NonEmpty xs. By default, Aesop's rule set contains a number of straightforward rules for handling the logical connectives →, ∧, ∨ and ¬ as well as the quantifiers ∀ and ∃ and some other basic types.
• The cases rule for NonEmpty performs case analysis on h.
• The simp rule cons_append, which we added earlier, unfolds the ++ operation.
• The constructor rule for NonEmpty applies NonEmpty.cons.

If you want to see how Aesop proves your goal (or why it doesn't prove your goal, or why it takes too long to prove your goal), you can enable tracing:

set_option trace.aesop true

This makes Aesop print out the steps it takes while searching for a proof. You can also look at the search tree Aesop constructed by enabling the trace.aesop.tree option. For more tracing options, type set_option trace.aesop and see what auto-completion suggests.

If, in the example above, you call aesop? instead, then Aesop prints a proof script. At time of writing, it looks like this:

intro a
obtain @⟨x, xs_1⟩ := a
simp_all only [cons_append]
apply MyList.NonEmpty.cons

With a bit of post-processing, you can use this script instead of the Aesop call. This way you avoid the performance penalty of making Aesop search for a proof over and over again. The proof script generation currently has some known bugs, but it produces usable scripts most of the time.

The @[aesop] attribute on nonEmpty_append₁ adds this lemma as an unsafe rule to the default rule set. For this rule we use the apply rule builder, which generates a rule that tries to apply nonEmpty_append₁ whenever the target is of the form NonEmpty (_ ++ _).

Unsafe rules are rules which can backtrack, so after they have been applied to a goal, Aesop may still try other rules to solve the same goal. This makes sense for nonEmpty_append₁: if we have a goal NonEmpty (xs ++ ys), we may prove it either by showing NonEmpty xs (i.e., by applying nonEmpty_append₁) or by showing NonEmpty ys. If nonEmpty_append₁ were registered as a safe rule, we would always choose NonEmpty xs and never investigate NonEmpty ys.

Each unsafe rule is annotated with a success probability, here 50%. This is a very rough estimate of how likely it is that the rule will to lead to a successful proof. It is used to prioritise goals: the initial goal starts with a priority of 100% and whenever we apply an unsafe rule, the priority of its subgoals is the priority of its parent goal multiplied with the success probability of the applied rule. So applying nonEmpty_append₁ repeatedly would give us goals with priority 50%, 25%, etc. Aesop always considers the highest-priority unsolved goal first, so it prefers proof attempts involving few and high-probability rules. Additionally, when Aesop has a choice between multiple unsafe rules, it prefers the one with the highest success probability. (Ties are broken arbitrarily but deterministically.)

After adding nonEmpty_append, Aesop can prove some consequences of this lemma:

example {α : Type u} {xs : MyList α} ys zs :
    NonEmpty xs → NonEmpty (xs ++ ys ++ zs) := by
  aesop

Next, we prove another simple theorem about NonEmpty:

theorem nil_not_nonEmpty (xs : MyList α) : xs = nil → ¬ NonEmpty xs := by
  aesop (add 10% cases MyList)

Here we use an add clause to add a rule which is only used in this specific Aesop call. The rule is an unsafe cases rule for MyList. (As you can see, you can leave out the unsafe keyword and specify only a success probability.) This rule is dangerous: when we apply it to a hypothesis xs : MyList α, we get x : α and ys : MyList α, so we can apply the cases rule again to ys, and so on. We therefore give this rule a very low success probability, to make sure that Aesop applies other rules if possible.

Here are some examples where Aesop's normalisation phase is particularly useful:

@[simp]
theorem append_nil {xs : MyList α} :
    xs ++ nil = xs := by
  induction xs <;> aesop

theorem append_assoc {xs ys zs : MyList α} :
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  induction xs <;> aesop

Since we previously added unfolding lemmas for append to the global simp set, Aesop can prove theorems about this function more or less by itself (though in fact simp_all would already suffice.) However, we still need to perform induction explicitly. This is a deliberate design choice: techniques for automating induction exist, but they are complex, somewhat slow and not entirely reliable, so we prefer to do it manually.

Many more examples can be found in the AesopTest folder of this repository. In particular, the file AesopTest/List.lean contains an Aesop-ified port of 200 basic list lemmas from the Lean 3 version of mathlib, and the file AesopTest/SeqCalcProver.lean shows how Aesop can help with the formalisation of a simple sequent calculus prover.

Reference

This section contains a systematic and fairly comprehensive account of how Aesop operates.

Rules

A rule is a tactic plus some associated metadata. Rules come in three flavours:

• Normalisation rules (keyword norm) must generate zero or one subgoal. (Zero means that the rule closed the goal). Each normalisation rule is associated with an integer penalty (default 1). Normalisation rules are applied in a fixpoint loop in order of penalty, lowest first. For rules with equal penalties, the order is unspecified. See below for details on the normalisation algorithm.

  Normalisation rules can also be simp lemmas. These are constructed with the simp builder. They are used by a special simp call during the normalisation process.

• Safe rules (keyword safe) are applied after normalisation but before any unsafe rules. When a safe rule is successfully applied to a goal, the goal becomes inactive, meaning no other rules are considered for it. Like normalisation rules, safe rules are associated with a penalty (default 1) which determines the order in which the rules are tried.

  Safe rules should be provability-preserving, meaning that if a goal is provable and we apply a safe rule to it, the generated subgoals should still be provable. This is a less precise notion than it may appear since what is provable depends on the entire Aesop rule set.

• Unsafe rules (keyword unsafe) are tried only if all available safe rules have failed on a goal. When an unsafe rule is applied to a goal, the goal is not marked as inactive, so other (unsafe) rules may be applied to it. These rule applications are considered independently until one of them proves the goal (or until we've exhausted all available rules and determine that the goal is not provable with the current rule set).

  Each unsafe rule has a success probability between 0% and 100%. These probabilities are used to determine the priority of a goal. The initial goal has priority 100% and whenever we apply an unsafe rule, the priorities of its subgoals are the priority of the rule's parent goal times the rule's success probability. Safe rules are treated as having 100% success probability.

Rules can also be multi-rules. These are rules which add multiple rule applications to a goal. For example, registering the constructors of the Or type will generate a multi-rule that, given a goal with target A ∨ B, generates one rule application with goal A and one with goal B. This is equivalent to registering one rule for each constructor, but multi-rules can be both slightly more efficient and slightly more natural.

Search Tree

Aesop's central data structure is a search tree. This tree alternates between two kinds of nodes:

• Goal nodes: these nodes store a goal, plus metadata relevant to the search. The parent and children of a goal node are rule application nodes. In particular, each goal node has a priority between 0% and 100%.
• Rule application ('rapp') nodes: these goals store a rule (plus metadata). The parent and children of a rapp node are goal nodes. When the search tree contains a rapp node with rule r, parent p and children c₁, ..., cₙ, this means that the tactic of rule r was applied to the goal of p, generating the subgoals of the cᵢ.

When a goal node has multiple child rapp nodes, we have a choice of how to solve the goals. This makes the tree an AND-OR tree: to prove a rapp, all its child goals must be proved; to prove a goal, any of its child rapps must be proved.

Search

We start with a search tree containing a single goal node. This node's goal is the goal which Aesop is supposed to solve. Then we perform the following steps in a loop, stopping if (a) the root goal has been proved; (b) the root goal becomes unprovable; or (c) one of Aesop's rule limits has been reached. (There are configurable limits on, e.g., the total number of rules applied or the search depth.)

• Pick the highest-priority active goal node G. Roughly speaking, a goal node is active if it is not proved and we haven't yet applied all possible rules to it.

• If the goal of G has not been normalised yet, normalise it. That means we run the following normalisation loop:

  • Run the normalisation rules with negative penalty (lowest penalty first). If any of these rules is successful, restart the normalisation loop with the goal produced by the rule.
  • Run simp on all hypotheses and the target, using the global simp set (i.e. lemmas tagged @[simp]) plus Aesop's simp rules.
  • Run the normalisation rules with positive penalty (lowest penalty first). If any of these rules is successful, restart the normalisation loop.

  The loop ends when all normalisation rules fail. It destructively updates the goal of G (and may prove it outright).

• If we haven't tried to apply the safe rules to the goal of G yet, try to apply each safe rule (lowest penalty first). As soon as a rule succeeds, add the corresponding rapp and child goals to the tree and mark G as inactive. The child goals receive the same priority as G.
• Otherwise there is at least one unsafe rule that hasn't been tried on G yet (or else G would have been inactive). Try the unsafe rule with the highest success probability and if it succeeds, add the corresponding rapp and child goals to the tree. The child goals receive the priority of G times the success probability of the applied rule.

A goal is unprovable if we have applied all possible rules to it and all resulting child rapps are unprovable. A rapp is unprovable if any of its subgoals is unprovable.

During the search, a goal or rapp can also become irrelevant. This means that we don't have to visit it again. Informally, goals and rapps are irrelevant if they are part of a branch of the search tree which has either successfully proved its goal already or which can never prove its goal. More formally:

• A goal is irrelevant if its parent rapp is unprovable. (This means that a sibling of the goal is already unprovable, in which case we know that the parent rapp will never be proved.)
• A rapp is irrelevant if its parent goal is proved. (This means that a sibling of the rapp is already proved, and we only need one proof.)
• A goal or rapp is irrelevant if any of its ancestors is irrelevant.

Rule Builders

A rule builder is a metaprogram that turns an expression into an Aesop rule. When you tag a declaration with the @[aesop] attribute, the builder is applied to the declared constant. When you use the add clause, as in `(add