Syntax error with < in Coq notations

Link:: https://stackoverflow.com/q/42239138

Display all goals and responses

Question

The following code:

Reserved Notation "g || t |- x < y" (at level 10).

Inductive SubtypeOf :
  GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set :=
| SubRefl :
  forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType),
    gamma || theta |- u < u
where "g || t |- x < y" := (SubtypeOf g t x y).

gives the following error:

Syntax error: '<' expected after [constr:operconstr level 200] (in [constr:operconstr])

I get a similar error if I use <: in place of <.

But this code works fine:

Reserved Notation "g || t |- x << y" (at level 10).

Inductive SubtypeOf :
  GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set :=
| SubRefl :
  forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType),
    gamma || theta |- u << u
where "g || t |- x << y" := (SubtypeOf g t x y).

Why? Is there a precedence setting that can be changed to allow < or <: in notation? Is there built-in syntax that I'm colliding with, and need to watch for when defining notations?

Answer

Coq uses an LL1 parser to process notations. It also can output the grammar. So, let's check what we are getting with the following

Reserved Notation "g || t |- x < y" (at level 10).

Print Grammar constr.Entry constr is
[ LEFTA
  [ "@"; global; univ_annot
  | term LEVEL "8" ] ]
and lconstr is
[ LEFTA
  [ term LEVEL "200" ] ]
where binder_constr is
[ LEFTA
  [ "exists2"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; ","; term LEVEL
    "200"; "&"; term LEVEL "200"
  | "exists2"; "'"; pattern LEVEL "0"; ","; term LEVEL "200"; "&"; term LEVEL
    "200"
  | "exists2"; name; ":"; term LEVEL "200"; ","; term LEVEL "200"; "&"; term
    LEVEL "200"
  | "exists2"; name; ","; term LEVEL "200"; "&"; term LEVEL "200"
  | "exists"; "!"; open_binders; ","; term LEVEL "200"
  | "exists"; open_binders; ","; term LEVEL "200"
  | "IF"; term LEVEL "200"; "then"; term LEVEL "200"; "else"; term LEVEL
    "200"
  | "forall"; open_binders; ","; term LEVEL "200"
  | "fun"; open_binders; "=>"; term LEVEL "200"
  | "let"; "fix"; fix_decl; "in"; term LEVEL "200"
  | "let"; "cofix"; cofix_body; "in"; term LEVEL "200"
  | "let"; "'"; pattern LEVEL "200"; ":="; term LEVEL "200"; "in"; term LEVEL
    "200"
  | "let"; "'"; pattern LEVEL "200"; ":="; term LEVEL "200"; case_type; "in";
    term LEVEL "200"
  | "let"; "'"; pattern LEVEL "200"; "in"; pattern LEVEL "200"; ":="; term
    LEVEL "200"; case_type; "in"; term LEVEL "200"
  | "let"; name; binders; let_type_cstr; ":="; term LEVEL "200"; "in"; term
    LEVEL "200"
  | "let"; [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":=";
    term LEVEL "200"; "in"; term LEVEL "200"
  | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else";
    term LEVEL "200"
  | "fix"; fix_decls
  | "cofix"; cofix_decls ] ]
and term is
[ "200" RIGHTA
  [ binder_constr ]
| "100" RIGHTA
  [ SELF; "<:"; term LEVEL "200"
  | SELF; "<<:"; term LEVEL "200"
  | SELF; ":"; term LEVEL "200"
  | SELF; ":>" ]
| "99" RIGHTA
  [ SELF; "->"; term LEVEL "200" ]
| "95" RIGHTA
  [ SELF; "<->"; NEXT ]
| "90" RIGHTA
  [  ]
| "85" RIGHTA
  [ SELF; "\\/"; term LEVEL "85" ]
| "80" RIGHTA
  [ SELF; "/\\"; term LEVEL "80" ]
| "75" RIGHTA
  [ "~"; term LEVEL "75" ]
| "70" RIGHTA
  [ SELF; ">"; NEXT
  | SELF; ">="; NEXT
  | SELF; "<"; NEXT; "<="; NEXT
  | SELF; "<"; NEXT; "<"; NEXT
  | SELF; "<"; NEXT
  | SELF; "<="; NEXT; "<"; NEXT
  | SELF; "<="; NEXT; "<="; NEXT
  | SELF; "<="; NEXT
  | SELF; "<>"; NEXT; ":>"; NEXT
  | SELF; "<>"; NEXT
  | SELF; "="; NEXT; "="; NEXT
  | SELF; "="; NEXT; ":>"; NEXT
  | SELF; "="; NEXT ]
| "60" RIGHTA
  [ SELF; "++"; term LEVEL "60"
  | SELF; "::"; term LEVEL "60" ]
| "50" LEFTA
  [ SELF; "||"; NEXT
  | SELF; "-"; NEXT
  | SELF; "+"; NEXT ]
| "40" LEFTA
  [ SELF; "&&"; NEXT
  | SELF; "/"; NEXT
  | SELF; "*"; NEXT ]
| "35" RIGHTA
  [ "/"; term LEVEL "35"
  | "-"; term LEVEL "35" ]
| "30" RIGHTA
  [ SELF; "^"; term LEVEL "30" ]
| "10" LEFTA
  [ SELF; "||"; term LEVEL "200"; "|-"; term LEVEL "200"; "<"; NEXT
  | SELF; LIST1 arg
  | "@"; global; univ_annot; LIST0 NEXT
  | "@"; pattern_ident; LIST1 identref ]
| "9" LEFTA
  [ ".."; term LEVEL "0"; ".." ]
| "8" LEFTA
  [  ]
| "1" LEFTA
  [ SELF; ".("; "@"; global; LIST0 (term LEVEL "9"); ")"
  | SELF; ".("; global; LIST0 arg; ")"
  | SELF; "%"; IDENT ]
| "0" LEFTA
  [ IDENT "ltac"; ":"; "("; ltac_expr; ")"
  | "("; term LEVEL "200"; ","; term LEVEL "200"; ","; LIST1 (term LEVEL
    "200") SEP ","; ")"
  | "("; term LEVEL "200"; ","; term LEVEL "200"; ")"
  | "("; term LEVEL "200"; ")"
  | "{|"; record_declaration; '|}'
  | "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "&"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "&"; term LEVEL
    "200"; "&"; term LEVEL "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "&"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "|"; term LEVEL
    "200"; "&"; term LEVEL "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "|"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; "|"; term LEVEL "200"; "&"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; "|"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "&"; term LEVEL "200"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "&"; term LEVEL "200"; "&";
    term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "|"; term LEVEL "200"; "&";
    term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "|"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "|"; term LEVEL "200"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "|"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "}"
  | "{"; binder_constr; "}"
  | "`{"; term LEVEL "200"; "}"
  | "`("; term LEVEL "200"; ")"
  | atomic_constr
  | term_match
  | test_array_opening; "["; "|"; array_elems; "|"; lconstr; type_cstr;
    test_array_closing; "|"; "]"; univ_annot ] ]

outputs:

...
| "10" LEFTA
  [ SELF; "||"; term LEVEL "200"; "|-"; term LEVEL "200"; "<"; NEXT
...

Here,

10 is our precedence level;
LEFTA means left associativity;
200 is the default precedence level for inner subexpressions.

Taking into account the fact that a lower level binds more tightly than a higher level and the fact that the level of < is 70 (see Coq.Init.Notations), we can deduce that Coq is trying to parse the x < y part as a subexpression for x, consuming the < token, hence the error message.

To remedy the situation we can explicitly disallow parsing the third parameter as the less-than expression by assigning x higher precedence, i.e. a lower level.

Reserved Notation "g || t |- x < y" (at level 10, x at level 69).

Print Grammar constr.Entry constr is
[ LEFTA
  [ "@"; global; univ_annot
  | term LEVEL "8" ] ]
and lconstr is
[ LEFTA
  [ term LEVEL "200" ] ]
where binder_constr is
[ LEFTA
  [ "exists2"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; ","; term LEVEL
    "200"; "&"; term LEVEL "200"
  | "exists2"; "'"; pattern LEVEL "0"; ","; term LEVEL "200"; "&"; term LEVEL
    "200"
  | "exists2"; name; ":"; term LEVEL "200"; ","; term LEVEL "200"; "&"; term
    LEVEL "200"
  | "exists2"; name; ","; term LEVEL "200"; "&"; term LEVEL "200"
  | "exists"; "!"; open_binders; ","; term LEVEL "200"
  | "exists"; open_binders; ","; term LEVEL "200"
  | "IF"; term LEVEL "200"; "then"; term LEVEL "200"; "else"; term LEVEL
    "200"
  | "forall"; open_binders; ","; term LEVEL "200"
  | "fun"; open_binders; "=>"; term LEVEL "200"
  | "let"; "fix"; fix_decl; "in"; term LEVEL "200"
  | "let"; "cofix"; cofix_body; "in"; term LEVEL "200"
  | "let"; "'"; pattern LEVEL "200"; ":="; term LEVEL "200"; "in"; term LEVEL
    "200"
  | "let"; "'"; pattern LEVEL "200"; ":="; term LEVEL "200"; case_type; "in";
    term LEVEL "200"
  | "let"; "'"; pattern LEVEL "200"; "in"; pattern LEVEL "200"; ":="; term
    LEVEL "200"; case_type; "in"; term LEVEL "200"
  | "let"; name; binders; let_type_cstr; ":="; term LEVEL "200"; "in"; term
    LEVEL "200"
  | "let"; [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":=";
    term LEVEL "200"; "in"; term LEVEL "200"
  | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else";
    term LEVEL "200"
  | "fix"; fix_decls
  | "cofix"; cofix_decls ] ]
and term is
[ "200" RIGHTA
  [ binder_constr ]
| "100" RIGHTA
  [ SELF; "<:"; term LEVEL "200"
  | SELF; "<<:"; term LEVEL "200"
  | SELF; ":"; term LEVEL "200"
  | SELF; ":>" ]
| "99" RIGHTA
  [ SELF; "->"; term LEVEL "200" ]
| "95" RIGHTA
  [ SELF; "<->"; NEXT ]
| "90" RIGHTA
  [  ]
| "85" RIGHTA
  [ SELF; "\\/"; term LEVEL "85" ]
| "80" RIGHTA
  [ SELF; "/\\"; term LEVEL "80" ]
| "75" RIGHTA
  [ "~"; term LEVEL "75" ]
| "70" RIGHTA
  [ SELF; ">"; NEXT
  | SELF; ">="; NEXT
  | SELF; "<"; NEXT; "<="; NEXT
  | SELF; "<"; NEXT; "<"; NEXT
  | SELF; "<"; NEXT
  | SELF; "<="; NEXT; "<"; NEXT
  | SELF; "<="; NEXT; "<="; NEXT
  | SELF; "<="; NEXT
  | SELF; "<>"; NEXT; ":>"; NEXT
  | SELF; "<>"; NEXT
  | SELF; "="; NEXT; "="; NEXT
  | SELF; "="; NEXT; ":>"; NEXT
  | SELF; "="; NEXT ]
| "69" RIGHTA
  [  ]
| "69" RIGHTA
  [  ]
| "69" RIGHTA
  [  ]
| "69" RIGHTA
  [  ]
| "60" RIGHTA
  [ SELF; "++"; term LEVEL "60"
  | SELF; "::"; term LEVEL "60" ]
| "50" LEFTA
  [ SELF; "||"; NEXT
  | SELF; "-"; NEXT
  | SELF; "+"; NEXT ]
| "40" LEFTA
  [ SELF; "&&"; NEXT
  | SELF; "/"; NEXT
  | SELF; "*"; NEXT ]
| "35" RIGHTA
  [ "/"; term LEVEL "35"
  | "-"; term LEVEL "35" ]
| "30" RIGHTA
  [ SELF; "^"; term LEVEL "30" ]
| "10" LEFTA
  [ SELF; "||"; term LEVEL "200"; "|-"; term LEVEL "69"; "<"; NEXT
  | SELF; LIST1 arg
  | "@"; global; univ_annot; LIST0 NEXT
  | "@"; pattern_ident; LIST1 identref ]
| "9" LEFTA
  [ ".."; term LEVEL "0"; ".." ]
| "8" LEFTA
  [  ]
| "1" LEFTA
  [ SELF; ".("; "@"; global; LIST0 (term LEVEL "9"); ")"
  | SELF; ".("; global; LIST0 arg; ")"
  | SELF; "%"; IDENT ]
| "0" LEFTA
  [ IDENT "ltac"; ":"; "("; ltac_expr; ")"
  | "("; term LEVEL "200"; ","; term LEVEL "200"; ","; LIST1 (term LEVEL
    "200") SEP ","; ")"
  | "("; term LEVEL "200"; ","; term LEVEL "200"; ")"
  | "("; term LEVEL "200"; ")"
  | "{|"; record_declaration; '|}'
  | "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "&"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "&"; term LEVEL
    "200"; "&"; term LEVEL "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "&"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "|"; term LEVEL
    "200"; "&"; term LEVEL "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "|"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; "|"; term LEVEL "200"; "&"; term LEVEL
    "200"; "}"
  | "{"; "'"; pattern LEVEL "0"; "|"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "&"; term LEVEL "200"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "&"; term LEVEL "200"; "&";
    term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "|"; term LEVEL "200"; "&";
    term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; ":"; term LEVEL "200"; "|"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "|"; term LEVEL "200"; "&"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "|"; term LEVEL "200"; "}"
  | "{"; term LEVEL "99"; "}"
  | "{"; binder_constr; "}"
  | "`{"; term LEVEL "200"; "}"
  | "`("; term LEVEL "200"; ")"
  | atomic_constr
  | term_match
  | test_array_opening; "["; "|"; array_elems; "|"; lconstr; type_cstr;
    test_array_closing; "|"; "]"; univ_annot ] ]

...
| "10" LEFTA
  [ SELF; "||"; term LEVEL "200"; "|-"; term LEVEL "69"; "<"; NEXT
...