Coq: Notations

Info

• If defined within a section, notation is usable only within that section
• Notations in here are reserved and cannot be changed.
  • Eg: _ /\ _, _ || _
• Default precedence level of a pattern is 0.
• Coq's parsing is with camlp5. An LL1 parser
  • Left factorization may be needed to avoid parsing conflicts
• 'level 200 is the default for inner expressions' ʳ
• There is a list of predefined notation (with their levels and associativity): https://coq.inria.fr/doc/V8.19.0/refman/language/coq-library.html#thecoqlibrary
• Print Notation "_ :: _": Show info of a notation, including its level and associativity
• 'lonely notation': a notation that doesn't have a notation scope associated with it.

Print Grammar

• There are grammar entries (courtesy of camlp5). Default one is constr

From camlp5 docs:

A grammar entry is an abstract value internally containing a stream parser

—

• Print Grammar constr.: Print grammar for the entry named constr
  • Print Grammar.: Print whole gramamr
• Print Custom Grammar <custom-entry-name>: print grammar of a custom entry

Print Grammar constructor.
(*
Entry constructor is
[ LEFTA
  [ quoted_attributes; identref; constructor_type ] ]
*)

Entries:

• constr: terms
• vernac: vernacular commands
• tactic: tactics
• ltac2: ltac2 stuff, I guess

Also see:

• https://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar

Syntax modifiers

https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#grammar-token-syntax_modifier

• name: parse something as a single identifier
• pattern:
• at level:
• ident

local attribute

If local attribute is used, notation is available only within the same module.

Module FooMod.
  #[local] Notation "⊥" := false.

  Check ⊥.  (* ⊥ : bool *)
End FooMod.

Import FooMod.
Compute ⊥.
(* Syntax Error: Lexer: Undefined token *)

Reserved Notation

Same notations may have different meaning in different contexts. But they must all have the same precedence and associativity.

We can 'reserve' notations to ensure that.

Reserved Infix is the same thing except that the notation is infix.

Syntax modifier

• x name: 'parse x as a single identifier'
• x at level 10: x is parsed as a term at level 10, but is actually to be a name
• at level
• in custom <custom-entry-name>
• ident
• constr
• binder

Other:

• p pattern: p is a pattern. Like the kind used in pattern matching.

Custom entries

constr: the predefined grammar entry. As in the default interpretation.

• ie, the main grammar.

We can make our own grammar entries via Custom Entry.

• Print grammar of the custom entry: Print Custom Grammar <custom-entry-name>
• Print grammar of constr: Print Grammar constr

Precedence

Lower the precedence level, higher the precedence.

• Highest precedence: 0
• Least precedence: 100 (for user)
• Least precedence: 200 (for coq)

Examples

Documentation mentions this example of having left-associative tuples:

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).

Set Printing Parentheses.
Check (1,2,3).
(* ((1, 2), 3) : (nat * nat) * nat *)

We can have a right-associative version like:

Notation "( x , .. , y , z )" := (pair x .. (pair y z) .. ) (at level 0).

Set Printing Parentheses.
Check (1,2,3).
(* (1, (2, 3)) : nat * (nat * nat) *)

Thanks to https://coq.zulipchat.com/#narrow/stream/423352-Coq-Notation-system

Todo

• [ ] Tactic notation
• [ ] Number notation: can be used to change how numbers are parsed
• [ ] String notation: can be used to change how strings are parsed