Michael Soegtrop (Dec 07 2023 at 18:21): Michael Soegtrop (Dec 07 2023 at 18:21):One strange effect when I use Ltac2 in proofs is that sometimes global names hide local names where this is unexpected. Here is an example:
Require Import Ltac2.Ltac2.
Definition x:=true.
Example E1: forall (x: nat), x=x.
Proof.
intros x.
assert(x=0).
results in
Error: In environment
x : nat
The term "0" has type "nat" while it is expected to have type "bool".
Is this a bug?
Michael Soegtrop (Dec 07 2023 at 18:22):(This is with 8.18.0)
Pierre-Marie Pédrot (Dec 07 2023 at 18:23):This is documented in the paragraph about the non-strict mode: https://coq.inria.fr/refman/proof-engine/ltac2.html#strict-vs-non-strict-mode
Pierre-Marie Pédrot (Dec 07 2023 at 18:24):This is a conscious design choice, the problem is that the other behaviour makes the tactic non-monotonic (and thus fragile).
Pierre-Marie Pédrot (Dec 07 2023 at 18:24):Use &x wherever possible, and even better, switch the strict mode on.
Gaëtan Gilbert (Dec 07 2023 at 18:49):switch the strict mode on
that's possible?
Pierre-Marie Pédrot (Dec 07 2023 at 20:32):I thought we had a flag, hadn't we?
Gaëtan Gilbert (Dec 07 2023 at 20:40):there's nothing near the doc you linked at least
Paolo Giarrusso (Dec 07 2023 at 21:42):What does "non-monotonic" mean? And it seems both choices differ from the binding behavior of lambda calculus and refine
Paolo Giarrusso (Dec 07 2023 at 21:46):And what's the semantics of Std.VarRef? https://coq.inria.fr/doc/V8.18.0/stdlib/Ltac2.Std.html has the syntax (with no comment).
Paolo Giarrusso (Dec 07 2023 at 21:49):ah, non-monotonicity is explained better later, in https://coq.inria.fr/refman/proof-engine/ltac2.html#static-semantics
Paolo Giarrusso (Dec 07 2023 at 21:50):There is a simple reason for that, which is that the following expression would not make sense in general. [...] Indeed, a hypothesis can suddenly disappear from the runtime context if some other tactic pulls the rug from under you.
Rather, the tactic writer has to resort to the dynamic goal environment, and must write instead explicitly that she is accessing a hypothesis, typically as follows.
Paolo Giarrusso (Dec 07 2023 at 21:53):So, I guess the semantics of VarRef is explained by the following text, which does not mention VarRef.
&x as an Ltac2 expression expands to hyp @x.
Internalization is also referenced before being introduced.
Pierre-Marie Pédrot (Dec 07 2023 at 22:58):VarRef is just a constructor of an AST, the tactics taking this type as an argument are the ones responsible for what happens
Paolo Giarrusso (Dec 07 2023 at 23:01):Sure, but lambda abstraction and application are also just constructors.
Paolo Giarrusso (Dec 07 2023 at 23:02):Doesn't stop one from describing what they mean — say "a reference to a hypothesis"
Michael Soegtrop (Dec 08 2023 at 09:38):@Pierre-Marie Pédrot : As far as I remember you said in a previous thread that inside a proof script, that is when not defining an Ltac2 tactic but using Ltac2 as proof script commands, we are in non strict mode. And usually this does work inside a proof script, but it does not work for using assert inside a proof script.
Last updated: Oct 12 2024 at 12:01 UTC