Using finishing tactics inside aesop

Stream: mathlib4

[Bhavik Mehta]

Here's my example:

import Aesop
import Mathlib.Tactic.Linarith

example {a b : Nat} : a < b → a ≤ b := by
  intro h
  aesop (add unsafe 1% linarith)

I expected this to succeed, since linarith closes the goal, and I was hoping that this could be a nice pattern to use in general (use aesop to make some logical steps, then linarith to close what's left). Why does this fail? And more generally, how could I have figured out myself why this fails?

[Alex J. Best]

seems you can do

import Aesop
import Mathlib.Tactic.Linarith

open Lean Elab Tactic
def myLin : TacticM Unit := do
  evalTactic $ ← `(tactic| linarith)
set_option trace.aesop true
example {a b : Nat} : a < b → a ≤ b := by
  intro h
  aesop (add tactic unsafe myLin)

I guess https://github.com/JLimperg/aesop/issues/45 is what you are hoping for

[Bhavik Mehta]

That makes sense, thanks!

[Bhavik Mehta]

I can answer my two questions from earlier - it fails because I used the syntax wrongly, and I could have figured this out using the trace.aesop option.

[Bhavik Mehta]

But what did my (add unsafe 1% linarith) actually do, and should it have given an error?

[Bhavik Mehta]

And I agree that having some nicer syntax for this would be nice, but the linked issue does describe why a general solution is more tricky than it appears

[Shreyas Srinivas]

So when I use linarith as you have done (minus the 1%) directly instead of myLin in Alex's solution, the following error is thrown:

aesop: linarith was expected to be a tactic, i.e. to have one of these types:
  TacticM Unit
  SimpleRuleTac
  RuleTac
However, it has type
  Lean.ParserDescr

[Shreyas Srinivas]

Bhavik Mehta said:

But what did my (add unsafe 1% linarith) actually do, and should it have given an error?

I am responding to this message.

[Alex J. Best]

Bhavik Mehta said:

But what did my (add unsafe 1% linarith) actually do, and should it have given an error?

I think it tells aesop to use the statement named linarith (which does exist) as a rule, which is almost certainly junk, but not clearly wrong for type reasons

[Jannis Limperg]

What Alex says. Extending the rule grammar so that you can give tactics directly (as well as (add norm simp [<- foo, bar]) and (add safe apply foo x y z)) is fairly high up on the todo list, but I need to figure out how to integrate this nicely with the rest of the grammar.

[Timo Carlin-Burns]

Is unsafe 1% a reasonable configuration for an expensive finishing tactic like linarith? There is a sense in which it is vacuously safe because it never produces subgoals at all so can never produce unprovable ones..

[Timo Carlin-Burns]

I suppose part of the problem with marking it safe would be that it gets tried on every single goal, even the ones that aren't inequalities

[Jannis Limperg]

I have no strong intuition about this, so we'd have to try it. Perhaps a separate arith rule set where linarith is safe could make sense, so you'd be able to use it only when the goal actually needs arithmetic. (I have some ideas for a tighter, more performant integration of linarith and aesop, but it's entirely vapourware so far.)