diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/index.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 312 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sections.rst | 104 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 1106 |
4 files changed, 1524 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst index 07dcfff444..5ee960d99b 100644 --- a/doc/sphinx/language/core/index.rst +++ b/doc/sphinx/language/core/index.rst @@ -32,6 +32,8 @@ will have to check their output. ../gallina-specification-language ../cic + records ../../addendum/universe-polymorphism ../../addendum/sprop + sections ../module-system diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst new file mode 100644 index 0000000000..d380d83d6c --- /dev/null +++ b/doc/sphinx/language/core/records.rst @@ -0,0 +1,312 @@ +.. _record-types: + +Record types +---------------- + +The :cmd:`Record` construction is a macro allowing the definition of +records as is done in many programming languages. Its syntax is +described in the grammar below. In fact, the :cmd:`Record` macro is more general +than the usual record types, since it allows also for “manifest” +expressions. In this sense, the :cmd:`Record` construction allows defining +“signatures”. + +.. _record_grammar: + +.. cmd:: {| Record | Structure } @record_definition {* with @record_definition } + :name: Record; Structure + + .. insertprodn record_definition field_body + + .. prodn:: + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations } + field_body ::= {* @binder } @of_type + | {* @binder } @of_type := @term + | {* @binder } := @term + + Each :n:`@record_definition` defines a record named by :n:`@ident_decl`. + The constructor name is given by :n:`@ident`. + If the constructor name is not specified, then the default name :n:`Build_@ident` is used, + where :n:`@ident` is the record name. + + If :n:`@type` is + omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names. + The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`. + Notice that the type of an identifier can depend on a previously-given identifier. Thus the + order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole + or to individual fields. + + Notations can be attached to fields using the :n:`@decl_notations` annotation. + + :cmd:`Record` and :cmd:`Structure` are synonyms. + + 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. + +More generally, a record may have explicitly defined (a.k.a. manifest) +fields. For instance, we might have: +:n:`Record @ident {* @binder } : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. +in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`. + +.. example:: + + The set of rational numbers may be defined as: + + .. coqtop:: reset all + + Record Rat : Set := mkRat + { sign : bool + ; top : nat + ; bottom : nat + ; Rat_bottom_cond : 0 <> bottom + ; Rat_irred_cond : + forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 + }. + + Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` + and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``. + +Let us now see the work done by the ``Record`` macro. First the macro +generates a variant type definition with just one constructor: +:n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`. + +To build an object of type :token:`ident`, one should provide the constructor +:n:`@ident__0` with the appropriate number of terms filling the fields of the record. + +.. example:: + + Let us define the rational :math:`1/2`: + + .. coqtop:: in + + Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. + Admitted. + + Definition half := mkRat true 1 2 (O_S 1) one_two_irred. + Check half. + +Alternatively, the following syntax allows creating objects by using named fields, as +shown in this grammar. The fields do not have to be in any particular order, nor do they have +to be all present if the missing ones can be inferred or prompted for +(see :ref:`programs`). + +.. coqtop:: all + + Definition half' := + {| sign := true; + Rat_bottom_cond := O_S 1; + Rat_irred_cond := one_two_irred |}. + +The following settings let you control the display format for types: + +.. flag:: Printing Records + + If set, use the record syntax (shown above) as the default display format. + +You can override the display format for specified types by adding entries to these tables: + +.. table:: Printing Record @qualid + :name: Printing Record + + Specifies a set of qualids which are displayed as records. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. + +.. table:: Printing Constructor @qualid + :name: Printing Constructor + + Specifies a set of qualids which are displayed as constructors. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. + +This syntax can also be used for pattern matching. + +.. coqtop:: all + + Eval compute in ( + match half with + | {| sign := true; top := n |} => n + | _ => 0 + end). + +The macro generates also, when it is possible, the projection +functions for destructuring an object of type :token:`ident`. These +projection functions are given the names of the corresponding +fields. If a field is named `_` then no projection is built +for it. In our example: + +.. coqtop:: all + + Eval compute in top half. + Eval compute in bottom half. + Eval compute in Rat_bottom_cond half. + +An alternative syntax for projections based on a dot notation is +available: + +.. coqtop:: all + + Eval compute in half.(top). + +.. flag:: Printing Projections + + This flag activates the dot notation for printing. + + .. example:: + + .. coqtop:: all + + Set Printing Projections. + Check top half. + +.. FIXME: move this to the main grammar in the spec chapter + +.. _record_projections_grammar: + + .. insertprodn term_projection term_projection + + .. prodn:: + term_projection ::= @term0 .( @qualid {* @arg } ) + | @term0 .( @ @qualid {* @term1 } ) + + Syntax of Record projections + +The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` +denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`, +the syntax :n:`@term0.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term0`. +and the syntax :n:`@term0.(@@qualid {+ @term0 })` to :n:`@@qualid {+ @term0 } @term0`. +In each case, :token:`term0` is the object projected and the +other arguments are the parameters of the inductive type. + + +.. note:: Records defined with the ``Record`` keyword are not allowed to be + recursive (references to the record's name in the type of its field + raises an error). To define recursive records, one can use the ``Inductive`` + and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. + Definition of mutually inductive or co-inductive records are also allowed, as long + as all of the types in the block are records. + +.. note:: Induction schemes are automatically generated for inductive records. + Automatic generation of induction schemes for non-recursive records + defined with the ``Record`` keyword can be activated with the + :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`). + +.. warn:: @ident cannot be defined. + + It can happen that the definition of a projection is impossible. + This message is followed by an explanation of this impossibility. + There may be three reasons: + + #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The body of :token:`ident` uses an incorrect elimination for + :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). + #. The type of the projections :token:`ident` depends on previous + projections which themselves could not be defined. + +.. exn:: Records declared with the keyword Record or Structure cannot be recursive. + + The record name :token:`ident` appears in the type of its fields, but uses + the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. + +.. exn:: Cannot handle mutually (co)inductive records. + + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. + +During the definition of the one-constructor inductive definition, all +the errors of inductive definitions, as described in Section +:ref:`gallina-inductive-definitions`, may also occur. + +.. seealso:: Coercions and records in section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. + +.. _primitive_projections: + +Primitive Projections +~~~~~~~~~~~~~~~~~~~~~ + +.. flag:: Primitive Projections + + Turns on the use of primitive + projections when defining subsequent records (even through the ``Inductive`` + and ``CoInductive`` commands). Primitive projections + extended the Calculus of Inductive Constructions with a new binary + term constructor `r.(p)` representing a primitive projection `p` applied + to a record object `r` (i.e., primitive projections are always applied). + Even if the record type has parameters, these do not appear + in the internal representation of + applications of the projection, considerably reducing the sizes of + terms when manipulating parameterized records and type checking time. + On the user level, primitive projections can be used as a replacement + for the usual defined ones, although there are a few notable differences. + +.. flag:: Printing Primitive Projection Parameters + + This compatibility flag reconstructs internally omitted parameters at + printing time (even though they are absent in the actual AST manipulated + by the kernel). + +Primitive Record Types +++++++++++++++++++++++ + +When the :flag:`Primitive Projections` flag is on, definitions of +record types change meaning. When a type is declared with primitive +projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). +To eliminate the (co-)inductive type, one must use its defined primitive projections. + +.. The following paragraph is quite redundant with what is above + +For compatibility, the parameters still appear to the user when +printing terms even though they are absent in the actual AST +manipulated by the kernel. This can be changed by unsetting the +:flag:`Printing Primitive Projection Parameters` flag. + +There are currently two ways to introduce primitive records types: + +#. Through the ``Record`` command, in which case the type has to be + non-recursive. The defined type enjoys eta-conversion definitionally, + that is the generalized form of surjective pairing for records: + `r` ``= Build_``\ `R` ``(``\ `r`\ ``.(``\ |p_1|\ ``) …`` `r`\ ``.(``\ |p_n|\ ``))``. + Eta-conversion allows to define dependent elimination for these types as well. +#. Through the ``Inductive`` and ``CoInductive`` commands, when + the body of the definition is a record declaration of the form + ``Build_``\ `R` ``{`` |p_1| ``:`` |t_1|\ ``; … ;`` |p_n| ``:`` |t_n| ``}``. + In this case the types can be recursive and eta-conversion is disallowed. These kind of record types + differ from their traditional versions in the sense that dependent + elimination is not available for them and only non-dependent case analysis + can be defined. + +Reduction ++++++++++ + +The basic reduction rule of a primitive projection is +|p_i| ``(Build_``\ `R` |t_1| … |t_n|\ ``)`` :math:`{\rightarrow_{\iota}}` |t_i|. +However, to take the :math:`{\delta}` flag into +account, projections can be in two states: folded or unfolded. An +unfolded primitive projection application obeys the rule above, while +the folded version delta-reduces to the unfolded version. This allows to +precisely mimic the usual unfolding rules of constants. Projections +obey the usual ``simpl`` flags of the ``Arguments`` command in particular. +There is currently no way to input unfolded primitive projections at the +user-level, and there is no way to display unfolded projections differently +from folded ones. + + +Compatibility Projections and :g:`match` +++++++++++++++++++++++++++++++++++++++++ + +To ease compatibility with ordinary record types, each primitive +projection is also defined as a ordinary constant taking parameters and +an object of the record type as arguments, and whose body is an +application of the unfolded primitive projection of the same name. These +constants are used when elaborating partial applications of the +projection. One can distinguish them from applications of the primitive +projection if the :flag:`Printing Primitive Projection Parameters` flag +is off: For a primitive projection application, parameters are printed +as underscores while for the compatibility projections they are printed +as usual. + +Additionally, user-written :g:`match` constructs on primitive records +are desugared into substitution of the projections, they cannot be +printed back as :g:`match` constructs. diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst new file mode 100644 index 0000000000..9ad8df2b1b --- /dev/null +++ b/doc/sphinx/language/core/sections.rst @@ -0,0 +1,104 @@ +.. _section-mechanism: + +Section mechanism +----------------- + +Sections create local contexts which can be shared across multiple definitions. + +.. example:: + + Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. + + .. coqtop:: all + + Section s1. + + Inside a section, local parameters can be introduced using :cmd:`Variable`, + :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for + the first two). + + .. coqtop:: all + + Variables x y : nat. + + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. + + .. coqtop:: in + + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. + + .. coqtop:: all + + Print x'. + Print x''. + + End s1. + + Print x'. + Print x''. + + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. + +.. cmd:: Section @ident + + This command is used to open a section named :token:`ident`. + Section names do not need to be unique. + + +.. cmd:: End @ident + + This command closes the section or module named :token:`ident`. + See :ref:`Terminating an interactive module or module type definition<terminating_module>` + for a description of its use with modules. + + After closing the + section, the local declarations (variables and local definitions, see :cmd:`Variable`) are + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. + + .. exn:: There is nothing to end. + :undocumented: + + .. exn:: Last block to end has name @ident. + :undocumented: + +.. note:: + Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which + appear inside a section are canceled when the section is closed. + +.. cmd:: Let @ident @def_body + Let Fixpoint @fix_definition {* with @fix_definition } + Let CoFixpoint @cofix_definition {* with @cofix_definition } + :name: Let; Let Fixpoint; Let CoFixpoint + + These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that + the declared constant is local to the current section. + When the section is closed, all persistent + definitions and theorems within it that depend on the constant + will be wrapped with a :n:`@term_let` with the same declaration. + + As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, + 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`. + +.. cmd:: Context {+ @binder } + + Declare variables in the context of the current section, like :cmd:`Variable`, + but also allowing implicit variables, :ref:`implicit-generalization`, and + let-binders. + + .. coqdoc:: + + Context {A : Type} (a b : A). + Context `{EqDec A}. + Context (b' := b). + +.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst new file mode 100644 index 0000000000..a859aa46eb --- /dev/null +++ b/doc/sphinx/language/gallina-extensions.rst @@ -0,0 +1,1106 @@ +.. _extensionsofgallina: + +Extensions of |Gallina| +======================= + +|Gallina| is the kernel language of |Coq|. We describe here extensions of +|Gallina|’s syntax. + +Variants and extensions of :g:`match` +------------------------------------- + +.. _mult-match: + +Multiple and nested pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The basic version of :g:`match` allows pattern matching on simple +patterns. As an extension, multiple nested patterns or disjunction of +patterns are allowed, as in ML-like languages. + +The extension just acts as a macro that is expanded during parsing +into a sequence of match on simple patterns. Especially, a +construction defined using the extended match is generally printed +under its expanded form (see :flag:`Printing Matching`). + +.. seealso:: :ref:`extendedpatternmatching`. + +.. _if-then-else: + +Pattern-matching on boolean values: the if expression +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +For inductive types with exactly two constructors and for pattern matching +expressions that do not depend on the arguments of the constructors, it is possible +to use a ``if … then … else`` notation. For instance, the definition + +.. coqtop:: all + + Definition not (b:bool) := + match b with + | true => false + | false => true + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition not (b:bool) := if b then false else true. + +More generally, for an inductive type with constructors :n:`@ident__1` +and :n:`@ident__2`, the following terms are equal: + +:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2` + +:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end` + +.. example:: + + .. coqtop:: all + + Check (fun x (H:{x=0}+{x<>0}) => + match H with + | left _ => true + | right _ => false + end). + +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is +declared as such (see :ref:`controlling-match-pp`). + +.. _irrefutable-patterns: + +Irrefutable patterns: the destructuring let variants +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern-matching on terms inhabiting inductive type having only one +constructor can be alternatively written using :g:`let … in …` +constructions. There are two variants of them. + + +First destructuring let syntax +++++++++++++++++++++++++++++++ + +The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` +performs case analysis on :n:`@term__0` whose type must be an +inductive type with exactly one constructor. The number of variables +:n:`@ident__i` must correspond to the number of arguments of this +contrustor. Then, in :n:`@term__1`, these variables are bound to the +arguments of the constructor in :n:`@term__0`. For instance, the +definition + +.. coqtop:: reset all + + Definition fst (A B:Set) (H:A * B) := match H with + | pair x y => x + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. + +Notice that reduction is different from regular :g:`let … in …` +construction since it happens only if :n:`@term__0` is in constructor form. +Otherwise, the reduction is blocked. + +The pretty-printing of a definition by matching on a irrefutable +pattern can either be done using :g:`match` or the :g:`let` construction +(see Section :ref:`controlling-match-pp`). + +If term inhabits an inductive type with one constructor `C`, we have an +equivalence between + +:: + + let (ident₁, …, identₙ) [dep_ret_type] := term in term' + +and + +:: + + match term [dep_ret_type] with + C ident₁ … identₙ => term' + end + + +Second destructuring let syntax ++++++++++++++++++++++++++++++++ + +Another destructuring let syntax is available for inductive types with +one constructor by giving an arbitrary pattern instead of just a tuple +for all the arguments. For example, the preceding example can be +written: + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. + +This is useful to match deeper inside tuples and also to use notations +for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary +patterns to do the deconstruction. For example: + +.. coqtop:: all + + Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := + let '((a,b), (c, d)) := x in (a,b,c,d). + + Notation " x 'With' p " := (exist _ x p) (at level 20). + + Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := + let 'x With p := t in x. + +When printing definitions which are written using this construct it +takes precedence over let printing directives for the datatype under +consideration (see Section :ref:`controlling-match-pp`). + + +.. _controlling-match-pp: + +Controlling pretty-printing of match expressions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following commands give some control over the pretty-printing +of :g:`match` expressions. + +Printing nested patterns ++++++++++++++++++++++++++ + +.. flag:: Printing Matching + + The Calculus of Inductive Constructions knows pattern matching only + over simple patterns. It is however convenient to re-factorize nested + pattern matching into a single pattern matching over a nested + pattern. + + When this flag is on (default), |Coq|’s printer tries to do such + limited re-factorization. + Turning it off tells |Coq| to print only simple pattern matching problems + in the same way as the |Coq| kernel handles them. + + +Factorization of clauses with same right-hand side +++++++++++++++++++++++++++++++++++++++++++++++++++ + +.. flag:: Printing Factorizable Match Patterns + + When several patterns share the same right-hand side, it is additionally + possible to share the clauses using disjunctive patterns. Assuming that the + printing matching mode is on, this flag (on by default) tells |Coq|'s + printer to try to do this kind of factorization. + +Use of a default clause ++++++++++++++++++++++++ + +.. flag:: Printing Allow Match Default Clause + + When several patterns share the same right-hand side which do not depend on the + arguments of the patterns, yet an extra factorization is possible: the + disjunction of patterns can be replaced with a `_` default clause. Assuming that + the printing matching mode and the factorization mode are on, this flag (on by + default) tells |Coq|'s printer to use a default clause when relevant. + +Printing of wildcard patterns +++++++++++++++++++++++++++++++ + +.. flag:: Printing Wildcard + + Some variables in a pattern may not occur in the right-hand side of + the pattern matching clause. When this flag is on (default), the + variables having no occurrences in the right-hand side of the + pattern matching clause are just printed using the wildcard symbol + “_”. + + +Printing of the elimination predicate ++++++++++++++++++++++++++++++++++++++ + +.. flag:: Printing Synth + + In most of the cases, the type of the result of a matched term is + mechanically synthesizable. Especially, if the result type does not + depend of the matched term. When this flag is on (default), + the result type is not printed when |Coq| knows that it can re- + synthesize it. + + +Printing matching on irrefutable patterns +++++++++++++++++++++++++++++++++++++++++++ + +If an inductive type has just one constructor, pattern matching can be +written using the first destructuring let syntax. + +.. table:: Printing Let @qualid + :name: Printing Let + + Specifies a set of qualids for which pattern matching is displayed using a let expression. + Note that this only applies to pattern matching instances entered with :g:`match`. + It doesn't affect pattern matching explicitly entered with a destructuring + :g:`let`. + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. + + +Printing matching on booleans ++++++++++++++++++++++++++++++ + +If an inductive type is isomorphic to the boolean type, pattern matching +can be written using ``if`` … ``then`` … ``else`` …. This table controls +which types are written this way: + +.. table:: Printing If @qualid + :name: Printing If + + Specifies a set of qualids for which pattern matching is displayed using + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` + commands to update this set. + +This example emphasizes what the printing settings offer. + +.. example:: + + .. coqtop:: all + + Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. + + Test Printing Let for prod. + + Print snd. + + Remove Printing Let prod. + + Unset Printing Synth. + + Unset Printing Wildcard. + + Print snd. + +Module system +------------- + +The module system provides a way of packaging related elements +together, as well as a means of massive abstraction. + + +.. cmd:: Module {? {| Import | Export } } @ident {* @module_binder } {? @of_module_type } {? := {+<+ @module_expr_inl } } + + .. insertprodn module_binder module_expr_inl + + .. prodn:: + module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl ) + module_type_inl ::= ! @module_type + | @module_type {? @functor_app_annot } + functor_app_annot ::= [ inline at level @num ] + | [ no inline ] + module_type ::= @qualid + | ( @module_type ) + | @module_type @module_expr_atom + | @module_type with @with_declaration + with_declaration ::= Definition @qualid {? @univ_decl } := @term + | Module @qualid := @qualid + module_expr_atom ::= @qualid + | ( {+ @module_expr_atom } ) + of_module_type ::= : @module_type_inl + | {* <: @module_type_inl } + module_expr_inl ::= ! {+ @module_expr_atom } + | {+ @module_expr_atom } {? @functor_app_annot } + + Defines a module named :token:`ident`. See the examples :ref:`here<module_examples>`. + + The :n:`Import` and :n:`Export` flags specify whether the module should be automatically + imported or exported. + + Specifying :n:`{* @module_binder }` starts a functor with + parameters given by the :n:`@module_binder`\s. (A *functor* is a function + from modules to modules.) + + .. todo: would like to find a better term than "interactive", not very descriptive + + :n:`@of_module_type` specifies the module type. :n:`{+ <: @module_type_inl }` + starts a module that satisfies each :n:`@module_type_inl`. + + :n:`:= {+<+ @module_expr_inl }` specifies the body of a module or functor + definition. If it's not specified, then the module is defined *interactively*, + meaning that the module is defined as a series of commands terminated with :cmd:`End` + instead of in a single :cmd:`Module` command. + Interactively defining the :n:`@module_expr_inl`\s in a series of + :cmd:`Include` commands is equivalent to giving them all in a single + non-interactive :cmd:`Module` command. + + The ! prefix indicates that any assumption command (such as :cmd:`Axiom`) with an :n:`Inline` clause + in the type of the functor arguments will be ignored. + + .. todo: What is an Inline directive? sb command but still unclear. Maybe referring to the + "inline" in functor_app_annot? or assumption_token Inline assum_list? + +.. cmd:: Module Type @ident {* @module_binder } {* <: @module_type_inl } {? := {+<+ @module_type_inl } } + + Defines a module type named :n:`@ident`. See the example :ref:`here<example_def_simple_module_type>`. + + Specifying :n:`{* @module_binder }` starts a functor type with + parameters given by the :n:`@module_binder`\s. + + :n:`:= {+<+ @module_type_inl }` specifies the body of a module or functor type + definition. If it's not specified, then the module type is defined *interactively*, + meaning that the module type is defined as a series of commands terminated with :cmd:`End` + instead of in a single :cmd:`Module Type` command. + Interactively defining the :n:`@module_type_inl`\s in a series of + :cmd:`Include` commands is equivalent to giving them all in a single + non-interactive :cmd:`Module Type` command. + +.. _terminating_module: + +**Terminating an interactive module or module type definition** + +Interactive modules are terminated with the :cmd:`End` command, which +is also used to terminate :ref:`Sections<section-mechanism>`. +:n:`End @ident` closes the interactive module or module type :token:`ident`. +If the module type was given, the command verifies that the content of the module +matches the module type. If the module is not a +functor, its components (constants, inductive types, submodules etc.) +are now available through the dot notation. + +.. exn:: No such label @ident. + :undocumented: + +.. exn:: Signature components for label @ident do not match. + :undocumented: + +.. exn:: The field @ident is missing in @qualid. + :undocumented: + +.. |br| raw:: html + + <br> + +.. note:: + + #. Interactive modules and module types can be nested. + #. Interactive modules and module types can't be defined inside of :ref:`sections<section-mechanism>`. + Sections can be defined inside of interactive modules and module types. + #. Hints and notations (:cmd:`Hint` and :cmd:`Notation` commands) can also appear inside interactive + modules and module types. Note that with module definitions like: + + :n:`Module @ident__1 : @module_type := @ident__2.` + + or + + :n:`Module @ident__1 : @module_type.` |br| + :n:`Include @ident__2.` |br| + :n:`End @ident__1.` + + hints and the like valid for :n:`@ident__1` are the ones defined in :n:`@module_type` + rather then those defined in :n:`@ident__2` (or the module body). + #. Within an interactive module type definition, the :cmd:`Parameter` command declares a + constant instead of definining a new axiom (which it does when not in a module type definition). + #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically + expanded when the functor is applied, except when the function application is prefixed by ``!``. + +.. cmd:: Include @module_type_inl {* <+ @module_expr_inl } + + Includes the content of module(s) in the current + interactive module. Here :n:`@module_type_inl` can be a module expression or a module + type expression. If it is a high-order module or module type + expression then the system tries to instantiate :n:`@module_type_inl` with the current + interactive module. + + Including multiple modules is a single :cmd:`Include` is equivalent to including each module + in a separate :cmd:`Include` command. + +.. cmd:: Include Type {+<+ @module_type_inl } + + .. deprecated:: 8.3 + + Use :cmd:`Include` instead. + +.. cmd:: Declare Module {? {| Import | Export } } @ident {* @module_binder } : @module_type_inl + + Declares a module :token:`ident` of type :token:`module_type_inl`. + + If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of + :token:`module_binder`\s. + +.. cmd:: Import {+ @qualid } + + If :token:`qualid` denotes a valid basic module (i.e. its module type is a + signature), makes its components available by their short names. + + .. example:: + + .. coqtop:: reset in + + Module Mod. + Definition T:=nat. + Check T. + End Mod. + Check Mod.T. + + .. coqtop:: all + + Fail Check T. + Import Mod. + Check T. + + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). + + Declarations made with the :attr:`local` attribute are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. + + .. example:: + + .. coqtop:: in + + Module A. + Module B. + Local Definition T := nat. + End B. + End A. + Import A. + + .. coqtop:: all fail + + Check B.T. + +.. cmd:: Export {+ @qualid } + :name: Export + + Similar to :cmd:`Import`, except that when the module containing this command + is imported, the :n:`{+ @qualid }` are imported as well. + + .. exn:: @qualid is not a module. + :undocumented: + + .. warn:: Trying to mask the absolute name @qualid! + :undocumented: + +.. cmd:: Print Module @qualid + + Prints the module type and (optionally) the body of the module :n:`@qualid`. + +.. cmd:: Print Module Type @qualid + + Prints the module type corresponding to :n:`@qualid`. + +.. flag:: Short Module Printing + + This flag (off by default) disables the printing of the types of fields, + leaving only their names, for the commands :cmd:`Print Module` and + :cmd:`Print Module Type`. + +.. _module_examples: + +Examples +~~~~~~~~ + +.. example:: Defining a simple module interactively + + .. coqtop:: in + + Module M. + Definition T := nat. + Definition x := 0. + + .. coqtop:: all + + Definition y : bool. + exact true. + + .. coqtop:: in + + Defined. + End M. + +Inside a module one can define constants, prove theorems and do anything +else that can be done in the toplevel. Components of a closed +module can be accessed using the dot notation: + +.. coqtop:: all + + Print M.x. + +.. _example_def_simple_module_type: + +.. example:: Defining a simple module type interactively + + .. coqtop:: in + + Module Type SIG. + Parameter T : Set. + Parameter x : T. + End SIG. + +.. _example_filter_module: + +.. example:: Creating a new module that omits some items from an existing module + + Since :n:`SIG`, the type of the new module :n:`N`, doesn't define :n:`y` or + give the body of :n:`x`, which are not included in :n:`N`. + + .. coqtop:: all + + Module N : SIG with Definition T := nat := M. + Print N.T. + Print N.x. + Fail Print N.y. + + .. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG + .. coqtop:: none reset + + Module M. + Definition T := nat. + Definition x := 0. + Definition y : bool. + exact true. + Defined. + End M. + + Module Type SIG. + Parameter T : Set. + Parameter x : T. + End SIG. + +The following definition of :g:`N` using the module type expression :g:`SIG` with +:g:`Definition T := nat` is equivalent to the following one: + +.. todo: what is other definition referred to above? + "Module N' : SIG with Definition T := nat. End N`." is not it. + +.. coqtop:: in + + Module Type SIG'. + Definition T : Set := nat. + Parameter x : T. + End SIG'. + + Module N : SIG' := M. + +If we just want to be sure that our implementation satisfies a +given module type without restricting the interface, we can use a +transparent constraint + +.. coqtop:: in + + Module P <: SIG := M. + +.. coqtop:: all + + Print P.y. + +.. example:: Creating a functor (a module with parameters) + + .. coqtop:: in + + Module Two (X Y: SIG). + Definition T := (X.T * Y.T)%type. + Definition x := (X.x, Y.x). + End Two. + + and apply it to our modules and do some computations: + + .. coqtop:: in + + + Module Q := Two M N. + + .. coqtop:: all + + Eval compute in (fst Q.x + snd Q.x). + +.. example:: A module type with two sub-modules, sharing some fields + + .. coqtop:: in + + Module Type SIG2. + Declare Module M1 : SIG. + Module M2 <: SIG. + Definition T := M1.T. + Parameter x : T. + End M2. + End SIG2. + + .. coqtop:: in + + Module Mod <: SIG2. + Module M1. + Definition T := nat. + Definition x := 1. + End M1. + Module M2 := M. + End Mod. + +Notice that ``M`` is a correct body for the component ``M2`` since its ``T`` +component is ``nat`` as specified for ``M1.T``. + +Libraries and qualified names +--------------------------------- + +.. _names-of-libraries: + +Names of libraries +~~~~~~~~~~~~~~~~~~ + +The theories developed in |Coq| are stored in *library files* which are +hierarchically classified into *libraries* and *sublibraries*. To +express this hierarchy, library names are represented by qualified +identifiers qualid, i.e. as list of identifiers separated by dots (see +:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard +|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts +the name of a library is called a *library root*. All library files of +the standard library of |Coq| have the reserved root |Coq| but library +filenames based on other roots can be obtained by using |Coq| commands +(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`). +Also, when an interactive |Coq| session starts, a library of root ``Top`` is +started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`). + +.. _qualified-names: + +Qualified names +~~~~~~~~~~~~~~~ + +Library files are modules which possibly contain submodules which +eventually contain constructions (axioms, parameters, definitions, +lemmas, theorems, remarks or facts). The *absolute name*, or *full +name*, of a construction in some library file is a qualified +identifier starting with the logical name of the library file, +followed by the sequence of submodules names encapsulating the +construction and ended by the proper name of the construction. +Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’ +equality defined in the module Logic in the sublibrary ``Init`` of the +standard library of |Coq|. + +The proper name that ends the name of a construction is the short name +(or sometimes base name) of the construction (for instance, the short +name of ``Coq.Init.Logic.eq`` is ``eq``). Any partial suffix of the absolute +name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially +qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a +construction is its shortest partially qualified name. + +|Coq| does not accept two constructions (definition, theorem, …) with +the same absolute name but different constructions can have the same +short name (or even same partially qualified names as soon as the full +names are different). + +Notice that the notion of absolute, partially qualified and short +names also applies to library filenames. + +**Visibility** + +|Coq| maintains a table called the name table which maps partially qualified +names of constructions to absolute names. This table is updated by the +commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` and +also each time a new declaration is added to the context. An absolute +name is called visible from a given short or partially qualified name +when this latter name is enough to denote it. This means that the +short or partially qualified name is mapped to the absolute name in +|Coq| name table. Definitions with the :attr:`local` attribute are only accessible with +their fully qualified name (see :ref:`gallina-definitions`). + +It may happen that a visible name is hidden by the short name or a +qualified name of another construction. In this case, the name that +has been hidden must be referred to using one more level of +qualification. To ensure that a construction always remains +accessible, absolute names can never be hidden. + +.. example:: + + .. coqtop:: all + + Check 0. + + Definition nat := bool. + + Check 0. + + Check Datatypes.nat. + + Locate nat. + +.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`. + +.. _libraries-and-filesystem: + +Libraries and filesystem +~~~~~~~~~~~~~~~~~~~~~~~~ + +.. note:: The questions described here have been subject to redesign in |Coq| 8.5. + Former versions of |Coq| use the same terminology to describe slightly different things. + +Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer +to them inside |Coq|, a translation from file-system names to |Coq| names +is needed. In this translation, names in the file system are called +*physical* paths while |Coq| names are contrastingly called *logical* +names. + +A logical prefix Lib can be associated with a physical path using +the command line option ``-Q`` `path` ``Lib``. All subfolders of path are +recursively associated to the logical path ``Lib`` extended with the +corresponding suffix coming from the physical path. For instance, the +folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding +to invalid |Coq| identifiers are skipped, and, by convention, +subdirectories named ``CVS`` or ``_darcs`` are skipped too. + +Thanks to this mechanism, ``.vo`` files are made available through the +logical name of the folder they are in, extended with their own +basename. For example, the name associated to the file +``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for +invalid identifiers. When compiling a source file, the ``.vo`` file stores +its logical name, so that an error is issued if it is loaded with the +wrong loadpath afterwards. + +Some folders have a special status and are automatically put in the +path. |Coq| commands associate automatically a logical path to files in +the repository trees rooted at the directory from where the command is +launched, ``coqlib/user-contrib/``, the directories listed in the +``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/`` +environment variables (see `XDG base directory specification +<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_) +with the same physical-to-logical translation and with an empty logical prefix. + +The command line option ``-R`` is a variant of ``-Q`` which has the strictly +same behavior regarding loadpaths, but which also makes the +corresponding ``.vo`` files available through their short names in a way +similar to the :cmd:`Import` command. For instance, ``-R path Lib`` +associates to the file ``/path/fOO/Bar/File.vo`` the logical name +``Lib.fOO.Bar.File``, but allows this file to be accessed through the +short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with +identical base name are present in different subdirectories of a +recursive loadpath, which of these files is found first may be system- +dependent and explicit qualification is recommended. The ``From`` argument +of the ``Require`` command can be used to bypass the implicit shortening +by providing an absolute root to the required file (see :ref:`compiled-files`). + +There also exists another independent loadpath mechanism attached to +OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object +files as described above. The OCaml loadpath is managed using +the option ``-I`` `path` (in the OCaml world, there is neither a +notion of logical name prefix nor a way to access files in +subdirectories of path). See the command :cmd:`Declare ML Module` in +:ref:`compiled-files` to understand the need of the OCaml loadpath. + +See :ref:`command-line-options` for a more general view over the |Coq| command +line options. + +.. _Coercions: + +Coercions +--------- + +Coercions can be used to implicitly inject terms from one *class* in +which they reside into another one. A *class* is either a sort +(denoted by the keyword ``Sortclass``), a product type (denoted by the +keyword ``Funclass``), or a type constructor (denoted by its name), e.g. +an inductive type or any constant with a type of the form +:n:`forall {+ @binder }, @sort`. + +Then the user is able to apply an object that is not a function, but +can be coerced to a function, and more generally to consider that a +term of type ``A`` is of type ``B`` provided that there is a declared coercion +between ``A`` and ``B``. + +More details and examples, and a description of the commands related +to coercions are provided in :ref:`implicitcoercions`. + +.. _printing_constructions_full: + +Printing constructions in full +------------------------------ + +.. flag:: Printing All + + Coercions, implicit arguments, the type of pattern matching, but also + notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some + tactics (typically the tactics applying to occurrences of subterms are + sensitive to the implicit arguments). Turning this flag on + deactivates all high-level printing features such as coercions, + implicit arguments, returned type of pattern matching, notations and + various syntactic sugar for pattern matching or record projections. + Otherwise said, :flag:`Printing All` includes the effects of the flags + :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`, + :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate + the high-level printing features, use the command ``Unset Printing All``. + +.. _printing-universes: + +Printing universes +------------------ + +.. flag:: Printing Universes + + Turn this flag on to activate the display of the actual level of each + occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in + combination with :flag:`Printing All` can help to diagnose failures to unify + terms apparently identical but internally different in the Calculus of Inductive + Constructions. + +.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string } + :name: Print Universes + + This command can be used to print the constraints on the internal level + of the occurrences of :math:`\Type` (see :ref:`Sorts`). + + The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting + constraints to preserve the implied transitive constraints between + kept universes). + + The :n:`Sorted` clause makes each universe + equivalent to a numbered label reflecting its level (with a linear + ordering) in the universe hierarchy. + + :n:`@string` is an optional output filename. + If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT + language, and can be processed by Graphviz tools. The format is + unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. + +.. _existential-variables: + +Existential variables +--------------------- + +.. insertprodn term_evar term_evar + +.. prodn:: + term_evar ::= ?[ @ident ] + | ?[ ?@ident ] + | ?@ident {? @%{ {+; @ident := @term } %} } + +|Coq| terms can include existential variables which represents unknown +subterms to eventually be replaced by actual subterms. + +Existential variables are generated in place of unsolvable implicit +arguments or “_” placeholders when using commands such as ``Check`` (see +Section :ref:`requests-to-the-environment`) or when using tactics such as +:tacn:`refine`, as well as in place of unsolvable instances when using +tactics such that :tacn:`eapply`. An existential +variable is defined in a context, which is the context of variables of +the placeholder which generated the existential variable, and a type, +which is the expected type of the placeholder. + +As a consequence of typing constraints, existential variables can be +duplicated in such a way that they possibly appear in different +contexts than their defining context. Thus, any occurrence of a given +existential variable comes with an instance of its original context. +In the simple case, when an existential variable denotes the +placeholder which generated it, or is used in the same context as the +one in which it was generated, the context is not displayed and the +existential variable is represented by “?” followed by an identifier. + +.. coqtop:: all + + Parameter identity : forall (X:Set), X -> X. + + Check identity _ _. + + Check identity _ (fun x => _). + +In the general case, when an existential variable :n:`?@ident` appears +outside of its context of definition, its instance, written under the +form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +how the variables of its defining context are instantiated. +The variables of the context of the existential variables which are +instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag +is on (see Section :ref:`explicit-display-existentials`), and this is why an +existential variable used in the same context as its context of definition is written with no instance. + +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + +Existential variables can be named by the user upon creation using +the syntax :n:`?[@ident]`. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see :ref:`goal-selectors`). + +.. _explicit-display-existentials: + +Explicit displaying of existential instances for pretty-printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. flag:: Printing Existential Instances + + This flag (off by default) activates the full display of how the + context of an existential variable is instantiated at each of the + occurrences of the existential variable. + +.. _tactics-in-terms: + +Solving existential variables using tactics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Instead of letting the unification engine try to solve an existential +variable by itself, one can also provide an explicit hole together +with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user +can put a tactic anywhere a term is expected. The order of resolution +is not specified and is implementation-dependent. The inner tactic may +use any variable defined in its scope, including repeated alternations +between variables introduced by term binding as well as those +introduced by tactic binding. The expression `tacexpr` can be any tactic +expression as described in :ref:`ltac`. + +.. coqtop:: all + + Definition foo (x : nat) : nat := ltac:(exact x). + +This construction is useful when one wants to define complicated terms +using highly automated tactics without resorting to writing the proof-term +by means of the interactive proof engine. + +.. _primitive-integers: + +Primitive Integers +------------------ + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. + +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). + +.. _primitive-floats: + +Primitive Floats +---------------- + +The language of terms features Binary64 floating-point numbers as values. +The type of such a value is *axiomatized*; it is declared through the +following sentence (excerpt from the :g:`PrimFloat` module): + +.. coqdoc:: + + Primitive float := #float64_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, the product of two primitive floats can be computed using the +:g:`PrimFloat.mul` function, declared and specified as follows: + +.. coqdoc:: + + Primitive mul := #float64_mul. + Notation "x * y" := (mul x y) : float_scope. + + Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). + +where :g:`Prim2SF` is defined in the :g:`FloatOps` module. + +The set of such operators is described in section :ref:`floats_library`. + +These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the +:g:`Print Assumptions` command. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient rules to reduce the applications of these primitive +operations, using the floating-point processor operators that are assumed +to comply with the IEEE 754 standard for floating-point arithmetic. + +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Float64` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. + +Literal values (of type :g:`Float64.t`) are extracted to literal OCaml +values (of type :g:`float`) written in hexadecimal notation and +wrapped into the :g:`Float64.of_float` constructor, e.g.: +:g:`Float64.of_float (0x1p+0)`. + +.. _bidirectionality_hints: + +Bidirectionality hints +---------------------- + +When type-checking an application, Coq normally does not use information from +the context to infer the types of the arguments. It only checks after the fact +that the type inferred for the application is coherent with the expected type. +Bidirectionality hints make it possible to specify that after type-checking the +first arguments of an application, typing information should be propagated from +the context to help inferring the types of the remaining arguments. + +An :cmd:`Arguments` command containing :n:`@argument_spec_block__1 & @argument_spec_block__2` +provides :ref:`bidirectionality_hints`. +It tells the typechecking algorithm, when type-checking +applications of :n:`@qualid`, to first type-check the arguments in +:n:`@argument_spec_block__1` and then propagate information from the typing context to +type-check the remaining arguments (in :n:`@argument_spec_block__2`). + +.. example:: Bidirectionality hints + + In a context where a coercion was declared from ``bool`` to ``nat``: + + .. coqtop:: in reset + + Definition b2n (b : bool) := if b then 1 else 0. + Coercion b2n : bool >-> nat. + + Coq cannot automatically coerce existential statements over ``bool`` to + statements over ``nat``, because the need for inserting a coercion is known + only from the expected type of a subterm: + + .. coqtop:: all + + Fail Check (ex_intro _ true _ : exists n : nat, n > 0). + + However, a suitable bidirectionality hint makes the example work: + + .. coqtop:: all + + Arguments ex_intro _ _ & _ _. + Check (ex_intro _ true _ : exists n : nat, n > 0). + +Coq will attempt to produce a term which uses the arguments you +provided, but in some cases involving Program mode the arguments after +the bidirectionality starts may be replaced by convertible but +syntactically different terms. |