Syntax extensions and interpretation scopes¶
In this chapter, we introduce advanced commands to modify the way Coq parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands.
The main commands to provide custom symbolic notations for terms are
Notation
and Infix
; they will be described in the
next section. There is also a
variant of Notation
which does not modify the parser; this provides a
form of abbreviation. It is
sometimes expected that the same symbolic notation has different meanings in
different contexts; to achieve this form of overloading, Coq offers a notion
of interpretation scopes.
The main command to provide custom notations for tactics is Tactic Notation
.
- Set Printing Depth 50.
Notations¶
Basic notations¶
-
Command
Notation
¶
A notation is a symbolic expression denoting some term or term pattern.
A typical notation is the use of the infix symbol /\
to denote the
logical conjunction (and). Such a notation is declared by
- Notation "A /\ B" := (and A B).
The expression (and A B)
is the abbreviated term and the string "A /\ B"
(called a notation) tells how it is symbolically written.
A notation is always surrounded by double quotes (except when the
abbreviation has the form of an ordinary applicative expression;
see Abbreviations). The notation is composed of tokens separated by
spaces. Identifiers in the string (such as A
and B
) are the parameters
of the notation. Each of them must occur at least once in the denoted term. The
other elements of the string (such as /\
) are the symbols.
An identifier can be used as a symbol but it must be surrounded by single quotes to avoid the confusion with a parameter. Similarly, every symbol of at least 3 characters and starting with a simple quote must be quoted (then it starts by two single quotes). これが例です。
- Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
A notation binds a syntactic expression to a term. Unless the parser and pretty-printer of Coq already know how to deal with the syntactic expression (see Reserving notations), explicit precedences and associativity rules have to be given.
注釈
The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, implicit arguments, coercions, etc. are resolved at the time of the declaration of the notation.
Precedences and associativity¶
Mixing different symbolic notations in the same text may cause serious parsing ambiguity. To deal with the ambiguity of notations, Coq uses precedence levels ranging from 0 to 100 (plus one extra level numbered 200) and associativity rules.
Consider for example the new notation
- Notation "A \/ B" := (or A B).
Clearly, an expression such as forall A:Prop, True /\ A \/ A \/ False
is ambiguous. To tell the Coq parser how to interpret the
expression, a priority between the symbols /\
and \/
has to be
given. Assume for instance that we want conjunction to bind more than
disjunction. This is expressed by assigning a precedence level to each
notation, knowing that a lower level binds more than a higher level.
Hence the level for disjunction must be higher than the level for
conjunction.
Since connectives are not tight articulation points of a text, it is reasonable to choose levels not so far from the highest level which is 100, for example 85 for disjunction and 80 for conjunction 1.
Similarly, an associativity is needed to decide whether True /\ False /\ False
defaults to True /\ (False /\ False)
(right associativity) or to
(True /\ False) /\ False
(left associativity). We may even consider that the
expression is not well-formed and that parentheses are mandatory (this is a “no
associativity”) 2. We do not know of a special convention of
the associativity of disjunction and conjunction, so let us apply for instance a
right associativity (which is the choice of Coq).
Precedence levels and associativity rules of notations have to be
given between parentheses in a list of modifiers that the Notation
command understands. Here is how the previous examples refine.
- Notation "A /\ B" := (and A B) (at level 80, right associativity).
- Notation "A \/ B" := (or A B) (at level 85, right associativity).
By default, a notation is considered nonassociative, but the
precedence level is mandatory (except for special cases whose level is
canonical). The level is either a number or the phrase next level
whose meaning is obvious.
Some associativities are predefined in the
Notations
module.
Complex notations¶
Notations can be made from arbitrarily complex symbols. One can for instance define prefix notations.
- Notation "~ x" := (not x) (at level 75, right associativity).
One can also define notations for incomplete terms, with the hole expected to be inferred during type checking.
- Notation "x = y" := (@eq _ x y) (at level 70, no associativity).
One can define closed notations whose both sides are symbols. In this case, the default precedence level for the inner subexpression is 200, and the default level for the notation itself is 0.
- Notation "( x , y )" := (@pair _ _ x y).
- Setting notation at level 0.
One can also define notations for binders.
- Notation "{ x : A | P }" := (sig A (fun x => P)).
In the last case though, there is a conflict with the notation for
type casts. The notation for types casts, as shown by the command Print
Grammar constr
is at level 100. To avoid x : A
being parsed as a type cast,
it is necessary to put x
at a level below 100, typically 99. Hence, a correct
definition is the following:
- Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99).
- Setting notation at level 0.
More generally, it is required that notations are explicitly factorized on the left. See the next section for more about factorization.
Simple factorization rules¶
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. これが例です。
- Notation "x < y" := (lt x y) (at level 70).
- Notation "x < y < z" := (x < y /\ y < z) (at level 70).
- Toplevel input, characters 0-55: > Notation "x < y < z" := (x < y /\ y < z) (at level 70). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Notation "_ < _ < _" is already defined at level 70 with arguments constr at next level, constr at next level, constr at next level while it is now required to be at level 70 with arguments constr at next level, constr at level 200, constr at next level.
In order to factorize the left part of the rules, the subexpression
referred to by y
has to be at the same level in both rules. However the
default behavior puts y
at the next level below 70 in the first rule
(no associativity
is the default), and at level 200 in the second
rule (level 200
is the default for inner expressions). To fix this, we
need to force the parsing level of y
, as follows.
- Notation "x < y" := (lt x y) (at level 70).
- Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
For the sake of factorization with Coq predefined rules, simple rules
have to be observed for notations starting with a symbol, e.g., rules
starting with “{
” or “(
” should be put at level 0. The list
of Coq predefined notations can be found in the chapter on The Coq library.
-
Command
Print Grammar constr.
¶ This command displays the current state of the Coq term parser.
-
Command
Print Grammar pattern.
¶ This displays the state of the subparser of patterns (the parser used in the grammar of the match with constructions).
Displaying symbolic notations¶
The command Notation
has an effect both on the Coq parser and on the Coq printer. 例えば:
- Check (and True True).
- True /\ True : Prop
However, printing, especially pretty-printing, also requires some care. We may want specific indentations, line breaks, alignment if on several lines, etc. For pretty-printing, Coq relies on OCaml formatting library, which provides indentation and automatic line breaks depending on page width by means of formatting boxes.
The default printing of notations is rudimentary. For printing a notation, a formatting box is opened in such a way that if the notation and its arguments cannot fit on a single line, a line break is inserted before the symbols of the notation and the arguments on the next lines are aligned with the argument on the first line.
A first, simple control that a user can have on the printing of a notation is the insertion of spaces at some places of the notation. This is performed by adding extra spaces between the symbols and parameters: each extra space (other than the single space needed to separate the components) is interpreted as a space to be inserted by the printer. Here is an example showing how to add spaces around the bar of the notation.
- Notation "{{ x : A | P }}" := (sig (fun x : A => P)) (at level 0, x at level 99).
- Check (sig (fun x : nat => x=x)).
- {{x : nat | x = x}} : Set
The second, more powerful control on printing is by using the format modifier. Here is an example
- Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) (at level 200, right associativity, format "'[v ' 'If' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'").
- Identifier 'If' now a keyword
- Check (IF_then_else (IF_then_else True False True) (IF_then_else True False True) (IF_then_else True False True)).
- If If True then False else True then If True then False else True else If True then False else True : Prop
A format is an extension of the string denoting the notation with the possible following elements delimited by single quotes:
extra spaces are translated into simple spaces
tokens of the form
'/ '
are translated into breaking point, in case a line break occurs, an indentation of the number of spaces after the “/
” is applied (2 spaces in the given example)token of the form
'//'
force writing on a new linewell-bracketed pairs of tokens of the form
'[ '
and']'
are translated into printing boxes; in case a line break occurs, an extra indentation of the number of spaces given after the “[
” is applied (4 spaces in the example)well-bracketed pairs of tokens of the form
'[hv '
and']'
are translated into horizontal-or-else-vertical printing boxes; if the content of the box does not fit on a single line, then every breaking point forces a newline and an extra indentation of the number of spaces given after the “[
” is applied at the beginning of each newline (3 spaces in the example)well-bracketed pairs of tokens of the form
'[v '
and']'
are translated into vertical printing boxes; every breaking point forces a newline, even if the line is large enough to display the whole content of the box, and an extra indentation of the number of spaces given after the “[
” is applied at the beginning of each newline
Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation.
注釈
Sometimes, a notation is expected only for the parser. To do
so, the option only parsing
is allowed in the list of modifiers
of Notation
. Conversely, the only printing
modifier can be
used to declare that a notation should only be used for printing and
should not declare a parsing rule. In particular, such notations do
not modify the parser.
Reserving notations¶
A given notation may be used in different contexts. Coq expects all uses of the notation to be defined at the same precedence and with the same associativity. To avoid giving the precedence and associativity every time, it is possible to declare a parsing rule in advance without giving its interpretation. Here is an example from the initial state of Coq.
- Reserved Notation "x = y" (at level 70, no associativity).
Reserving a notation is also useful for simultaneously defining an inductive type or a recursive constant and a notation for it.
注釈
The notations mentioned in the module Notations are reserved. Hence their precedence and associativity cannot be changed.
Simultaneous definition of terms and notations¶
Thanks to reserved notations, the inductive, co-inductive, record, recursive and
corecursive definitions can benefit from customized notations. To do this, insert
a where
notation clause after the definition of the (co)inductive type or
(co)recursive term (or after the definition of each of them in case of mutual
definitions). The exact syntax is given by decl_notation
for inductive,
co-inductive, recursive and corecursive definitions and in レコード型
for records. Here are examples:
- Reserved Notation "A & B" (at level 80).
- Inductive and' (A B : Prop) : Prop := conj' : A -> B -> A & B where "A & B" := (and' A B).
- and' is defined and'_rect is defined and'_ind is defined and'_rec is defined
- Fixpoint plus (n m : nat) {struct n} : nat := match n with | O => m | S p => S (p+m) end where "n + m" := (plus n m).
- plus is defined plus is recursively defined (decreasing on 1st argument)
Displaying information about notations¶
-
Flag
Printing Notations
¶ Controls whether to use notations for printing terms wherever possible. Default is on.
参考
Printing All
To disable other elements in addition to notations.
Locating notations¶
To know to which notations a given symbol belongs to, use the Locate
command. You can call it on any (composite) symbol surrounded by double quotes.
To locate a particular notation, use a string where the variables of the
notation are replaced by “_
” and where possible single quotes inserted around
identifiers or tokens starting with a single quote are dropped.
- Locate "exists".
- Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation) "'exists' ! x .. y , p" := ex (unique (fun x => .. (ex (unique (fun y => p))) ..)) : type_scope (default interpretation)
- Locate "exists _ .. _ , _".
- Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation)
Notations and binders¶
Notations can include binders. This section lists different ways to deal with binders. For further examples, see also Notations with recursive patterns involving binders.
Binders bound in the notation and parsed as identifiers¶
Here is the basic example of a notation using a binder:
- Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) (at level 200, x ident, A at level 200, right associativity).
- Identifier 'sigma' now a keyword
The binding variables in the right-hand side that occur as a parameter
of the notation (here x
) dynamically bind all the occurrences
in their respective binding scope after instantiation of the
parameters of the notation. This means that the term bound to B
can
refer to the variable name bound to x
as shown in the following
application of the notation:
- Check sigma z : nat, z = 0.
- sigma z : nat, z = 0 : Set
Notice the modifier x ident
in the declaration of the
notation. It tells to parse x
as a single identifier.
Binders bound in the notation and parsed as patterns¶
In the same way as patterns can be used as binders, as in
fun '(x,y) => x+y
or fun '(existT _ x _) => x
, notations can be
defined so that any pattern
can be used in place of the
binder. Here is an example:
- Notation "'subset' ' p , P " := (sig (fun p => P)) (at level 200, p pattern, format "'subset' ' p , P").
- Identifier 'subset' now a keyword
- Check subset '(x,y), x+y=0.
- subset '(x, y), x + y = 0 : Set
The modifier p pattern
in the declaration of the notation tells to parse
p
as a pattern. Note that a single variable is both an identifier and a
pattern, so, e.g., the following also works:
- Check subset 'x, x=0.
- subset 'x, x = 0 : Set
If one wants to prevent such a notation to be used for printing when the
pattern is reduced to a single identifier, one has to use instead
the modifier p strict pattern
. For parsing, however, a
strict pattern
will continue to include the case of a
variable. Here is an example showing the difference:
- Notation "'subset_bis' ' p , P" := (sig (fun p => P)) (at level 200, p strict pattern).
- Identifier 'subset_bis' now a keyword
- Notation "'subset_bis' p , P " := (sig (fun p => P)) (at level 200, p ident).
- Check subset_bis 'x, x=0.
- subset_bis x, x = 0 : Set
The default level for a pattern
is 0. One can use a different level by
using pattern at level
\(n\) where the scale is the same as the one for
terms (see Notations).
Binders bound in the notation and parsed as terms¶
Sometimes, for the sake of factorization of rules, a binder has to be parsed as a term. This is typically the case for a notation such as the following:
- Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0, x at level 99 as ident).
- Toplevel input, characters 0-92: > Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0, x at level 99 as ident). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Notation "{ _ : _ | _ }" is already defined at level 0 with arguments constr at level 99, constr at level 200, constr at level 200 while it is now required to be at level 0 with arguments as ident at level 99, constr at level 200, constr at level 200.
This is so because the grammar also contains rules starting with {}
and
followed by a term, such as the rule for the notation { A } + { B }
for the
constant sumbool
(see Specification).
Then, in the rule, x ident
is replaced by x at level 99 as ident
meaning
that x
is parsed as a term at level 99 (as done in the notation for
sumbool
), but that this term has actually to be an identifier.
The notation { x | P }
is already defined in the standard
library with the as ident
modifier. We cannot redefine it but
one can define an alternative notation, say { p such that P }
,
using instead as pattern
.
- Notation "{ p 'such' 'that' P }" := (sig (fun p => P)) (at level 0, p at level 99 as pattern).
- Identifier 'such' now a keyword
Then, the following works:
- Check {(x,y) such that x+y=0}.
- {(x, y) such that x + y = 0} : Set
To enforce that the pattern should not be used for printing when it
is just an identifier, one could have said
p at level 99 as strict pattern
.
Note also that in the absence of a as ident
, as strict pattern
or
as pattern
modifiers, the default is to consider subexpressions occurring
in binding position and parsed as terms to be as ident
.
Binders not bound in the notation¶
We can also have binders in the right-hand side of a notation which are not themselves bound in the notation. In this case, the binders are considered up to renaming of the internal binder. E.g., for the notation
- Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200).
- Identifier 'exists_different' now a keyword
the next command fails because p does not bind in the instance of n.
- Fail Check (exists_different p).
- The command has indeed failed with message: The reference p was not found in the current environment.
- Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
- Setting notation at level 0.
Notations with recursive patterns¶
A mechanism is provided for declaring elementary notations with recursive patterns. The basic example is:
- Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
- Setting notation at level 0.
On the right-hand side, an extra construction of the form .. t ..
can
be used. Notice that ..
is part of the Coq syntax and it must not be
confused with the three-dots notation “…
” used in this manual to denote
a sequence of arbitrary size.
On the left-hand side, the part “x s .. s y
” of the notation parses
any number of times (but at least once) a sequence of expressions
separated by the sequence of tokens s
(in the example, s
is just “;
”).
The right-hand side must contain a subterm of the form either
φ(x, .. φ(y,t) ..)
or φ(y, .. φ(x,t) ..)
where \(φ([~]_E , [~]_I)\),
called the iterator of the recursive notation is an arbitrary expression with
distinguished placeholders and where \(t\) is called the terminating
expression of the recursive notation. In the example, we choose the names
\(x\) and \(y\) but in practice they can of course be chosen
arbitrarily. Note that the placeholder \([~]_I\) has to occur only once but
\([~]_E\) can occur several times.
Parsing the notation produces a list of expressions which are used to fill the first placeholder of the iterating pattern which itself is repeatedly nested as many times as the length of the list, the second placeholder being the nesting point. In the innermost occurrence of the nested iterating pattern, the second placeholder is finally filled with the terminating expression.
In the example above, the iterator \(φ([~]_E , [~]_I)\) is \(cons [~]_E [~]_I\)
and the terminating expression is nil
. Here are other examples:
- Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
- Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z)) (pair .. (pair (pair a u) (pair b u)) .. (pair c u))) (t at level 39).
- Setting notation at level 0.
Notations with recursive patterns can be reserved like standard notations, they can also be declared within interpretation scopes.
Notations with recursive patterns involving binders¶
Recursive notations can also be used with binders. The basic example is:
- Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, y binder, right associativity).
The principle is the same as in Notations with recursive patterns
except that in the iterator
\(φ([~]_E , [~]_I)\), the placeholder \([~]_E\) can also occur in
position of the binding variable of a fun
or a forall
.
To specify that the part “x .. y
” of the notation parses a sequence of
binders, x
and y
must be marked as binder
in the list of modifiers
of the notation. The binders of the parsed sequence are used to fill the
occurrences of the first placeholder of the iterating pattern which is
repeatedly nested as many times as the number of binders generated. If ever the
generalization operator '
(see 暗黙の一般化) is
used in the binding list, the added binders are taken into account too.
There are two flavors of binder parsing. If x
and y
are marked as binder,
then a sequence such as a b c : T
will be accepted and interpreted as
the sequence of binders (a:T) (b:T) (c:T)
. For instance, in the
notation above, the syntax exists a b : nat, a = b
is valid.
The variables x
and y
can also be marked as closed binder in which
case only well-bracketed binders of the form (a b c:T)
or {a b c:T}
etc. are accepted.
With closed binders, the recursive sequence in the left-hand side can
be of the more general form x s .. s y
where s
is an arbitrary sequence of
tokens. With open binders though, s
has to be empty. Here is an
example of recursive notation with closed binders:
- Notation "'mylet' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) (at level 200, x closed binder, y closed binder, right associativity).
- Identifier 'mylet' now a keyword
A recursive pattern for binders can be used in position of a recursive pattern for terms. Here is an example:
- Notation "'FUNAPP' x .. y , f" := (fun x => .. (fun y => (.. (f x) ..) y ) ..) (at level 200, x binder, y binder, right associativity).
- Identifier 'FUNAPP' now a keyword
If an occurrence of the \([~]_E\) is not in position of a binding variable but of a term, it is the name used in the binding which is used. Here is an example:
- Notation "'exists_non_null' x .. y , P" := (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) (at level 200, x binder).
- Identifier 'exists_non_null' now a keyword
Predefined entries¶
By default, sub-expressions are parsed as terms and the corresponding
grammar entry is called constr
. However, one may sometimes want
to restrict the syntax of terms in a notation. For instance, the
following notation will accept to parse only global reference in
position of x
:
- Notation "'apply' f a1 .. an" := (.. (f a1) .. an) (at level 10, f global, a1, an at level 9).
- Identifier 'apply' now a keyword Identifier 'apply' now a keyword
In addition to global
, one can restrict the syntax of a
sub-expression by using the entry names ident
or pattern
already seen in Binders not bound in the notation, even when the
corresponding expression is not used as a binder in the right-hand
side. E.g.:
- Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9).
- Identifier 'apply_id' now a keyword Identifier 'apply_id' now a keyword
Summary¶
Syntax of notations¶
The different syntactic variants of the command Notation are given on the
following figure. The optional scope
is described in
Interpretation scopes.
notation ::= [Local] Notationstring
:=term
[modifiers
] [:scope
]. | [Local] Infixstring
:=qualid
[modifiers
] [:scope
]. | [Local] Reserved Notationstring
[modifiers
] . | Inductiveind_body
[decl_notation
] with … withind_body
[decl_notation
]. | CoInductiveind_body
[decl_notation
] with … withind_body
[decl_notation
]. | Fixpointfix_body
[decl_notation
] with … withfix_body
[decl_notation
]. | CoFixpointcofix_body
[decl_notation
] with … withcofix_body
[decl_notation
]. decl_notation ::= [wherestring
:=term
[:scope
] and … andstring
:=term
[:scope
]]. modifiers ::= at levelnatural
|ident
, … ,ident
at levelnatural
[binderinterp
] |ident
, … ,ident
at next level [binderinterp
] |ident
ident |ident
global |ident
bigint |ident
[strict] pattern [at levelnatural
] |ident
binder |ident
closed binder | left associativity | right associativity | no associativity | only parsing | only printing | formatstring
binderinterp ::= as ident | as pattern | as strict pattern
注釈
No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation.
注釈
Many examples of Notation may be found in the files composing
the initial state of Coq (see directory $COQLIB/theories/Init
).
注釈
The notation "{ x }"
has a special status in such a way that
complex notations of the form "x + { y }"
or "x * { y }"
can be
nested with correct precedences. Especially, every notation involving
a pattern of the form "{ x }"
is parsed as a notation where the
pattern "{ x }"
has been simply replaced by "x"
and the curly
brackets are parsed separately. E.g. "y + { z }"
is not parsed as a
term of the given form but as a term of the form "y + z"
where z
has been parsed using the rule parsing "{ x }"
. Especially, level
and precedences for a rule including patterns of the form "{ x }"
are relative not to the textual notation but to the notation where the
curly brackets have been removed (e.g. the level and the associativity
given to some notation, say "{ y } & { z }"
in fact applies to the
underlying "{ x }"
-free rule which is "y & z"
).
Interpretation scopes¶
An interpretation scope is a set of notations for terms with their
interpretations. Interpretation scopes provide a weak, purely
syntactical form of notation overloading: the same notation, for
instance the infix symbol +
, can be used to denote distinct
definitions of the additive operator. Depending on which interpretation
scopes are currently open, the interpretation is different.
Interpretation scopes can include an interpretation for numerals and
strings. However, this is only made possible at the Objective Caml
level.
See above for the syntax of notations including the
possibility to declare them in a given scope. Here is a typical example which
declares the notation for conjunction in the scope type_scope
.
- Notation "A /\ B" := (and A B) : type_scope.
注釈
A notation not defined in a scope is called a lonely notation.
Global interpretation rules for notations¶
At any time, the interpretation of a notation for a term is done within
a stack of interpretation scopes and lonely notations. In case a
notation has several interpretations, the actual interpretation is the
one defined by (or in) the more recently declared (or opened) lonely
notation (or interpretation scope) which defines this notation.
Typically if a given notation is defined in some scope scope
but has
also an interpretation not assigned to a scope, then, if scope
is open
before the lonely interpretation is declared, then the lonely
interpretation is used (and this is the case even if the
interpretation of the notation in scope is given after the lonely
interpretation: otherwise said, only the order of lonely
interpretations and opening of scopes matters, and not the declaration
of interpretations within a scope).
The initial state of Coq declares three interpretation scopes and no
lonely notations. These scopes, in opening order, are core_scope
,
type_scope
and nat_scope
.
-
Command
Open Scope scope
¶ The command to add a scope to the interpretation scope stack is
Open Scope scope
.
-
Command
Close Scope scope
¶ It is also possible to remove a scope from the interpretation scope stack by using the command
Close Scope scope
.Notice that this command does not only cancel the last
Open Scope scope
but all its invocations.
注釈
Open Scope
and Close Scope
do not survive the end of sections
where they occur. When defined outside of a section, they are exported
to the modules that import the module where they occur.
Local interpretation rules for notations¶
In addition to the global rules of interpretation of notations, some ways to change the interpretation of subterms are available.
Local opening of an interpretation scope¶
It is possible to locally extend the interpretation scope stack using the syntax
(term)%key
(or simply term%key
for atomic terms), where key is a
special identifier called delimiting key and bound to a given scope.
In such a situation, the term term, and all its subterms, are interpreted in the scope stack extended with the scope bound tokey.
Binding arguments of a constant to an interpretation scope¶
-
Command
Arguments qualid name%scope+
¶ It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is
Arguments qualid name%scope+
where the list is a prefix of the arguments ofqualid
eventually annotated with theirscope
. Grouping round parentheses can be used to decorate multiple arguments with the same scope.scope
can be either a scope name or its delimiting key. For example the following command puts the first two arguments ofplus_fct
in the scope delimited by the keyF
(Rfun_scope
) and the last argument in the scope delimited by the keyR
(R_scope
).- Arguments plus_fct (f1 f2)%F x%R.
- Toplevel input, characters 10-18: > Arguments plus_fct (f1 f2)%F x%R. > ^^^^^^^^ Error: The reference plus_fct was not found in the current environment.
The
Arguments
command accepts scopes decoration to all grouping parentheses. In the following example arguments A and B are marked as maximally inserted implicit arguments and are put into the type_scope scope.- Arguments respectful {A B}%type (R R')%signature _ _.
- Toplevel input, characters 10-20: > Arguments respectful {A B}%type (R R')%signature _ _. > ^^^^^^^^^^ Error: The reference respectful was not found in the current environment.
When interpreting a term, if some of the arguments of qualid are built from a notation, then this notation is interpreted in the scope stack extended by the scope bound (if any) to this argument. The effect of the scope is limited to the argument itself. It does not propagate to subterms but the subterms that, after interpretation of the notation, turn to be themselves arguments of a reference are interpreted accordingly to the argument scopes bound to this reference.
-
Variant
Arguments qualid : clear scopes
This command can be used to clear argument scopes of
qualid
.
-
Variant
Arguments qualid name%scope+ : extra scopes
Defines extra argument scopes, to be used in case of coercion to
Funclass
(see the Implicit Coercions chapter) or with a computed type.
参考
The command About
can be used to show the scopes bound to the
arguments of a function.
注釈
In notations, the subterms matching the identifiers of the notations are interpreted in the scope in which the identifiers occurred at the time of the declaration of the notation. Here is an example:
- Parameter g : bool -> bool.
- g is declared
- Notation "@@" := true (only parsing) : bool_scope.
- Setting notation at level 0.
- Notation "@@" := false (only parsing): mybool_scope.
- Bind Scope bool_scope with bool.
- Notation "# x #" := (g x) (at level 40).
- Check # @@ #.
- # true # : bool
- Arguments g _%mybool_scope.
- Check # @@ #.
- # true # : bool
- Delimit Scope mybool_scope with mybool.
- Check # @@%mybool #.
- # false # : bool
Binding types of arguments to an interpretation scope¶
-
Command
Bind Scope scope with qualid
¶ When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it to this type. When a scope
scope
is bound to a typetype
, any new function defined later on gets its arguments of typetype
interpreted by default in scope scope (this default behavior can however be overwritten by explicitly using the commandArguments
).Whether the argument of a function has some type
type
is determined statically. For instance, iff
is a polymorphic function of typeforall X:Type, X -> X
and typet
is bound to a scopescope
, thena
of typet
inf t a
is not recognized as an argument to be interpreted in scopescope
.More generally, any coercion
class
(see the Implicit Coercions chapter) can be bound to an interpretation scope. The command to do it isBind Scope scope with class
- Parameter U : Set.
- U is declared
- Bind Scope U_scope with U.
- Parameter Uplus : U -> U -> U.
- Uplus is declared
- Parameter P : forall T:Set, T -> U -> Prop.
- P is declared
- Parameter f : forall T:Set, T -> U.
- f is declared
- Infix "+" := Uplus : U_scope.
- Unset Printing Notations.
- Open Scope nat_scope.
- Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
- fun (x y1 y2 : nat) (z : U) (t : nat) => P nat (Nat.add x t) (Uplus (f nat (Nat.add y1 y2)) z) : forall (_ : nat) (_ : nat) (_ : nat) (_ : U) (_ : nat), Prop
注釈
The scopes
type_scope
andfunction_scope
also have a local effect on interpretation. See the next section.
The type_scope
interpretation scope¶
The scope type_scope
has a special status. It is a primitive interpretation
scope which is temporarily activated each time a subterm of an expression is
expected to be a type. It is delimited by the key type
, and bound to the
coercion class Sortclass
. It is also used in certain situations where an
expression is statically known to be a type, including the conclusion and the
type of hypotheses within an Ltac goal match (see
Pattern matching on goals), the statement of a theorem, the type of a definition,
the type of a binder, the domain and codomain of implication, the codomain of
products, and more generally any type argument of a declared or defined
constant.
The function_scope
interpretation scope¶
The scope function_scope
also has a special status.
It is temporarily activated each time the argument of a global reference is
recognized to be a Funclass
istance, i.e., of type forall x:A, B
or
A -> B
.
Interpretation scopes used in the standard library of Coq¶
We give an overview of the scopes used in the standard library of Coq.
For a complete list of notations in each scope, use the commands Print
Scopes
or Print Scope
.
type_scope
This scope includes infix * for product types and infix + for sum types. It is delimited by the key
type
, and bound to the coercion classSortclass
, as described above.function_scope
This scope is delimited by the key
function
, and bound to the coercion classFunclass
, as described above.nat_scope
This scope includes the standard arithmetical operators and relations on type nat. Positive numerals in this scope are mapped to their canonical representent built from
O
andS
. The scope is delimited by the keynat
, and bound to the typenat
(see above).N_scope
This scope includes the standard arithmetical operators and relations on type
N
(binary natural numbers). It is delimited by the keyN
and comes with an interpretation for numerals as closed terms of typeN
.Z_scope
This scope includes the standard arithmetical operators and relations on type
Z
(binary integer numbers). It is delimited by the keyZ
and comes with an interpretation for numerals as closed terms of typeZ
.positive_scope
This scope includes the standard arithmetical operators and relations on type
positive
(binary strictly positive numbers). It is delimited by keypositive
and comes with an interpretation for numerals as closed terms of typepositive
.Q_scope
This scope includes the standard arithmetical operators and relations on type
Q
(rational numbers defined as fractions of an integer and a strictly positive integer modulo the equality of the numerator- denominator cross-product). As for numerals, only 0 and 1 have an interpretation in scopeQ_scope
(their interpretations are 0/1 and 1/1 respectively).Qc_scope
This scope includes the standard arithmetical operators and relations on the type
Qc
of rational numbers defined as the type of irreducible fractions of an integer and a strictly positive integer.real_scope
This scope includes the standard arithmetical operators and relations on type
R
(axiomatic real numbers). It is delimited by the keyR
and comes with an interpretation for numerals using theIZR
morphism from binary integer numbers toR
.bool_scope
This scope includes notations for the boolean operators. It is delimited by the key
bool
, and bound to the typebool
(see above).list_scope
This scope includes notations for the list operators. It is delimited by the key
list
, and bound to the typelist
(see above).core_scope
This scope includes the notation for pairs. It is delimited by the key
core
.string_scope
This scope includes notation for strings as elements of the type string. Special characters and escaping follow Coq conventions on strings (see 字句規則). Especially, there is no convention to visualize non printable characters of a string. The file
String.v
shows an example that contains quotes, a newline and a beep (i.e. the ASCII character of code 7).char_scope
This scope includes interpretation for all strings of the form
"c"
wherec
is an ASCII character, or of the form"nnn"
where nnn is a three-digits number (possibly with leading 0's), or of the form""""
. Their respective denotations are the ASCII code ofc
, the decimal ASCII codennn
, or the ascii code of the character"
(i.e. the ASCII code 34), all of them being represented in the typeascii
.
Displaying information about scopes¶
-
Command
Print Visibility
¶ This displays the current stack of notations in scopes and lonely notations that is used to interpret a notation. The top of the stack is displayed last. Notations in scopes whose interpretation is hidden by the same notation in a more recently opened scope are not displayed. Hence each notation is displayed only once.
-
Command
Print Scopes
¶ This displays all the notations, delimiting keys and corresponding classes of all the existing interpretation scopes. It also displays the lonely notations.
Abbreviations¶
-
Command
Local? Notation ident ident+ := term (only parsing)?.
An abbreviation is a name, possibly applied to arguments, that denotes a (presumably) more complex expression. Here are examples:
- Require Import List.
- Require Import Relations.
- Set Printing Notations.
- Notation Nlist := (list nat).
- Check 1 :: 2 :: 3 :: nil.
- [1; 2; 3] : Nlist
- Notation reflexive R := (forall x, R x x).
- Check forall A:Prop, A <-> A.
- reflexive iff : Prop
- Check reflexive iff.
- reflexive iff : Prop
An abbreviation expects no precedence nor associativity, since it is parsed as an usual application. Abbreviations are used as much as possible by the Coq printers unless the modifier
(only parsing)
is given.An abbreviation is bound to an absolute name as an ordinary definition is and it also can be referred to by a qualified name.
Abbreviations are syntactic in the sense that they are bound to expressions which are not typed at the time of the definition of the abbreviation but at the time they are used. Especially, abbreviations can be bound to terms with holes (i.e. with “
_
”). 例えば:- Set Strict Implicit.
- Set Printing Depth 50.
- Definition explicit_id (A:Set) (a:A) := a.
- explicit_id is defined
- Notation id := (explicit_id _).
- Check (id 0).
- id 0 : nat
Abbreviations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation.
Tactic Notations¶
Tactic notations allow to customize the syntax of tactics. They have the following syntax:
tacn ::= Tactic Notation [tactic_level
] [prod_item
…prod_item
] :=tactic
. prod_item ::=string
|tactic_argument_type
(ident
) tactic_level ::= (at levelnatural
) tactic_argument_type ::= ident | simple_intropattern | reference | hyp | hyp_list | ne_hyp_list | constr | uconstr | constr_list | ne_constr_list | integer | integer_list | ne_integer_list | int_or_var | int_or_var_list | ne_int_or_var_list | tactic | tactic0 | tactic1 | tactic2 | tactic3 | tactic4 | tactic5
-
Command
Tactic Notation (at level level)? prod_item+ := tactic.
¶ A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the tactic expression
tactic
. For simple tactics, it is recommended to use a terminal symbol, i.e. a string, for the first production item. The tactic level indicates the parsing precedence of the tactic notation. This information is particularly relevant for notations of tacticals. Levels 0 to 5 are available (default is 5).-
Command
Print Grammar tactic
¶ To know the parsing precedences of the existing tacticals, use the command
Print Grammar tactic
.
Each type of tactic argument has a specific semantic regarding how it is parsed and how it is interpreted. The semantic is described in the following table. The last command gives examples of tactics which use the corresponding kind of argument.
Tactic argument type
parsed as
interpreted as
as in tactic
ident
identifier
a user-given name
intro
simple_intropattern
intro_pattern
an intro pattern
intros
hyp
identifier
a hypothesis defined in context
clear
reference
qualified identifier
a global reference of term
unfold
constr
term
a term
exact
uconstr
term
an untyped term
refine
integer
integer
an integer
int_or_var
identifier or integer
an integer
do
tactic
tactic at level 5
a tactic
tacticn
tactic at level n
a tactic
entry
_list
list of entry
a list of how entry is interpreted
ne_
entry_list
non-empty list of entry
a list of how entry is interpreted
注釈
In order to be bound in tactic definitions, each syntactic entry for argument type must include the case of a simple Ltac identifier as part of what it parses. This is naturally the case for
ident
,simple_intropattern
,reference
,constr
, ... but not forinteger
. This is the reason for introducing a special entryint_or_var
which evaluates to integers only but which syntactically includes identifiers in order to be usable in tactic definitions.注釈
The entry
_list
andne_
entry_list
entries can be used in primitive tactics or in other notations at places where a list of the underlying entry can be used: entry is eitherconstr
,hyp
,integer
orint_or_var
.-
Command
-
Variant
Local Tactic Notation
Tactic notations disappear when a section is closed. They survive when a module is closed unless the command
Local Tactic Notation
is used instead ofTactic Notation
.
Footnotes
- 1
which are the levels effectively chosen in the current implementation of Coq
- 2
Coq accepts notations declared as nonassociative but the parser on which Coq is built, namely Camlp5, currently does not implement
no associativity
and replaces it withleft associativity
; hence it is the same for Coq:no associativity
is in factleft associativity
for the purposes of parsing