A lot of people that I have talked to expressed their interest in learning about Ltac2, the new tactic language of the coq proof assistant, yet most did not manage to do so because the language is not well-documented. After spending a lot of time reading the official documentation of Ltac2 myself, I came to the realization that Ltac2 really is a shockingly simple language. To quote the documentation, “Ltac2 is … a member of the ML family of language”. If you already know Coq, OCaml, or even Haskell, you can already write a decent chunk of Ltac2 code once you have a minimal understanding of the basic syntax, such as top-level definitions and pattern match constructs. Most of the time, you can write Ltac2 based on intuition. It works pretty much the same way how you would expect a ML-family language works.

For most people, I see two main factors that block people from learning Ltac2:

• An understanding of the basic primitives of meta-programming. In the Coq proof assistant, Ltac2 can be used to manipulate the proof state and generate Gallina terms. When programming in Ltac2, it is possible to refer to Gallina terms. Sometimes, it becomes hard to distinguish between the terms from these two languages. Ltac2 introduces new mechanics to help the programmer and the proof assistant itself to distinguish between these two fragments. If you already under how backquotes and unquote work in Lisp, it is easy to apply that knowledge to Ltac2. If you already know Ltac, you should also have some basic understanding of meta-programming techniques, and once you have seen a few examples, you’ll understand why the extra verboseness in Ltac2 is a good thing.
• The lack of resources with simple, familiar examples that do not overwhelm you with technical details. Ltac2, at its core, is a simple ML-family language. However, if you simply type in a piece of OCaml code in your proof buffer, the code simply will not run. Your next best bet is to decipher the formal syntax from the coq documentation. I don’t think it has to be like that. It is so much easier to learn from examples.

Functional programming with Ltac2

Ltac2 is a functional programming language. It makes sense to start the tutorial with functional programs rather than the familiar hello world.