Introduction to tactic programming

Stream: metaprogramming / tactics

[Mirek Olšák]

Inspired by discussions on BigProof, we wrote an introduction to tactic programming with @Jovan Gerbscheid , also thanks @Anand Rao Tadipatri for checking early version.
https://github.com/mirefek/lean-tactic-programming-guide
If you are a Lean user interested in how tactics work, and how you could one day write your own, we would love to hear your feedback!
(of course we are also curious about critique from experts)

[Shreyas Srinivas]

I was following this tutorial and I had a question: For MetaM, there is a MonadEval instance. This lets me #eval <insert function returning MetaM> and get the result. I can't do the same for TacticM returning functions. What is the reason for this design/implementation decision

[Aaron Liu]

For TacticM returning functions, you need to have a tactic state available to execute them, which you don't get with just #eval.

[Mirek Olšák]

You could implement MonadEval in principle, perhaps just no one needed it. The intermediate monad between TacticM, and MetaM is Lean.Elab.TermElabM, and it already has MonadEval, so all you would need is to provide the name of the tactic file (can be anonymous), and the list of goals (empty, or all existing unassigned metavariables...), like in the implementation of Lean.Elab.Tactic.run

[Kyle Miller]

Aaron Liu said:

For TacticM returning functions, you need to have a tactic state available to execute them, which you don't get with just #eval.

Exactly, TacticM is a monad that doesn't have a direct way to spin it up, except by knowing it's a reader and state monad over TermElabM.

Here's an implementation that uses an empty goal list:

instance : MonadEval TacticM TermElabM where
  monadEval m := m |>.run { elaborator := .anonymous } |>.run' { goals := [] }

[Shreyas Srinivas]

Isn't there an empty/default state?

[Shreyas Srinivas]

Oh I see that's what Kyle has written

[Shreyas Srinivas]

Could anything go wrong if this MonadEval instance was inferred in the absence of any explicit tactic state?

[Jovan Gerbscheid]

The issue is that most functions written in TacticM will operate on the main goal (that is, the first element in the list of goals). But we are passing it an empty list here, so it looks to the tactic like all goals are solved.

[Mirek Olšák]

Shreyas Srinivas said:

Could anything go wrong if this MonadEval instance was inferred in the absence of any explicit tactic state?

To see how tactics react without a goal being set, you could try out e.g.

example : True := by
  trivial
  run_tac
    logInfo "message1"
    let goal ← getMainGoal
    logInfo "message2"

it is not a problem to create a new dummy metavariable with some type (e.g. True) and set it as the main goal but for the purpose of #eval, that feels quite arbitrary.

And just to be clear, the tactic state was set -- as an empty list. Of course, e.g. filling it with sorry would not work.

[Shreyas Srinivas]

I am aware of this since it is one of the first examples in your tutorial :sweat_smile:

[Mirek Olšák]

Good, I just wanted to show that it works also after closing the goal (somewhat)

[Mario Carneiro]

Jovan Gerbscheid said:

The issue is that most functions written in TacticM will operate on the main goal (that is, the first element in the list of goals). But we are passing it an empty list here, so it looks to the tactic like all goals are solved.

In lean 3, I believe the default tactic state was a single goal proving True

[Mario Carneiro]

this was used when you used #eval to evaluate some code since back then there was only the tactic monad

[Floris van Doorn]

I haven't looked at the Lean file yet, but thank you so much for writing this!

[Floris van Doorn]

We should add a link to this here: https://leanprover-community.github.io/learn.html#meta-programming-and-tactic-writing (please make a PR).

[Mirek Olšák]

https://github.com/leanprover-community/leanprover-community.github.io/pull/659

[neil]

I just read through it (note: I didn't work all the exercises). Overall, I liked it, but it is quite introductory, and I really felt the lack of detail sometimes. Also, the prose gets a bit loose after the first bit, so a copyediting pass could help. It did feel like I wasn't really the target audience, since I have more FP experience than the guide seems to require, so maybe a clearer expression of who this is for and what sort of treatment is given could be useful near the top

(Note: I read this last night, and these are just my opinions from memory the next day. So maybe some of these are already addressed, but didn't impress upon me properly in my one session I spent reading it)

[Mirek Olšák]

Thanks for the feedback!

neil said:

it is quite introductory, and I really felt the lack of detail sometimes

Is there a particular domain that you think would deserve more attention? I would prefer not to extend the guide much, but perhaps we can add pointers.

neil said:

Also, the prose gets a bit loose after the first bit, so a copyediting pass could help.

We didn't update the document much recently, suggestions for stylistic improvements are welcome.

neil said:

It did feel like I wasn't really the target audience, since I have more FP experience than the guide seems to require, so maybe a clearer expression of who this is for and what sort of treatment is given could be useful near the top

It is true that the comments in section (1) were targeted at people used to procedural programming. Do you think adding something like this after the content-defining questions would help?

Let us answer them. Each question will have its own chapter.
If you are familiar with functional programming, you can skip chapter (1), just check out Lean's procedural features such as return, for .. do, or inlined ←. If you are familiar with Lean's theory (proof terms, meta-variables), you can skip chapter (2).

[Shreyas Srinivas]

I think it might help to have some non-trivial examples of how to write tactics. But this might be a separate task. Something like a "how to write your own rw tactic from scratch", where you start with an elementary version and slowly progress to the real version.

[Mirek Olšák]

Good suggestion, yes that should be probably a different document. I agree it would showcase much more of the term-digging & unification. I will think about it.

[Jovan Gerbscheid]

One inconvenience for writing a tutorial about rw is that its behaviour may soon change on bound variables. @Kyle Miller, could you say what the plan is for the way rw will work when rewriting terms with bound variables? @Mirek Olšák and I had two ideas for what proof term might be generated by a more advanced rw tactic. Will it be one of these two?

example (f g : Nat → Nat) : ∀ x y, f x + g y = 0 := by
  refine @Eq.mp (∀ x y, g y + f x = 0) _
    (congrArg (fun a => ∀ x y, a x y = 0)
      (funext fun x => funext fun y => Nat.add_comm (g y) (f x))) ?_

example (f g : Nat → Nat) : ∀ x y, f x + g y = 0 := by
  refine @Eq.mp (∀ x y, g y + f x = 0) _
    (congrArg (fun a => ∀ x y, a (f x) (g y) = 0)
      (funext fun x => funext fun y => Nat.add_comm y x)) ?_

[Aaron Liu]

I hope it doesn't change

[Jovan Gerbscheid]

Really? I think the failure of rw [Nat.add_comm] on the above example is quite clearly more of a bug than a feature.

[Aaron Liu]

It explicitly skips bound variables in the code, so clearly it's intentional

[Kyle Miller]

The rough idea @Jovan Gerbscheid is that it will do the rewrite and then do a post-hoc congruence construction, the specifics of which can depend on a number of factors. If congrArg works, great; if using funext in conjunction with congrArg works, great; but in general it might do other things too, like make use of proof irrelevance to iron out "motive not type correct" errors, or take a simp-like congruence lemma approach to navigate to particular locations that have nontrivial dependencies.

[Kyle Miller]

Jovan Gerbscheid said:

One inconvenience for writing a tutorial about rw is that its behaviour may soon change on bound variables.

I don't think there's any harm in having tutorials that show how to make simple tactics. Someone could make a nice rw-lite, without any of the occs logic, one that just uses kabstract, makes a motive, and creates a proof with congrArg.

It's a good introduction to what motives are about, which isn't specific to rw.

[Kyle Miller]

@Aaron Liu We'll keep the current rw around in some form. It's nice having low-level tactics that you can understand completely (so long as you understand motives!), but it's very clear that the limitations of rw have been a stumbling block for Lean users forever. When someone uses rw, they're not thinking about motives, they have a rewrite they want to do. The system should make it possible to "just" rewrite. It's also long been confusing how simp can do rewrites that rw can't too.

[Mirek Olšák]

Of course, I don't want to explain full scale of rw / simp. It was rather "Let's start by looking at the proof term that rw produces.", or having a comment that the approach of rw doesn't work under binders, and I wanted to know if such would become soon outdated.

[Kyle Miller]

@Mirek Olšák Motives will never be outdated. A tutorial with a simple kabstract-based algorithm would be great.

By the way, it's not about not working under binders; this is a very-often-repeated simplified version of the actual limitation. It's that rw can't rewrite subexpressions that contain bound variables. This limitation is because of kabstract.

A more advanced tutorial would then go into how kabstract works, then make a version of it that can match subexpressions that have bound variables by using MetaM and abstracting local fvars in the match, and then implement an improved rw using the funext term that @Jovan Gerbscheid mentions.

[Shreyas Srinivas]

@Mirek Olšák : Partially my motivation in asking for such a tutorial is to have a resource where one can learn the computer science that goes behind a seemingly elementary tactic like rw

[Shreyas Srinivas]

In addition, effective metaprogramming requires learning quite a bit of the API and understanding some reasoning principles to guide good implementations. rw is just a good Trojan horse to sneak this in without too much conceptual complexity at the user level.

[Shreyas Srinivas]

This doesn't necessarily require the most recent and advanced version of rw to be explained. Just a fairly sophisticated version, starting from an elementary one

[Mirek Olšák]

Not sure what computer science you have in mind, so far I wrote some explanation about the difference between simp and rw.

[Shreyas Srinivas]

Subexpression matching

[Shreyas Srinivas]

normalisation

[Shreyas Srinivas]

substitution with the proof of correctness (How congruence, Eq.subst, etc get used).

[Shreyas Srinivas]

Basically this could take off where the equality section of #tpil leaves the story

[Shreyas Srinivas]

Even computer scientists don't usually go through very deep PL theory courses at the undergrad level (depending on where they study and what courses they choose)

[Mirek Olšák]

Shreyas Srinivas said:

Subexpression matching

It composes of two parts

• traversing a term (nothing "deep" really)
• matching (there is actually theory behind general unification)

normalisation

There is a bunch of theory about term rewriting (Knuth-Bendix, etc.) that Lean's simp doesn't care about -- it is up to the library writer to tag the correct & correctly oriented lemmas. rw is even more basic.

substitution with the proof of correctness (How congruence, Eq.subst, etc get used).

Check out the draft I linked above.

[Shreyas Srinivas]

lean cares about certain basic kinds of normalisation, most prominently whnf

[Mirek Olšák]

Yes, on the other hand, there is no proving around that -- kernel just checks that two terms are equal up to beta-reduction. I was not planning to focus on that much...

[Mirek Olšák]

You can check out the implementation of Lean.Meta.whnfImp, it looks quite readable.

[Mirek Olšák]

@Shreyas Srinivas The custom rw implementation / tutorial is now available in the branch custom_simp_rw. Let me know if it is what you imagined, and if it makes sense to merge to the main branch as a follow-up intermediate text.

[Shreyas Srinivas]

At a cursory glance it looks very good. I might get a chance to play with it in the next seven days and give better feedback

[Shreyas Srinivas]

One suggestion: Don't get into simp before getting a basic version of rw running

[Shreyas Srinivas]

Let rw be the first self-contained goal

[Shreyas Srinivas]

Another thing. It might really help to give some simper examples to manually perform rewrites with in the beginning. I find that when I want to understand an algorithm, working it out on some examples first helps. In these examples, you would first have users construct term mode proofs of increasing complexity. You would be introducing all the equality lemmas that we rewrite with, and increasing the complexity of expressions we rewrite under. Tactics are not easy. A little bit of slow cooking in term mode can motivate tactics much better. Also, tactics are ultimately about constructing Exprs

[Shreyas Srinivas]

why is this if statement not directly placed inside the match arm inside myAbstract?

if !e.hasLooseBVars then  -- we cannot rewrite a subterm containing a variable bound in `e`
    if (← isDefEq e a) then  -- check if already `a` is already the root
      return mkBVar offset  -- replace with bvar

it would also help to provide an explanation of the update<insertExprConstructor> functions here. What they do and why we are using them.

[Shreyas Srinivas]

Another quibble, when I #print kabstract it shows me a completely different function where it looks like all the bvars have been constructed and the abstraction is being built. This seems to correspond to your abstractToMapping whereas your myAbstract seems to correspond to Expr.abstract

[Shreyas Srinivas]

The comments don’t reflect that.

I have read upto the beginning of section 2. I would suggest moving simp and simp_rw to a separate file and have some exercises on rwto keep it self contained. For example adding the occ argument for rwmight be a good exercise.

[Mirek Olšák]

Shreyas Srinivas said:

Another quibble, when I #print kabstract it shows me a completely different function where it looks like all the bvars have been constructed and the abstraction is being built. This seems to correspond to your abstractToMapping whereas your myAbstract seems to correspond to Expr.abstract

No, kabstract doesn't build the lambda, it corresponds to myAbstract. Its definition is a little more complicated because it can be provided with a position where to perform the rewrite, so it must count occurrences. I would not try to print a function to understand it, I would rather recommend to look at the definition in the library, or to test it.

[Mirek Olšák]

Shreyas Srinivas said:

why is this if statement not directly placed inside the match arm inside myAbstract?

if !e.hasLooseBVars then  -- we cannot rewrite a subterm containing a variable bound in `e`
    if (← isDefEq e a) then  -- check if already `a` is already the root
      return mkBVar offset  -- replace with bvar

Besides ← isDefEq e a being often a better than pure equality check, you cannot match against a variable, for example even this doesn't work.

def f (a b : Nat) : Bool :=
  match a with
  | b => true
  | _ => false

[Mirek Olšák]

Shreyas Srinivas said:

it would also help to provide an explanation of the update<insertExprConstructor> functions here. What they do and why we are using them.

Ctrl-click, and you will see what it does.

[Mirek Olšák]

I thought that for an intermediate tutorial, it makes sense to leave figuring easy things such as this one for the reader.

[Mirek Olšák]

Shreyas Srinivas said:

I have read up to the beginning of section 2. I would suggest moving simp and simp_rw to a separate file and have some exercises on rwto keep it self contained. For example adding the occ argument for rwmight be a good exercise.

Thanks, I will consider splitting simp into another file. The annoying part is that rewriting a quantified equality is again related to both rw and simp. But I agree that an exercise for implementing occurence count on your own is a good exercise, and the file is getting quite long & heavy.

[Kyle Miller]

For simp, it might be worth splitting into two to have some space to expand on generating specialized congruence lemmas (though your approach to only support app congruences that can be achieved with congr/congrArg/congrFun is fine too for a tutorial version! simp gets pretty far with just these; that said, you need to make sure you're not creating some type incorrect terms here, and that the type isn't changing from the LHS to the RHS)

[Mirek Olšák]

Originally, I thought of supporting only app with congr, and explain how to add other later. Then I thought that doing it all together also with implies_congr, and forall_congr from the start doesn't make too much difference. If I split simp into a separate file, I might again start with only supporting congr.

[Mirek Olšák]

Shreyas Srinivas said:

The comments don’t reflect that.

I have read upto the beginning of section 2. I would suggest moving simp and simp_rw to a separate file and have some exercises on rwto keep it self contained. For example adding the occ argument for rwmight be a good exercise.

I split it into two files -- CustomRw.lean & CustomSimp.lean with the idea of rw being the first part, and simp second. I keep the combined file there too so far but planning to remove it if we agree this is better.

[Shreyas Srinivas]

I think just splitting the file and importing the rw into simp for simp_rw is better.

[Shreyas Srinivas]

Tutorials work best when they are in byte sized chunks

[Mirek Olšák]

Now, I split it in a way that doesn't have a Lean-dependency (so I don't import, importing is a bit annoying). Do you think the current split is not pedagogically ideal?

[Mirek Olšák]

The rw / simp is now in the main tutorial. I think concept-wise it can stay this way but it might need some fixes (feedback still welcome)

[Shreyas Srinivas]

I was reviewing this tutorial properly when I discovered a UX trick to get lean to give you good type errors for term mode proofs, and so allow programming with holes. Experts might know it already, but it might be useful for newcomers: The idea is to insert () for each hole. Lean will complain that you are giving a value of type unit where you should be giving a value of type ... which is the correct type. Suppose the type is a function type, then you give it a fun x y z => (), then the type error gets updated. and one can repeat this ad infinitum

[Shreyas Srinivas]

Now if only there was a code action to look at the type errors and insert these terms with these "holes"

[Aaron Liu]

hopefully not ad infinitum and only until you solve the problem

[Shreyas Srinivas]

yeah, but you know what I mean. I think I have done this before with tpil and mpil last year, but not much afterwards. Lean usually gives you terrible error messages if you are in term mode in a proof.

[Shreyas Srinivas]

It parses upto the next declaration.

[Shreyas Srinivas]

If you use braces, you again get bad metavariable containing error messages

[Aaron Liu]

I just insert sorry and look at the expected type

[Aaron Liu]

sometimes if the errors are especially tricky I will start putting :)

[Shreyas Srinivas]

This trick only works because () is the unit element, but it can also contain terms as brackets so one just has to insert new stuff inside the brackets.

[Shreyas Srinivas]

because () is a complete term, the type is determined to be Unit and lean can stop parsing further, and give a decent error message.

[Shreyas Srinivas]

For what it is worth, I think that writing term mode proofs is a good introduction to metaprogramming.

[Mirek Olšák]

when I am writing a term, I usually indeed leave (), or _.

[Kyle Miller]

I don't understand the trick; using () can easily change how things elaborate due to the way types propagate. Using _ is more neutral, and it reports the type in the error message. You can use ?_ if you want to avoid unification accidentally assigning it. These seem like a better choice over (). What am I missing about the UI for _/?_?

example : Nat := 1 + ()
/-               ~~~~~~
failed to synthesize
  HAdd Nat Unit Nat
-/

example : Nat := 1 + _
/-                   ~
don't know how to synthesize placeholder
context:
⊢ Nat
-/

[Shreyas Srinivas]

I took this example from the tutorial. See how in the () case you get localised error messages while with _ you get a big global error message.

-- it should look similar to
example : ∀ (a b : Nat) (f : Nat → Nat) (p : Nat → Prop),
  (∀ (x : Nat), f x = x) → p (a + b + a + b) → p (f a + f b + f a + f b) :=
  (
    fun (a b f p h hp) => (@Eq.mpr Nat () ()))
  )

example : ∀ (a b : Nat) (f : Nat → Nat) (p : Nat → Prop),
  (∀ (x : Nat), f x = x) → p (a + b + a + b) → p (f a + f b + f a + f b) :=
  (
    fun (a b f p h hp) => (@Eq.mpr Nat _ _)
  )

[Shreyas Srinivas]

The localised error message is more readable than the big global error on the entire body of fun. That's the UX I am after

[Aaron Liu]

when would you even have @Eq.mpr?

[Shreyas Srinivas]

I took it from the tutorial which starts with an Eq.mpr and decided to write all arguments explicitly to start with.

[Aaron Liu]

well you've taken a wrong turn somewhere because @Eq.mpr Nat is already wrong and I think the latter error message is a lot more helpful in telling me that

[Kyle Miller]

Aaron Liu said:

when would you even have @Eq.mpr?

Let's not ask that here. It's illustrating a point, and it's not fair to ask that an illustration be optimal code on its own.

[Shreyas Srinivas]

The original proof was already in the code. I just took it apart from inside out for building this example and then added the explicit @:

example : ∀ (a b : Nat) (f : Nat → Nat) (p : Nat → Prop),
  (∀ (x : Nat), f x = x) → p (a + b + a + b) → p (f a + f b + f a + f b) :=
fun a b f p h_eq h_finish =>
  Eq.mpr (
    congrArg (fun X => p (X + f b + X + f b)) (h_eq a : f a = a)
    : p (f a + f b + f a + f b) = p (a + f b + a + f b)
  )
  (Eq.mpr (
    congrArg (fun X => p (a + X + a + X)) (h_eq b : f b = b)
    : p (a + f b + a + f b) = p (a + b + a + b)
  ) h_finish)

[Kyle Miller]

Ok, I see what you mean @Shreyas Srinivas. Putting in a wrong term with a concrete type can help localize errors, in a way that neither _, ?_, nor sorry can.

[Shreyas Srinivas]

yes that's the point

[Aaron Liu]

in this case I think you don't want a localized error because the entire term has the wrong type anyways, so even if you fix the local errors you will still have to deal with the type mismatch

[Kyle Miller]

There's the proviso that () might cause other errors, which is worth keeping in mind, and there's no way to fix that.

[Kyle Miller]

@Aaron Liu Yes, that's an error, but if you're building up a term you might not be finished creating the terms that it will eventually sit within.

[Aaron Liu]

but sometimes it is useful to localize your errors and to do that maybe () can be helpful (I haven't tried it so I wouldn't know)

[Shreyas Srinivas]

Aaron Liu said:

in this case I think you don't want a localized error because the entire term has the wrong type anyways, so even if you fix the local errors you will still have to deal with the type mismatch

That's not the point. I just built the quickest example I could to show my point. If one wants to program with proof holes in term mode, I think that's basically necessary for type errors to be localised. Whether this is a style lean should encourage is a different matter, but it has its uses.

[Aaron Liu]

I wouldn't say it's necessary, since I have built terms without doing this and without much trouble either

[Shreyas Srinivas]

I am thinking of a more systematic approach here. Of course one can build term mode proofs without editor assistance as well.

[Kyle Miller]

@Aaron Liu What if the term just hasn't gotten to a relevant |> yet and Shreyas wants to get the Eq.mpr term right first?

[Aaron Liu]

Kyle Miller said:

Aaron Liu What if the term just hasn't gotten to a relevant |> yet and Shreyas wants to get the Eq.mpr term right first?

you could have???

[Shreyas Srinivas]

I could have shown a better example I admit. But it was just easier to delete a subterm tree and show how different terms work as holes w.r.t the error messages we get

[Kyle Miller]

But why should he need to write have just to get some localized type errors? Maybe he doesn't want have in the final term.

[Aaron Liu]

do the :) then

[Shreyas Srinivas]

Also, in this context, the purpose of building up these maximally explicit terms (maximal upto human convenience) is to show what we will later be building with tactics.

[Kyle Miller]

Be careful with the line of thought "I can do this unassisted so what's the problem?" It's very easy to get into a situation where we don't realize all the nonsense we're doing to work around issues because we are capable and able to navigate the system. There might be workarounds (e.g. using have, using :)) but that doesn't mean they are solutions that we can say are the obvious things that others should do (rather than could do). We need to take a critical eye toward the system.

[Shreyas Srinivas]

Which then gave me the idea that if we had localised errors like we get here with (), then maybe we could automate the process of opening up the brackets and putting the cursor in there, along with a type hint.

[Shreyas Srinivas]

Maybe the key takeaway is that a special symbol for holes that produces localised errors is a nice thing to have.

[Aaron Liu]

Kyle Miller said:

Be careful with the line of thought "I can do this unassisted so what's the problem?" It's very easy to get into a situation where we don't realize all the nonsense we're doing to work around issues because we are capable and able to navigate the system. There might be workarounds (e.g. using have, using :)) but that doesn't mean they are solutions that we can say are the obvious things that others should do (rather than could do). We need to take a critical eye toward the system.

My point is that there are many solutions to this problem already and sometimes it's not a problem

[Shreyas Srinivas]

What's special about the unit symbol is that it can be trivially turned into brackets by putting terms into it since it consists of two delimiters when converted into brackets. So lean stops reading past the closing brackets both when () is the unit term and when (<term>) are supplied as the body of the def

[Shreyas Srinivas]

The closest symbol combination I can think of that would serve this role without being the unit element is (_). Currently it doesn't count as a term so the global error message issue still exists.

[Mirek Olšák]

Let me know if there is a conclusion about what tip I should write to the text. To me, it feels a bit inconclusive so far. In the meantime, I at least added a tip on filling match ... with

[Shreyas Srinivas]

Will do. I think some of the text can be phrased in a more complete and simple manner.

[Mirek Olšák]

I meant regarding (), but general feedback is of course also very welcome.

[Mirek Olšák]

Especially, if you can make it more complete, and simpler at the same time -- these requirements usually compete. :slight_smile:

[Shreyas Srinivas]

I think the _ issue is less an issue with the tutorial. It’s more about 1. Giving lean users a tip. 2. Feedback to the lean devs

[Robin Arnez]

Mirek Olšák schrieb:

Let me know if there is a conclusion about what tip I should write to the text. To me, it feels a bit inconclusive so far. In the meantime, I at least added a tip on filling match ... with

Well, there's also batteries#1307 now

[Mirek Olšák]

Interesting, I just tried on lean 4 web, and it didn't work, let me try again

[Mirek Olšák]

It is not yet in the main release, right?

[Robin Arnez]

Well, it landed 2 hours ago

[Mirek Olšák]

ok cool, then I update the Lean version, and remove the "hack" again