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.