sneakiness with `auto_param`

Stream: general

[Scott Morrison]

I would like to be able to change the tactic specified via auto_param to fill in a structure field automatically.

[Scott Morrison]

I know I can't actually do it, so I would like a nice workaround.

[Scott Morrison]

Somehow I want to write

structure F :=
(t : Type . sneaky)

and then for a while during the development have sneaky do one thing, and then be able to utter a secret incantation, after which sneaky does something else.

[Scott Morrison]

For example, the sneaky tactic could in some way inspect the environment, and delegate its actual work to a different tactic based on what it sees.

[Scott Morrison]

Does anyone know what I'm looking for?

[Scott Morrison]

I already do a little bit of this: my tidy tactic looks for definitions tagged with the @[tidy] attribute, and if they are of type tactic unit it also invokes them during it's attempt to solve a goal.

[Scott Morrison]

But now I want something slight different: e.g. have sneaky call the last-to-be-defined tactic tagged with @[sneaky_implementation], or something like that.

[Mario Carneiro]

Here's a way to do it if you want to have only one implementation at a given time:

@[user_attribute]
meta def sneaky_attr : user_attribute :=
{ name := `sneaky_impl,
  descr := "implementation for sneaky",
  before_unset := some $ λ _ _, skip,
  after_set := some $ λ n _ _, do
    env ← get_env,
    ns ← attribute.get_instances sneaky_attr.name,
    ns.mmap (λ n', when (n ≠ n') $ unset_attribute sneaky_attr.name n'),
    attribute.get_instances sneaky_attr.name >>= trace }

meta def sneaky : tactic unit :=
do [n] ← attribute.get_instances sneaky_attr.name,
  monad.join (mk_const n >>= eval_expr (tactic unit))

structure F :=
(t : Type . sneaky)

@[sneaky_impl] meta def mk_nat : tactic unit :=
trace "running mk_nat" >> `[exact nat]

example : F := {} -- running mk_nat

@[sneaky_impl] meta def mk_sorry : tactic unit :=
trace "running mk_sorry" >> `[sorry]

example : F := {} -- running mk_sorry

[Mario Carneiro]

Each time you define a tactic with @[sneaky_impl], the last one to have it has it unset, and sneaky calls which ever definition has the attribute right now

[Mario Carneiro]

Alternatively, you could have the attributes remain permanently, but you just check which was the last to be written

[Scott Morrison]

awesome! I didn't know about those hooks on attributes.

[Scott Morrison]

okay, so next I want approval to use this in mathlib. :-) Later in my category theory work, I really rely on most of the functoriality (oops, map_comp :slight_smile:) and naturality fields being filled in automatically by tidy or obviously. Of course, it's going to be a little while before tidy is mathlib ready, and maybe much longer before obviously is. I'd really like to be able to keep using them in my work, however... (in particular, I'm going to need to leave in "in action" everywhere in my later category theory stuff while I try and get them ready mathlib ready).

[Scott Morrison]

So... the hope is that I can have the id_comp, comp_id, assoc, map_id, map_comp and naturality fields all invoke a tactic defined like sneaky above.

[Scott Morrison]

In mathlib for now they will do nothing. In my development they will hook into whatever I want them to. Eventually, hopefully, they will start doing something in mathlib too.

[Johan Commelin]

But what would the first mathlib version of sneaky do?

[Scott Morrison]

`[skip]

[Scott Morrison]

So if you don't provide the field explicitly, you just get the usual error message about an unsolved goal.

[Johan Commelin]

Hmmm. Sorry, I don't get what your strategy is.

[Johan Commelin]

Does that mean that you still have to prove this stuff by hand in mathlib?

[Johan Commelin]

If so, why would you want a sneaky?

[Scott Morrison]

If you look at https://github.com/leanprover/mathlib/blob/master/category_theory/category.lean#L43

[Mario Carneiro]

because he wants the auto param for a structure defined in mathlib to call his tactic

[Scott Morrison]

you'll see that category.assoc is already marked with the auto_param obviously.

[Scott Morrison]

it's just that obviously in mathlib is just defined to be skip. ( a few lines above!)

[Scott Morrison]

I want to leave it like that in mathlib (for now), but still be able to use it outside while I'm getting it ready.

[Mario Carneiro]

I'm okay with this in principle. I always thought that the static nature of auto params made them a bit limited, but this is a nice way to forward reference

[Mario Carneiro]

I just need to figure out how to structure it nicely

[Scott Morrison]

obviously it would make sense to write something slightly more general than sneaky above :-)

[Mario Carneiro]

One thing which bothers me about this proposal is that you probably want to have just one sneaky which then goes everywhere

[Scott Morrison]

I'm not sure what you mean?

[Scott Morrison]

I'm imagining we could set up an attribute that you use like @[replace tidy] meta def foo : tactic unit := ...

[Scott Morrison]

and then as an auto_param you put in (field : Type . invoke_tidy)

[Scott Morrison]

and invoke_tidy goes and finds the latest declaration tagged with @[replace tidy].

[Mario Carneiro]

is tidy parametric here? what else can you replace

[Scott Morrison]

well, I was imagining that other people might want to replace other things

[Scott Morrison]

but maybe that's not helpful...

[Mario Carneiro]

I agree. But how would that work?

[Scott Morrison]

I don't really know about parameters to attributes, so I was just dreaming there.

[Scott Morrison]

I was imagining that you'd only define an attribute once, just like sneaky but taking a parameter.

[Scott Morrison]

For each value of that parameter you'd have to make a definition of an invoke_XXX tactic

[Scott Morrison]

that would then invoke the last thing tagged with @[replace XXX]

[Scott Morrison]

For me, I'm happy to have a single tactic for all of those fields (and many others later)

[Scott Morrison]

as long as I can still hook into it post mathlib

[Mario Carneiro]

Oh wow, I tried using sneaky_impl with local attributes and it actually went back to the old definition after the section closed

[Mario Carneiro]

@[sneaky_impl] meta def mk_nat : tactic unit :=
trace "running mk_nat" >> `[exact nat]

example : F := {} -- running mk_nat

section
meta def mk_sorry : tactic unit :=
trace "running mk_sorry" >> `[sorry]
local attribute [sneaky_impl] mk_sorry

example : F := {} -- running mk_sorry
end

example : F := {} -- running mk_nat

[Scott Morrison]

Nice! (I think?)

[Mario Carneiro]

I guess that's the power of functional data structures, you get "time travel" for free

[Johan Commelin]

That means that you could add particular superpowers, but not others, to tidy, depending on the file you are working in?

[Scott Morrison]

Yes

[Scott Morrison]

I already do this all the time, actually, just at a whole file level.

[Scott Morrison]

For me so far the definition of tidy has been invariant, except that it looks up everything marked with @[tidy] and tries those tactics too.

[Scott Morrison]

Mario's observation means you can do it at section level too, which I hadn't really appreciated.

[Mario Carneiro]

Check out https://github.com/leanprover/mathlib/blob/master/tactic/replacer.lean for my attempt at a general framework

[Mario Carneiro]

def_replacer tidy
structure T := (t : Type . tidy)

@[tidy] meta def tac1 := tactic.trace "tac1"
example : T := {} -- tac1

@[tidy] meta def tac2 (prev : tactic unit) := prev >> tactic.trace "tac2"
example : T := {} -- tac1 tac2

@[tidy] meta def tac3 := tactic.trace "tac3"
example : T := {} -- tac3