Where are the lean4 finishing tactics?

Stream: lean4

[Joey Eremondi]

Where are the "auto" tactics in lean4? Things like finish, tidy, etc that solve tedious but obvious goals by search, case splitting, simplifying, constructor trying, etc.

Are there things like Coq's auto, eauto, or crush in Lean4? I found this but I think it's for Lean3: https://brandonrozek.com/blog/leantactics/

[Timo Carlin-Burns]

aesop is capable of all those things. duper also is based on a promising design but looks undocumented/wip

[Joey Eremondi]

Ohhhh very cool! How much does it rely on marking things with the Aesop attribute? Are things marked simp automatically aesop?

[Timo Carlin-Burns]

Yep, Aesop automatically uses simp to normalize all terms at every step of its proof search

[Timo Carlin-Burns]

Looks like the rules that are included without explicit @[aesop] are in this file. If you're using mathlib though, hopefully eventually many things will already be marked @[aesop] for you. Right now that's only true in certain parts of the library, like category theory.

[Scott Morrison]

(In particular, mathlib3's tidy has been completely replaced by aesop: it is both faster and more capable.)

[Scott Morrison]

I would love to see someone "power up" aesop with induction and cases. I think a great rule would be "you are allowed to try induction, as long as in at least one branch simp makes progress".

[Scott Morrison]

There are many many lemmas where we use a few rounds of induction ... generalizing ..., with all branches solvable by simp_all. The requirement that simp_all makes progress ensures that we don't just induct inductively.

[Kyle Miller]

Scott Morrison said:

a great rule would be "you are allowed to try induction, as long as in at least one branch simp makes progress".

I wonder how this rule could be refined to make sure it doesn't go down the path of trying to prove a theorem by infinite ascent...

def f (n : Nat) : Nat := n + 1
@[simp] theorem f_zero : f 0 = 1 := rfl
@[simp] theorem f_succ (n : Nat) : f (n + 1) = f n + 1 := rfl

example (n : Nat) : n < f n := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp
    induction n with
    | zero => simp
    | succ n ih =>
      simp
      induction n with
      | zero => simp
      | succ n ih =>
        simp
        ...

[Scott Morrison]

Hmmm... good example. :-) I wonder if you required it to make use of new simp lemmas at each stage?

[Timo Carlin-Burns]

(I just came upon https://github.com/avigad/lean-auto/ which looks like a better documented frontend for duper)

[Jannis Limperg]

It's not. duper is a superposition prover implemented in native Lean. lean-auto seems to be a tactic that sends translated Lean terms to external automated theorem provers (based on superposition or SMT, I guess) and reconstructs the proofs returned by these, in a manner reminiscent of Isabelle's Sledgehammer. Also, neither of these projects have yet been announced as ready for serious use.

[Patrick Massot]

Jannis, auto doesn't have to call an external prover, it can use duper both for proof search and proof reconstruction. However you are right that it is a work in progress that is not at all ready for use.

[Jannis Limperg]

Wait but then auto wouldn't need to do the whole translation dance described in the README, no?

[Patrick Massot]

If I understand correctly, the translation dance is useful even for duper.

[Bolton Bailey]

Scott Morrison said:

I would love to see someone "power up" aesop with induction and cases. I think a great rule would be "you are allowed to try induction, as long as in at least one branch simp makes progress".

Is there a way currently to get aesop to apply induction at all? I know there are ways to get it to apply cases for types that you specify.

[Scott Morrison]

You can give arbitrary tactics to aesop, e.g.

attribute [aesop safe tactic (rule_sets [CategoryTheory])] Std.Tactic.Ext.extCore'

[Bolton Bailey]

Ok, but does that let me tell aesop "you are allowed to apply induction to lists"

[Bolton Bailey]

(lists specifically, rather than just feeding "induction'" to the tactic)

[Scott Morrison]

So write a list-specific induction tactic. It should only be a few lines.

[Bolton Bailey]

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

[Scott Morrison]

grep for the line of code I posted above in Mathlib, and see how it is done there.

[Scott Morrison]

You can't use the "user facing" syntactical tactics, you need to go one level deeper and provide a TacticM Unit.

[Bolton Bailey]

The problem with writing a list-specific induction tactic is that at that point, I expect I will have written more lines of code than it would take to just prove the lemma normally.

[Joey Eremondi]

Right but then it will be there for the next time you need it

[Jannis Limperg]

Patrick Massot said:

If I understand correctly, the translation dance is useful even for duper.

Ah, interesting. I vaguely remember similar results where Slegdehammer's HOL-to-FOL translation turned out to be better than running HOL-based ATPs directly. So a similar thing happening with duper wouldn't be crazy.