tactic modes(?)

Stream: metaprogramming / tactics

[Reid Barton]

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

[Reid Barton]

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

[Rob Lewis]

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

[Simon Hudon]

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

[Kevin Buzzard]

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]

:up: that's one of the handful

[Kevin Buzzard]

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

[Reid Barton]

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?

[Simon Hudon]

Yes

[Bryan Gin-ge Chen]

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]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Simon Hudon]

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

[Reid Barton]

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]

Ha! Sorry to mislead you like this!

[Simon Hudon]

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

[Simon Hudon]

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]

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]

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]

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]

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]

sorry, that path only goes one way

[Mario Carneiro]

tactics can't run parsers

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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]

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

[Mario Carneiro]

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]

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

[Reid Barton]

presumably as macros or something?

[Mario Carneiro]

yes, it has those things

[Reid Barton]

I see

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

and then use to_expr right

[Mario Carneiro]

Isn't that exactly what a parameter does?

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

There is expr.replace I think

[Mario Carneiro]

which was updated to work on pexprs at some point

[Reid Barton]

this looks fancy

[Reid Barton]

but, it also looks like it only works on expr

[Reid Barton]

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

[Mario Carneiro]

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

[Rob Lewis]

Not me

[Mario Carneiro]

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

[Mario Carneiro]

this was something like 18 months ago or so

[Mario Carneiro]

pexprs need a general overhaul to make them more lean friendly

[Simon Hudon]

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

[Reid Barton]

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]

yes, that will work

[Reid Barton]

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

[Adam Topaz]

Is there a tactic for that?