tactics support

Stream: general

[Jürgen Uhl]

I'm trying to formalize Hilbert's Geometry axioms and theorems using lean4.
I've seen the (two) projects in github with the same title (Hilbert/Euclid Geometry), but they are apparently not being worked on any more and do not really mimic Hilbert's proofs. Anyway...
Before that I tried Isabelle; got most of the first two axiom/theorem groups done. I switched to lean4, because I could not control memory consumption with Isabelle and it kept halting/crashing my complete system.
I got the first theorem proved in lean4, but compared to Isabelle it looks very lengthy and was really tedious. In Isabelle I could proof the theorem in two steps which were supported by the "try" and "blast" mechanisms, which suggests proofs/tactics solving (intermediate) goals. I already saw simp and aesop in lean4 which somehow correspond to Isabelle's simp and auto, and I know about "apply?", which I find produces just too much options to handle.
So I have two questions:

1. Are there similar techniques in lean4 to Isabelle's "try" or "blast" which attempt to apply a broad range of primitive tactics?
2. I have attached my current results with lean4. If someone could have a look at what I did and comment what could be improved/simplified/automated it would be of great help.
   I also attached the Isabelle results so far in case someone is interested.
   Hilbert.lean
   Hilberts-Foundations-of-Geometry.pdf

[Anne Baanen]

Are there similar techniques in lean4 to Isabelle's "try" or "blast" which attempt to apply a broad range of primitive tactics?

The aesop tactic as you mentioned is intended to be an equivalent to auto, but it is also useful in more basic situations. I'm not familiar with try and blast: could you explain why they would be more useful than auto in these cases?

[Joachim Breitner]

IIRC try would try simp and aesop and rw_search and a bunch of other tactics in parallel and reports whatever works.

[Scott Morrison]

Yes, we had hint in mathlib3 that did this, and I would love to reinstate it!

[Jürgen Uhl]

try and blast simple apply a lot more theorems and strategies. As you can see from the attachment, the proof for lemma -I-1 was found by typing "try" and it produced "(metis Suc-diff-le Suc-eq-plus1 Zero-not-Suc cancel-comm-monoid-add-class.diff-cancel card.empty is-singletonI′ is-singleton-altdef not-numeral-le-zero one-add-one)" - I don't even know what exactly these different rewrites/theorems are - which include set and number theory. "try" can take really long while searching for different strategies, whereas "blast" is a fairly fast yes/no tactic and is much stronger than auto, but weaker than try. Which theorems/strategies exactly are contained in try/blast, I do not know.