diff options
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 262 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 1555 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 1209 |
3 files changed, 1817 insertions, 1209 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst new file mode 100644 index 0000000000..03da59e0bf --- /dev/null +++ b/doc/sphinx/language/core/basic.rst @@ -0,0 +1,262 @@ +.. _lexical-conventions: + +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, embedded :n:`@string` literals must be + correctly closed. Comments are treated as blanks. + +Identifiers + Identifiers, written :n:`@ident`, 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): + + .. insertprodn ident subsequent_letter + + .. prodn:: + ident ::= @first_letter {* @subsequent_letter } + first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter } + subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part } + + All characters are meaningful. In particular, identifiers are case-sensitive. + :production:`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. :production:`unicode_id_part` + non-exhaustively includes symbols for prime letters and subscripts. + +Numerals + Numerals are sequences of digits with an optional fractional part + and exponent, optionally preceded by a minus sign. :n:`@int` is an integer; + a numeral without fractional or exponent parts. :n:`@num` is a non-negative + integer. Underscores embedded in the digits are ignored, for example + ``1_000_000`` is the same as ``1000000``. + + .. insertprodn numeral digit + + .. prodn:: + numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } } + int ::= {? - } {+ @digit } + num ::= {+ @digit } + digit ::= 0 .. 9 + +Strings + Strings begin and end with ``"`` (double quote). Use ``""`` to represent + a double quote character within a string. In the grammar, strings are + identified with :production:`string`. + +Keywords + The following character sequences are reserved keywords that cannot be + used as identifiers:: + + _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop + SProp Set Theorem Type Variable as at by cofix discriminated else + end exists exists2 fix for forall fun if in lazymatch let match + multimatch return then using where with + + Note that plugins may define additional keywords when they are loaded. + +Other tokens + The set of + tokens defined at any given time can vary because the :cmd:`Notation` + command can define new tokens. A :cmd:`Require` command may load more notation definitions, + while the end of a :cmd:`Section` may remove notations. Some notations + are defined in the basic library (see :ref:`thecoqlibrary`) and are normally + loaded automatically at startup time. + + Here are the character sequences that Coq directly defines as tokens + without using :cmd:`Notation` (omitting 25 specialized tokens that begin with + ``#int63_``):: + + ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + . .( .. ... / : ::= := :> :>> ; < <+ <- <: + <<: <= = => > >-> >= ? @ @{ [ [= ] _ + `( `{ { {| | |- || } + + When multiple tokens match the beginning of a sequence of characters, + the longest matching token 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. + +.. _gallina-attributes: + +Attributes +----------- + +.. insertprodn all_attrs legacy_attr + +.. prodn:: + all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr } + attr ::= @ident {? @attr_value } + attr_value ::= = @string + | ( {*, @attr } ) + legacy_attr ::= {| Local | Global } + | {| Polymorphic | Monomorphic } + | {| Cumulative | NonCumulative } + | Private + | Program + +Attributes modify the behavior of a command or tactic. +Syntactically, most commands and tactics can be decorated with attributes, but +attributes not supported by the command or tactic will be flagged as errors. + +The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, +``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. + +The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax +for certain attributes. They are equivalent to new attributes as follows: + +================ ================================ +Legacy attribute New attribute +================ ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic` :attr:`universes(polymorphic)` +`Monomorphic` :attr:`universes(monomorphic)` +`Cumulative` :attr:`universes(cumulative)` +`NonCumulative` :attr:`universes(noncumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +================ ================================ + +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + +.. _flags-options-tables: + +Flags, Options and Tables +----------------------------- + +Coq has many settings to control its behavior. Setting types include flags, options +and tables: + +* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`. +* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A *table* contains a set of strings or qualids. +* In addition, some commands provide settings, such as :cmd:`Extraction Language`. + +.. FIXME Convert "Extraction Language" to an option. + +Flags, options and tables are identified by a series of identifiers, each with an initial +capital letter. + +.. cmd:: Set @setting_name {? {| @int | @string } } + :name: Set + + .. insertprodn setting_name setting_name + + .. prodn:: + setting_name ::= {+ @ident } + + If :n:`@setting_name` is a flag, no value may be provided; the flag + is set to on. + If :n:`@setting_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 :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here <set_unset_scope_qualifiers>`. + + .. warn:: There is no flag or option with this name: "@setting_name". + + This warning message can be raised by :cmd:`Set` and + :cmd:`Unset` when :n:`@setting_name` is unknown. It is a + warning rather than an error because this helps library authors + produce Coq code that is compatible with several Coq versions. + To preserve the same behavior, they may need to set some + compatibility flags or options that did not exist in previous + Coq versions. + +.. cmd:: Unset @setting_name + :name: Unset + + If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is + set to its default value. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here <set_unset_scope_qualifiers>`. + +.. cmd:: Add @setting_name {+ {| @qualid | @string } } + + Adds the specified values to the table :n:`@setting_name`. + +.. cmd:: Remove @setting_name {+ {| @qualid | @string } } + + Removes the specified value from the table :n:`@setting_name`. + +.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } } + + If :n:`@setting_name` is a flag or option, prints its current value. + If :n:`@setting_name` is a table: if the `for` clause is specified, reports + whether the table contains each specified value, otherise this is equivalent to + :cmd:`Print Table`. The `for` clause is not valid for flags and options. + + .. exn:: There is no flag, option or table with this name: "@setting_name". + + This error message is raised when calling the :cmd:`Test` + command (without the `for` clause), or the :cmd:`Print Table` + command, for an unknown :n:`@setting_name`. + + .. exn:: There is no qualid-valued table with this name: "@setting_name". + There is no string-valued table with this name: "@setting_name". + + These error messages are raised when calling the :cmd:`Add` or + :cmd:`Remove` commands, or the :cmd:`Test` command with the + `for` clause, if :n:`@setting_name` is unknown or does not have + the right type. + +.. cmd:: Print Options + + Prints the current value of all flags and options, and the names of all tables. + +.. cmd:: Print Table @setting_name + + Prints the values in the table :n:`@setting_name`. + +.. cmd:: Print Tables + + A synonym for :cmd:`Print Options`. + +.. _set_unset_scope_qualifiers: + +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. + +.. note:: + + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. 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 + (cf. :ref:`command-line-options`). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst new file mode 100644 index 0000000000..e43fa84e67 --- /dev/null +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -0,0 +1,1555 @@ +.. _gallinaspecificationlanguage: + +------------------------------------ + The Gallina specification language +------------------------------------ + +This chapter describes Gallina, the specification language of Coq. It allows +developing 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 :ref:`term`. The +language of commands, called *The Vernacular* is described in Section +:ref:`vernacular`. + +In Coq, logical objects are typed to ensure their logical correctness. The +rules implemented by the typing algorithm are described in Chapter :ref:`calculusofinductiveconstructions`. + + +.. About the grammars in the manual + ================================ + + Grammars are presented in Backus-Naur form (BNF). Terminal symbols are + set in black ``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 “``entry sep … sep entry``” stands for a non empty sequence + of expressions parsed by entry and separated by the literal “``sep``” [1]_. + + Similarly, the notation “``entry … entry``” stands for a non empty + sequence of expressions parsed by the “``entry``” entry, without any + separator between. + + At the end, the notation “``[entry sep … sep entry]``” stands for a + possibly empty sequence of expressions parsed by the “``entry``” entry, + separated by the literal “``sep``”. + +.. _term: + +Terms +===== + +Syntax of terms +--------------- + +The following grammars describe the basic syntax of the terms of the +*Calculus of Inductive Constructions* (also called Cic). The formal +presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`. Extensions of this syntax +are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax +is described in Chapter :ref:`syntaxextensionsandnotationscopes`. + +.. insertprodn term field_def + +.. prodn:: + term ::= forall @open_binders , @term + | fun @open_binders => @term + | @term_let + | if @term {? {? as @name } return @term100 } then @term else @term + | @term_fix + | @term_cofix + | @term100 + term100 ::= @term_cast + | @term10 + term10 ::= @term1 {+ @arg } + | @ @qualid {? @univ_annot } {* @term1 } + | @term1 + arg ::= ( @ident := @term ) + | @term1 + one_term ::= @term1 + | @ @qualid {? @univ_annot } + term1 ::= @term_projection + | @term0 % @scope_key + | @term0 + term0 ::= @qualid {? @univ_annot } + | @sort + | @numeral + | @string + | _ + | @term_evar + | @term_match + | ( @term ) + | %{%| {* @field_def } %|%} + | `%{ @term %} + | `( @term ) + | ltac : ( @ltac_expr ) + field_def ::= @qualid {* @binder } := @term + +.. note:: + + Many commands and tactics use :n:`@one_term` rather than :n:`@term`. + 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 with a :n:`@term1` applied to a list of arguments. + +.. _types: + +Types +----- + +.. prodn:: + type ::= @term + +:n:`@type`\s are a subset of :n:`@term`\s; not every :n:`@term` is a :n:`@type`. +Every term has an associated type, which +can be determined by applying the :ref:`typing-rules`. Distinct terms +may share the same type, for example 0 and 1 are both of type `nat`, the +natural numbers. + +.. _gallina-identifiers: + +Qualified identifiers and simple identifiers +-------------------------------------------- + +.. insertprodn qualid field_ident + +.. prodn:: + qualid ::= @ident {* @field_ident } + field_ident ::= .@ident + +*Qualified identifiers* (:n:`@qualid`) denote *global constants* +(definitions, lemmas, theorems, remarks or facts), *global variables* +(parameters or axioms), *inductive types* or *constructors of inductive +types*. *Simple identifiers* (or shortly :n:`@ident`) are a syntactic subset +of qualified identifiers. Identifiers may also denote *local variables*, +while qualified identifiers do not. + +Field identifiers, written :n:`@field_ident`, are identifiers prefixed by +`.` (dot) with no blank between the dot and the identifier. + + +Numerals and strings +-------------------- + +Numerals and strings have no predefined semantics in the calculus. They are +merely notations that can be bound to objects through the notation mechanism +(see Chapter :ref:`syntaxextensionsandnotationscopes` for details). +Initially, numerals are bound to Peano’s representation of natural +numbers (see :ref:`datatypes`). + +.. note:: + + Negative integers are not at the same level as :n:`@num`, for this + would make precedence unnatural. + +.. index:: + single: Set (sort) + single: SProp + single: Prop + single: Type + +Sorts +----- + +.. insertprodn sort univ_constraint + +.. prodn:: + sort ::= Set + | Prop + | SProp + | Type + | Type @%{ _ %} + | Type @%{ @universe %} + universe ::= max ( {+, @universe_expr } ) + | @universe_expr + universe_expr ::= @universe_name {? + @num } + universe_name ::= @qualid + | Set + | Prop + univ_annot ::= @%{ {* @universe_level } %} + universe_level ::= Set + | Prop + | Type + | _ + | @qualid + univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + univ_constraint ::= @universe_name {| < | = | <= } @universe_name + +There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. + +- :g:`SProp` is the universe of *definitionally irrelevant + propositions* (also called *strict propositions*). + +- :g:`Prop` is the universe of *logical propositions*. The logical propositions + themselves are typing the proofs. We denote propositions by :n:`@form`. + This constitutes a semantic subclass of the syntactic class :n:`@term`. + +- :g:`Set` is the universe of *program types* or *specifications*. The + specifications themselves are typing the programs. We denote + specifications by :n:`@specif`. This constitutes a semantic subclass of + the syntactic class :n:`@term`. + +- :g:`Type` is the type of sorts. + +More on sorts can be found in Section :ref:`sorts`. + +.. _binders: + +Binders +------- + +.. insertprodn open_binders binder + +.. prodn:: + open_binders ::= {+ @name } : @term + | {+ @binder } + name ::= _ + | @ident + binder ::= @name + | ( {+ @name } : @type ) + | ( @name {? : @type } := @term ) + | @implicit_binders + | @generalizing_binder + | ( @name : @type %| @term ) + | ' @pattern0 + +Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix` +*bind* variables. A binding is represented by an identifier. If the binding +variable is not used in the expression, the identifier can be replaced by the +symbol :g:`_`. When the type of a bound variable cannot be synthesized by the +system, it can be specified with the notation :n:`(@ident : @type)`. There is also +a notation for a sequence of binding variables sharing the same type: +:n:`({+ @ident} : @type)`. A +binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`. + +Some constructions allow the binding of a variable to value. This is +called a “let-binder”. The entry :n:`@binder` of the grammar accepts +either an assumption binder as defined above or a let-binder. The notation in +the latter case is :n:`(@ident := @term)`. In a let-binder, only one +variable can be introduced at the same time. It is also possible to give +the type of the variable as follows: +:n:`(@ident : @type := @term)`. + +Lists of :n:`@binder`\s are allowed. In the case of :g:`fun` and :g:`forall`, +it is intended that at least one binder of the list is an assumption otherwise +fun and forall gets identical. Moreover, parentheses can be omitted in +the case of a single sequence of bindings sharing the same type (e.g.: +:g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). + +.. index:: fun ... => ... + +Abstractions: fun +----------------- + +The expression :n:`fun @ident : @type => @term` defines the +*abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term +:n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to +the expression :n:`@term` (e.g. :g:`fun x : A => x` denotes the identity +function on type :g:`A`). The keyword :g:`fun` can be followed by several +binders as given in Section :ref:`binders`. Functions over +several variables are equivalent to an iteration of one-variable +functions. For instance the expression +:n:`fun {+ @ident__i } : @type => @term` +denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If +a let-binder occurs in +the list of binders, it is expanded to a let-in definition (see +Section :ref:`let-in`). + +.. index:: forall + +Products: forall +---------------- + +The expression :n:`forall @ident : @type, @term` denotes the +*product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. +As for abstractions, :g:`forall` is followed by a binder list, and products +over several variables are equivalent to an iteration of one-variable +products. Note that :n:`@term` is intended to be a type. + +If the variable :n:`@ident` occurs in :n:`@term`, the product is called +*dependent product*. The intention behind a dependent product +:g:`forall x : A, B` is twofold. It denotes either +the universal quantification of the variable :g:`x` of type :g:`A` +in the proposition :g:`B` or the functional dependent product from +:g:`A` to :g:`B` (a construction usually written +:math:`\Pi_{x:A}.B` in set theory). + +Non dependent product types have a special notation: :g:`A -> B` stands for +:g:`forall _ : A, B`. The *non dependent product* is used both to denote +the propositional implication and function types. + +Applications +------------ + +:n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`. + +:n:`@term__fun {+ @term__i }` denotes applying +:n:`@term__fun` to the arguments :n:`@term__i`. It is +equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: +associativity is to the left. + +The notation :n:`(@ident := @term)` for arguments is used for making +explicit the value of implicit arguments (see +Section :ref:`explicit-applications`). + +.. index:: + single: ... : ... (type cast) + single: ... <: ... + single: ... <<: ... + +Type cast +--------- + +.. insertprodn term_cast term_cast + +.. prodn:: + term_cast ::= @term10 <: @term + | @term10 <<: @term + | @term10 : @term + | @term10 :> + +The expression :n:`@term : @type` is a type cast expression. It enforces +the type of :n:`@term` to be :n:`@type`. + +:n:`@term <: @type` locally sets up the virtual machine for checking that +:n:`@term` has type :n:`@type`. + +:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +has type :n:`@type`. + +.. index:: _ + +Inferable subterms +------------------ + +Expressions often contain redundant pieces of information. Subterms that can be +automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will +guess the missing piece of information. + +.. index:: let ... := ... (term) + +.. _let-in: + +Let-in definitions +------------------ + +.. insertprodn term_let term_let + +.. prodn:: + term_let ::= let @name {? : @type } := @term in @term + | let @name {+ @binder } {? : @type } := @term in @term + | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term + | let ' @pattern := @term {? return @term100 } in @term + | let ' @pattern in @pattern := @term return @term100 in @term + +:n:`let @ident := @term in @term’` +denotes the local binding of :n:`@term` to the variable +:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in +definition of functions: :n:`let @ident {+ @binder} := @term in @term’` +stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. + +.. index:: match ... with ... + +Definition by cases: match +-------------------------- + +.. insertprodn term_match pattern0 + +.. prodn:: + term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end + case_item ::= @term100 {? as @name } {? in @pattern } + eqn ::= {+| {+, @pattern } } => @term + pattern ::= @pattern10 : @term + | @pattern10 + pattern10 ::= @pattern1 as @name + | @pattern1 {* @pattern1 } + | @ @qualid {* @pattern1 } + pattern1 ::= @pattern0 % @scope_key + | @pattern0 + pattern0 ::= @qualid + | %{%| {* @qualid := @pattern } %|%} + | _ + | ( {+| @pattern } ) + | @numeral + | @string + +Objects of inductive types can be destructured by a case-analysis +construction called *pattern matching* expression. A pattern matching +expression is used to analyze the structure of an inductive object and +to apply specific treatments accordingly. + +This paragraph describes the basic form of pattern matching. See +Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description +of the general form. The basic form of pattern matching is characterized +by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a +single :n:`@pattern` and :n:`@pattern` restricted to the form +:n:`@qualid {* @ident}`. + +The expression +:n:`match @term {? return @term100 } with {+| @pattern__i => @term__i } end` denotes a +*pattern matching* over the term :n:`@term` (expected to be +of an inductive type :math:`I`). The :n:`@term__i` +are the *branches* of the pattern matching +expression. Each :n:`@pattern__i` has the form :n:`@qualid @ident` +where :n:`@qualid` must denote a constructor. There should be +exactly one branch for every constructor of :math:`I`. + +The :n:`return @term100` clause gives the type returned by the whole match +expression. There are several cases. In the *non dependent* case, all +branches have the same type, and the :n:`return @term100` specifies that type. +In this case, :n:`return @term100` can usually be omitted as it can be +inferred from the type of the branches [1]_. + +In the *dependent* case, there are three subcases. In the first subcase, +the type in each branch may depend on the exact value being matched in +the branch. In this case, the whole pattern matching itself depends on +the term being matched. This dependency of the term being matched in the +return type is expressed with an :n:`@ident` clause where :n:`@ident` +is dependent in the return type. For instance, in the following example: + +.. coqtop:: in + + Inductive bool : Type := true : bool | false : bool. + Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. + Inductive or (A:Prop) (B:Prop) : Prop := + | or_introl : A -> or A B + | or_intror : B -> or A B. + + Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := + match b as x return or (eq bool x true) (eq bool x false) with + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) + end. + +the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" +and ":g:`or (eq bool false true) (eq bool false false)`" while the whole +pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +the identifier :g:`b` being used to represent the dependency. + +.. note:: + + When the term being matched is a variable, the ``as`` clause can be + omitted and the term being matched can serve itself as binding name in + the return type. For instance, the following alternative definition is + accepted and has the same meaning as the previous one. + + .. coqtop:: none + + Reset bool_case. + + .. coqtop:: in + + Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := + match b return or (eq bool b true) (eq bool b false) with + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) + end. + +The second subcase is only relevant for annotated inductive types such +as the equality predicate (see Section :ref:`coq-equality`), +the order predicate on natural numbers or the type of lists of a given +length (see Section :ref:`matching-dependent`). In this configuration, the +type of each branch can depend on the type dependencies specific to the +branch and the whole pattern matching expression has a type determined +by the specific dependencies in the type of the term being matched. This +dependency of the return type in the annotations of the inductive type +is expressed with a clause in the form +:n:`in @qualid {+ _ } {+ @pattern }`, where + +- :n:`@qualid` is the inductive type of the term being matched; + +- the holes :n:`_` match the parameters of the inductive type: the + return type is not dependent on them. + +- each :n:`@pattern` matches the annotations of the + inductive type: the return type is dependent on them + +- in the basic case which we describe below, each :n:`@pattern` + is a name :n:`@ident`; see :ref:`match-in-patterns` for the + general case + +For instance, in the following example: + +.. coqtop:: in + + Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := + match H in eq _ _ z return eq A z x with + | eq_refl _ _ => eq_refl A x + end. + +the type of the branch is :g:`eq A x x` because the third argument of +:g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the +type of the whole pattern matching expression has type :g:`eq A y x` because the +third argument of eq is y in the type of H. This dependency of the case analysis +in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the +return type. + +Finally, the third subcase is a combination of the first and second +subcase. In particular, it only applies to pattern matching on terms in +a type with annotations. For this third subcase, both the clauses ``as`` and +``in`` are available. + +There are specific notations for case analysis on types with one or two +constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see +Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). + +.. index:: + single: fix + single: cofix + +Recursive and co-recursive functions: fix and cofix +--------------------------------------------------- + +.. insertprodn term_fix fixannot + +.. prodn:: + term_fix ::= let fix @fix_body in @term + | fix @fix_body {? {+ with @fix_body } for @ident } + fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term + fixannot ::= %{ struct @ident %} + | %{ wf @one_term @ident %} + | %{ measure @one_term {? @ident } {? @one_term } %} + + +The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the +:math:`i`-th component of a block of functions defined by mutual structural +recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When +:math:`n=1`, the ":n:`for @ident__i`" clause is omitted. + +The association of a single fixpoint and a local definition have a special +syntax: :n:`let fix @ident {* @binder } := @term in` stands for +:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints. + +Some options of :n:`@fixannot` are only supported in specific constructs. :n:`fix` and :n:`let fix` +only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in +commands such as :cmd:`Function` and :cmd:`Program Fixpoint`. + +.. insertprodn term_cofix cofix_body + +.. prodn:: + term_cofix ::= let cofix @cofix_body in @term + | cofix @cofix_body {? {+ with @cofix_body } for @ident } + cofix_body ::= @ident {* @binder } {? : @type } := @term + +The expression +":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`" +denotes the :math:`i`-th component of a block of terms defined by a mutual guarded +co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When +:math:`n=1`, the ":n:`for @ident__i`" clause is omitted. + +.. _vernacular: + +The Vernacular +============== + +.. insertprodn vernacular sentence + +.. prodn:: + vernacular ::= {* @sentence } + sentence ::= {? @all_attrs } @command . + | {? @all_attrs } {? @num : } @query_command . + | {? @all_attrs } {? @toplevel_selector } @ltac_expr {| . | ... } + | @control_command + +The top-level input to |Coq| is a series of :n:`@sentence`\s, +which are :production:`tactic`\s or :production:`command`\s, +generally terminated with a period +and optionally decorated with :ref:`gallina-attributes`. :n:`@ltac_expr` syntax supports both simple +and compound tactics. For example: ``split`` is a simple tactic while ``split; auto`` combines two +simple tactics. + +Tactics specify how to transform the current proof state as a step in creating a proof. They +are syntactically valid only when |Coq| is in proof mode, such as after a :cmd:`Theorem` command +and before any subsequent proof-terminating command such as :cmd:`Qed`. See :ref:`proofhandling` for more +on proof mode. + +By convention, command names begin with uppercase letters, while +tactic names begin with lowercase letters. Commands appear in the +HTML documentation in blue boxes after the label "Command". In the pdf, they appear +after the boldface label "Command:". Commands are listed in the :ref:`command_index`. + +Similarly, tactics appear after the label "Tactic". Tactics are listed in the :ref:`tactic_index`. + +.. _gallina-assumptions: + +Assumptions +----------- + +Assumptions extend the environment with axioms, parameters, hypotheses +or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted +by Coq if and only if this :n:`@type` is a correct type in the environment +preexisting the declaration and if :n:`@ident` was not previously defined in +the same module. This :n:`@type` is considered to be the type (or +specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` +has type :n:`@type`. + +.. _Axiom: + +.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt } + :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables + + .. insertprodn assumption_token of_type + + .. prodn:: + assumption_token ::= {| Axiom | Axioms } + | {| Conjecture | Conjectures } + | {| Parameter | Parameters } + | {| Hypothesis | Hypotheses } + | {| Variable | Variables } + assumpt ::= {+ @ident_decl } @of_type + ident_decl ::= @ident {? @univ_decl } + of_type ::= {| : | :> | :>> } @type + + These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in + the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence + of an object of this type) is accepted as a postulate. + + :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms + are equivalent. They can take the :attr:`local` attribute (see :ref:`gallina-attributes`), + which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants + only through their fully qualified names. + + Similarly, :cmd:`Hypothesis`, :cmd:`Variable` and their plural forms are equivalent. Outside + of a section, these are equivalent to :n:`Local Parameter`. Inside a section, the + :n:`@ident`\s defined are only accessible within the section. When the current section + is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly + parameterized (i.e., the variables are *discharged*). See Section :ref:`section-mechanism`. + + The :n:`Inline` clause is only relevant inside functors. See :cmd:`Module`. + +.. example:: Simple assumptions + + .. coqtop:: reset in + + Parameter X Y : Set. + Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop). + Axiom R_S_inv : forall x y, R x y <-> S y x. + +.. exn:: @ident already exists. + :name: @ident already exists. (Axiom) + :undocumented: + +.. warn:: @ident is declared as a local axiom + + Warning generated when using :cmd:`Variable` or its equivalent + instead of :n:`Local Parameter` or its equivalent. + +.. note:: + We advise using the commands :cmd:`Axiom`, :cmd:`Conjecture` and + :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when + the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands + :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases + (corresponding to the declaration of an abstract object of the given type). + +.. _gallina-definitions: + +Definitions +----------- + +Definitions extend the environment with associations of names to terms. +A definition can be seen as a way to give a meaning to a name or as a +way to abbreviate a term. In any case, the name can later be replaced at +any time by its definition. + +The operation of unfolding a name into its definition is called +:math:`\delta`-conversion (see Section :ref:`delta-reduction`). A +definition is accepted by the system if and only if the defined term is +well-typed in the current context of the definition and if the name is +not already used. The name defined by the definition is called a +*constant* and the term it refers to is its *body*. A definition has a +type which is the type of its body. + +A formal presentation of constants and environments is given in +Section :ref:`typing-rules`. + +.. cmd:: {| Definition | Example } @ident_decl @def_body + :name: Definition; Example + + .. insertprodn def_body def_body + + .. prodn:: + def_body ::= {* @binder } {? : @type } := {? @reduce } @term + | {* @binder } : @type + + These commands bind :n:`@term` to the name :n:`@ident` in the environment, + provided that :n:`@term` is well-typed. They can take the :attr:`local` attribute (see :ref:`gallina-attributes`), + which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants + only through their fully qualified names. + If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified + computation on :n:`@term`. + + These commands also support the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`program` and + :attr:`canonical` attributes. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + + The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term` + is definitionally equal to :n:`@type`, and registers :n:`@ident` as being of type + :n:`@type`, and bound to value :n:`@term`. + + The form :n:`Definition @ident {* @binder } : @type := @term` is equivalent to + :n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`. + + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + + .. exn:: @ident already exists. + :name: @ident already exists. (Definition) + :undocumented: + + .. exn:: The term @term has type @type while it is expected to have type @type'. + :undocumented: + +.. _gallina-inductive-definitions: + +Inductive types +--------------- + +.. cmd:: Inductive @inductive_definition {* with @inductive_definition } + + .. insertprodn inductive_definition constructor + + .. prodn:: + inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + constructors_or_record ::= {? %| } {+| @constructor } + | {? @ident } %{ {*; @record_field } %} + constructor ::= @ident {* @binder } {? @of_type } + + This command defines one or more + inductive types and its constructors. Coq generates destructors + depending on the universe that the inductive type belongs to. + + The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``, + :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_sind``, which + respectively correspond to elimination principles on :g:`Type`, :g:`Prop`, + :g:`Set` and :g:`SProp`. The type of the destructors + expresses structural induction/recursion principles over objects of + type :n:`@ident`. The constant :n:`@ident`\ ``_ind`` is always + generated, whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect`` + may be impossible to derive (for example, when :n:`@ident` is a + proposition). + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + + Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. + The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. + Each :n:`@ident` can be used independently thereafter. + See :ref:`mutually_inductive_types`. + + If the entire inductive definition is parameterized with :n:`@binder`\s, the parameters correspond + to a local context in which the entire set of inductive declarations is interpreted. + For this reason, the parameters must be strictly the same for each inductive type. + See :ref:`parametrized-inductive-types`. + + Constructor :n:`@ident`\s can come with :n:`@binder`\s, in which case + the actual type of the constructor is :n:`forall {* @binder }, @type`. + + .. exn:: Non strictly positive occurrence of @ident in @type. + + The types of the constructors have to satisfy a *positivity condition* + (see Section :ref:`positivity`). This condition ensures the soundness of + the inductive definition. The positivity checking can be disabled using + the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`). + + .. exn:: The conclusion of @type is not valid; it must be built from @ident. + + The conclusion of the type of the constructors must be the inductive type + :n:`@ident` being defined (or :n:`@ident` applied to arguments in + the case of annotated inductive types — cf. next section). + +The following subsections show examples of simple inductive types, +simple annotated inductive types, simple parametric inductive types, +mutually inductive types and private (matching) inductive types. + +.. _simple-inductive-types: + +Simple inductive types +~~~~~~~~~~~~~~~~~~~~~~ + +A simple inductive type belongs to a universe that is a simple :n:`@sort`. + +.. example:: + + The set of natural numbers is defined as: + + .. coqtop:: reset all + + Inductive nat : Set := + | O : nat + | S : nat -> nat. + + The type nat is defined as the least :g:`Set` containing :g:`O` and closed by + the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the + environment. + + This definition generates four elimination principles: + :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is: + + .. coqtop:: all + + Check nat_ind. + + This is the well known structural induction principle over natural + numbers, i.e. the second-order form of Peano’s induction principle. It + allows proving universal properties of natural numbers (:g:`forall + n:nat, P n`) by induction on :g:`n`. + + The types of :g:`nat_rect`, :g:`nat_rec` and :g:`nat_sind` are similar, except that they + apply to, respectively, :g:`(P:nat->Type)`, :g:`(P:nat->Set)` and :g:`(P:nat->SProp)`. They correspond to + primitive induction principles (allowing dependent types) respectively + over sorts ```Type``, ``Set`` and ``SProp``. + +In the case where inductive types don't have annotations (the next section +gives an example of annotations), a constructor can be defined +by giving the type of its arguments alone. + +.. example:: + + .. coqtop:: reset none + + Reset nat. + + .. coqtop:: in + + Inductive nat : Set := O | S (_:nat). + +Simple annotated inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In annotated inductive types, the universe where the inductive type +is defined is no longer a simple :n:`@sort`, but what is called an arity, +which is a type whose conclusion is a :n:`@sort`. + +.. example:: + + As an example of annotated inductive types, let us define the + :g:`even` predicate: + + .. coqtop:: all + + Inductive even : nat -> Prop := + | even_0 : even O + | even_SS : forall n:nat, even n -> even (S (S n)). + + The type :g:`nat->Prop` means that :g:`even` is a unary predicate (inductively + defined) over natural numbers. The type of its two constructors are the + defining clauses of the predicate :g:`even`. The type of :g:`even_ind` is: + + .. coqtop:: all + + Check even_ind. + + From a mathematical point of view, this asserts that the natural numbers satisfying + the predicate :g:`even` are exactly in the smallest set of naturals satisfying the + clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any + predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O` + and to prove that if any natural number :g:`n` satisfies :g:`P` its double + successor :g:`(S (S n))` satisfies also :g:`P`. This is analogous to the + structural induction principle we got for :g:`nat`. + +.. _parametrized-inductive-types: + +Parameterized inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In the previous example, each constructor introduces a different +instance of the predicate :g:`even`. In some cases, all the constructors +introduce the same generic instance of the inductive definition, in +which case, instead of an annotation, we use a context of parameters +which are :n:`@binder`\s shared by all the constructors of the definition. + +Parameters differ from inductive type annotations in that the +conclusion of each type of constructor invokes the inductive type with +the same parameter values of its specification. + +.. example:: + + A typical example is the definition of polymorphic lists: + + .. coqtop:: all + + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. + + In the type of :g:`nil` and :g:`cons`, we write ":g:`list A`" and not + just ":g:`list`". The constructors :g:`nil` and :g:`cons` have these types: + + .. coqtop:: all + + Check nil. + Check cons. + + Observe that the destructors are also quantified with :g:`(A:Set)`, for example: + + .. coqtop:: all + + Check list_ind. + + Once again, the types of the constructor arguments and of the conclusion can be omitted: + + .. coqtop:: none + + Reset list. + + .. coqtop:: in + + Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). + +.. note:: + + The constructor type can + recursively invoke the inductive definition on an argument which is not + the parameter itself. + + One can define : + + .. coqtop:: all + + Inductive list2 (A:Set) : Set := + | nil2 : list2 A + | cons2 : A -> list2 (A*A) -> list2 A. + + that can also be written by specifying only the type of the arguments: + + .. coqtop:: all reset + + Inductive list2 (A:Set) : Set := + | nil2 + | cons2 (_:A) (_:list2 (A*A)). + + But the following definition will give an error: + + .. coqtop:: all + + Fail Inductive listw (A:Set) : Set := + | nilw : listw (A*A) + | consw : A -> listw (A*A) -> listw (A*A). + + because the conclusion of the type of constructors should be :g:`listw A` + in both cases. + + + A parameterized inductive definition can be defined using annotations + instead of parameters but it will sometimes give a different (bigger) + sort for the inductive definition and will produce a less convenient + rule for case elimination. + +.. flag:: Uniform Inductive Parameters + + When this flag is set (it is off by default), + inductive definitions are abstracted over their parameters + before type checking constructors, allowing to write: + + .. coqtop:: all + + Set Uniform Inductive Parameters. + Inductive list3 (A:Set) : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + + This behavior is essentially equivalent to starting a new section + and using :cmd:`Context` to give the uniform parameters, like so + (cf. :ref:`section-mechanism`): + + .. coqtop:: all reset + + Section list3. + Context (A:Set). + Inductive list3 : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + End list3. + + For finer control, you can use a ``|`` between the uniform and + the non-uniform parameters: + + .. coqtop:: in reset + + Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. + + The flag can then be seen as deciding whether the ``|`` is at the + beginning (when the flag is unset) or at the end (when it is set) + of the parameters when not explicitly given. + +.. seealso:: + Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. + +.. _mutually_inductive_types: + +Mutually defined inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Mutually defined inductive types + + A typical example of mutually inductive data types is trees and + forests. We assume two types :g:`A` and :g:`B` that are given as variables. The types can + be declared like this: + + .. coqtop:: in + + Parameters A B : Set. + + Inductive tree : Set := node : A -> forest -> tree + + with forest : Set := + | leaf : B -> forest + | cons : tree -> forest -> forest. + + This declaration automatically generates eight induction principles. They are not the most + general principles, but they correspond to each inductive part seen as a single inductive definition. + + To illustrate this point on our example, here are the types of :g:`tree_rec` + and :g:`forest_rec`. + + .. coqtop:: all + + Check tree_rec. + + Check forest_rec. + + Assume we want to parameterize our mutual inductive definitions with the + two type variables :g:`A` and :g:`B`, the declaration should be + done as follows: + + .. coqdoc:: + + Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B + + with forest (A B:Set) : Set := + | leaf : B -> forest A B + | cons : tree A B -> forest A B -> forest A B. + + Assume we define an inductive definition inside a section + (cf. :ref:`section-mechanism`). When the section is closed, the variables + declared in the section and occurring free in the declaration are added as + parameters to the inductive definition. + +.. seealso:: + A generic command :cmd:`Scheme` is useful to build automatically various + mutual induction principles. + +Private (matching) inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. attr:: private(matching) + + This attribute can be used to forbid the use of the :g:`match` + construct on objects of this inductive type outside of the module + where it is defined. There is also a legacy syntax using the + ``Private`` prefix (cf. :n:`@legacy_attr`). + + The main use case of private (matching) inductive types is to emulate + quotient types / higher-order inductive types in projects such as + the `HoTT library <https://github.com/HoTT/HoTT>`_. + +.. example:: + + .. coqtop:: all + + Module Foo. + #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat. + Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + End Foo. + Import Foo. + Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + +Variants +~~~~~~~~ + +.. cmd:: Variant @variant_definition {* with @variant_definition } + + .. insertprodn variant_definition variant_definition + + .. prodn:: + variant_definition ::= @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations } + + The :cmd:`Variant` command is similar to the :cmd:`Inductive` command, except + that it disallows recursive definition of types (for instance, lists cannot + be defined using :cmd:`Variant`). No induction scheme is generated for + this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + + .. exn:: The @num th argument of @ident must be @ident in @type. + :undocumented: + +.. _coinductive-types: + +Co-inductive types +------------------ + +The objects of an inductive type are well-founded with respect to the +constructors of the type. In other words, such objects contain only a +*finite* number of constructors. Co-inductive types arise from relaxing +this condition, and admitting types whose objects contain an infinity of +constructors. Infinite objects are introduced by a non-ending (but +effective) process of construction, defined in terms of the constructors +of the type. + +.. cmd:: CoInductive @inductive_definition {* with @inductive_definition } + + This command introduces a co-inductive type. + The syntax of the command is the same as the command :cmd:`Inductive`. + No principle of induction is derived from the definition of a co-inductive + type, since such principles only make sense for inductive types. + For co-inductive types, the only elimination principle is case analysis. + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + +.. example:: + + The type of infinite sequences of natural numbers, usually called streams, + is an example of a co-inductive type. + + .. coqtop:: in + + CoInductive Stream : Set := Seq : nat -> Stream -> Stream. + + The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` + can be defined as follows: + + .. coqtop:: in + + Definition hd (x:Stream) := let (a,s) := x in a. + Definition tl (x:Stream) := let (a,s) := x in s. + +Definitions of co-inductive predicates and blocks of mutually +co-inductive definitions are also allowed. + +.. example:: + + The extensional equality on streams is an example of a co-inductive type: + + .. coqtop:: in + + CoInductive EqSt : Stream -> Stream -> Prop := + eqst : forall s1 s2:Stream, + hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. + + In order to prove the extensional equality of two streams :g:`s1` and :g:`s2` + we have to construct an infinite proof of equality, that is, an infinite + object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite + objects in Section :ref:`cofixpoint`. + +Caveat +~~~~~~ + +The ability to define co-inductive types by constructors, hereafter called +*positive co-inductive types*, is known to break subject reduction. The story is +a bit long: this is due to dependent pattern-matching which implies +propositional η-equality, which itself would require full η-conversion for +subject reduction to hold, but full η-conversion is not acceptable as it would +make type checking undecidable. + +Since the introduction of primitive records in Coq 8.5, an alternative +presentation is available, called *negative co-inductive types*. This consists +in defining a co-inductive type as a primitive record type through its +projections. Such a technique is akin to the *co-pattern* style that can be +found in e.g. Agda, and preserves subject reduction. + +The above example can be rewritten in the following way. + +.. coqtop:: none + + Reset Stream. + +.. coqtop:: all + + Set Primitive Projections. + CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. + CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_hd : hd s1 = hd s2; + eqst_tl : EqSt (tl s1) (tl s2); + }. + +Some properties that hold over positive streams are lost when going to the +negative presentation, typically when they imply equality over streams. +For instance, propositional η-equality is lost when going to the negative +presentation. It is nonetheless logically consistent to recover it through an +axiom. + +.. coqtop:: all + + Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s). + +More generally, as in the case of positive coinductive types, it is consistent +to further identify extensional equality of coinductive types with propositional +equality: + +.. coqtop:: all + + Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. + +As of Coq 8.9, it is now advised to use negative co-inductive types rather than +their positive counterparts. + +.. seealso:: + :ref:`primitive_projections` for more information about negative + records and primitive projections. + + +Definition of recursive functions +--------------------------------- + +Definition of functions by recursion over inductive objects +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This section describes the primitive form of definition by recursion over +inductive objects. See the :cmd:`Function` command for more advanced +constructions. + +.. _Fixpoint: + +.. cmd:: Fixpoint @fix_definition {* with @fix_definition } + + .. insertprodn fix_definition fix_definition + + .. prodn:: + fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } + + This command allows defining functions by pattern matching over inductive + objects using a fixed point construction. The meaning of this declaration is + to define :n:`@ident` as a recursive function with arguments specified by + the :n:`@binder`\s such that :n:`@ident` applied to arguments + corresponding to these :n:`@binder`\s has type :n:`@type`, and is + equivalent to the expression :n:`@term`. The type of :n:`@ident` is + consequently :n:`forall {* @binder }, @type` and its value is equivalent + to :n:`fun {* @binder } => @term`. + + To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical + constraints on a special argument called the decreasing argument. They + are needed to ensure that the :cmd:`Fixpoint` definition always terminates. + The point of the :n:`{struct @ident}` annotation (see :n:`@fixannot`) is to + let the user tell the system which argument decreases along the recursive calls. + + The :n:`{struct @ident}` annotation may be left implicit, in which case the + system successively tries arguments from left to right until it finds one + that satisfies the decreasing condition. + + :cmd:`Fixpoint` without the :attr:`program` attribute does not support the + :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. + + The :n:`with` clause allows simultaneously defining several mutual fixpoints. + It is especially useful when defining functions over mutually defined + inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + + .. note:: + + + Some fixpoints may have several arguments that fit as decreasing + arguments, and this choice influences the reduction of the fixpoint. + Hence an explicit annotation must be used if the leftmost decreasing + argument is not the desired one. Writing explicit annotations can also + speed up type checking of large mutual fixpoints. + + + In order to keep the strong normalization property, the fixed point + reduction will only be performed when the argument in position of the + decreasing argument (which type should be in an inductive definition) + starts with a constructor. + + + .. example:: + + One can define the addition function as : + + .. coqtop:: all + + Fixpoint add (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (add p m) + end. + + The match operator matches a value (here :g:`n`) with the various + constructors of its (inductive) type. The remaining arguments give the + respective values to be returned, as functions of the parameters of the + corresponding constructor. Thus here when :g:`n` equals :g:`O` we return + :g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`. + + The match operator is formally described in + Section :ref:`match-construction`. + The system recognizes that in the inductive call :g:`(add p m)` the first + argument actually decreases because it is a *pattern variable* coming + from :g:`match n with`. + + .. example:: + + The following definition is not correct and generates an error message: + + .. coqtop:: all + + Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := + match m with + | O => n + | S p => S (wrongplus n p) + end. + + because the declared decreasing argument :g:`n` does not actually + decrease in the recursive call. The function computing the addition over + the second argument should rather be written: + + .. coqtop:: all + + Fixpoint plus (n m:nat) {struct m} : nat := + match m with + | O => n + | S p => S (plus n p) + end. + + .. example:: + + The recursive call may not only be on direct subterms of the recursive + variable :g:`n` but also on a deeper subterm and we can directly write + the function :g:`mod2` which gives the remainder modulo 2 of a natural + number. + + .. coqtop:: all + + Fixpoint mod2 (n:nat) : nat := + match n with + | O => O + | S p => match p with + | O => S O + | S q => mod2 q + end + end. + +.. _example_mutual_fixpoints: + + .. example:: Mutual fixpoints + + The size of trees and forests can be defined the following way: + + .. coqtop:: all + + Fixpoint tree_size (t:tree) : nat := + match t with + | node a f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | leaf b => 1 + | cons t f' => (tree_size t + forest_size f') + end. + +.. _cofixpoint: + +Definitions of recursive objects in co-inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition } + + .. insertprodn cofix_definition cofix_definition + + .. prodn:: + cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations } + + This command introduces a method for constructing an infinite object of a + coinductive type. For example, the stream containing all natural numbers can + be introduced applying the following method to the number :g:`O` (see + Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` + and :g:`tl`): + + .. coqtop:: all + + CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). + + Unlike recursive definitions, there is no decreasing argument in a + co-recursive definition. To be admissible, a method of construction must + provide at least one extra constructor of the infinite object for each + iteration. A syntactical guard condition is imposed on co-recursive + definitions in order to ensure this: each recursive call in the + definition must be protected by at least one constructor, and only by + constructors. That is the case in the former definition, where the single + recursive call of :g:`from` is guarded by an application of :g:`Seq`. + On the contrary, the following recursive function does not satisfy the + guard condition: + + .. coqtop:: all + + Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := + if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). + + The elimination of co-recursive definition is done lazily, i.e. the + definition is expanded only when it occurs at the head of an application + which is the argument of a case analysis expression. In any other + context, it is considered as a canonical expression which is completely + evaluated. We can test this using the command :cmd:`Eval`, which computes + the normal forms of a term: + + .. coqtop:: all + + Eval compute in (from 0). + Eval compute in (hd (from 0)). + Eval compute in (tl (from 0)). + + As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously + defining several mutual cofixpoints. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + +.. _Computations: + +Computations +------------ + +.. insertprodn reduce pattern_occ + +.. prodn:: + reduce ::= Eval @red_expr in + red_expr ::= red + | hnf + | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | cbv {? @strategy_flag } + | cbn {? @strategy_flag } + | lazy {? @strategy_flag } + | compute {? @delta_flag } + | vm_compute {? @ref_or_pattern_occ } + | native_compute {? @ref_or_pattern_occ } + | unfold {+, @unfold_occ } + | fold {+ @one_term } + | pattern {+, @pattern_occ } + | @ident + delta_flag ::= {? - } [ {+ @smart_qualid } ] + strategy_flag ::= {+ @red_flags } + | @delta_flag + red_flags ::= beta + | iota + | match + | fix + | cofix + | zeta + | delta {? @delta_flag } + ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums } + | @one_term {? at @occs_nums } + occs_nums ::= {+ {| @num | @ident } } + | - {| @num | @ident } {* @int_or_var } + int_or_var ::= @int + | @ident + unfold_occ ::= @smart_qualid {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } + +See :ref:`Conversion-rules`. + +.. todo:: Add text here + +.. _Assertions: + +Assertions and proofs +--------------------- + +An assertion states a proposition (or a type) of which the proof (or an +inhabitant of the type) is interactively built using tactics. The interactive +proof mode is described in Chapter :ref:`proofhandling` and the tactics in +Chapter :ref:`Tactics`. The basic assertion command is: + +.. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type } + :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property + + .. insertprodn thm_token thm_token + + .. prodn:: + thm_token ::= Theorem + | Lemma + | Fact + | Remark + | Corollary + | Proposition + | Property + + After the statement is asserted, Coq needs a proof. Once a proof of + :n:`@type` under the assumptions represented by :n:`@binder`\s is given and + validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and + the theorem is bound to the name :n:`@ident` in the environment. + + Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction + over a mutually inductive assumption, or that assert mutually dependent + statements in some mutual co-inductive type. It is equivalent to + :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of + the statements (or the body of the specification, depending on the point of + view). The inductive or co-inductive types on which the induction or + coinduction has to be done is assumed to be non ambiguous and is guessed by + the system. + + Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses + have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or + be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that + recursive proof arguments are correct is done only at the time of registering + the lemma in the environment. To know if the use of induction hypotheses is + correct at some time of the interactive development of a proof, use the + command :cmd:`Guarded`. + + .. exn:: The term @term has type @type which should be Set, Prop or Type. + :undocumented: + + .. exn:: @ident already exists. + :name: @ident already exists. (Theorem) + + The name you provided is already defined. You have then to choose + another name. + + .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on. + + You are asserting a new statement while already being in proof editing mode. + This feature, called nested proofs, is disabled by default. + To activate it, turn the :flag:`Nested Proofs Allowed` flag on. + +Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +until the proof is completed. In proof editing mode, the user primarily enters +tactics, which are described in chapter :ref:`Tactics`. The user may also enter +commands to manage the proof editing mode. They are described in Chapter +:ref:`proofhandling`. + +When the proof is complete, use the :cmd:`Qed` command so the kernel verifies +the proof and adds it to the environment. + +.. note:: + + #. Several statements can be simultaneously asserted provided the + :flag:`Nested Proofs Allowed` flag was turned on. + + #. Not only other assertions but any vernacular command can be given + while in the process of proving a given assertion. In this case, the + command is understood as if it would have been given before the + statements still to be proved. Nonetheless, this practice is discouraged + and may stop working in future versions. + + #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be + unfolded (see :ref:`performingcomputations`), thus + realizing some form of *proof-irrelevance*. To be able to unfold a + proof, the proof should be ended by :cmd:`Defined`. + + #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite + side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. + + #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the + current asserted statement into an axiom and exit the proof editing mode. + +.. [1] + Except if the inductive type is empty in which case there is no + equation that can be used to infer the return type. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst deleted file mode 100644 index 3d69126b2d..0000000000 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ /dev/null @@ -1,1209 +0,0 @@ -.. _vernacularcommands: - -Vernacular commands -============================= - -.. _displaying: - -Displaying ----------- - - -.. _Print: - -.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list } - - .. insertprodn univ_name_list univ_name_list - - .. prodn:: - univ_name_list ::= @%{ {* @name } %} - - Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`. - - * :n:`Term` - a syntactic marker to allow printing a term - that is the same as one of the various :n:`Print` commands. For example, - :cmd:`Print All` is a different command, while :n:`Print Term All` shows - information on the object whose name is ":n:`All`". - - * :n:`@univ_name_list` - locally renames the - polymorphic universes of :n:`@smart_qualid`. - The name `_` means the usual name is printed. - - .. exn:: @qualid not a defined object. - :undocumented: - - .. exn:: Universe instance should have length @num. - :undocumented: - - .. exn:: This object does not support universe names. - :undocumented: - - -.. cmd:: Print All - - This command displays information about the current state of the - environment, including sections and modules. - -.. cmd:: Inspect @num - - This command displays the :n:`@num` last objects of the - current environment, including sections and modules. - -.. cmd:: Print Section @qualid - - Displays the objects defined since the beginning of the section named :n:`@qualid`. - - .. todo: "A.B" is permitted but unnecessary for modules/sections. - should the command just take an @ident? - - -.. _flags-options-tables: - -Flags, Options and Tables ------------------------------ - -Coq has many settings to control its behavior. Setting types include flags, options -and tables: - -* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`. -* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`. -* A *table* contains a set of strings or qualids. -* In addition, some commands provide settings, such as :cmd:`Extraction Language`. - -.. FIXME Convert "Extraction Language" to an option. - -Flags, options and tables are identified by a series of identifiers, each with an initial -capital letter. - -.. cmd:: Set @setting_name {? {| @int | @string } } - :name: Set - - .. insertprodn setting_name setting_name - - .. prodn:: - setting_name ::= {+ @ident } - - If :n:`@setting_name` is a flag, no value may be provided; the flag - is set to on. - If :n:`@setting_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 :attr:`local`, :attr:`global` and :attr:`export` attributes. - They are described :ref:`here <set_unset_scope_qualifiers>`. - - .. warn:: There is no flag or option with this name: "@setting_name". - - This warning message can be raised by :cmd:`Set` and - :cmd:`Unset` when :n:`@setting_name` is unknown. It is a - warning rather than an error because this helps library authors - produce Coq code that is compatible with several Coq versions. - To preserve the same behavior, they may need to set some - compatibility flags or options that did not exist in previous - Coq versions. - -.. cmd:: Unset @setting_name - :name: Unset - - If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is - set to its default value. - - This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. - They are described :ref:`here <set_unset_scope_qualifiers>`. - -.. cmd:: Add @setting_name {+ {| @qualid | @string } } - - Adds the specified values to the table :n:`@setting_name`. - -.. cmd:: Remove @setting_name {+ {| @qualid | @string } } - - Removes the specified value from the table :n:`@setting_name`. - -.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } } - - If :n:`@setting_name` is a flag or option, prints its current value. - If :n:`@setting_name` is a table: if the `for` clause is specified, reports - whether the table contains each specified value, otherise this is equivalent to - :cmd:`Print Table`. The `for` clause is not valid for flags and options. - - .. exn:: There is no flag, option or table with this name: "@setting_name". - - This error message is raised when calling the :cmd:`Test` - command (without the `for` clause), or the :cmd:`Print Table` - command, for an unknown :n:`@setting_name`. - - .. exn:: There is no qualid-valued table with this name: "@setting_name". - There is no string-valued table with this name: "@setting_name". - - These error messages are raised when calling the :cmd:`Add` or - :cmd:`Remove` commands, or the :cmd:`Test` command with the - `for` clause, if :n:`@setting_name` is unknown or does not have - the right type. - -.. cmd:: Print Options - - Prints the current value of all flags and options, and the names of all tables. - -.. cmd:: Print Table @setting_name - - Prints the values in the table :n:`@setting_name`. - -.. cmd:: Print Tables - - A synonym for :cmd:`Print Options`. - -.. _set_unset_scope_qualifiers: - -Locality attributes supported by :cmd:`Set` and :cmd:`Unset` -```````````````````````````````````````````````````````````` - -The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, -:attr:`global` and :attr:`export` locality attributes: - -* no attribute: the original setting is *not* restored at the end of - the current module or section. -* :attr:`local` (an alternative syntax is to use the ``Local`` - prefix): the setting is applied within the current module or - section. The original value of the setting is restored at the end - of the current module or section. -* :attr:`export` (an alternative syntax is to use the ``Export`` - prefix): similar to :attr:`local`, the original value of the setting - is restored at the end of the current module or section. In - addition, if the value is set in a module, then :cmd:`Import`\-ing - the module sets the option or flag. -* :attr:`global` (an alternative syntax is to use the ``Global`` - prefix): the original setting is *not* restored at the end of the - current module or section. In addition, if the value is set in a - file, then :cmd:`Require`\-ing the file sets the option. - -Newly opened modules and sections inherit the current settings. - -.. note:: - - The use of the :attr:`global` attribute with the :cmd:`Set` and - :cmd:`Unset` commands is discouraged. 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 - (cf. :ref:`command-line-options`). - -Query commands --------------- - -Unlike other commands, :production:`query_command`\s may be prefixed with -a goal selector (:n:`@num:`) to specify which goal context it applies to. -If no selector is provided, -the command applies to the current goal. If no proof is open, then the command only applies -to accessible objects. (see Section :ref:`invocation-of-tactics`). - -.. cmd:: About @smart_qualid {? @univ_name_list } - - Displays information about the :n:`@smart_qualid` object, which, - if a proof is open, may be a hypothesis of the selected goal, - or an accessible theorem, axiom, etc.: - its kind (module, constant, assumption, inductive, - constructor, abbreviation, …), long name, type, implicit arguments and - argument scopes (as set in the definition of :token:`smart_qualid` or - subsequently with the :cmd:`Arguments` command). It does not print the body of definitions or proofs. - -.. cmd:: Check @term - - Displays the type of :n:`@term`. When called in proof mode, the - term is checked in the local context of the selected goal. - -.. cmd:: Eval @red_expr in @term - - Performs the specified reduction on :n:`@term` and displays - the resulting term with its type. If a proof is open, :n:`@term` - may reference hypotheses of the selected goal. - - .. seealso:: Section :ref:`performingcomputations`. - - -.. cmd:: Compute @term - - Evaluates :n:`@term` using the bytecode-based virtual machine. - It is a shortcut for :cmd:`Eval` :n:`vm_compute in @term`. - - .. seealso:: Section :ref:`performingcomputations`. - -.. cmd:: Search {+ {? - } @search_item } {? {| inside | outside } {+ @qualid } } - - .. insertprodn search_item search_item - - .. prodn:: - search_item ::= @one_term - | @string {? % @scope_key } - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context - matching :n:`@search_item`\s. - It's useful for finding the names of library lemmas. - - * :n:`@one_term` - Search for objects containing a subterm matching the pattern - :n:`@one_term` in which holes of the pattern are indicated by `_` or :n:`?@ident`. - If the same :n:`?@ident` occurs more than once in the pattern, all occurrences must - match the same value. - - * :n:`@string` - If :n:`@string` is a substring of a valid identifier, - search for objects whose name contains :n:`@string`. If :n:`@string` is a notation - string associated with a :n:`@qualid`, that's equivalent to :cmd:`Search` :n:`@qualid`. - For example, specifying `"+"` or `"_ + _"`, which are notations for `Nat.add`, are equivalent - to :cmd:`Search` `Nat.add`. - - * :n:`% @scope` - limits the search to the scope bound to - the delimiting key :n:`@scope`, such as, for example, :n:`%nat`. - This clause may be used only if :n:`@string` contains a notation string. - (see Section :ref:`LocalInterpretationRulesForNotations`) - - If you specify multiple :n:`@search_item`\s, all the conditions must be satisfied - for the object to be displayed. The minus sign `-` excludes objects that contain - the :n:`@search_item`. - - Additional clauses: - - * :n:`inside {+ @qualid }` - limit the search to the specified modules - * :n:`outside {+ @qualid }` - exclude the specified modules from the search - - .. exn:: Module/section @qualid not found. - - There is no constant in the environment named :n:`@qualid`, where :n:`@qualid` - is in an `inside` or `outside` clause. - - .. example:: :cmd:`Search` examples - - .. coqtop:: in - - Require Import ZArith. - - .. coqtop:: all - - Search Z.mul Z.add "distr". - Search "+"%Z "*"%Z "distr" -Prop. - Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - - -.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } } - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term` - matches a prefix of `C`. For example, a :n:`@one_term` of `f _ b` - matches `f a b`, which is a prefix of `C` when `C` is `f a b c`. - - See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - - .. example:: :cmd:`SearchHead` examples - - .. coqtop:: reset all - - SearchHead le. - SearchHead (@eq bool). - -.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } } - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context - ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern - :n:`@one_term`. - - See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - - .. example:: :cmd:`SearchPattern` examples - - .. coqtop:: in - - Require Import Arith. - - .. coqtop:: all - - SearchPattern (_ + _ = _ + _). - SearchPattern (nat -> bool). - SearchPattern (forall l : list _, _ l l). - - .. coqtop:: all - - SearchPattern (?X1 + _ = _ + ?X1). - -.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } } - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context that have the form - :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term` - matches either `LHS` or `RHS`. - - See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - - .. example:: :cmd:`SearchRewrite` examples - - .. coqtop:: in - - Require Import Arith. - - .. coqtop:: all - - SearchRewrite (_ + _ + _). - -.. table:: Search Blacklist @string - :name: Search Blacklist - - Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, - :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose - fully-qualified name contains any of the strings will be excluded from the - search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and - ``Private_``. - - Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of - blacklisted strings. - - -.. _requests-to-the-environment: - -Requests to the environment -------------------------------- - -.. cmd:: Print Assumptions @smart_qualid - - Displays all the assumptions (axioms, parameters and - variables) a theorem or definition depends on. - - The message "Closed under the global context" indicates that the theorem or - definition has no dependencies. - -.. cmd:: Print Opaque Dependencies @smart_qualid - - Displays the assumptions and opaque constants that :n:`@smart_qualid` depends on. - -.. cmd:: Print Transparent Dependencies @smart_qualid - - Displays the assumptions and transparent constants that :n:`@smart_qualid` depends on. - -.. cmd:: Print All Dependencies @smart_qualid - - Displays all the assumptions and constants :n:`@smart_qualid` depends on. - -.. cmd:: Locate @smart_qualid - - Displays the full name of objects from |Coq|'s various qualified namespaces such as terms, - modules and Ltac. It also displays notation definitions. - - If the argument is: - - * :n:`@qualid` - displays the full name of objects that - end with :n:`@qualid`, thereby showing the module they are defined in. - * :n:`@string {? "%" @ident }` - displays the definition of a notation. :n:`@string` - can be a single token in the notation such as "`->`" or a pattern that matches the - notation. See :ref:`locating-notations`. - - .. todo somewhere we should list all the qualified namespaces - -.. cmd:: Locate Term @smart_qualid - - Like :cmd:`Locate`, but limits the search to terms - -.. cmd:: Locate Module @qualid - - Like :cmd:`Locate`, but limits the search to modules - -.. cmd:: Locate Ltac @qualid - - Like :cmd:`Locate`, but limits the search to tactics - -.. cmd:: Locate Library @qualid - - Displays the full name, status and file system path of the module :n:`@qualid`, whether loaded or not. - -.. cmd:: Locate File @string - - Displays the file system path of the file ending with :n:`@string`. - Typically, :n:`@string` has a suffix such as ``.cmo`` or ``.vo`` or ``.v`` file, such as :n:`Nat.v`. - - .. todo: also works for directory names such as "Data" (parent of Nat.v) - also "Data/Nat.v" works, but not a substring match - -.. example:: Locate examples - - .. coqtop:: all - - Locate nat. - Locate Datatypes.O. - Locate Init.Datatypes.O. - Locate Coq.Init.Datatypes.O. - Locate I.Dont.Exist. - -.. _printing-flags: - -Printing flags -------------------------------- - -.. flag:: Fast Name Printing - - When turned on, |Coq| uses an asymptotically faster algorithm for the - generation of unambiguous names of bound variables while printing terms. - While faster, it is also less clever and results in a typically less elegant - display, e.g. it will generate more names rather than reusing certain names - across subterms. This flag is not enabled by default, because as Ltac - observes bound names, turning it on can break existing proof scripts. - - -.. _loading-files: - -Loading files ------------------ - -|Coq| offers the possibility of loading different parts of a whole -development stored in separate files. Their contents will be loaded as -if they were entered from the keyboard. This means that the loaded -files are text files containing sequences of commands for |Coq|’s -toplevel. This kind of file is called a *script* for |Coq|. The standard -(and default) extension of |Coq|’s script files is .v. - - -.. cmd:: Load {? Verbose } {| @string | @ident } - - Loads a file. If :n:`@ident` is specified, the command loads a file - named :n:`@ident.v`, searching successively in - each of the directories specified in the *loadpath*. (see Section - :ref:`libraries-and-filesystem`) - - If :n:`@string` is specified, it must specify a complete filename. - `~` and .. abbreviations are - allowed as well as shell variables. If no extension is specified, |Coq| - will use the default extension ``.v``. - - Files loaded this way can't leave proofs open, nor can :cmd:`Load` - be used inside a proof. - - We discourage the use of :cmd:`Load`; use :cmd:`Require` instead. - :cmd:`Require` loads `.vo` files that were previously - compiled from `.v` files. - - :n:`Verbose` displays the |Coq| output for each command and tactic - in the loaded file, as if the commands and tactics were entered interactively. - - .. exn:: Can’t find file @ident on loadpath. - :undocumented: - - .. exn:: Load is not supported inside proofs. - :undocumented: - - .. exn:: Files processed by Load cannot leave open proofs. - :undocumented: - -.. _compiled-files: - -Compiled files ------------------- - -This section describes the commands used to load compiled files (see -Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A compiled -file is a particular case of a module called a *library file*. - - -.. cmd:: Require {? {| Import | Export } } {+ @qualid } - :name: Require; Require Import; Require Export - - Loads compiled modules into the |Coq| environment. For each :n:`@qualid`, which has the form - :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented - by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated - filesystem directory. - - The process is applied recursively to all the loaded files; - if they contain :cmd:`Require` commands, those commands are executed as well. - The compiled files must have been compiled with the same version of |Coq|. - The compiled files are neither replayed nor rechecked. - - * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined - in the module available by their short names - * :n:`Export` - additionally does an :cmd:`Export` on the loaded module, making components defined - in the module available by their short names *and* marking them to be exported by the current - module - - If the required module has already been loaded, :n:`Import` and :n:`Export` make the command - equivalent to :cmd:`Import` or :cmd:`Export`. - - The loadpath must contain the same mapping used to compile the file - (see Section :ref:`libraries-and-filesystem`). If - several files match, one of them is picked in an unspecified fashion. - Therefore, library authors should use a unique name for each module and - users are encouraged to use fully-qualified names - or the :cmd:`From ... Require` command to load files. - - - .. todo common user error on dirpaths see https://github.com/coq/coq/pull/11961#discussion_r402852390 - - .. cmd:: From @dirpath Require {? {| Import | Export } } {+ @qualid } - :name: From ... Require - - Works like :cmd:`Require`, but loads, for each :n:`@qualid`, - the library whose fully-qualified name matches :n:`@dirpath.{* @ident . }@qualid` - for some :n:`{* @ident . }`. This is useful to ensure that the :n:`@qualid` library - comes from a particular package. - - .. exn:: Cannot load @qualid: no physical path bound to @dirpath. - :undocumented: - - .. exn:: Cannot find library foo in loadpath. - - The command did not find the - file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a - directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`). - - .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library @qualid. - - The command tried to load library file :n:`@ident`.vo that - depends on some specific version of library :n:`@qualid` which is not the - one already loaded in the current |Coq| session. Probably :n:`@ident.v` was - not properly recompiled with the last version of the file containing - module :token:`qualid`. - - .. exn:: Bad magic number. - - The file :n:`@ident.vo` was found but either it is not a - |Coq| compiled module, or it was compiled with an incompatible - version of |Coq|. - - .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2. - - The library :n:`@qualid__2` is indirectly required by a :cmd:`Require` or - :cmd:`From ... Require` command. The loadpath maps :n:`@qualid__2` to :n:`@ident.vo`, - which was compiled using a loadpath that bound it to :n:`@qualid__1`. Usually - the appropriate solution is to recompile :n:`@ident.v` using the correct loadpath. - See :ref:`libraries-and-filesystem`. - - .. warn:: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. - - Note that the :cmd:`Import` and :cmd:`Export` commands can be used inside modules. - - .. seealso:: Chapter :ref:`thecoqcommands` - -.. cmd:: Print Libraries - - This command displays the list of library files loaded in the - current |Coq| session. - -.. cmd:: Declare ML Module {+ @string } - - This commands dynamically loads OCaml compiled code from - a :n:`.mllib` file. - It is used to load plugins dynamically. The - files must be accessible in the current OCaml loadpath (see the - command :cmd:`Add ML Path`). The :n:`.mllib` suffix may be omitted. - - This command is reserved for plugin developers, who should provide - a .v file containing the command. Users of the plugins will then generally - load the .v file. - - This command supports the :attr:`local` attribute. If present, - the listed files are not exported, even if they're outside a section. - - .. exn:: File not found on loadpath: @string. - :undocumented: - - -.. cmd:: Print ML Modules - - This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. - To know from where these module were loaded, the user - should use the command :cmd:`Locate File`. - - -.. _loadpath: - -Loadpath ------------- - -Loadpaths are preferably managed using |Coq| command line options (see -Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them -for practical purposes. Such commands are only meant to be issued in -the toplevel, and using them in source files is discouraged. - - -.. cmd:: Pwd - - This command displays the current working directory. - - -.. cmd:: Cd {? @string } - - If :n:`@string` is specified, changes the current directory according to :token:`string` which - can be any valid path. Otherwise, it displays the current directory. - - -.. cmd:: Add LoadPath @string as @dirpath - - .. insertprodn dirpath dirpath - - .. prodn:: - dirpath ::= {* @ident . } @ident - - This command is equivalent to the command line option - :n:`-Q @string @dirpath`. It adds a mapping to the loadpath from - the logical name :n:`@dirpath` to the file system directory :n:`@string`. - - * :n:`@dirpath` is a prefix of a module name. The module name hierarchy - follows the file system hierarchy. On Linux, for example, the prefix - `A.B.C` maps to the directory :n:`@string/B/C`. Avoid using spaces after a `.` in the - path because the parser will interpret that as the end of a command or tactic. - -.. cmd:: Add Rec LoadPath @string as @dirpath - - This command is equivalent to the command line option - :n:`-R @string @dirpath`. It adds the physical directory string and all its - subdirectories to the current |Coq| loadpath. - - -.. cmd:: Remove LoadPath @string - - This command removes the path :n:`@string` from the current |Coq| loadpath. - - -.. cmd:: Print LoadPath {? @dirpath } - - This command displays the current |Coq| loadpath. If :n:`@dirpath` is specified, - displays only the paths that extend that prefix. - - -.. cmd:: Add ML Path @string - - This command adds the path :n:`@string` to the current OCaml - loadpath (cf. :cmd:`Declare ML Module`). - - -.. cmd:: Print ML Path - - This command displays the current OCaml loadpath. This - command makes sense only under the bytecode version of ``coqtop``, i.e. - using option ``-byte`` - (cf. :cmd:`Declare ML Module`). - - -.. _backtracking: - -Backtracking ----------------- - -The backtracking commands described in this section can only be used -interactively, they cannot be part of a vernacular file loaded via -``Load`` or compiled by ``coqc``. - - -.. cmd:: Reset @ident - - This command removes all the objects in the environment since :n:`@ident` - was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or - declared object as well as the name of a section. One cannot reset - over the name of a module or of an object inside a module. - - .. exn:: @ident: no such entry. - :undocumented: - -.. cmd:: Reset Initial - - Goes back to the initial state, just after the start - of the interactive session. - - -.. cmd:: Back {? @num } - - Undoes all the effects of the last :n:`@num @sentence`\s. If - :n:`@num` is not specified, the command undoes one sentence. - Sentences read from a `.v` file via a :cmd:`Load` are considered a - single sentence. While :cmd:`Back` can undo tactics and commands executed - within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all - the statements executed within are thereafter considered a single sentence. - :cmd:`Back` immediately following :cmd:`Qed` gets you back to the state - just after the statement of the proof. - - .. exn:: Invalid backtrack. - - The user wants to undo more commands than available in the history. - -.. cmd:: BackTo @num - - This command brings back the system to the state labeled :n:`@num`, - forgetting the effect of all commands executed after this state. The - state label is an integer which grows after each successful command. - It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see - above), the :cmd:`BackTo` command now handles proof states. For that, it may - have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if - necessary. - -.. _quitting-and-debugging: - -Quitting and debugging --------------------------- - -.. cmd:: Quit - - Causes |Coq| to exit. Valid only in coqtop. - - -.. cmd:: Drop - - This command temporarily enters the OCaml toplevel. - It is a debug facility used by |Coq|’s implementers. Valid only in the - bytecode version of coqtop. - The OCaml command: - - :: - - #use "include";; - - adds the right loadpaths and loads some toplevel printers for all - abstract types of |Coq|- section_path, identifiers, terms, judgments, …. - You can also use the file base_include instead, that loads only the - pretty-printers for section_paths and identifiers. You can return back - to |Coq| with the command: - - :: - - go();; - - .. warning:: - - #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, - see Section `interactive-use`). - #. You must have compiled |Coq| from the source package and set the - environment variable COQTOP to the root of your copy of the sources - (see Section `customization-by-environment-variables`). - - -.. cmd:: Time @sentence - - Executes :n:`@sentence` and displays the - time needed to execute it. - - -.. cmd:: Redirect @string @sentence - - Executes :n:`@sentence`, redirecting its - output to the file ":n:`@string`.out". - - -.. cmd:: Timeout @num @sentence - - Executes :n:`@sentence`. If the operation - has not terminated after :n:`@num` seconds, then it is interrupted and an error message is - displayed. - - .. opt:: Default Timeout @num - :name: Default Timeout - - If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`, - except for :cmd:`Timeout` commands themselves. If unset, - no timeout is applied. - - -.. cmd:: Fail @sentence - - For debugging scripts, sometimes it is desirable to know whether a - command or a tactic fails. If :n:`@sentence` fails, then - :n:`Fail @sentence` succeeds (except for - critical errors, such as "stack overflow"), without changing the - proof state. In interactive mode, the system prints a message - confirming the failure. - - .. exn:: The command has not failed! - - If the given :n:`@command` succeeds, then :n:`Fail @sentence` - fails with this error message. - -.. note:: - - :cmd:`Time`, :cmd:`Redirect`, :cmd:`Timeout` and :cmd:`Fail` are - :production:`control_command`\s. For these commands, attributes and goal - selectors, when specified, are part of the :n:`@sentence` argument, and thus come after - the control command prefix and before the inner command or tactic. For - example: `Time #[ local ] Definition foo := 0.` or `Fail Timeout 10 all: auto.` - -.. _controlling-display: - -Controlling display ------------------------ - -.. flag:: Silent - - This flag controls the normal displaying. - -.. opt:: Warnings "{+, {? {| - | + } } @ident }" - :name: Warnings - - This option configures the display of warnings. It is experimental, and - expects, between quotes, a comma-separated list of warning names or - categories. Adding - in front of a warning or category disables it, adding + - makes it an error. It is possible to use the special categories all and - default, the latter containing the warnings enabled by default. The flags are - interpreted from left to right, so in case of an overlap, the flags on the - right have higher priority, meaning that `A,-A` is equivalent to `-A`. - -.. flag:: Search Output Name Only - - This flag restricts the output of search commands to identifier names; - turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, - :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their - output, printing only identifiers. - -.. opt:: Printing Width @num - :name: Printing Width - - This command sets which left-aligned part of the width of the screen is used - for display. At the time of writing this documentation, the default value - is 78. - -.. opt:: Printing Depth @num - :name: Printing Depth - - This option controls the nesting depth of the formatter used for pretty- - printing. Beyond this depth, display of subterms is replaced by dots. At the - time of writing this documentation, the default value is 50. - -.. flag:: Printing Compact Contexts - - This flag controls the compact display mode for goals contexts. When on, - the printer tries to reduce the vertical size of goals contexts by putting - several variables (even if of different types) on the same line provided it - does not exceed the printing width (see :opt:`Printing Width`). At the time - of writing this documentation, it is off by default. - -.. flag:: Printing Unfocused - - This flag controls whether unfocused goals are displayed. Such goals are - created by focusing other goals with bullets (see :ref:`bullets` or - :ref:`curly braces <curly-braces>`). It is off by default. - -.. flag:: Printing Dependent Evars Line - - This flag controls the printing of the “(dependent evars: …)” information - after each tactic. The information is used by the Prooftree tool in Proof - General. (https://askra.de/software/prooftree) - - -.. _vernac-controlling-the-reduction-strategies: - -Controlling the reduction strategies and the conversion algorithm ----------------------------------------------------------------------- - - -|Coq| provides reduction strategies that the tactics can invoke and two -different algorithms to check the convertibility of types. The first -conversion algorithm lazily compares applicative terms while the other -is a brute-force but efficient algorithm that first normalizes the -terms before comparing them. The second algorithm is based on a -bytecode representation of terms similar to the bytecode -representation used in the ZINC virtual machine :cite:`Leroy90`. It is -especially useful for intensive computation of algebraic values, such -as numbers, and for reflection-based tactics. The commands to fine- -tune the reduction strategies and the lazy conversion algorithm are -described first. - -.. cmd:: Opaque {+ @smart_qualid } - - This command accepts the :attr:`global` attribute. By default, the scope - of :cmd:`Opaque` is limited to the current section or module. - - This command has an effect on unfoldable constants, i.e. on constants - defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command - assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc, - or by a proof ended by :cmd:`Defined`. The command tells not to unfold the - constants in the :n:`@smart_qualid` sequence in tactics using δ-conversion (unfolding - a constant is replacing it by its definition). - - :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling - it to delay the unfolding of a constant as much as possible when |Coq| - has to check the conversion (see Section :ref:`conversion-rules`) of two distinct - applied constants. - - .. seealso:: - - Sections :ref:`performingcomputations`, :ref:`tactics-automating`, - :ref:`proof-editing-mode` - -.. cmd:: Transparent {+ @smart_qualid } - - This command accepts the :attr:`global` attribute. By default, the scope - of :cmd:`Transparent` is limited to the current section or module. - - This command is the converse of :cmd:`Opaque` and it applies on unfoldable - constants to restore their unfoldability after an Opaque command. - - Note in particular that constants defined by a proof ended by Qed are - not unfoldable and Transparent has no effect on them. This is to keep - with the usual mathematical practice of *proof irrelevance*: what - matters in a mathematical development is the sequence of lemma - statements, not their actual proofs. This distinguishes lemmas from - the usual defined constants, whose actual values are of course - relevant in general. - - .. exn:: The reference @qualid was not found in the current environment. - - There is no constant named :n:`@qualid` in the environment. - - .. seealso:: - - Sections :ref:`performingcomputations`, - :ref:`tactics-automating`, :ref:`proof-editing-mode` - -.. _vernac-strategy: - -.. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - - .. insertprodn strategy_level strategy_level - - .. prodn:: - strategy_level ::= opaque - | @int - | expand - | transparent - - This command accepts the :attr:`local` attribute, which limits its effect - to the current section or module, in which case the section and module - behavior is the same as :cmd:`Opaque` and :cmd:`Transparent` (without :attr:`global`). - - This command generalizes the behavior of the :cmd:`Opaque` and :cmd:`Transparent` - commands. It is used to fine-tune the strategy for unfolding - constants, both at the tactic level and at the kernel level. This - command associates a :n:`@strategy_level` with the qualified names in the :n:`@smart_qualid` - sequence. Whenever two - expressions with two distinct head constants are compared (for - instance, this comparison can be triggered by a type cast), the one - with lower level is expanded first. In case of a tie, the second one - (appearing in the cast type) is expanded. - - Levels can be one of the following (higher to lower): - - + ``opaque`` : level of opaque constants. They cannot be expanded by - tactics (behaves like +∞, see next item). - + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the - default behavior, which corresponds to transparent constants. This - level can also be referred to as ``transparent``. Negative levels - correspond to constants to be expanded before normal transparent - constants, while positive levels correspond to constants to be - expanded after normal transparent constants. - + ``expand`` : level of constants that should be expanded first (behaves - like −∞) - + ``transparent`` : Equivalent to level 0 - -.. cmd:: Print Strategy @smart_qualid - - This command prints the strategy currently associated with :n:`@smart_qualid`. It - fails if :n:`@smart_qualid` is not an unfoldable reference, that is, neither a - variable nor a constant. - - .. exn:: The reference is not unfoldable. - :undocumented: - -.. cmd:: Print Strategies - - Print all the currently non-transparent strategies. - - -.. cmd:: Declare Reduction @ident := @red_expr - - Declares a short name for the reduction expression :n:`@red_expr`, for - instance ``lazy beta delta [foo bar]``. This short name can then be used - in :n:`Eval @ident in` or ``eval`` constructs. This command - accepts the :attr:`local` attribute, which indicates that the reduction - will be discarded at the end of the - file or module. The name is not qualified. In - particular declaring the same name in several modules or in several - functor applications will be rejected if these declarations are not - local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but - nothing prevents the user from also performing a - :n:`Ltac @ident := @red_expr`. - - .. seealso:: :ref:`performingcomputations` - - -.. _controlling-locality-of-commands: - -Controlling the locality of commands ------------------------------------------ - -.. attr:: global - local - - Some commands support a :attr:`local` or :attr:`global` attribute - to control the scope of their effect. There is also a legacy (and - much more commonly used) syntax using the ``Local`` or ``Global`` - prefixes (see :n:`@legacy_attr`). There are four kinds of - commands: - - + Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. For these - commands, the :attr:`local` attribute limits the effect of the command to the - current section or module it occurs in. As an example, the :cmd:`Coercion` - and :cmd:`Strategy` commands belong to this category. - + Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the :attr:`local` attribute limits the - effect of the command to the current module if the command does not occur in a - section and the :attr:`global` attribute extends the effect outside the current - sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong - to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the :attr:`global` attribute is not - applicable to them. - + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the :attr:`global` - attribute extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands - belong to this category. - + Commands whose default behavior is to extend their effect outside - sections but not outside modules when they occur in a section and to - extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the :attr:`local` attribute - limits the effect to the current section or module while the :attr:`global` - attribute extends the effect outside the module even when the command - occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this - category. - -.. attr:: export - - Some commands support an :attr:`export` attribute. The effect of - the attribute is to make the effect of the command available when - the module containing it is imported. It is supported in - particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` - commands. - -.. _controlling-typing-flags: - -Controlling Typing Flags ----------------------------- - -.. flag:: Guard Checking - - This flag can be used to enable/disable the guard checking of - fixpoints. Warning: this can break the consistency of the system, use at your - own risk. Decreasing argument can still be specified: the decrease is not checked - anymore but it still affects the reduction of the term. Unchecked fixpoints are - printed by :cmd:`Print Assumptions`. - -.. flag:: Positivity Checking - - This flag can be used to enable/disable the positivity checking of inductive - types and the productivity checking of coinductive types. Warning: this can - break the consistency of the system, use at your own risk. Unchecked - (co)inductive types are printed by :cmd:`Print Assumptions`. - -.. flag:: Universe Checking - - This flag can be used to enable/disable the checking of universes, providing a - form of "type in type". Warning: this breaks the consistency of the system, use - at your own risk. Constants relying on "type in type" are printed by - :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line - argument (see :ref:`command-line-options`). - -.. cmd:: Print Typing Flags - - Print the status of the three typing flags: guard checking, positivity checking - and universe checking. - -See also :flag:`Cumulative StrictProp` in the |SProp| chapter. - -.. example:: - - .. coqtop:: all reset - - Unset Guard Checking. - - Print Typing Flags. - - Fixpoint f (n : nat) : False - := f n. - - Fixpoint ackermann (m n : nat) {struct m} : nat := - match m with - | 0 => S n - | S m => - match n with - | 0 => ackermann m 1 - | S n => ackermann m (ackermann (S m) n) - end - end. - - Print Assumptions ackermann. - - Note that the proper way to define the Ackermann function is to use - an inner fixpoint: - - .. coqtop:: all reset - - Fixpoint ack m := - fix ackm n := - match m with - | 0 => S n - | S m' => - match n with - | 0 => ack m' 1 - | S n' => ack m' (ackm n') - end - end. - - -.. _internal-registration-commands: - -Internal registration commands --------------------------------- - -Due to their internal nature, the commands that are presented in this section -are not for general use. They are meant to appear only in standard libraries and -in support libraries of plug-ins. - -.. _exposing-constants-to-ocaml-libraries: - -Exposing constants to OCaml libraries -````````````````````````````````````` - -.. cmd:: Register @qualid__1 as @qualid__2 - - Makes the constant :n:`@qualid__1` accessible to OCaml libraries under - the name :n:`@qualid__2`. The constant can then be dynamically located - in OCaml code by - calling :n:`Coqlib.lib_ref "@qualid__2"`. The OCaml code doesn't need - to know where the constant is defined (what file, module, library, etc.). - - As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, - the constant is exposed to the kernel. For instance, the `Int63` module - features the following declaration: - - .. coqdoc:: - - Register bool as kernel.ind_bool. - - This makes the kernel aware of the `bool` type, which is used, for example, - to define the return type of the :g:`#int63_eq` primitive. - - .. seealso:: :ref:`primitive-integers` - -Inlining hints for the fast reduction machines -`````````````````````````````````````````````` - -.. cmd:: Register Inline @qualid - - Gives a hint to the reduction machines (VM and native) that - the body of the constant :n:`@qualid` should be inlined in the generated code. - -Registering primitive operations -```````````````````````````````` - -.. cmd:: Primitive @ident {? : @term } := #@ident__prim - - Makes the primitive type or primitive operator :n:`#@ident__prim` defined in OCaml - accessible in |Coq| commands and tactics. - For internal use by implementors of |Coq|'s standard library or standard library - replacements. No space is allowed after the `#`. Invalid values give a syntax - error. - - For example, the standard library files `Int63.v` and `PrimFloat.v` use :cmd:`Primitive` - to support, respectively, the features described in :ref:`primitive-integers` and - :ref:`primitive-floats`. - - The types associated with an operator must be declared to the kernel before declaring operations - that use the type. Do this with :cmd:`Primitive` for primitive types and - :cmd:`Register` with the :g:`kernel` prefix for other types. For example, - in `Int63.v`, `#int63_type` must be declared before the associated operations. - - .. exn:: The type @ident must be registered before this construction can be typechecked. - :undocumented: - - The type must be defined with :cmd:`Primitive` command before this - :cmd:`Primitive` command (declaring an operation using the type) will succeed. |