How can I prevent Coq notations in closed scopes interfering with notations in open ones?

I'm fairly new to Coq, and I'm trying to use ListNotations in Coq so that I can write lists like [ 1 ; 2 ] rather than cons 1 (cons 2 nil). However, I'm using a library that defines its own notation for the ; character. I was thinking that I could simply close the right scopes so that the notation I want is visible, but it's not working as I expected.

As a simple example, if I create a file test.v:

Declare Scope example_scope.
Notation "a ; b" := (or a b) (at level 50) : example_scope.
Close Scope example_scope.

Require Import List.
Import ListNotations.
Locate ";".
Compute [ 1 ; 2 ].

...then the output of coqc test.v is:

Notation
"a ; b" := or a b : example_scope
"[ x ; y ; .. ; z ]" := cons x (cons y .. (cons z nil) ..) : list_scope
(default interpretation)
File "./test.v", line 8, characters 10-15:
Error: Unknown interpretation for notation "_ ; _".

If the top three lines are removed from test.v, then it works fine.

Two questions:

Why does this happen? It seems to recognize that the notation I want exists and marks it as the "default interpretation." So then why does it become an "unknown notation" when I try to use it?
What can I do in my code (without altering the top three lines of test.v, for example) to get the notation I want?

Solution

Why does this happen? It seems to recognize that the notation I want exists and marks it as the "default interpretation." So then why does it become an "unknown notation" when I try to use it?

There are three points to be aware in this case:

Even if the notations definitions (a.k.a. interpretations) are indeed attached to a scope (or to the default scope), their syntactic definition "goes beyond a given scope" (namely, there is a Reserved Notation vernacular that defines the precedence level and associativity for a notation, independently of the scope).

Here is a related remark in the "Reserving notations" section of Coq refman:

Coq expects all uses of the notation to be defined at the same precedence and with the same associativity. [emphasis mine] To avoid giving the precedence and associativity every time, this command declares a parsing rule (string) in advance without giving its interpretation.

So, your example does not satisfy this rule, as the two occurrences of the ; operands have a different precedence level:
```
Print Grammar constr. (* tested using Coq 8.11.1 *)

…
| "50" LEFTA
  [ SELF;  ";"; NEXT
  | …

| "0" LEFTA
  [  "[";  "]"
  |  "["; constr:operconstr LEVEL "200";  ";"; constr:operconstr LEVEL "200";
     ";"; LIST1 (constr:operconstr LEVEL "200") SEP ";";  "]"
  |  "["; constr:operconstr LEVEL "200";  ";"; constr:operconstr LEVEL "200";
     "]"
  |  "["; constr:operconstr LEVEL "200";  "]"
  | …
```
(200 being the default precedence level for inner expressions)
Sometimes, it happens we want to define two notations which share some tokens, typically x < y and x < y < z, to borrow the example from the "Simple factorization rules" section of Coq refman:

Coq extensible parsing is performed by Camlp5 which is essentially a LL1 parser: it decides which notation to parse by looking at tokens from left to right. Hence, some care has to be taken not to hide already existing rules by new rules. Some simple left factorization work has to be done. Here is an example.
```
Notation "x < y" := (lt x y) (at level 70).
Fail Notation "x < y < z" := (x < y /\ y < z) (at level 70).
(*…*)
Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
```
Even if this remark is loosely related to your example, it highlights the fact that defining several notations that share several tokens (a common prefix) can be feasible by tuning the precedence level of the inner sub-expressions.
Last but not least, it appears that combining the notations a ; b and [x ; y ; .. ; z] leads to an ambiguous syntax, because (assuming the precedence-level issue mentioned in point 1. were solved), if both scopes are opened, how do you distinguish between cons True (cons True nil) and cons (or True True) nil? both would be a possible interpretation of [True; True].

What can I do in my code (without altering the top three lines of test.v, for example) to get the notation I want?

I guess you can't.

Adding

Notation "a ; b" := (or a b) (at level 50) : example_scope.

at the beginning of your module has an (unintended) side-effect that cannot be workarounded afterwards.

If you really need a semicolon-like notation for or, maybe you could try using ;;, for example:

Notation "a ;; b" := (or a b) (at level 50) : example_scope.

More generally, it seems quite risky to use a mere "separator" (semicolon or comma) as a binary operator: usually, a single ; or , will only be used within (square) brackets.

Finally as an aside, using square brackets in notations (even if ListNotations do so) might confuse the parser in some cases. So regarding lists in particular, if ever you are a math-comp user, you may want to rely on the seq theory instead, which is fully compatible with the Coq standard library (Notation seq := list.), has a comprehensive set of lemmas, and introduce this alternative notation which doesn't rely on a leading single square bracket:

Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: .. [:: xn] ..)
  (at level 0, format "[ :: '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]"
  ) : seq_scope.