Chapter 1: The Gallina specification language
This chapter describes Gallina, the specification language of Coq. It allows to develop mathematical theories and to prove specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in theories is described in section 1.2. The language of commands, called The Vernacular is described in section 1.3.In Coq, logical objects are typed to ensure their logical correctness. The rules implemented by the typing algorithm are described in chapter 4.
About the grammars in the manual
Grammars are presented in Backus-Naur form (BNF). Terminal symbols are set in typewriter font. In addition, there are special notations for regular expressions.An expression enclosed in square brackets [...] means at most one occurrence of this expression (this corresponds to an optional component).
The notation ``symbol sep ... sep symbol'' stands for a non empty sequence of expressions parsed by the ``symbol'' entry and separated by the literal ``sep''(This is similar to the expression ``symbol { sep symbol }'' in standard BNF, or``symbol ( sep symbol )*'' in the syntax of regular expressions.).
Similarly, the notation ``symbol ... symbol'' stands for a non empty sequence of expressions parsed by the ``symbol'' entry, without any separator between.
At the end, the notation ``[symbol sep ... sep symbol]'' stands for a possibly empty sequence of expressions parsed by the ``symbol'' entry, separated by the literal ``sep''.