@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.
This looks weird because it seems that you're in strict mode when you shouldn't.
There are two modes for Ltac2 (just as Ltac1 but this is hidden by dynamic typing)
in strict mode, variables from the context need to be explicitly accessed via the designated primitives
.
your workaround does that, but there is a much shorter notation, namely &z
in non-strict mode, there is leeway, i.e. the tactic tries to access first the local context, and otherwise go for the global
Strict is enforced for definitions, and inside a proof, there is an option to switch it, non-strict being the default.
(this is for easiness of writing and backwards compatibility, otherwise most terms would be a festival of &x &y &z)
So it looks like the quotation is incorrectly using the strict mode although the option should be set to non-strict.
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.
(see https://coq.inria.fr/refman/proof-engine/ltac2.html#strict-vs-non-strict-mode)
actually the doc literally says that it'll prefer the global over the local.
(which seems a weird design choice a posteriori, but I might be missing something right now)
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.
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?
& is for referring to local symbols, while @
no, these two expressions don't have the same type
the first one is a constr, and &x is a shorthand for Control.hyp @x
it can fail if there is no variable in the context with that name
meanwhile, @x
is an identifier.
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)
Can you point me to the place in the doc which says that?
That's in the link I posted.
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).
But I agree it's a bit surprising since it goes against the locality hierarchy
Maybe it deserves to be swapped.
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.
BTW I don't think I would consider writing definitions inside a proof to be a recommended practice.
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: Jun 01 2023 at 11:01 UTC