The Coq mailing list

[Andreas Abel <abela AT chalmers.se>]

Printing identifiers in a real-world proof assistant setting is a hard 
problem in the sense that, in practice, people don't get it right.  And 
this is because it is a "boring" problem.  I pay a bottle of Champagne 
to the next one who gets a paper on printing identifiers in a sound and 
practically useful way into POPL.

If you want to amuse yourself with problems of that sort on our side, 
you can start reading here

  https://github.com/agda/agda/issues/998

and follow tags like "printing", "display", "shadowing" to dig out more...

On 03.02.2017 14:34, Beta Ziliani wrote:
> Thanks Bruno and Maxime.
>
> It is a bug then, although a tough one to fix, I suppose.
>
> FWIW, In MetaCoq we used to have the de Bruijn context. Recently we
> decided to drop it and only use the named context; same as Ltac. But
> unlike Ltac, when we introduce the de Bruijn variables in the named
> context, we also rename the code, therefore changing x to x0 *inside the
> exact*, as should be done.
>
> Best,
> Beta
>
> On Fri, Feb 3, 2017 at 10:18 AM, Maxime Dénès 
> <mail AT maximedenes.fr
> <mailto:mail AT maximedenes.fr>>
>  wrote:
>
>     Hi Beta,
>
>     I can't answer your question, since I'm not sure how much of Ltac's
>     binding is documented, but I can try to explain the symptom.
>
>     Since your binder clashes with the section variable name, the rooster
>     renames it on the fly. But then of course "x" designates the section
>     variable.
>
>     The following script should illustrate what goes on under the hood:
>
>     Section test.
>     Variable x : nat.
>     Definition ex := fun x y:nat=>ltac:(exact (x0 + y)).
>     Print ex.
>
>     Maxime.
>
>     On 02/03/17 13:56, Beta Ziliani wrote:
>     > Hi list,
>     >
>     > I stumble across what I think is an odd behavior when mixing named and
>     > dB contexts, and I’m going to file it as a bug unless someone
>     convinces
>     > me that this is a feature:
>     >
>     > |Section test. Variable x : nat. Definition ex := fun x
>     > y:nat=>ltac:(exact (x + y)). Print ex. |
>     >
>     > outputs
>     >
>     > |ex = fun _ y : nat => x + y : nat -> nat -> nat |
>     >
>     > I am expecting, of course,
>     >
>     > |ex = fun x y : nat => x + y : nat -> nat -> nat |
>     >
>     > Note that defining `x` in a |Section| is important; if I make |x|
>     a top
>     > level variable, the example is constructed as expected.
>     >
>     > Best,
>     > Beta
>     >
>     > ​


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www.cse.chalmers.se/~abela/