Aesop etc in the background

Stream: lean4

[Siddhartha Gadgil]

Thanks to the TryThis code and some code from the say tactic, using the Task framework here is a tool for running a tactic automatically in the background. By default this is aesop? but anything else can be used. The idea is to prove with a slightly different syntax: using by# in place of by with processes running in the background trying to complete the proof.

I am posting here for initial feedback but will PR to mathlib for detailed feedback soon. @Anand Rao Tadipatri is working on something related.

Easy proofs

async-1.gif

If a proof is reasonably simple aesop will complete it. The by# notation is a macro for the more flexible notation:
async-2.gif

Proofs needing help

The following is introduced to make sure Aesop cannot solve automatically:

opaque sillyN : Nat

axiom silly : sillyN = 2

In the next two illustrations once we have given enough hints, the proof is completed. Note that for even a complete proof we need a code-action to make by# into by to be valid Lean syntax.

async-3.gif

async-4.gif

Using other automation

In the next example we use apply? instead of aesop?. This is a little slower so does not finish within the builtin delay (50ms by default) but kicks in as we continue proving.

async-5.gif

Using tactics without "try this"

Both aesop? and apply? have a "Try this:" message which is intercepted and used. If a tactic is not such a search, then it is tried and the proof is completed when it is enough to finish. This is illustrated by using linarith.

async-6.gif

This also illustrates a limitation: we do not look through induction, cases, match etc. An easy workaround is to have a macro and manually enter this mode.

The source

The source is at https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanAide/Async.lean

[Patrick Massot]

The demos would be a lot easier to follow if you could switch off whatever is producing the grey text (assuming this is indeed completely unrelated to what you want to show us).

[Siddhartha Gadgil]

Sure. That is Github copilot in the background (and is unrelated). I will redo with it off.

[Matthew Ballard]

I wondered what that was :)

[Patrick Massot]

This is what I guessed. Thanks!

[Siddhartha Gadgil]

Here are the demos with copilot off to avoid the distracting grey stuff:

1. Easy proofs: short and full syntax
   async-1a.gif
   async-2a.gif

   
   

2. Proofs that cannot be fully automatic: with rewriting to standard notation even when the user gives the full proof.
   async-3a.gif
   async-4a.gif

   
   

3. Using apply: also illustrating continuing running in the background even after the waiting period.
   async-5a.gif

   

4. Using linarith instead of a search tactic: still tried after each step.
   async-6a.gif

   

[Siddhartha Gadgil]

PRed as #6176

One small piece of this is a "sorry tactic detector". Is there something builtin for this? I try to use a tactic to prove False and it is sorry if it succeeds.

def isSorry (tacticCode: TSyntax `tactic) : TermElabM Bool := do
  let goal ← mkFreshExprMVar (mkConst ``False)
  try
    let (goals, _) ← Elab.runTactic  goal.mvarId! tacticCode
    return goals.isEmpty
  catch _ =>
    return false

[Siddhartha Gadgil]

@Scott Morrison
I forgot that none of my examples illustrated the point that the main mode is tactics continuing to run in the background. If they finish successfully, the result is saved. A fresh elaboration with the same goal state and some stage triggers this.

The following gif illustrates this (by making delay 0).
async-7.gif

• When one runs by#, though the search is started there is no delay so it does not finish.
• When skip is run, the elaborator goes through the tactics again, and this time sees the completed proof and offers a code action (again there is no delay, but the proof was ready).

[Siddhartha Gadgil]

The idea is that the user keeps trying to prove. If aesop (or chosen automation) could finish at some earlier stage, or essentially instantly after the current stage, a code action is offered to finish the proof.

[Bolton Bailey]

Thanks to @Alex J. Best for directing me here from the other thread.

This tactic mode is very cool! I think my only complaint so far is that even when by# finds a "Try This", it still highlights the by# in red squiggly underline rather than blue squiggly underline:
Screenshot-2024-03-08-at-7.27.47AM.png

[Siddhartha Gadgil]

Thanks a lot for the feedback @Bolton Bailey and @Alex J. Best. I have now made a standalone repository LeanAideTools with minimized dependencies (only Aesop) that can hopefully be used:

• In a user repository which may or may not depend on Mathlib.
• While working in a branch on Mathlib.

I have incorporated the feedback that it seemed wrong to show an error when a proof was complete. So now a sorry is returned giving better behaviour I hope.

Here are the details of the modified setup:

Running tactics automatically

While proving results in tactic mode in Lean, proofs can often be completed by tactics like simp, exact?, aesop etc., but it is a nuisance to try this at each step. We provide a tactic mode where a list of tactics is run automatically in the background after each step.

If a proof can be completed, then:

• A hyperlink in the infoview and a code action is offered to replace the code by a valid proof.
• The sorry tactic is run to complete the proof, so the user sees a warning (this is to avoid showing an error, following a suggestion by Bolton Bailey).

To work with this mode, follow the below installation instructions, including adding import LeanAideTools to your file. You can enter the auto-tactic mode by:

• Beginning a tactic block with byy instead of by.
• At any stage, starting a sequence of tactics with doo.

The doo syntax is provided as, at present, the mode does not see within case, match, bullet points etc., so one has to use it to re-enter the auto-tactic mode in these cases.

The tactics that run by default are rfl, simp?, omega, aesop?, exact?. More tactics can be added as long as they are in scope. For example, in a Mathlib dependent project (or a branch of Mathlib) one may
want to add linarith and ring. One can add either a single tactic or multiple tactics as in the following.

#auto ring
#autos [ring, linarith]

Examples in action

Here are some examples illustrating the tactic mode.

Simple Example

In the following simple example, the result can be proved straight away. The syntax byy by itself is valid and tries to prove the goal.

lat1.gif

Checks after each tactic

In the following (rather contrived) example, the result cannot be proved automatically. However, once the tactic rw [silly] is entered the proof is completed and results are suggested.

lat2.gif

Background Running

The following shows that the tactics are running in the background. After the tactics to run are spawned, there is a configurable delay, 50 milliseconds by default, before control is returned to the user. The tactics continue running in the background till they finish after this delay.

Here the delay is set to 0. Hence after rw [silly] the proof is not automatically completed. Every time the interpreter is triggered we check whether the proof was found by the background processes. In this case, hitting enter triggered the interpreter which found that the proof was found in the background.

lat3.gif

Configuration: Adding tactics

The following illustrates adding tactics. Here simp [silly] is added. In the presence of this tactic the example can be proved straight away.

lat4.gif

Installation

Add the following or equivalent to your lakefile.lean to use the auto-tactic mode. The branch/tag v4.7.0 works with the corresponding version of Lean's toolchain. Replace it with the toolchain you use in your project. I will try to have a branch/tag for each toolchain starting with v4.7.0-rc2.

require LeanAideTools from git
  "https://github.com/siddhartha-gadgil/LeanAideTools.git" @ "v4.7.0"

For use with a Mathlib branch, add the dependency in the lakefile while working on the branch and remove it before the PR is merged.

To use the mode in a file, add import LeanAideTools along with your other imports.

Missing features?

There are two features that I hope to work on eventually:

• When a tactic like exact? finds a proof, the user gets a hyperlink and code-action to complete the proof with this tactic. But this tactic in turn gives a suggested proof with which it can be replaced. The two steps should ideally be replaced by just one.
• The tactic mode does not see within case, match, bullet points etc. This is a limitation of the current implementation. The doo syntax is provided to re-enter the auto-tactic mode in these cases, but ideally one should not have to do this.

Any comments, suggestions, or bug reports are welcome. Also contributions are welcome.

[Siddhartha Gadgil]

@Bolton Bailey Sorry I did not notice the review for the Mathlib PR. In any case I have now implemented a different approach as I mentioned above.

Do folks think it is worth porting this to the Mathlib PR, or would it make more sense to simply close the PR? If the mode turns out to be useful, a fresh PR can be made.

[Bolton Bailey]

Siddhartha Gadgil said:

• While working in a branch on Mathlib.

If this is a totally independent repo from mathlib, how can it be used from a branch of mathlib?

[Eric Rodriguez]

you can change the mathlib commit hash in the lakefile

[Siddhartha Gadgil]

I assumed one could just edit the lakefile of mathlib in a branch. After all mathlib has Aesop as a dependency.

[Siddhartha Gadgil]

Before the merger, the dependency should be removed

[Bolton Bailey]

Right, ok, that makes sense. Sorry to pour cold water, but I will probably not be using for mathlib it if it's going to require editing and reverting the lakefile on any branch I want to use it for. In my mind the key upside of this approach is that it takes a single keystroke to activate. I still think it's very cool and I'll try to use it for independent projects to test it out.

[Siddhartha Gadgil]

Thanks.
I assumed the single keystroke only applies if it is merged in mathlib and was pessimistic about this happening. Let me also experiment for some weeks and then make a fresh PR

[Bolton Bailey]

Yes, very sorry your PR hasn't gotten more traction, if it were up to me your PR would have been merged months ago, I don't actually think something as trivial as code review should block cool things like this from getting used faster but my understanding is that community reviews are supposed to help the process along.