Basic notions and conventions¶
This section provides some essential notions and conventions for reading the manual.
We start by explaining the syntax and lexical conventions used in the manual. Then, we present the essential vocabulary necessary to read the rest of the manual. Other terms are defined throughout the manual. The reader may refer to the glossary index for a complete list of defined terms. Finally, we describe the various types of settings that Rocq provides.
Syntax and lexical conventions¶
Syntax conventions¶
The syntax described in this documentation is equivalent to that accepted by the Rocq parser, but the grammar has been edited to improve readability and presentation.
In the grammar presented in this manual, the terminal symbols are
black (e.g. forall
), whereas the nonterminals are green, italic
and hyperlinked (e.g. term
). Some syntax is represented
graphically using the following kinds of blocks:
item?
An optional item.
item+
A list of one or more items.
item*
An optional list of items.
item+s
A list of one or more items separated by "s" (e.g.
item1 s item2 s item3
).item*s
An optional list of items separated by "s".
item1item2...
Alternatives (either
item1
oritem2
or ...).
Precedence levels that are
implemented in the Rocq parser are shown in the documentation by
appending the level to the nonterminal name (as in term100
or
ltac_expr3
).
Note
Rocq uses an extensible parser. Plugins and the notation system can extend the syntax at run time. Some notations are defined in the prelude, which is loaded by default. The documented grammar doesn't include these notations. Precedence levels not used by the base grammar are omitted from the documentation, even though they could still be populated by notations or plugins.
Furthermore, some parsing rules are only activated in certain contexts (proof mode, custom entries...).
Warning
Given the complexity of these parsing rules, it would be extremely difficult to create an external program that can properly parse a Rocq document. Therefore, tool writers are advised to delegate parsing to Rocq, by communicating with it, for instance through coq-lsp.
See also
Lexical conventions¶
- Blanks
Space, newline and horizontal tab are considered blanks. Blanks are ignored but they separate tokens.
- Comments
Comments are enclosed between
(*
and*)
. They can be nested. They can contain any character. However, embeddedstring
literals must be correctly closed. Comments are treated as blanks.- Identifiers
Identifiers, written
identident
, are sequences of letters, digits,_
and'
, that do not start with a digit or'
. That is, they are recognized by the following grammar (except that the string_
is reserved; it is not a valid identifier):::=
first_letter subsequent_letter*first_letter
::=
a .. zA .. Z_unicode_lettersubsequent_letter
::=
first_letterdigit'unicode_id_partAll characters are meaningful. In particular, identifiers are case-sensitive.
unicode_letter
non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like symbols and non-breaking space.unicode_id_part
non-exhaustively includes symbols for prime letters and subscripts.- Numbers
Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numbers start with
number0x
or0X
.integer
s are signed numbers without fraction or exponent parts.natural
s are non-negative integers. Underscores embedded in the digits are ignored, for example1_000_000
is the same as1000000
.::=
-? decnat . digit_+? eE +-? decnat?|
-? hexnat . hexdigit_+? pP +-? decnat?integer
::=
bigintbigint
::=
-? bignatnatural
::=
bignatbignat
::=
decnathexnatdecnat
::=
digit digit_*digit
::=
0 .. 9hexnat
::=
0x0X hexdigit hexdigit_*hexdigit
::=
0 .. 9a .. fA .. Fnumber
,bigint
andbignat
, which are used interm
s, generally have no range limitation.integer
andnatural
, which are used as arguments in tactics and commands, are limited to the range that fits into an OCaml integer (63-bit integers on most architectures).The standard library provides a few interpretations for
number
. Some of these interpretations support exponential notation for decimal numbers, for example5.02e-6
means 5.02×10-6; and base 2 exponential notation for hexadecimal numbers denoted byp
orP
, for example0xAp12
means 10×212. TheNumber Notation
mechanism lets the user define custom parsers and printers fornumber
.By default, numbers are interpreted as
nat
s, which is a unary representation. For example,3
is represented asS (S (S O))
. While this is a convenient representation for doing proofs, computing with largenat
s can lead to stack overflows or running out of memory. You can explicitly specify a different interpretation to avoid this problem. For example,1000000%Z
is a more efficient binary representation of that number as an integer. See Notation scopes andterm_scope
.Example: Stack overflow with
nat
- Fail Eval compute in 100000 + 100000. (* gives a stack overflow (not shown) *)
- The command has indeed failed with message: To avoid stack overflow, large numbers in nat are interpreted as applications of Nat.of_num_uint. [abstract-large-number,numbers,default]
- Require Import ZArith. (* for definition of Z *)
- [Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file zify_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
- Eval compute in (1000000000000000000000000000000000 + 1)%Z.
- = 1000000000000000000000000000000001%Z : Z
- Strings
Strings begin and end with
"
(double quote). Use""
to represent a double quote character within a string. In the grammar, strings are identified withstring
.The
String Notation
mechanism offers the user a way to define custom parsers and printers forstring
.
- Keywords
The following character sequences are keywords defined in the main Rocq grammar that cannot be used as identifiers (even when starting Rocq with the
-noinit
command-line flag):_ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with
The following are keywords defined in notations or plugins loaded in the prelude:
by exists exists2 using
Note that loading additional modules or plugins may expand the set of reserved keywords.
Print Keywords
can be used to print the current keywords and tokens.- Other tokens
The following character sequences are tokens defined in the main Rocq grammar (even when starting Rocq with the
-noinit
command-line flag):! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> ; < <+ <- <: <<: <= = => > >-> >= ? @ @{ [ ] _ `( `{ { {| | }
The following character sequences are tokens defined in notations or plugins loaded in the prelude:
** |- || ->
Note that loading additional modules or plugins may expand the set of defined tokens.
When multiple tokens match the beginning of a sequence of characters, the longest matching token not cutting a subsequence of contiguous letters in the middle is used. Occasionally you may need to insert spaces to separate tokens. For example, if
~
and~~
are both defined as tokens, the inputs~ ~
and~~
generate different tokens, whereas if~~
is not defined, then the two inputs are equivalent. Also, if~
and~_h
are both defined as tokens, the input~_ho
is interpreted as~ _ho
rather than~_h o
so as not to cut the identifier-like subsequenceho
. Contrastingly, if only~_h
is defined as a token, then~_ho
is an error because no token can be found that includes the whole subsequenceho
without cutting it in the middle. Finally, if all of~
,~_h
and~_ho
are defined as tokens, the input~_ho
is interpreted using the longest match rule, i.e. as the token~_ho
.
Essential vocabulary¶
This section presents the most essential notions to understand the rest of the Rocq Prover manual: terms and types on the one hand, commands and tactics on the other hand.
- term¶
Terms are the basic expressions of Rocq. Terms can represent mathematical expressions, propositions and proofs, but also executable programs and program types.
Here is the top-level syntax of terms. Each of the listed constructs is presented in a dedicated section. Some of these constructs (like
termterm_forall_or_fun
) are part of the core language that the kernel of Rocq understands and are therefore described in this chapter, while others (liketerm_if
) are language extensions that are presented in the next chapter.::=
term100term100
::=
term_cast|
term10term10
::=
term_application|
term_forall_or_fun|
term_let|
term_fix|
term_cofix|
term_if|
one_termone_term
::=
term_explicit|
term1term1
::=
term_projection|
term_scope|
term0term0
::=
qualid_annotated|
sort|
number_or_string|
term_evar|
term_match|
term_record|
term_generalizing|
[| term*; | term : type? |] univ_annot?|
term_ltac|
( term )qualid_annotated
::=
qualid univ_annot?Note
Many commands and tactics use
one_term
(in the syntax of their arguments) rather thanterm
. The former need to be enclosed in parentheses unless they're very simple, such as a single identifier. This avoids confusing a space-separated list of terms or identifiers with aterm_application
.- type¶
To be valid and accepted by the Rocq kernel, a term needs an associated type. We express this relationship by “\(x\) of type \(T\)”, which we write as “\(x:T\)”. Informally, “\(x:T\)” can be thought as “\(x\) belongs to \(T\)”.
The Rocq kernel is a type checker: it verifies that a term has the expected type by applying a set of typing rules (see Typing rules). If that's indeed the case, we say that the term is well-typed.
A special feature of the Rocq language is that types can depend on terms (we say that the language is dependently-typed). Because of this, types and terms share a common syntax. All types are terms, but not all terms are types. The syntactic aliases
typetype
andone_type
are used to make clear when the provided term must semantically be a type:::=
termone_type
::=
one_termIntuitively, types may be viewed as sets containing terms. We say that a type is inhabited if it contains at least one term (i.e. if we can find a term which is associated with this type). We call such terms inhabitants. Note that deciding whether a type is inhabited is undecidable.
Formally, types can be used to construct logical foundations for mathematics alternative to the standard "set theory": we call such logical foundations "type theories". The Rocq Prover is based on the Calculus of Inductive Constructions, which is a particular instance of type theory.
- sentence¶
Rocq documents are made of a series of sentences that contain commands or tactics, generally terminated with a period and optionally decorated with attributes.
document::=
sentence*sentence
::=
attributes? command .|
attributes? natural :? query_command .|
attributes? toplevel_selector :? ltac_expr ....|
control_commandltac_expr
syntax supports both simple and compound tactics. For example:split
is a simple tactic whilesplit; auto
combines two simple tactics.- command¶
A
command
can be used to modify the state of a Rocq document, for instance by declaring a new object, or to get information about the current state.By convention, command names begin with uppercase letters. Commands appear in the HTML documentation in blue or gray boxes after the label "Command". In the pdf, they appear after the boldface label "Command:". Commands are listed in the Command index. Example:
- tactic¶
A
tactic
specifies how to transform the current proof state as a step in creating a proof. They are syntactically valid only when Rocq is in proof mode, such as after aTheorem
command and before any subsequent proof-terminating command such asQed
. See Proof mode for more on proof mode.By convention, tactic names begin with lowercase letters. Tactic appear in the HTML documentation in blue or gray boxes after the label "Tactic". In the pdf, they appear after the boldface label "Tactic:". Tactics are listed in the Tactic index.
Settings¶
There are several mechanisms for changing the behavior of Rocq. The attribute mechanism is used to modify the default behavior of a sentence or to attach information to Rocq objects. The flag, option and table mechanisms are used to modify the behavior of Rocq more globally in a document or project.
Attributes¶
An attribute is used to modify the default behavior of a
sentence or to attach information to a Rocq object.
Syntactically, most commands and tactics can be decorated with
attributes (cf. sentence
), but attributes not supported by the
command or tactic will trigger This command does not support
this attribute
. There is also a command Attributes
to
assign attributes to a whole document.
::=
#[ attribute*, ]* legacy_attr*
attribute::=
ident attr_value?
attr_value::=
= string
|
= qualid
|
( attribute+, )
legacy_attr::=
LocalGlobal
|
PolymorphicMonomorphic
|
CumulativeNonCumulative
|
Private
|
Program
The order of top-level attributes doesn't affect their meaning. #[foo,bar]
, #[bar,foo]
,
#[foo]#[bar]
and #[bar]#[foo]
are equivalent.
Boolean attributes take the form identattr= yesno?
.
When the yesno
value is omitted, the default is yes
.
The legacy attributes (legacy_attr
) provide an older, alternate syntax
for certain attributes. They are equivalent to new attributes as follows:
Legacy attribute |
New attribute |
---|---|
|
|
|
|
|
|
|
|
|
|
|
Attributes appear in the HTML documentation in blue or gray boxes after the label "Attribute". In the pdf, they appear after the boldface label "Attribute:". Attributes are listed in the Attribute index.
- Warning This command does not support this attribute: ident.¶
This warning is configured to behave as an error by default. You may turn it into a normal warning by using the
Warnings
option:- Set Silent.
- Set Warnings "unsupported-attributes".
- #[ foo ] Comments.
- Toplevel input, characters 3-6: > #[ foo ] Comments. > ^^^ Warning: This command does not support this attribute: foo. [unsupported-attributes,parsing,default]
Generic attributes¶
The following attribute is supported by every command:
- Attribute warnings = string¶
Sets the given warning string locally for the command. After the command finishes the warning state is reset to what it was before the command. For instance if the current warning state is
some-warnings,-other-warning
,#[warnings="+other-warning"] Command.is equivalent to
Set Warnings "+other-warning". Command. Set Warnings "some-warnings,-other-warning".and
other-warning
is an error while executing the command.Consequently, using this attribute around an
Import
command will prevent it from changing the warning state.See also
Warnings
for the concrete syntax to use inside the quoted string.
Document-level attributes¶
- Command Attributes attribute+,¶
Associates attributes with the document. When compiled with
coqc
(see Section The Rocq Prover commands), the attributes are associated with the compiled file and may have an effect when the file is loaded withRequire
. Supported attributes includedeprecated
andwarn
.
Flags, Options and Tables¶
The following types of settings can be used to change the behavior of Rocq in subsequent commands and tactics (see Locality attributes supported by Set and Unset for a more precise description of the scope of these settings):
A flag has a boolean value, such as
Universe Polymorphism
.An option generally has a numeric or string value, such as
Firstorder Depth
.In addition, some commands provide settings, such as
Extraction Language
.
::=
ident+
Flags, options and tables are identified by a series of identifiers. By convention, each of the identifiers start with an initial capital letter.
Flags, options and tables appear in the HTML documentation in blue or gray boxes after the labels "Flag", "Option" and "Table". In the pdf, they appear after a boldface label. They are listed in the Flags, options and tables index.
- Command Set setting_name integerstring?¶
If
setting_name
is a flag, no value may be provided; the flag is set to on. Ifsetting_name
is an option, a value of the appropriate type must be provided; the option is set to the specified value.This command supports the
local
,global
andexport
attributes. They are described here.- Warning There is no flag or option with this name: "setting_name".¶
This warning message can be raised by
Set
andUnset
whensetting_name
is unknown. It is a warning rather than an error because this helps library authors produce Rocq code that is compatible with several Rocq versions. To preserve the same behavior, they may need to set some compatibility flags or options that did not exist in previous Rocq versions.
- Command Unset setting_name¶
If
setting_name
is a flag, it is set to off. Ifsetting_name
is an option, it is set to its default value.This command supports the
local
,global
andexport
attributes. They are described here.
- Command Add setting_name qualidstring+¶
Adds the specified values to the table
setting_name
.This command supports the
local
,global
andexport
attributes. The default isexport
outside sections andlocal
inside sections. Depending on the table some values may only allowlocal
, typically section variables cannot be added withexport
orglobal
.
- Command Remove setting_name qualidstring+¶
Removes the specified value from the table
setting_name
.This command supports the same attributes as
Add
.
- Command Test setting_name for qualidstring+?¶
If
setting_name
is a flag or option, prints its current value. Ifsetting_name
is a table: if thefor
clause is specified, reports whether the table contains each specified value, otherwise this is equivalent toPrint Table
. Thefor
clause is not valid for flags and options.- Error There is no flag, option or table with this name: "setting_name".¶
This error message is raised when calling the
Test
command (without thefor
clause), or thePrint Table
command, for an unknownsetting_name
.
- Error There is no qualid-valued table with this name: "setting_name".¶
- Error There is no string-valued table with this name: "setting_name".¶
These error messages are raised when calling the
Add
orRemove
commands, or theTest
command with thefor
clause, ifsetting_name
is unknown or does not have the right type.
- Command Print Options¶
Prints the current value of all flags and options, and the names of all tables.
- Command Print Table setting_name¶
Prints the values in the table
setting_name
.
- Command Print Tables¶
A synonym for
Print Options
.
Locality attributes supported by Set
and Unset
¶
The Set
and Unset
commands support the mutually
exclusive local
, export
and global
locality
attributes.
If no attribute is specified, the original value of the flag or option is restored at the end of the current module but it is not restored at the end of the current section.
The
local
attribute makes the setting local to the currentSection
(if applicable) orModule
.The
export
attribute makes the setting local to the currentModule
, unlessImport
(or one of its variants) is used on theModule
.The
global
attribute makes the setting persist outside the currentModule
in the current file, or wheneverRequire
is used on the current file.
Note
We discourage using the global
locality attribute with the
Set
and Unset
commands. If your goal is to define
project-wide settings, you should rather use the command-line
arguments -set
and -unset
for setting flags and options
(see Command line options).