Stream: Ltac2

Topic: Notation for refine


view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 14:41):

The notation for refine is defined as

Ltac2 Notation refine := Control.refine.

As a consequence, the syntax differs from plain Ltac, while most tactics try to have the same syntax in both Ltac1 and Ltac2.

Is there a reason it is not defined as follows?

Ltac2 Notation refine c(thunk(open_constr)) := Control.refine c.

view this post on Zulip Janno (Feb 04 2022 at 14:48):

exact is defined like that and I think it is a mistake to make Ltac2 code look like Ltac1. I prefer refine '(my term) over refine (my term). (As a consequence I never use exact because it forces me to write exact $x when I have already let-bound my term to x. Which I almost always do anyway.)

view this post on Zulip Janno (Feb 04 2022 at 14:48):

I do see the inconsistency, though. I guess my suggested solution would be to fix exact..

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:08):

Yeah, in general Ltac1 has hardwired support for parsing argument constrs, but in retrospective it's a bad idea.

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:08):

I agree that all constr-only Ltac2 functions shouldn't be declared through a notation.

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:09):

But then you would not even be able to write refine x. You would have to fall back to refine (fun () => x), wouldn't you?

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:10):

Notation != syntactic alias.

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:10):

Syntactic aliases implicitly thunk their argument

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:10):

but it doesn't require adding a parsing rule

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:11):

so you write refine 'x and it's expanded to Control.refine (fun () => open_constr:(x))

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:12):

Syntax is not modular so every time you add a parsing rule you break some code out there

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:12):

How does that work? Is that type-directed? If you write refine x, Coq checks the type of x and if it is not of type unit -> constr, it thunks it?

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:12):

it's a phase that occurs before type-checking

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:12):

it's just that some global definitions have a special status and are expanded syntactically

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:12):

nothing else

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:13):

So, refine x systematically thunks its argument?

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:13):

yes

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:14):

in practice it's what you want most of the time (hence the fundamental dilemma of Ltac1 between forced values and lazy tactics)

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:15):

Sure, but with this "in practice" argument, I also always want to pass an open constr to refine.

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:15):

no, because that one is a different grammar

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:15):

and it's not true

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:15):

sometimes you want to pass an Ltac2 variable

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:16):

When I say "I", I mean "I".

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:16):

you never pass meta variables to refine?

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:16):

you're free to add a notation if you want

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:17):

but it shouldn't be exposed by default in Ltac2, that's it

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:17):

the less parsing rules, the more modular

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:17):

Why would I pass a meta-variable to refine? What does it even achieve?

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:17):

Ltac foo := intro x; refine x?

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:18):

(meta as in Ltac variable, not a Meta as in the AST)

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:18):

No, I would certainly use exact here.

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:18):

aha, but it doesn't use the same unification algo

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:19):

also it's very bad for HO stuff

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:19):

like, passing refine as an argument to a tactical is hell in Ltac1

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:20):

And even if I were to use refine here, I would never write Ltac foo := let x := fresh in intro x; refine x. I would write Ltac foo := refine (fun x => x).

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:21):

whatever (and these two things are not equivalent)

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:21):

you're free to add your own notations in your devs

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2022 at 15:21):

but you'll have a hard time convincing me that we need more Ltac1-like crappy notations in Ltac2

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 15:22):

You are absolutely right. That is why I will keep using Control.refine.


Last updated: Jan 31 2023 at 10:01 UTC