Introduction to Tactic Writing in Lean

Originally, this was a single Lean file, later we extended the tutorial with further files with more advanced topics.

If you are a metaprogramming beginner, we recommend to start with TacticProgrammingGuide.lean. There are 762 lines coverging the basics of Lean tactic writing. We assume you already know Lean, and probably use VS Code, in that case clone this repository, or simply download the file.

Alternatively, you can also copy it to Lean 4 Web but you will miss the Ctrl-click feature.

We tried to explain all the basic concepts but keep at least the introduction it beginner friendly. Enjoy learning Lean metaprogramming. If you are getting confused somewhere, it is probably not your fault. Let us know what needs more clarification in the Zulip thread.

Content

So far, there are three tutorials of increasing difficulty. Although you can scroll through it on Github, we indeed recommend to download the files and play with them.

• Introduction: the basic introduction mentioned above.
  • How imperative programs work in Lean
  • What is a proof state
  • Basic data structures around Lean metaprogramming
  • Implementing basic tactics
  • How to declare syntax for a new tactic
• Implementing rw from scratch: a tactic that does a single rewrite.
  • What rw does on proof term level
  • Implementing basic rw
  • Options for normalization
  • Unification - rewriting a quantified equality.
• Implementing simp from scratch: more advanced expression manipulation.
  • What simp does on proof term level
  • Filling implicit arguments
  • Custom SimpResult datastructure
  • Basic simp implementation
  • Debugging with traces
  • Implementing simp inside binders
  • Collecting tagged lemmas