Writing basic tactics

Stream: general

[Andrej Bauer]

I am struggling to get my own tactics going, and would appreciate a hint as to where to look (as in "documentation") or how to fix the following attempt at implementing a tactic which takes a : α and simply fulfills the goal α × α:

meta def diag_tactic {α : Type} (a : α) : tactic (α × α) :=
  return (a, a)

example : ℕ × ℕ := by diag_tactic 5

[Johan Commelin]

Have you seen https://leanprover-community.github.io/extras/tactic_writing.html ?

[Andrej Bauer]

Yes, but I am unable to fix my broken example above by looking at that document. For starters, should diag_tactic have type tactic unit, by any chance?

[Patrick Massot]

yes

[Patrick Massot]

Interactive tactics have type tactic unit. Type tactic stuff is useful as intermediate tools where you want to create some stuff during a tactic by accessing the current tactic state (and allowing failure)

[Jannis Limperg]

Iow the current goal (or list of goals) is ambient in the monadic state. I've found that the best documentation is looking through all the primitives in init/meta/tactic.lean.

[Jannis Limperg]

exact is what you're looking for here.

[Andrej Bauer]

How do I say that the argument of a tactic is an expressions? For instance, if the argument is an identifier, then I say (h : parse ident), as far as I can tell, but what if it is supposed to be any expression?

[Johan Commelin]

(e : expr)?

[Andrej Bauer]

Sorry, wrong question. How do I tell Lean to parse the argument to an expression. Consider the following example:

meta def my_tactic (e : expr) : tactic unit :=
  do { tactic.exact e }

example : ℕ × ℕ := by my_tactic `((5, 5))

It is of course crazy that we would have to quote the expression when we use diag_tactic. I want to reverse the process, so that I can write diag_tactic (5,5) and the tactic then parses (5,5) into an expression. (Or if I am doing it all wrong and there is a better way to achieve what I am trying to do, please tell me.)

[Gabriel Ebner]

This is explained in the document Johan linked to: https://leanprover-community.github.io/extras/tactic_writing.html#parsing-locations-and-expressions

[Floris van Doorn]

You can also take a look at the implementation of docs#tactic.interactive.exact.

[Floris van Doorn]

Here is a short example

import tactic.core

open tactic
setup_tactic_parser

meta def tactic.interactive.my_tactic (e : parse texpr) : tactic unit :=
do tgt : expr ← target,
   i_to_expr_strict ``((%%e, %%e) : %%tgt) >>= exact

def foo : ℕ × ℕ := by my_tactic 5
#print foo -- (5, 5)

[Andrej Bauer]

Thanks @Floris van Doorn , that's exactly what was eluding me!

[Andrej Bauer]

Ugh, why is tactic p not allowed when p : Prop? What if I want a tactic that returns a proof of equality?

[Rob Lewis]

You almost certainly want it to return that proof as an expr, not a Prop.

[Rob Lewis]

Andrej Bauer said:

I am struggling to get my own tactics going, and would appreciate a hint as to where to look (as in "documentation") or how to fix the following attempt at implementing a tactic which takes a : α and simply fulfills the goal α × α:

meta def diag_tactic {α : Type} (a : α) : tactic (α × α) :=
  return (a, a)

example : ℕ × ℕ := by diag_tactic 5

I know you got this sorted out, but let me use it as an example, since it shows a common misconception: your interactive tactic isn't supposed to produce data that solves the goal. It's a function from tactic state to tactic state, and it's supposed to provide an expression whose type matches the type of the initial goal. So (as you figured out) you use the exact tactic to close this goal. And as you also saw (hidden in some notation), you gave exact an expr, not a pair of natural numbers.

[Rob Lewis]

Same thing with proof producing tactics. It doesn't really make sense for a tactic to compute a proof of P : Prop. Rather, if you have an expr P, whose type is Prop, you want to compute an expr e whose type is represented by the expr P.

[Andrej Bauer]

Thanks! I've lived in the LCF-proof-assistant land for too long, where tactics actually return judgements.

[Andrej Bauer]

If I may bother you a little more. Suppose, for the sake of example, that I would like to have a tactic which takes in expressions a and b and attempts to use the refl tactic to prove a = b. (In a realistic example I wouldn't use refl but something complicated). Am I correct to think that I start like this:

meta def by_refl (a b : parse texpr) : tactic pexpr :=  do something

[Rob Lewis]

Almost. pexpr (and texpr, same thing) are unelaborated. Basically think of them as input level syntax. You want to return a full proof term, so the type should be tactic expr.

[Andrej Bauer]

And somehow I need to create a subgoal for refl to work on (hmmm, how?) because all of this is stateful and side-effecting.

[Rob Lewis]

Yup, that was what I was about to write :smile: some tactics will return the terms they create, but things like refl which are meant to be used interactively operate on the goal state.

[Rob Lewis]

meta def by_refl (a b : parse texpr) : tactic expr := do
tgt ← to_expr ``(%%a = %%b),
(_, e) ← solve_aux tgt (tactic.reflexivity),
return e

[Rob Lewis]

There are various ways to do this, but docs#tactic.solve_aux is my go-to

[Andrej Bauer]

Thank you again! I think I was just trying to invent solve_aux, glad to see it's there already.

[Rob Lewis]

tactic.reflexivity is what the interactive tactic refl does under the hood, but if you really explicitly wanted to use the interactive one, you could replace that with `[refl]

[Andrej Bauer]

Is meta instance what I think it is? I.e., a tactic that generates instances (but it may also fail)?

[Rob Lewis]

No, nothing so fancy. meta instance is the same as instance except the type and body can refer to meta things.

[Rob Lewis]

You can't write instance t : inhabited expr := ⟨expr.var 0⟩ since expr is meta, so this has to be a meta instance.

[Eric Wieser]

Andrej Bauer said:

Is meta instance what I think it is? I.e., a tactic that generates instances (but it may also fail)?

It's not meta that means "tactic", it's tactic as the return type that does. You can write regular functions with meta too, you just can't prove things about them.