Michael Soegtrop (Mar 19 2021 at 17:23): 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.
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.
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)
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
.
Pierre-Marie Pédrot (Mar 19 2021 at 22:22):your workaround does that, but there is a much shorter notation, namely &z
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
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.
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)
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.
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.
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)
Pierre-Marie Pédrot (Mar 19 2021 at 22:27):actually the doc literally says that it'll prefer the global over the local.
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)
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.
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.
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?
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
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
Pierre-Marie Pédrot (Mar 20 2021 at 18:32):it can fail if there is no variable in the context with that name
Pierre-Marie Pédrot (Mar 20 2021 at 18:32):meanwhile, @x is an identifier.
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)
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.
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).
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
Pierre-Marie Pédrot (Mar 20 2021 at 18:35):Maybe it deserves to be swapped.
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.
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.
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: Dec 01 2023 at 06:01 UTC