Arguments to defined tactic

Stream: general

[Jacob Neumann]

Hi all! I'm using Lean 3 and it's behaving in a way which has me absolutely baffled. Here's a mwe:

namespace foo
  variable {F : Type}

  meta def ex [has_add F] : tactic unit :=
    `[ assume x : F, assume y : F, exact (x+y) ]

  def Term [Add : has_add F]: F → F → F :=
  begin
    -- let p := Add.add,
    @ex F Add,
  end
end foo

It complains that the occurrence of Add after @ex F is undefined, even though the goal state is shown as

F: Type
Add: has_add F
⊢ F → F → F

and the commented-out line defining p in terms of Add works fine. Can anyone explain what's going on? Is there something special about passing arguments to tactics which I'm not understanding?
Thanks for the help!

[Patrick Massot]

Hi! You'll find it much easier to get help after reading #mwe and editing your question accordingly.

[Jacob Neumann]

Patrick Massot said:

Hi! You'll find it much easier to get help after reading #mwe and editing your question accordingly.

Sorry. Been trying to reproduce the same behavior in a mwe but having trouble. I'll edit it if I can

[Patrick Massot]

There is no need to be sorry. I'm not blaming you, I'm helping you getting help.

[Kevin Buzzard]

"minimal" is far less important than "working"; if you want to just dump 200 lines of code enabling someone else to see the error at their end then this would still make the question much easier to answer. However my personal experience is that minimising can sometimes help you solve your own problem! You remove some "irrelevant" line which "clearly" has nothing to do with anything and your problem magically goes away, and then the penny drops.

[Martin Dvořák]

Jacob Neumann said:

trying to reproduce the same behavior in a mwe but

Been there!

[Kevin Buzzard]

The answer to your question might be "type class inference doesn't look in your local context; try resetI if you want it to know about what is there" (but it might not be)

[Jacob Neumann]

Ok updated with mwe!

[Patrick Massot]

This is simply not how tactic writing works in Lean 3.

[Patrick Massot]

Did you read https://leanprover-community.github.io/extras/tactic_writing.html?

[Patrick Massot]

I need to go, but I'll write more later if nobody else does it in the mean time.

[Patrick Massot]

The example is so minimized that it is hard to solve the #xy issue, but maybe meditating on the following will help a tiny bit:

meta def ex : tactic unit :=
  `[assume x : F, assume y : F, exact (x+y) ]

def Term {F : Type*} [Add : has_add F]: F → F → F :=
begin
  ex,
end

[Jacob Neumann]

Yeah of course I've read the tutorial, but as far as I can tell it doesn't address this issue. I'm curious what you mean "that's not how tactic writing works in Lean 3"...to me it seems quite natural to write a tactic associated with a given type class, and to achieve this by taking in the instance as an argument to the tactic. If there's a more proper way to do so, I'd definitely be interested to know it. Thanks

[Patrick Massot]

This is not how you give arguments to tactics, as explained in the tutorial.

[Alex J. Best]

Lean is both a proof assistant and a programming language. So a tactic, simply put is an executable program that produces proofs. When you write a def that takes an argument has_add T this produces executable code that when executed calls the addition function provided. The argument is basically a pointer to some other function that yours can call when you want it to. This is not the same as a representation of the same function you can prove things about, it’s just a pointer. What you want to do instead is write a tactic that parses an expression representing a function (in many cases this is essentially just its name), this expression can then be substituted wherever you want when building proofs about this function, but cannot be directly executed, the function may not be computable after all, or we could be doing a proof by contradiction and no such function exists!

[Jacob Neumann]

Patrick Massot said:

This is not how you give arguments to tactics, as explained in the tutorial.

Sorry but I don't see what you mean. The tutorial contains examples where arguments are passed in like normal function arguments as well as examples where the arguments are extracted from the local context using parsing identifiers. I assume the latter is what you intend, but it's still not clear to me (nor addressed in the tutorial) when to use the former and when to use the latter, and why having a tactic accept an argument like Add is forbidden.

[Johan Commelin]

But in those examples the types of those arguments are usually something like expr or parse ident.

[Johan Commelin]

That's not true for your MWE

[Johan Commelin]

The example about reflection is an exception to that rule.

[Patrick Massot]

Johan is right. Specifically you need to read again https://leanprover-community.github.io/extras/tactic_writing.html#parsing-locations-and-expressions.

[Jacob Neumann]

Johan Commelin said:

But in those examples the types of those arguments are usually something like expr or parse ident.

Sure but there are numerous examples where arguments of type nat or list are accepted. Why not has_add F?

[Johan Commelin]

Where do you see those numerous examples?

[Jacob Neumann]

Johan Commelin said:

Where do you see those numerous examples?

In tactic.lean. Likeiterate_exactly for instance

[Johan Commelin]

Note that that is not an interactive tactic.

[Jacob Neumann]

Johan Commelin said:

Note that that is not an interactive tactic.

Oh okay so non-interactive tactics can take usual arguments, but interactive ones are confined to just expr, parse ident and the like? Is there a documentation of what can be passed to interactive tactics?

[Johan Commelin]

Anything can be passed to anything. The question is whether it is useful. You probably want to use expr and parse foo as explained in the tutorial.

[Eric Wieser]

Maybe it helps to realize that within a tactic, you don't have an actual term F : Type, you have the term `(F) : expr

[Kyle Miller]

In Lean 3, you're not really able to write tactic macros of the type you want using `[...] notation (Lean 4 lets you do something like that though.)

It's not a very sophisticated way to make tactics, and you should just assume that everything in this notation has no access to any of the arguments to the function. I'm sure there are exceptions, but the tactic writing tutorial doesn't show any of them (in fact, it only mentions `[...] twice.)

[Jacob Neumann]

Kyle Miller said:

In Lean 3, you're not really able to write tactic macros of the type you want using `[...] notation (Lean 4 lets you do something like that though.)

It's not a very sophisticated way to make tactics, and you should just assume that everything in this notation has no access to any of the arguments to the function. I'm sure there are exceptions, but the tactic writing tutorial doesn't show any of them (in fact, it only mentions `[...] twice.)

My original example is written as a do block, so that's just a feature of the mwe. But same result

[Sebastian Ullrich]

The tactic state lives in a symbolic world of terms, while the program of a tactic lives in a concrete world of runtime values. As it is not a priori possible to freely move values between these two phases, it does not make sense for a tactic to take a symbolic value such as F above. Other systems such as Ltac may behave very differently in this regard.