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?

(This is with 8.18.0)

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

This is a conscious design choice, the problem is that the other behaviour makes the tactic non-monotonic (and thus fragile).

Use &x wherever possible, and even better, switch the strict mode on.

switch the strict mode on

that's possible?

I thought we had a flag, hadn't we?

there's nothing near the doc you linked at least

What does "non-monotonic" mean? And it seems both choices differ from the binding behavior of lambda calculus and refine

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).

ah, non-monotonicity is explained better later, in https://coq.inria.fr/refman/proof-engine/ltac2.html#static-semantics

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.

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.

VarRef is just a constructor of an AST, the tactics taking this type as an argument are the ones responsible for what happens

Sure, but lambda abstraction and application are also just constructors.

Doesn't stop one from describing what they mean — say "a reference to a hypothesis"

@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