State of first-class first-order tactics in Lean 3/4

Stream: general

[Karl Palmskog]

For first-order solving, Isabelle and HOL4 have Metis, HOL Light has Meson, and Coq has firstorder and sauto. What is the closest Lean analogue currently and is it known how it performs on some benchmark? (This would be interesting to know since the work on sauto will be presented at IJCAR next week).

[Simon Hudon]

As far as I know, by {[smt] eblast} is the only thing we have related to first order automation.

[Simon Hudon]

@Seul Baek has two PRs to write bindings, one for Vampire and one for SPASS, but I don't think they're almost finished.

[Simon Hudon]

@Jesse Michael Han, anything to add?

[Karl Palmskog]

so eblast calls external solvers and does proof reconstruction? (If so, this is a bit different from Metis or firstorder, which runs inside the proof assistant like a "regular" tactic.)

[Simon Hudon]

eblast is not a binding. It is implemented as part of Lean using smt reasoning style

[Jesse Michael Han]

Karl Palmskog said:

so eblast calls external solvers and does proof reconstruction? (If so, this is a bit different from Metis or firstorder, which runs inside the proof assistant like a "regular" tactic.)

this description more closely describes Seul's Vampire bindings

eblast performs e-matching (heuristic instantiation) and congruence closure in a loop

there was a super tactic for superposition reasoning, but iirc it's not being maintained

[Patrick Massot]

The paper on sauto focuses on the orthogonal complement of mathlib (intuitionistic computer science) so I wouldn't be surprised if we have nothing like that.

[Karl Palmskog]

sauto was evaluated on (problems from) CompCert, which uses classical logic. It had about 17% success rate, which is lower than for the general Coq library benchmark, but still pretty high I think.

[Gabriel Ebner]

Jesse Michael Han said:

there was a super tactic for superposition reasoning, but iirc it's not being maintained

Yes, here is the original one: https://github.com/leanprover/super And here is a recent rewrite: https://github.com/gebner/super2/
Here is talk about it from the Matryoshka 2018 workshop: https://gebner.org/pdfs/2018-06-27_super.pdf
super kind of works but its main problem is that it's slow. It uses the built-in unification of Lean, and while this works great in many cases, you quickly run into corner cases with horrific performance or obscure bugs. The other issue is that the Lean 3 API hasn't exposed the primitives (such as temporary metavariables) intended for this kind of application (this has improved a bit in the community edition though).