Call tactic by name

Stream: metaprogramming / tactics

[Scott Morrison]

Suppose I want to write a tactic foo that calls an interactive tactic bar. One simple way to do this is

import tactic.bar

meta def foo : tactic unit := `[bar]

Now suppose that I insist on not importing tactic.bar in the file where I define foo. I am happy to rely on the user to have also imported tactic.bar by the time foo is actually invoked. Thus I want foo to run a parser on the string "bar" at invocation time, and then run the discovered tactic.

Is there a simple way to achieve this?

I see that something along these lines happens at https://github.com/leanprover-community/mathlib/blob/master/src/tactic/hint.lean#L40, but this is doing something slightly different (resolving the "`[bar]" to an expr, and making a new declaration from it).

[Mario Carneiro]

Do you need to use the interactive parser here? (the `[ ... ])? It is a lot easier if you can write out the expr directly

[Scott Morrison]

Sorry, I should #xy. All I want to do is take a file that has a tactic that calls `[ring], and avoid the need to have import tactic.ring.

[Mario Carneiro]

that still doesn't quite answer my question. Is it possible for you to refactor the original file so that it does not need to use the `[] notation? It is the difference between calling a function which is looked up at tactic execution time (easy) and running a parser that only exists at tactic execution time (hard)

[Mario Carneiro]

Here's an example for calling `[ring]:

#eval do
  let e := (expr.const `tactic.interactive.ring []).app (`(@none unit):expr),
  tac ← eval_expr (tactic unit) e,
  tac

If at runtime the tactic.interactive.ring declaration exists, it will be executed, otherwise it fails with a unknown declaration 'tactic.interactive.ring' error

[Scott Morrison]

Great, that does it. I wanted to hack tactic.linarith so it doesn't need to import tactic.ring or tactic.norm_num (until, obviously, at runtime). This trick (and the variants which handle `[ring!] and `[norm_num]) is exactly what I wanted. I'm trying to sort out what exactly needs to be ported to port linarith, and the huge imports for tactic.ring were getting in the way.

[Yaël Dillies]

Oh that's interesting. I would like something similar to happen for positivity because having it defined after the point of declaration of many lemmas whose assumptions it could fulfill measn we can't use it as out_param there.

[Yaël Dillies]

This is of course a worse version fo Heather's new tactic, but quite a cheap one were the imports not getting in the way.

[Mario Carneiro]

I don't think we want to land something like that though, because import tactic.linarith and then using linarith shouldn't result in a crash

[Mario Carneiro]

What huge imports does tactic.ring have? I would assume it only needs basic properties of ring, i.e. algebra.ring.basic or so

[Yaël Dillies]

The answer is the same, always.

[Yaël Dillies]

The algebraic order hierarchy gets back into the pure algebraic hierarchy in several points because of concrete structures and the way we fix defeqs with forgetful inheritance.

[Yaël Dillies]

In that case, you need to define rat.cast before you can define field.

[Yaël Dillies]

This is very annoying and it keeps causing me headaches.

[Scott Morrison]

I agree we should be very cautious about actually landing this. A weird compromise might be for import tactic.linartih to do the import tactic.ring and import tactic.norm_num, while leaving the tactic/linarith/*.lean files without those imports. This would mean that hopefully no one gets a surprising failure from linarith, but it's still easy to pare down imports and see what is really being used.

[Mario Carneiro]

I'm not sure I understand the reasoning here though. linarith does use ring, it will fail if you try to call it without ring available

[Mario Carneiro]

it would make more sense to do this for norm_num's lemmas