Proof automation

Stream: lean4

[Jesse Slater]

I have just started with Lean, and I am wondering what tools are available for automatically finding proofs. I am coming from Isabelle, and as I understand it, lean currently has nothing as powerful as Blast or Sledgehammer. Is that true? Are there any similar type things? Are there plans for more powerful automation in the future?

[Kevin Buzzard]

Yes, there's nothing like Sledgehammer yet; people were basically put off from working on them I think, for years, because Lean 4 was always round the corner. Now it's here there is Aesop and there are plans for more automation but it's still very early days: Lean 4 is still running on nightly releases right now

[Henrik Böving]

Jesse Slater said:

I have just started with Lean, and I am wondering what tools are available for automatically finding proofs. I am coming from Isabelle, and as I understand it, lean currently has nothing as powerful as Blast or Sledgehammer. Is that true? Are there any similar type things? Are there plans for more powerful automation in the future?

Just by knowing a general description of blast in Isabelle andaesop (It's a library but pulled in as default in mathlib4) I would say aesop can come close to what blast can do. Lean 4's simp is supposed to be equivalent to your auto. We can do linear arithmetic with linartih like your arith, we are planning to port omega which is close to your presburger etc. For basic general proof search there is library_search but nothing as strong as sledgehammer although we do have foundations to integrate SAT solvers and Leo has told me he is very much interested in adding nice SMT support in the future so eventually we might end up with something in the direction of sledgehammer.

So in general we do have equivalents for some of Isabelle's stuff but in general the automation in Isabelle still far exceeds ours but we are planning to put work into that in the future.

[James Gallicchio]

(A lot of work has also gone into making metaprogramming nice, so if you wanted to help build better automation it’s not too hard to get into!)

[Henrik Böving]

While that's true our metaprogramming operates at a much lower level than Isabelle's eisbach, it's probably more comparable to writing an Isabelle extension in ML with a well designed API.

[Wojciech Nawrocki]

People are also actively working on a superposition prover duper. Afaik it is still very much work in progress, but it will hopefully serve to do what metis does in Isabelle.

[Jonathan Julian Huerta y Munive]

@Henrik Böving I am an Isabelle user too and I want to understand your comments a bit more. In Isabelle, simp is just rewriting with proven equations. While auto can be thought of as a combination of simp and blast (a first-order logic prover) that tackles all proof obligations. Generally, people recommend to only use auto to conclude a proof because of how hard it is to track what it did. If Lean's simp is equivalent to Isabelle's auto, I would take a similar careful approach. Does Lean have something equivalent to Isabelle's simp? i.e. something that just rewrites with proven equations?

[Mario Carneiro]

isabelle simp is like lean simp (it's a bit weaker because it doesn't have simpprocs), and isabelle auto is like lean aesop

[Jonathan Julian Huerta y Munive]

Thanks for the clarification @Mario Carneiro. When I toyed around with Lean, I needed a table of these tactics. For Isabelle, an incomplete one looks something like this. Can somebody share a link here with such a table?

prover	description	calls simplifier?	procedural	speed	goals
auto	blast + simplifier	yes	yes	+	all
safe	uses only safe rules	no	yes	++	all
blast	complete for FOL	no	no	+	first
fastforce	more aggressive than auto	yes	no	-	first
force	more aggressive than than fastforce	yes	no	--	first

[Mario Carneiro]

I don't think we have tactics that overlap in functionality enough such that a table like this would make sense

[Mario Carneiro]

for the most part tactics are intended to do different things, not just "more aggressive version of X"

[Mario Carneiro]

tauto is for FOL, aesop is a grab bag of stuff along the lines of auto, simp and rw are for rewriting with equalities, norm_num is for numeric calculations (this is covered by simp in isabelle I think), linarith is for linear arithmetic, omega is for presburger arithmetic and that covers most of the really big tactics

[Jonathan Julian Huerta y Munive]

Thanks! A reference with tactics and what they do is very useful. I really like Lean's library_search

[Mario Carneiro]

Lean 3 has https://leanprover-community.github.io/mathlib_docs/tactics.html; that page hasn't been ported to doc-gen4 yet but it is roughly the same for lean 4

[Henrik Böving]

Mario Carneiro said:

isabelle simp is like lean simp (it's a bit weaker because it doesn't have simpprocs), and isabelle auto is like lean aesop

Really? Leo explicitly told me to think of simp like auto.

[Mario Carneiro]

from what I know of isabelle simp, it acts almost exactly the same as lean simp

[Mario Carneiro]

you can probably use it in place of auto sometimes, but it's not really doing what auto does

[Mario Carneiro]

and given that aesop isn't in core it's probably the best replacement

[David Renshaw]

@Jonathan Julian Huerta y Munive what does "procedural" mean in that table?

[Jonathan Julian Huerta y Munive]

@David Renshaw good catch, it means that you can apply it in a proof, and if it fails, you can keep applying tactics after the resulting proof state. In contrast, if blast, force, or fastforce fail, they will keep trying to finish the proof indefinitely.

[Jonathan Julian Huerta y Munive]

Also, the descriptions are fuzzy and intended as rules of thumb. The auto tactic is not actually blast + simplifier, I think it also involves safe and does other things.

[Sebastian Ullrich]

We usually call such tactics "(non-)terminal"

[Jonathan Julian Huerta y Munive]

I like "non-terminal" better than "procedural". Although, it might encourage someone to use auto in the middle of proofs which is not recommended.

[Sebastian Ullrich]

Yes, it's the same for Aesop (and simp without only): not recommended for non-terminal use, but occasionally useful during exploration

[Chris Bailey]

Is there a trick to using library_search in Lean 4 other than importing it, or is it not intended for use yet? Most of the time I try to invoke it, I get ~100 seemingly random suggestions, like refine Lean.SyntaxNode.withArgs ?_ ?_ and refine Equiv.sigmaSubtypeFiberEquivSubtype.proof_4 B ?_ S ?_ then the tactic just closes the goal with sorryAx.

I'm using nightly-2023-01-04 and the master branch of mathlib.

[Kevin Buzzard]

This question should probably be in another stream! Short answer: library-search in lean 3 would fail but in lean 4 it produces many typically unhelpful suggestions instead. I just treat the gigantic outputs as a failure. If it works, it doesn't do this.

[Jeremy Salwen]

I have seen this behavior, but I have also seen cases where it outputs a mixture of irrelevant suggestions with more relevant ones sprinkled in. I will try to save an example when I see it next.

[Jeremy Salwen]

I have a very compelling example of #find failure that I wasted more time on than I'm willing to admit:

#find  (_ - (_- _)) = _ + _ - _

I was looking for tsub_tsub_assoc, but instead I got the following set of results:

1. Equiv.punitEquivPUnit.proof_2
2. Function.Embedding.punit.proof_1
3. PUnit.inf_eq
4. PUnit.unique.proof_
5. sub_sub_eq_add_sub
6. PUnit.instLinearOrderPUnit.proof_4
7. PUnit.hnot_eq
8. PUnit.booleanAlgebra.proof_7
9. PUnit.default_eq_unit
10. PUnit.subsingleton
11. PUnit.biheytingAlgebra.proof_10
12. PUnit.compl_eq
13. PUnit.sdiff_eq
14. PUnit.eq_punit
15.PUnit.min_eq
16. PUnit.sup_eq
17.Unit.ext
18. sub_sub_sub_eq
19. PUnit.max_eq
20. Equiv.punitEquivPUnit.proof_1

Of the 20 results returned, only #5 and #18 at all matched my query. And the result I was looking for (tsub_tsub_assoc) wasn't in the top 20 despite being an exact match.