## Stream: metaprogramming / tactics

### Topic: tactic modes(?)

#### Reid Barton (Sep 18 2020 at 17:44):

Is there documentation on (or, failing that, some examples of) writing new tactic modes such as conv?

#### Reid Barton (Sep 18 2020 at 17:44):

@Simon Hudon what's the link to your temporal logic tactic? I poked around your github repos but didn't see it

#### Rob Lewis (Sep 18 2020 at 17:46):

I've followed the smt mode from core as an example, the handful of times I've tried to do this

#### Simon Hudon (Sep 18 2020 at 17:46):

Here it is: https://github.com/unitb/temporal-logic

#### Kevin Buzzard (Sep 18 2020 at 17:47):

The natural number game used some kind of modded tactic mode begin [natnumgame] and Rob Lewis wrote some code which ported most of the tactics over and let me redefine a few

#### Rob Lewis (Sep 18 2020 at 17:47):

:up: that's one of the handful

#### Kevin Buzzard (Sep 18 2020 at 17:48):

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/tactic/nat_num_game.lean

#### Reid Barton (Sep 18 2020 at 17:53):

Thanks all. So I gather begin [smt] ... end means something like smt.interactive.execute t where t is the result of parsing the begin-end block using the smt.interactive namespace. And I guess if I want to support something like conv { ... }, then I just need to define my_tac.interactive.itactic := my_tac unit to represent the body and the parser will automatically use the my_tac parser for it?

Yes

#### Bryan Gin-ge Chen (Sep 18 2020 at 18:17):

There are a few tiny examples in the Lean tests as well: tests/lean/interactive/my_tac_class.lean, tests/lean/run/my_tac_class.lean, tests/lean/interactive/rb_map_ts.lean

#### Reid Barton (Sep 18 2020 at 18:18):

I found a helpful comment at https://github.com/unitb/temporal-logic/blob/master/src/temporal_logic/tactic.lean#L17-L31
clearly copied from somewhere else, but that's where I found it

#### Reid Barton (Sep 18 2020 at 18:19):

ah, it's indeed in the Lean C++ code somewhere

#### Mario Carneiro (Sep 18 2020 at 18:21):

https://github.com/leanprover-community/lean/blob/d907e6aed0b399f6512139c751b908979bf45eaf/src/frontends/lean/tactic_notation.cpp#L33-L52

#### Reid Barton (Sep 18 2020 at 18:31):

So with save_info, although all the examples I've found ultimately use tactic.to_formatto format the tactic state, I can also pass any old nonsense I like to save_info_thunk, right?

#### Reid Barton (Sep 18 2020 at 18:32):

(with the possible exception of the smt tactic which uses a different built-in formatter)

#### Simon Hudon (Sep 18 2020 at 18:34):

Yes that's right, that's where you feed in whatever you want to display

#### Reid Barton (Sep 18 2020 at 20:37):

To correct what I wrote earlier, Simon's temporal tactic does produce a custom format for the tactic state, it just does such a good job of imitating the standard one that I didn't notice :upside_down:

#### Simon Hudon (Sep 18 2020 at 20:39):

Ha! Sorry to mislead you like this!

#### Simon Hudon (Sep 18 2020 at 20:40):

Mainly what my pretty printing does is print hypotheses of the form h : Γ ⊢ φ as h : φ and omit the variable Γ from the context.

#### Simon Hudon (Sep 18 2020 at 20:41):

Was it hard to get it to build? I haven't ungraded it in a while (still in the process of upgrading the dependencies)

#### Reid Barton (Sep 18 2020 at 20:42):

Let's say it was not hard to get it to build to the point where I could inspect at least one [temporal] proof interactively

#### Reid Barton (Sep 18 2020 at 21:28):

In fact, what I want to do is broadly similar--basically I want to pretend that I have a variable x : X, while actually representing it by x : Γ → X.

#### Reid Barton (Sep 18 2020 at 21:30):

One thing I don't understand yet is what controls the environment that texpr gets parsed/typechecked in. When texpr is an argument of an interactive tactic, is the pexpr that gets passed to the tactic really independent of the environment? If it does depend on the environment, can I set the environment somehow?

#### Reid Barton (Sep 18 2020 at 22:12):

Oh, looking up a few inches I see

meta constant set_env : environment → parser unit


Can I run this from the tactic monad somehow? Or am I supposed to create a custom parser for my interactive tactics which manipulates the environment first? I see meta constant of_tactic : tactic α → parser α...

#### Mario Carneiro (Sep 18 2020 at 22:13):

sorry, that path only goes one way

#### Mario Carneiro (Sep 18 2020 at 22:14):

tactics can't run parsers

#### Mario Carneiro (Sep 18 2020 at 22:15):

Do you really want to replace the environment and not just the local context?

#### Reid Barton (Sep 18 2020 at 22:15):

I do just want to replace the local context but I don't understand how I'd do so

#### Mario Carneiro (Sep 18 2020 at 22:16):

An easy way is to revert_all and then backtrack when you are done

#### Reid Barton (Sep 18 2020 at 22:17):

that is, I want to have an underlying tactic state somewhere containing x : Γ → X but present to the user the illusion that x : X, and have my tactics fix up the expr in a certain way

#### Reid Barton (Sep 18 2020 at 22:18):

I guess what I don't really understand is how the parser knows what the local context is at all--couldn't I use some monad totally unrelated to tactic_state as my custom tactic monad?

#### Mario Carneiro (Sep 18 2020 at 22:18):

the parser doesn't have to care since it only produces pre-expressions

#### Mario Carneiro (Sep 18 2020 at 22:19):

If you are okay with the extra work the usual way I do more radical type reinterpretation is to perform post-processing directly on the pexpr, without calling to_expr on it

#### Reid Barton (Sep 18 2020 at 22:19):

ok, so does this mean a pre-expression might contain things like unresolved . syntax, overloaded notation, etc.?

#### Reid Barton (Sep 18 2020 at 22:20):

presumably as macros or something?

#### Mario Carneiro (Sep 18 2020 at 22:20):

yes, it has those things

I see

#### Mario Carneiro (Sep 18 2020 at 22:21):

If you need to change name resolution then things get a bit more tricky

#### Reid Barton (Sep 18 2020 at 22:21):

I guess that's fine for the "operate directly on the pexpr" approach since I want to replace x.foo by (x i).foo or whatever anyways

#### Mario Carneiro (Sep 18 2020 at 22:22):

in your case you can probably send it to to_expr after your fixups to still get most of lean goodness

#### Reid Barton (Sep 18 2020 at 22:22):

in fact, I basically just want to do a bunch of substitutions of the form "replace x by x i" so maybe this functionality already exists

#### Reid Barton (Sep 18 2020 at 22:22):

and then use to_expr right

#### Mario Carneiro (Sep 18 2020 at 22:22):

Isn't that exactly what a parameter does?

#### Reid Barton (Sep 18 2020 at 22:25):

I guess so? though here the parameter i will be another local constant

#### Reid Barton (Sep 18 2020 at 22:25):

I was thinking more along the lines of Lean knowing how perform substitution in general

#### Mario Carneiro (Sep 18 2020 at 22:25):

well technically if you are in a section then the parameter is in your local context

#### Mario Carneiro (Sep 18 2020 at 22:26):

There is expr.replace I think

#### Mario Carneiro (Sep 18 2020 at 22:26):

which was updated to work on pexprs at some point

this looks fancy

#### Reid Barton (Sep 18 2020 at 22:30):

but, it also looks like it only works on expr

#### Reid Barton (Sep 18 2020 at 22:31):

anyways, this is more than enough to keep me busy for a while

#### Mario Carneiro (Sep 18 2020 at 22:31):

@Rob Lewis Didn't you PR something like this?

Not me

#### Mario Carneiro (Sep 18 2020 at 22:32):

IIUC the only thing needed to make expr.replace work on pexprs is to generalize the signature

#### Mario Carneiro (Sep 18 2020 at 22:32):

this was something like 18 months ago or so

#### Mario Carneiro (Sep 18 2020 at 22:33):

pexprs need a general overhaul to make them more lean friendly

#### Simon Hudon (Sep 18 2020 at 22:34):

I think I made such adjustment for expr.fold the same should work for expr.replace

#### Reid Barton (Sep 18 2020 at 22:36):

Mario Carneiro said:

IIUC the only thing needed to make expr.replace work on pexprs is to generalize the signature

so, you're saying I can just unchecked_cast it :smiling_devil:

#### Mario Carneiro (Sep 18 2020 at 22:37):

yes, that will work

#### Reid Barton (Sep 18 2020 at 22:38):

is this the formal version of proof by reference to personal communication

#### Adam Topaz (Sep 19 2020 at 00:06):

Is there a tactic for that?

Last updated: May 09 2021 at 22:13 UTC