Stream: Ltac2

Topic: Introducing in the context

Guillaume Melquiond (Feb 03 2022 at 14:18):

I am trying to achieve the equivalent of intro in Ltac2, and I am failing. Here is one of my tries:

Std.intro None None;
let x :=
  lazy_match! reverse goal with
  | [ h : _ |- _ ] => h
  end in
...

I would expect x to contain an identifier that I could then use with &x. It does indeed contain an identifier from the context, but it is a random one. How can I get the one produced by Std.intro?

Pierre-Marie Pédrot (Feb 03 2022 at 14:20):

x should contain the identifier, but beware that &x doesn't do what you believe it does. With this syntax it just looks for the hypothesis named with the literal x, not the bound variable x.

Pierre-Marie Pédrot (Feb 03 2022 at 14:20):

Use Control.hyp to do that.

Pierre-Marie Pédrot (Feb 03 2022 at 14:21):

Alternatively, why don't you provide an identifier to intro? You could generate it with the Fresh module.

Guillaume Melquiond (Feb 03 2022 at 14:22):

As I said in the other thread, I have a hard time recovering a useful ident.
Anyway, the documentation says: "&x as a Coq constr expression expands to ltac2:(Control.refine (fun () => hyp @x))." So, isn't that exactly your suggestion? What am I missing?

Pierre-Marie Pédrot (Feb 03 2022 at 14:23):

@x means the literal ident x

Guillaume Melquiond (Feb 03 2022 at 14:23):

Oh!

Pierre-Marie Pédrot (Feb 03 2022 at 14:24):

(we should probably have a shorter syntax for Control.hyp but that's another story that opens bikeshedding mode)

Guillaume Melquiond (Feb 03 2022 at 14:25):

So, if I understand correctly, I should never use & and @ in Ltac2 scripts, should I?

Pierre-Marie Pédrot (Feb 03 2022 at 14:25):

Why not?

Pierre-Marie Pédrot (Feb 03 2022 at 14:25):

You never use "foo" in ML?

Guillaume Melquiond (Feb 03 2022 at 14:27):

But how would I guess the actual literal name of a binder?

Pierre-Marie Pédrot (Feb 03 2022 at 14:27):

you mean the stuff introduced by intros? tough luck on that one

Pierre-Marie Pédrot (Feb 03 2022 at 14:28):

instead, you should 1. generate a fresh ident, 2. introduce it and 3. return it as a value

Pierre-Marie Pédrot (Feb 03 2022 at 14:28):

like the infamously broken intro x; ... [some stuff mentioning x] in Ltac

Pierre-Marie Pédrot (Feb 03 2022 at 14:28):

that is, define a tactic fresh_intro : unit -> ident that you can use this way

Guillaume Melquiond (Feb 03 2022 at 14:28):

So, yes, that is my point, I never have an identifier at hand I can use with & and @, unless I am missing something.

Pierre-Marie Pédrot (Feb 03 2022 at 14:29):

it happens sometimes that the identifier is guaranteed to be preserved

Pierre-Marie Pédrot (Feb 03 2022 at 14:29):

e.g. refine (fun x => ...) guarantees that the last binder is going to be x

Pierre-Marie Pédrot (Feb 03 2022 at 14:29):

but yes, &x should mostly be reserved for inline proofs

Pierre-Marie Pédrot (Feb 03 2022 at 14:30):

as for @ that's another story, if you want to generate a fresh name with a given prefix obviously you'll use that

Pierre-Marie Pédrot (Feb 03 2022 at 14:30):

at least Ltac2 makes a difference between these concepts, and doesn't try at runtime to guess what you meant

Guillaume Melquiond (Feb 03 2022 at 14:33):

By the way, I am constantly writingltac2:(Control.refine (fun () => foo)). Is there some other way? If not, I would gladly have some ltac2val:(foo) to make it shorter.

Pierre-Marie Pédrot (Feb 03 2022 at 14:33):

from Ltac1 you mean? or from a constr?

Guillaume Melquiond (Feb 03 2022 at 14:33):

From constr.

Pierre-Marie Pédrot (Feb 03 2022 at 14:34):

there is the $x syntax

Guillaume Melquiond (Feb 03 2022 at 14:34):

Sorry, I meant that foo is a complex term. I was under the impression that $x only applies to an identifier.

Pierre-Marie Pédrot (Feb 03 2022 at 14:35):

yes, in this case you should let-bind the term to an Ltac2 variable

Gaëtan Gilbert (Feb 03 2022 at 14:35):

how's that different from just foo?

Pierre-Marie Pédrot (Feb 03 2022 at 14:35):

like let x := '(my complex term) in ... ($x) ...

Pierre-Marie Pédrot (Feb 03 2022 at 14:36):

(assuming the term makes sense in the toplevel context)

Guillaume Melquiond (Feb 03 2022 at 14:36):

Unfortunately, I cannot. Because I am usually in a context where I cannot bind an Ltac2 variable, e.g., constr:(forall x, ltac2:(Control.refine (fun () => something that needs to see x))).

Pierre-Marie Pédrot (Feb 03 2022 at 14:37):

you can always define your own notation, in this case

Pierre-Marie Pédrot (Feb 03 2022 at 14:38):

I am not sure that it's a great idea to write this kind of terms with quotations

Pierre-Marie Pédrot (Feb 03 2022 at 14:38):

it's currently lacking from the very barebone Ltac2 libraries but instead you should use some HOAS API

Pierre-Marie Pédrot (Feb 03 2022 at 14:39):

so, e.g. a function forall_ : constr -> (constr -> constr) -> constr

Pierre-Marie Pédrot (Feb 03 2022 at 14:39):

that one you can define it with quotations or low-level functions

Pierre-Marie Pédrot (Feb 03 2022 at 14:39):

by the way, this is one case where you're guaranteed statically that x will keep its name

Pierre-Marie Pédrot (Feb 03 2022 at 14:40):

inside a quotation, for any identifier the last introduced binder with this name is guaranteed to be preserved

Guillaume Melquiond (Feb 03 2022 at 14:54):

I am not sure HOAS would help here. The thing that needs to see x in the context are evars. So, I am not quite sure how I would even write the constr -> constr part of forall_.

Guillaume Melquiond (Feb 03 2022 at 14:56):

As I said in the other thread, I ended up writing a function evar that produces an evar with a given type. And this evar is only meaningful in a given context. So, I have things like:

Control.refine (fun _ => open_constr:(fun x : $t => _ : ltac2:(Control.refine (fun () => evar 'Prop))))

Pierre-Marie Pédrot (Feb 03 2022 at 15:33):

not very pretty, please open PRs if you want to get closer to a 'batteries included' state

Guillaume Melquiond (Feb 03 2022 at 15:41):

Pierre-Marie Pédrot said:

e.g. refine (fun x => ...) guarantees that the last binder is going to be x

So, I just tried it, and unfortunately, it does not seem to be true. If I do the following:

Control.refine (fun () => open_constr:(fun x : nat => _ : (_ : Prop))) ;
Control.focus 1 1 (fun () =>
Message.print (Message.of_constr (Control.goal ())) ;
let y := constr:(eq &x) in
Control.refine (fun () => open_constr:(fun x : nat => _ : (_ : Prop))) ;
Control.focus 1 1 (fun () =>
Message.print (Message.of_constr (Control.goal ())) ;
let y := constr:($y &x) in
Message.print (Message.of_constr y))).

the final term being printed is x = x, while I would expect x0 = x. (The intermediate prints are just there to double-check that I am focusing the correct subgoals.)
So, I cannot rely on refine (fun x => ...) guaranteeing anything about the name of the last binder.
Am I missing something?

Pierre-Marie Pédrot (Feb 03 2022 at 15:48):

that one is another issue (or call it a design choice if you want) which is that there has been a variable capture on an open var

Pierre-Marie Pédrot (Feb 03 2022 at 15:48):

I didn't claim anything about that situation, btw

Pierre-Marie Pédrot (Feb 03 2022 at 15:48):

my claim is about referring to the dynamic environment from within a quotation

Pierre-Marie Pédrot (Feb 03 2022 at 15:49):

here you built a term eq x that refers to a context variable x but then you pull the rug under the feet of that term because you change the dynamic environment to another one

Pierre-Marie Pédrot (Feb 03 2022 at 15:50):

it's your responsibility to check that the environment you're using the term in makes sense

Pierre-Marie Pédrot (Feb 03 2022 at 15:50):

(you could get into way worse situations, e.g. clearing the variable or changing its type)

Pierre-Marie Pédrot (Feb 03 2022 at 15:51):

That's another argument for HOAS, also, because it prevents this kind of situation (the renaming is implicit)

Guillaume Melquiond (Feb 03 2022 at 16:00):

Pierre-Marie Pédrot said:

here you built a term eq x that refers to a context variable x but then you pull the rug under the feet of that term because you change the dynamic environment to another one

I don't understand this part. The term eq x is already created. I am not trying to create it after the second refine.

Pierre-Marie Pédrot (Feb 03 2022 at 16:01):

Yes, it's already created and it's just eq x where x is a name

Pierre-Marie Pédrot (Feb 03 2022 at 16:01):

after the second refine, the last introduced binder is also x

Pierre-Marie Pédrot (Feb 03 2022 at 16:01):

so you get eq x x

Pierre-Marie Pédrot (Feb 03 2022 at 16:02):

the previous x was renamed into x0 in the dynamic context but we don't do anything for Ltac2 values

Pierre-Marie Pédrot (Feb 03 2022 at 16:02):

(and in general, we wouldn't be able to)

Pierre-Marie Pédrot (Feb 03 2022 at 16:04):

if instead of binding this term as an Ltac2 value, you had, say, posed it, you'd indeed see eq x0 x

Guillaume Melquiond (Feb 03 2022 at 16:08):

So, I am back to step one. I cannot trust &x. I have to manually create a fresh identifier.

Pierre-Marie Pédrot (Feb 03 2022 at 16:08):

what do you want to do exactly?

Pierre-Marie Pédrot (Feb 03 2022 at 16:10):

the original problem you raised at the beginning of the thread is solved IIUC

Guillaume Melquiond (Feb 03 2022 at 16:11):

It is not, because your suggestion of using Control.hyp x suffers from the same shadowing issue. So, I cannot use that.

Pierre-Marie Pédrot (Feb 03 2022 at 16:11):

?

Pierre-Marie Pédrot (Feb 03 2022 at 16:11):

you want to intro a variable

Pierre-Marie Pédrot (Feb 03 2022 at 16:11):

you intro it, you look at its name, poof

Gaëtan Gilbert (Feb 03 2022 at 16:12):

So, I just tried it, and unfortunately, it does not seem to be true. If I do the following:

ah it's wellknown: ltac variable bypasses typechecking again
but with ltac2 instead

Pierre-Marie Pédrot (Feb 03 2022 at 16:12):

Ltac2 is no more evolved than Ltac1 in that regard

Pierre-Marie Pédrot (Feb 03 2022 at 16:12):

it inherits the same low-level code

Guillaume Melquiond (Feb 03 2022 at 16:13):

Pierre-Marie Pédrot said:

you intro it, you look at its name, poof

But its name is always x. So, whichever term I create using it sooner or later becomes invalid.

Pierre-Marie Pédrot (Feb 03 2022 at 16:13):

well, if you escape the context yes

Pierre-Marie Pédrot (Feb 03 2022 at 16:14):

if you do this in a well-scoped way, without any clear and generating a fresh ident at every intro you'll be fine

Pierre-Marie Pédrot (Feb 03 2022 at 16:15):

whichever term I create using it sooner or later becomes invalid.

terms within a context do have a shelf life, and that's this context

Last updated: Sep 09 2024 at 05:02 UTC