Stream: Coq users

Topic: Declaring & as an infix notation breaks other notations


view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 17:57):

As the title says. I thought it might be fixable with appropriate scopes, but apparently not.

Require Import ssrbool.
Check [&& true, true & true]. (* everything is fine *)

Variable (T : Type).
Declare Scope T_scope.
Bind Scope T_scope with T.

Variable (f : T -> T -> T).
Infix "&" := f (at level 60) : T_scope.
Check [&& true, true & true]. (* fails *)
(* Syntax error: ',' or '&' expected after [term level 200] (in [term]). *)

What does work is declaring "&" at level 200, but that doesn't feel like a real solution... Is there a way to use & in such a notation, or should I just give up and pick another symbol?

view this post on Zulip Michael Soegtrop (Mar 10 2021 at 17:59):

Afaik scopes change the interpretation of the parse tree but not the parser. If you declare a notation the parser is changed, regardless what the scope is.

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:10):

So having a way of interpreting a & b just stops Coq from realizing that it is not even well-typed and looking for a different interpretation that uses more surrounding symbols? Must we always avoid notations that are substrings of existing notations?

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:11):

That can't be right, at the very least both a < b and a < b < c exist and one is a substring of the other.

view this post on Zulip Christian Doczkal (Mar 10 2021 at 19:21):

If you look at the point where the levels of the two notations are fixed (Coq.Init.Notations) you find:

Reserved Notation "x < y" (at level 70, no associativity).
Reserved Notation "x < y < z" (at level 70, y at next level).

The point here is, that the levels of the first/only < is the same in both notations, allowing the parser to parse both notations depending on what comes after.

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:30):

So that's why defining "&" at level 200 works, and there is no other workaround?

view this post on Zulip Christian Doczkal (Mar 10 2021 at 19:36):

I don't know what exactly you mean by "it works" for level "200". It still does not seem to parse x & x, it only parses the iterated conjunction.

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:38):

Oh, you're right, I forgot to check that.

view this post on Zulip Christian Doczkal (Mar 10 2021 at 19:38):

But yes, I would stay away from using an infix &, it's not only used in all the n-ary operators, but also & A is notation for (_ : A) and it occurs again in the notation for sigT: { x : T & T_ x}

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:41):

Fair enough, but this makes me a bit sad. I don't suppose you have any ideas for a symbol that means conjunction and is not yet being used in a number of notations?

view this post on Zulip Christian Doczkal (Mar 10 2021 at 19:44):

It depends a bit on your editor, emacs+company-coq has has decent support for entering unicode symbols. So you might even be able to take a symbol that gets mapped to exactly the same glyph. Not that I'm really suggesting this, but it could be a possibility.

view this post on Zulip Christian Doczkal (Mar 10 2021 at 19:44):

But yes, Unicode is probably the way to go for one-symbol infix notations.

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:46):

Haha yeah, I'm a bit allergic to fancy unicode symbols for some reason, but I guess I can't complain of lack of symbols if I refuse to use 75% of them. Thank you for the help!

view this post on Zulip Christian Doczkal (Mar 10 2021 at 19:48):

More like 99,9%, but yes. Of course, this doesn't solve the problem that one still cannot load two libraries together that use the same symbols with different precedence. But that's a topic for another discussion. :grinning:

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 19:53):

(I did briefly wonder which number to pick, but I admit I'm surprised and that on second thought I shouldn't be)
Has that discussion been had anywhere that I could read?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 10 2021 at 20:12):

@Ana de Almeida Borges maybe you can do what you using custom entrie

view this post on Zulip Emilio Jesús Gallego Arias (Mar 10 2021 at 20:13):

Indeed scopes are used for resolution after-parsing, so in that sense notations at the parsing level are global and have to shared, however we recently added support for user-defined "entries" [really, non-terminals if you would like to think that way] which allow for you to define a totally different grammar without conflicting with the usual "entry" that represents for example a Coq term [named constr]

view this post on Zulip Ana de Almeida Borges (Mar 10 2021 at 20:48):

Wow, I had no idea this was a thing. Thank you! It certainly looks like it would solve my issue.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 10 2021 at 21:36):

Most welcome! The whole setup is a bit experimental but with the goal to actually cover your use case, so don't hesitate to open issues about things that can be improved


Last updated: Jan 28 2023 at 06:30 UTC