The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

On Sun, Feb 5, 2017 at 5:46 AM, Andreas Abel <abela AT chalmers.se> wrote:

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.

True, however not really what's under discussion here. Here we are seeing that identifiers are not properly substituted, showing that the semantics for interpreting terms inside Ltac is wrong. It's not a matter of printing.

 

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

Amusing, indeed :)

Best,

Beta

 

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/