Stream: Ltac2

Topic: Gallina globals hide locals in Ltac2 terms


view this post on Zulip Michael Soegtrop (Mar 19 2021 at 17:23):

@Pierre-Marie Pédrot : this behavior is unexpected (to me):

Require Import Ltac2.Ltac2.
Require Import Ltac2.Option.

Ltac2 rct(x : constr) := Control.refine (fun () => x).

Set Default Proof Mode "Classic".

Parameter z : nat.

Example global_hides_local: forall (x z : nat), x=0 -> z=0 -> True.
intros x z Hz Hx.

(* If there is a glocal variable with the same name as the local, ltac2 seems to pick the global *)
Fail ltac2:(assert(z=0) by assumption).

(* If there is no glocal variable with the same name, it works as expected *)
ltac2:(assert(x=0) by assumption).

(* One can get in the local variable into the ltac2 term, but it is a bit complicated *)
let f := ltac2:(z |- assert((ltac2:(rct (Option.get (Ltac1.to_constr z))))=0) by assumption) in f z.

trivial.
Qed.

Is this a bug or is there a good reason why this is so? It definitely makes things much harder because one never knows what globals are around.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:21):

This looks weird because it seems that you're in strict mode when you shouldn't.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:22):

There are two modes for Ltac2 (just as Ltac1 but this is hidden by dynamic typing)

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:22):

in strict mode, variables from the context need to be explicitly accessed via the designated primitives
.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:22):

your workaround does that, but there is a much shorter notation, namely &z

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:23):

in non-strict mode, there is leeway, i.e. the tactic tries to access first the local context, and otherwise go for the global

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:24):

Strict is enforced for definitions, and inside a proof, there is an option to switch it, non-strict being the default.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:24):

(this is for easiness of writing and backwards compatibility, otherwise most terms would be a festival of &x &y &z)

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:25):

So it looks like the quotation is incorrectly using the strict mode although the option should be set to non-strict.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:26):

This qualifies as a bug (somehow) but as noted, it is recommended to use &x when you know that you're referring to a context variable.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:26):

(see https://coq.inria.fr/refman/proof-engine/ltac2.html#strict-vs-non-strict-mode)

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:27):

actually the doc literally says that it'll prefer the global over the local.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 22:28):

(which seems a weird design choice a posteriori, but I might be missing something right now)

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 08:57):

I see. I must say it was not so clear to me what the difference between a reference and an identifier was from the manual - now I think it is clear: & is for referring to local symbols, while @is referring to global symbols.

Hmm, but then, why does this work:

Require Import Ltac2.Ltac2.
Require Import Ltac2.Option.

Ltac2 rct(x : constr) := Control.refine (fun () => x).

Set Default Proof Mode "Classic".

Example global_hides_local: forall (z : nat), z=0 -> z=0.
intros z Hz.

assert(forall P, P -> P -> P) as DuplicateGoal by tauto.
apply DuplicateGoal.
ltac2:(exact &Hz).
ltac2:(exact @Hz).

Qed.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 09:06):

actually the doc literally says that it'll prefer the global over the local.

Can you point me to the place in the doc which says that? I can't find it, but I guess this is due to a lack of understanding something in this way.

(which seems a weird design choice a posteriori, but I might be missing something right now)

Indeed, since this means that defining a new global can break existing code, which is not a desirable property.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 09:09):

Btw.: I frequently prototype Ltac2 definitions inside a proof because it takes me a while to get to the point I want to automate. When I do an Ltac2 definition inside a proof, is it in strict or in non-strict mode?

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:31):

& is for referring to local symbols, while @

no, these two expressions don't have the same type

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:32):

the first one is a constr, and &x is a shorthand for Control.hyp @x

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:32):

it can fail if there is no variable in the context with that name

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:32):

meanwhile, @x is an identifier.

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:33):

it never fails and is just a way to easily input a name (similarly to a quoted string "x" which is just a shorthand for the contents)

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:33):

Can you point me to the place in the doc which says that?

That's in the link I posted.

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:35):

Indeed, since this means that defining a new global can break existing code, which is not a desirable property.

Well, the same happens swapping global for local, so there is no good solution here. I think the motivation was that it makes easier to copy-paste a snippet from a proof (in non-strict mode) into a tactic definition (in strict mode).

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:35):

But I agree it's a bit surprising since it goes against the locality hierarchy

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:35):

Maybe it deserves to be swapped.

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:38):

When I do an Ltac2 definition inside a proof, is it in strict or in non-strict mode?

Strict, for any definition. I thought there was an option to tweak that, but I don't find it neither in the code nor in the documentation so it's probably something I forgot to add.

view this post on Zulip Pierre-Marie Pédrot (Mar 20 2021 at 18:38):

BTW I don't think I would consider writing definitions inside a proof to be a recommended practice.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 18:54):

Thanks for the explanations!

BTW I don't think I would consider writing definitions inside a proof to be a recommended practice.

As I said, I do this only to develop automation where it takes me a few minutes to get to the point in the proof where I call it. This way I have a turn around time of seconds, otherwise of a few minutes. When I am ready with the automation, I copy it out of the proof.


Last updated: Jan 31 2023 at 09:01 UTC