Writing tactics that invoke other tactics

Stream: general

[Dan Velleman]

I have written a tactic that examines the goal and then calls the apply tactic with different rules depending on the form of the goal. To write that tactic, I had to learn this pattern, which I copied from another tactic:
do r <- tactic.mk_mapp ..., tactic.apply r
Now I want to do something similar, but with rw instead of apply. Is there a similar pattern to construct the argument to pass to tactic.interactive.rw?
More generally, if I know what I would type when writing a proof in tactic mode to execute some tactic, is there a way to figure out how to invoke that tactic from another tactic?

[Rob Lewis]

There are a few options, depending on what you're trying to do. Are the rw calls always the same for a particular shape of the goal? Or are there parameters in the goal that need to be inserted into the rw call? If the former, you can "quote" the interactive rewrite that you want to do. `[rw [add.comm, add.assoc]] has type tactic unit.

[Rob Lewis]

In general, any tactic-mode proof can be inserted into `[ ... ]. But if you wanted to e.g. change the rw lemmas depending on some input to your tactic, this won't work easily.

[Dan Velleman]

Yes, there are parameters that I want to insert.

[Rob Lewis]

Then you'll have to choose between figuring out the parameters to docs#tactic.interactive.rw or docs#tactic.rewrite_target . The latter is simpler, but you need to give it a fully elaborated expression (like you did for apply) instead of just the name of a lemma.

[Rob Lewis]

For the former: at the second argument (the location thingy) it suffices to put (interactive.loc.ns [none]) which says "do this rewrite on the goal"

[Rob Lewis]

In the first argument you need to give it {rules := [], end_pos := none} where the rules field is a list of docs#tactic.interactive.rw_rule

[Rob Lewis]

The pos field there is (I think) for error reporting. You can give it junk values but you might get oddly placed error messages.

[Dan Velleman]

OK, thanks.

[Rob Lewis]

The general pattern here is that when an interactive tactic takes an argument of type parse t, t will have type parser T, and you can call the tactic directly by replacing that argument with a term of type T.

[Scott Morrison]

Often looking at the implementation of the interactive tactic you will see that it just does some argument parsing and then calls a non-interactive tactic, and this can be a good way to learn how to invoke the non-interactive version.