Stream: Coq users

Topic: Ltac return an identifier

Louise Dubois de Prisque (Mar 25 2021 at 13:04):

Hello everyone !

I tried to write a tactic which does two things : it performs a tactic on the goal and it returns an identifier.
But I don't know how to make things work.
Indeed, if I do :

Ltac return_id := fun k => ( let x := fresh "test" in k ; x).

Goal False.
let y := return_id idtac in assert (y : True).

I get this error message : Ltac variable y is bound to <tactic closure> which cannot be coerced to an introduction pattern.

So, as soon as a tactic both performs something on the context and return an identifier, I cannot bound the variable as I intended to.
If someone has an idea or know if it is an intrinsic limitation of Ltac, let me know.
Thanks :)

Pierre-Marie Pédrot (Mar 25 2021 at 13:04):

This is a limitation of Ltac.

Pierre-Marie Pédrot (Mar 25 2021 at 13:05):

You can work around this using CPS style.

Guillaume Melquiond (Mar 25 2021 at 13:23):

This is an intrinsic (and really dumb) limitation of Ltac, but you can easily work around it by putting your tactic (here k) inside a dummy match goal with block. I think @Jason Gross has a very nice explanation of the mechanism somewhere but I do not remember where it is.

Pierre-Marie Pédrot (Mar 25 2021 at 13:26):

Indeed, match goal allows to force thunks.

Pierre-Marie Pédrot (Mar 25 2021 at 13:26):

But you have to be careful about what you return, sometimes it can bite you.

Guillaume Melquiond (Mar 25 2021 at 13:27):

Ltac return_id k :=
  let x := fresh "test" in
  let _ := match goal with _ => k end in
  x.

Jason Gross (Mar 25 2021 at 13:33):

Explanation: https://github.com/coq/coq/issues/4732#issuecomment-337542429

Louise Dubois de Prisque (Mar 25 2021 at 13:34):

Thank you @Guillaume Melquiond , @Pierre-Marie Pédrot and @Jason Gross. Indeed, this works well with the match goal with trick

Jason Gross (Mar 25 2021 at 13:37):

I'm nearly certain I explained it in more detail with more references somewhere in the 545-message-long conversation at https://github.com/coq/coq/pull/12103 (and perhaps some of my explanation even made it into the reference manual), but unfortunately finding the location where I referenced #4732 in that long PR discussion is non-trivial. If @Jim Fehrle gets email notifications on PRs he's made, he may be able to search his email for my comments on that issue mentioning lazymatch or "phase" (as in "tactic expression evaluation phase") and find a link to the relevant comment relatively easily.

Jason Gross (Mar 25 2021 at 13:41):

@Guillaume Melquiond I would not call it a "limitation" so much as an artifact of the fact that Ltac1 has non-function thunks, the syntax for forcing thunks entered the language sort-of by accident, and the decisions about which constructs are thunked by default vs not is sort-of an accident of history. In this case, it's sometimes useful to be able to bind a tactic to a name without running it eagerly, and you need match if you want to run it eagerly before binding it to the name.

Pierre-Marie Pédrot (Mar 25 2021 at 13:43):

you don't really have access to actual forcing, because match focusses.

Guillaume Melquiond (Mar 25 2021 at 13:46):

My point of view is a bit different. If at some point Coq encounters something that is not a tactic, it should just return the value rather than error out. (This does not contradict anything you have said about thunk vs non-thunk, just that Coq is too eager to error out while it could progress.)

Jim Fehrle (Mar 25 2021 at 18:10):

@Jason Gross I think you're looking for https://github.com/coq/coq/pull/12103#discussion_r423382531? I still had the email. Finding it in the PR requires showing everything marked "Show resolved" or "Hidden" before you do a text search. About 90 items. IMHO trivial but tedious :smile:
The harder problem is when you're searching for a concept rather than a specific string.

Jason Gross (Mar 25 2021 at 18:43):

Thanks!

Last updated: Oct 04 2023 at 23:01 UTC