Writing Tactics

Stream: lean4

[Marcus Rossel]

I would like to try out writing tactics. Are there any resources describing the syntax/mechanism for this?
The only I've found so far is in the Lean 4 Manual, which is rather an example than a description.

[Kevin Buzzard]

I don't know anything about this myself, but there are some examples of tactics in mathlib4.

[Jannis Limperg]

These talks are some of the better documentation we have right now:

https://www.youtube.com/watch?v=UeGvhfW1v9M
https://www.youtube.com/watch?v=vy4JWIiiXSY

[Marcus Rossel]

I tried writing an obtain tactic as follows:

macro "obtain " t:term " := " h:ident : tactic =>
  `(match $h with | $t => ?use)

I was basically just copying the implementation of by_cases in mathlib4:

macro "by_cases " h:ident ":" e:term : tactic =>
  `(cases Decidable.em $e with | inl $h => ?pos | inr $h => ?neg)

With my implementation of obtain I get an error though on the | symbol, saying expected '.'.
Why is this happening / what can I do to fix it?

[Mario Carneiro]

macro "obtain " t:term " := " h:ident : tactic =>
  `(match $h:ident with | $t => ?use)

works

[Marcus Rossel]

Do you happen to know why? ^^

[Mario Carneiro]

It probably guesses that $h has the wrong syntax class, like term or matchArg

[Mario Carneiro]

in fact I'm also not sure it guesses the syntax class of $t right either

[Mario Carneiro]

you should test it

[Marcus Rossel]

I don't understand why it has to guess at all. Isn't the syntax class specified in the first line?

[Mario Carneiro]

the type of t is Syntax

[Mario Carneiro]

and h

[Mario Carneiro]

there is no communication of the "type" of the syntax from the first line to the second

[Mario Carneiro]

because syntax is untyped

[Mario Carneiro]

the syntax class specifications are needed to define the parser, but the rhs of the => is just a function h t : Syntax |- MacroM Syntax

[Marcus Rossel]

Mario Carneiro said:

there is no communication of the "type" of the syntax from the first line to the second

Oh right, the macro command was just a macro for syntax with marco_rules right?

[Marcus Rossel]

Hmm, and another one...
I'm trying to do an unfold now:

syntax "unfold " ident+ : tactic

macro_rules
  | `(unfold $[$l:ident]+) => `(simp only [$[$l],+])

I get an error on the first $ saying that expected ')' or '|'.

This time I used an example by Leo as inspiration:

syntax assocEntry := term ":" term
syntax "{" assocEntry,* "}" : term

macro_rules
  | `({ $[$k:term : $v:term],* }) => `([$[($k, $v)],*].toAssocList)

At Lean Together 2021 Sebastian also showed an example using $[...]*, so I was guessing $[...]+ might work too.

I feel like I have no clue what I'm doing here, so forgive me if this is maddening to look at :big_smile:

[Kevin Buzzard]

Believe me you know more than me, I'm taking notes!

[Sebastian Ullrich]

There is no $[...]+ (yet), you can use $[$l:ident]* instead (or just $l*)

[Mac]

Sebastian Ullrich said:

you can use $[$l:ident]* instead (or just $l*)

Oh! I didn't know the $l*) shorthand existed! It seems there is always something new to learn about the macro system. :laughing: