Meta4dummies

Stream: metaprogramming / tactics

[Moritz Doll]

During the Banff workshop/my porting attempt for congrm I have started writing a list of important definitions for tactic writing, which now turned somewhat into a general introduction to tactic-writing geared towards mathematicians. Anne advised me to put this into the mathlib4-wiki and now it is here: https://github.com/leanprover-community/mathlib4/wiki/Metaprogramming-for-dummies
It is very far from finished, but I will probably not have too much time to work on this until next weekend. Additions and corrections are very welcome. Be careful, I now very little about metaprogramming, so there are probably lots of wrong things already (and more to come).

[Shreyas Srinivas]

Suggestion: Some examples with v/s without Qq

[Damiano Testa]

Inspired by this thread, I decided to start writing some examples. I am learning a little bit of parsing and writing a simple example along the way. If people think that it could be useful, I can add it to the wiki. Of course, comments are very welcome!

import Lean
open Lean Elab Tactic Term Meta
/-
This example shows how to take a user input `a` and add to the local context
the assumption `[a].length = 1`.

The underlying principle is that we want to take some user input, embed it
into the rich type-system that Lean has and then process it.

The following line of code, informs Lean that `single_me <something>` is a tactic.
It also makes Lean aware that `<something>` is a `term` (or, with all the
namespaces, a `Lean.Parser.Category.term`).
-/
syntax "single_me " term : tactic
/-
Thus, if we are in tactic mode and we write `single_me whatever`, then Lean
knows that this is a tactic and that `whatever` is a `term`.

Let's test this out!
-/
example : true := by
  single_me whatever  -- tactic 'tacticSingleMe_' has not been implemented
/-
Sure, Lean has no idea what the tactic is supposed to do.

However, if you remove `whatever`, leaving only `singleMe`, then the error
message changes to `expected term`: the tactic is not implemented, but Lean
knows that it should expect a `term`.
If you tried with something else, say `whoKnows`, Lean would have replied with
`unknown tactic`.

Let's implement the `single_me` tactic.
-/

-- these are the "elaboration rules" for a tactic
elab_rules : tactic
-- if Lean finds `single_me [stuff]`, it is going to assign the label `x`
-- to [stuff] and it is going to assume that it is a `term`.  This basically
-- affects what we can ask Lean to do with `x`.
| `(tactic| single_me $x:term) => do
  -- at this point, the tactic state contains ``x: TSyntax `term``:
  -- `x` "entered" the local context of our tactic development as a
  -- "Typed Syntax" with `Category` `term`.
  -- The next line essentially runs `have : [$x].length = 1 := by simp` in
  -- the local context of where our tactic will be called.
  evalTactic (← `(tactic| have : [$x].length = 1 := by simp))
  -- Note that we are using `$x` to refer to the "quoted" variable `x`.
  -- This is "our" input: we are going to type it in tactic mode, Lean
  -- parses it and performs actions with it.

example : True := by
  single_me 0  -- local context now contains `this: List.length [0] = 1`!
  trivial

/-
Great!  We managed to add to the local context the hypothesis that the
list consisting of `0` has length 1.

In a similar vein, here are more examples of our new tactic:
-/

example {α : Type} [Add α] {a b : α} : True := by
  single_me a
  -- local context now contains `this: List.length [a] = 1`
  single_me 1 + 2
  -- local context now contains `this: List.length [1 + 2] = 1`
  single_me a + b
  -- local context now contains `this: List.length [a + b] = 1`
  single_me [a]
  -- local context now contains `this: List.length [[a]] = 1`
  single_me ∀ x : Int, x + 5 = 0
  -- local context now contains `this: List.length [∀ x : Int, x + 5 = 0] = 1`
  trivial

/-
As you can see, the `term` Category is fairly flexible: basically, anything
that looks like an `Expr`ession will be allowed.

If we had used `ident` instead of `term`, then we would have been allowed
to use "identifiers", essentially the variables in our context.  If we did
that, then in the final example `single_me a` would have worked, but
nothing else would have.
-/