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.
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.)
I do see the inconsistency, though. I guess my suggested solution would be to fix exact
..
Yeah, in general Ltac1 has hardwired support for parsing argument constrs, but in retrospective it's a bad idea.
I agree that all constr-only Ltac2 functions shouldn't be declared through a notation.
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?
Notation != syntactic alias.
Syntactic aliases implicitly thunk their argument
but it doesn't require adding a parsing rule
so you write refine 'x
and it's expanded to Control.refine (fun () => open_constr:(x))
Syntax is not modular so every time you add a parsing rule you break some code out there
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?
it's a phase that occurs before type-checking
it's just that some global definitions have a special status and are expanded syntactically
nothing else
So, refine x
systematically thunks its argument?
yes
in practice it's what you want most of the time (hence the fundamental dilemma of Ltac1 between forced values and lazy tactics)
Sure, but with this "in practice" argument, I also always want to pass an open constr to refine
.
no, because that one is a different grammar
and it's not true
sometimes you want to pass an Ltac2 variable
When I say "I", I mean "I".
you never pass meta variables to refine?
you're free to add a notation if you want
but it shouldn't be exposed by default in Ltac2, that's it
the less parsing rules, the more modular
Why would I pass a meta-variable to refine? What does it even achieve?
Ltac foo := intro x; refine x?
(meta as in Ltac variable, not a Meta as in the AST)
No, I would certainly use exact
here.
aha, but it doesn't use the same unification algo
also it's very bad for HO stuff
like, passing refine
as an argument to a tactical is hell in Ltac1
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).
whatever (and these two things are not equivalent)
you're free to add your own notations in your devs
but you'll have a hard time convincing me that we need more Ltac1-like crappy notations in Ltac2
You are absolutely right. That is why I will keep using Control.refine
.
Last updated: Dec 07 2023 at 17:01 UTC