Guide to writing tactics

Stream: general

[Dan Velleman]

I've spent the last few weeks learning to write tactics. I learned a lot by trial and error, and decided to write up what I've learned in a Guide to Writing Tactics. I'd welcome feedback on this, especially corrections of any errors I've made.
-Dan Velleman
TacticGuide.pdf

[Patrick Massot]

First remark without reading any word: it would be much nicer with syntax highlighting.

[Mario Carneiro]

In section 1, it is not true that let cannot stand on its own, but the syntax is slightly different. In a do block it has the syntax let x : T := e, and outside a do block it is let x : T := e in e'

[Arthur Paulino]

Patrick Massot said:

First remark without reading any word: it would be much nicer with syntax highlighting.

I've wondered it before, how to get proper Lean syntax highlight in LaTex?

[Mario Carneiro]

https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md

[Dan Velleman]

What I meant by "cannot stand on its own" is that it has to be followed by either ", e'" or "in e'". The example I give with if-then-else illustrates the point I was trying to make, but perhaps it isn't clear enough.

[Eric Taucher]

Could this be the start of a new book?

[Mario Carneiro]

Think of a tactic string as a box that contains a string, together with all of the other information needed to deal with the complications described earlier that arise when one tactic calls another.

This should somehow be adjusted to reflect that tactic string is a function that can be called, not a value to be unwrapped. You can call a tactic multiple times and get different results

[Kevin Buzzard]

Eric Taucher said:

Could this be the start of a new book?

There's always the old book: https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf

There's also Rob Lewis' videos at https://www.youtube.com/watch?v=o6oUjcE6Nz4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N&index=19 (and see other links in the description)

[Mario Carneiro]

The discussion about backtick names reminds me of a recent run-in I had with the computer modern backtick character, which looks way too much like an apostrophe. I suggest changing the font to something that makes this more visually distinctive

[Dan Velleman]

I'm not sure I understand the comment about tactic string. The tactic itself is a function that can be called multiple times with different results. But what it returns is like a box with a string (and other stuff) inside, isn't it? Isn't tactic string specifying the type of what is returned?

[Mario Carneiro]

the "box containing a string" is actually interaction_monad.result tactic_state string, and tactic string is defined as tactic_state -> interaction_monad.result tactic_state string

[Mario Carneiro]

That is, tactic string is literally a function taking an opaque object of type tactic_state into some kind of box containing a new tactic_state and a string

[Mario Carneiro]

This is relevant in the implementation of functions like src#tactic.try

[Patrick Massot]

I've quickly read the whole thing. It's nice but I don't see much that isn't covered in our standard tutorial https://leanprover-community.github.io/extras/tactic_writing.html

[Dan Velleman]

Thanks Mario. That makes sense.

[Arthur Paulino]

Lots of great material on this thread. Thanks everyone!
And Thanks Dan, I love reading/learning the same subject from various perspectives :pray:

[Eric Taucher]

Kevin Buzzard said:

Eric Taucher said:

Could this be the start of a new book?

There's always the old book:

I knew someone would think that, I didn't expect it would be you. Dan knows what I am talking about.

[Dan Velleman]

Continuing the discussion of tactic string: I take it that a more accurate explanation of the meaning of s \leftarrow T would be something like: Run T. Apply the returned tactic string to the current proof state to get a box containing the new state and a string. Remove the string from the box and assign it to s, and pass the new state on to the next step?

[Rob Lewis]

"Run T" only makes sense with the current proof state. A term of type tactic s is like a function from tactic_state to s × tactic_state (with the possibility of failure, as discussed).

[Rob Lewis]

So the meaning of s ← T is "run T on the current proof state. Unbox the result; assign the string component to s, and update the proof state to the new one returned by T."

[Kevin Buzzard]

Eric Taucher said:

Kevin Buzzard said:

Eric Taucher said:

Could this be the start of a new book?

There's always the old book:

I knew someone would think that, I didn't expect it would be you. Dan knows what I am talking about.

Oh you mean Dan's old book :-) Yeah I was just pointing out the abandoned "Programming in Lean" book which nobody ever talks about any more but which has some info about tactic writing. Sorry for the crossed wires!

[Rob Lewis]

Or "pass on the proof state to the next step" instead of "update," if you prefer!

[Kevin Buzzard]

PiL was the book which taught me what a monad was, which is pretty much the limit of my understanding of what tactic X means.

[Bhavik Mehta]

I really like this document! It's the first thing I've read which clearly explains the description between pre-expressions and expressions.

[Dan Velleman]

Here's an updated version with syntax highlighting (thanks Mario for the link to Jeremy's lstlean file), corrections to the explanation of tactic string (thanks Mario and Rob for explaining this; I hope I have it right now), and some additional material on how to call tactics in the library.
TacticGuidell.pdf

[Dan Velleman]

OK, final version, with an illustration of the use of <|> at the end.
TacticGuide.pdf