diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 585 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 841 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 469 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 59 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 101 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 229 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 381 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 770 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 445 |
11 files changed, 3888 insertions, 9 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 64d4eddf04..1d3b661732 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -305,6 +305,8 @@ explicitations (as for terms 2.7.11). end). +.. _matching-dependent: + Matching objects of dependent types ----------------------------------- @@ -414,6 +416,7 @@ length, by writing I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. +.. _match-in-patterns: Patterns in ``in`` ~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst new file mode 100644 index 0000000000..38365e4035 --- /dev/null +++ b/doc/sphinx/addendum/extraction.rst @@ -0,0 +1,585 @@ +.. include:: ../replaces.rst + +.. _extraction: + +Extraction of programs in |OCaml| and Haskell +============================================= + +:Authors: Jean-Christophe Filliâtre and Pierre Letouzey + +We present here the |Coq| extraction commands, used to build certified +and relatively efficient functional programs, extracting them from +either |Coq| functions or |Coq| proofs of specifications. The +functional languages available as output are currently |OCaml|, Haskell +and Scheme. In the following, "ML" will be used (abusively) to refer +to any of the three. + +Before using any of the commands or options described in this chapter, +the extraction framework should first be loaded explicitly +via ``Require Extraction``, or via the more robust +``From Coq Require Extraction``. +Note that in earlier versions of Coq, these commands and options were +directly available without any preliminary ``Require``. + +.. coqtop:: in + + Require Extraction. + +Generating ML Code +------------------- + +.. note:: + + In the following, a qualified identifier `qualid` + can be used to refer to any kind of |Coq| global "object" : constant, + inductive type, inductive constructor or module name. + +The next two commands are meant to be used for rapid preview of +extraction. They both display extracted term(s) inside |Coq|. + +.. cmd:: Extraction @qualid. + + Extraction of the mentioned object in the |Coq| toplevel. + +.. cmd:: Recursive Extraction @qualid ... @qualid. + + Recursive extraction of all the mentioned objects and + all their dependencies in the |Coq| toplevel. + +All the following commands produce real ML files. User can choose to +produce one monolithic file or one file per |Coq| library. + +.. cmd:: Extraction "@file" @qualid ... @qualid. + + Recursive extraction of all the mentioned objects and all + their dependencies in one monolithic `file`. + Global and local identifiers are renamed according to the chosen ML + language to fulfill its syntactic conventions, keeping original + names as much as possible. + +.. cmd:: Extraction Library @ident. + + Extraction of the whole |Coq| library ``ident.v`` to an ML module + ``ident.ml``. In case of name clash, identifiers are here renamed + using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent + renaming. + +.. cmd:: Recursive Extraction Library @ident. + + Extraction of the |Coq| library ``ident.v`` and all other modules + ``ident.v`` depends on. + +.. cmd:: Separate Extraction @qualid ... @qualid. + + Recursive extraction of all the mentioned objects and all + their dependencies, just as ``Extraction "file"``, + but instead of producing one monolithic file, this command splits + the produced code in separate ML files, one per corresponding Coq + ``.v`` file. This command is hence quite similar to + ``Recursive Extraction Library``, except that only the needed + parts of Coq libraries are extracted instead of the whole. + The naming convention in case of name clash is the same one as + ``Extraction Library``: identifiers are here renamed using prefixes + ``coq_`` or ``Coq_``. + +The following command is meant to help automatic testing of +the extraction, see for instance the ``test-suite`` directory +in the |Coq| sources. + +.. cmd:: Extraction TestCompile @qualid ... @qualid. + + All the mentioned objects and all their dependencies are extracted + to a temporary |OCaml| file, just as in ``Extraction "file"``. Then + this temporary file and its signature are compiled with the same + |OCaml| compiler used to built |Coq|. This command succeeds only + if the extraction and the |OCaml| compilation succeed. It fails + if the current target language of the extraction is not |OCaml|. + +Extraction Options +------------------- + +Setting the target language +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ability to fix target language is the first and more important +of the extraction options. Default is ``OCaml``. + +.. cmd:: Extraction Language OCaml. +.. cmd:: Extraction Language Haskell. +.. cmd:: Extraction Language Scheme. + +Inlining and optimizations +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Since |OCaml| is a strict language, the extracted code has to +be optimized in order to be efficient (for instance, when using +induction principles we do not want to compute all the recursive calls +but only the needed ones). So the extraction mechanism provides an +automatic optimization routine that will be called each time the user +want to generate |OCaml| programs. The optimizations can be split in two +groups: the type-preserving ones (essentially constant inlining and +reductions) and the non type-preserving ones (some function +abstractions of dummy types are removed when it is deemed safe in order +to have more elegant types). Therefore some constants may not appear in the +resulting monolithic |OCaml| program. In the case of modular extraction, +even if some inlining is done, the inlined constant are nevertheless +printed, to ensure session-independent programs. + +Concerning Haskell, type-preserving optimizations are less useful +because of laziness. We still make some optimizations, for example in +order to produce more readable code. + +The type-preserving optimizations are controlled by the following |Coq| options: + +.. opt:: Extraction Optimize. + + Default is on. This controls all type-preserving optimizations made on + the ML terms (mostly reduction of dummy beta/iota redexes, but also + simplifications on Cases, etc). Turn this option off if you want a + ML term as close as possible to the Coq term. + +.. opt:: Extraction Conservative Types. + + Default is off. This controls the non type-preserving optimizations + made on ML terms (which try to avoid function abstraction of dummy + types). Turn this option on to make sure that ``e:t`` + implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted + code of ``e`` and ``t`` respectively. + +.. opt:: Extraction KeepSingleton. + + Default is off. Normally, when the extraction of an inductive type + produces a singleton type (i.e. a type with only one constructor, and + only one argument to this constructor), the inductive structure is + removed and this type is seen as an alias to the inner type. + The typical example is ``sig``. This option allows disabling this + optimization when one wishes to preserve the inductive structure of types. + +.. opt:: Extraction AutoInline. + + Default is on. The extraction mechanism inlines the bodies of + some defined constants, according to some heuristics + like size of bodies, uselessness of some arguments, etc. + Those heuristics are not always perfect; if you want to disable + this feature, turn this option off. + +.. cmd:: Extraction Inline @qualid ... @qualid. + + In addition to the automatic inline feature, the constants + mentionned by this command will always be inlined during extraction. + +.. cmd:: Extraction NoInline @qualid ... @qualid. + + Conversely, the constants mentionned by this command will + never be inlined during extraction. + +.. cmd:: Print Extraction Inline. + + Prints the current state of the table recording the custom inlinings + declared by the two previous commands. + +.. cmd:: Reset Extraction Inline. + + Empties the table recording the custom inlinings (see the + previous commands). + +**Inlining and printing of a constant declaration:** + +A user can explicitly ask for a constant to be extracted by two means: + + * by mentioning it on the extraction command line + + * by extracting the whole |Coq| module of this constant. + +In both cases, the declaration of this constant will be present in the +produced file. But this same constant may or may not be inlined in +the following terms, depending on the automatic/custom inlining mechanism. + +For the constants non-explicitly required but needed for dependency +reasons, there are two cases: + + * If an inlining decision is taken, whether automatically or not, + all occurrences of this constant are replaced by its extracted body, + and this constant is not declared in the generated file. + + * If no inlining decision is taken, the constant is normally + declared in the produced file. + +Extra elimination of useless arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following command provides some extra manual control on the +code elimination performed during extraction, in a way which +is independent but complementary to the main elimination +principles of extraction (logical parts and types). + +.. cmd:: Extraction Implicit @qualid [ @ident ... @ident ]. + + This experimental command allows declaring some arguments of + `qualid` as implicit, i.e. useless in extracted code and hence to + be removed by extraction. Here `qualid` can be any function or + inductive constructor, and the given `ident` are the names of + the concerned arguments. In fact, an argument can also be referred + by a number indicating its position, starting from 1. + +When an actual extraction takes place, an error is normally raised if the +``Extraction Implicit`` declarations cannot be honored, that is +if any of the implicited variables still occurs in the final code. +This behavior can be relaxed via the following option: + +.. opt:: Extraction SafeImplicits. + + Default is on. When this option is off, a warning is emitted + instead of an error if some implicited variables still occur in the + final code of an extraction. This way, the extracted code may be + obtained nonetheless and reviewed manually to locate the source of the issue + (in the code, some comments mark the location of these remaining + implicited variables). + Note that this extracted code might not compile or run properly, + depending of the use of these remaining implicited variables. + +Realizing axioms +~~~~~~~~~~~~~~~~ + +Extraction will fail if it encounters an informative axiom not realized. +A warning will be issued if it encounters a logical axiom, to remind the +user that inconsistent logical axioms may lead to incorrect or +non-terminating extracted terms. + +It is possible to assume some axioms while developing a proof. Since +these axioms can be any kind of proposition or object or type, they may +perfectly well have some computational content. But a program must be +a closed term, and of course the system cannot guess the program which +realizes an axiom. Therefore, it is possible to tell the system +what ML term corresponds to a given axiom. + +.. cmd:: Extract Constant @qualid => @string. + + Give an ML extraction for the given constant. + The `string` may be an identifier or a quoted string. + +.. cmd:: Extract Inlined Constant @qualid => @string. + + Same as the previous one, except that the given ML terms will + be inlined everywhere instead of being declared via a ``let``. + + .. note:: + This command is sugar for an ``Extract Constant`` followed + by a ``Extraction Inline``. Hence a ``Reset Extraction Inline`` + will have an effect on the realized and inlined axiom. + +.. caution:: It is the responsibility of the user to ensure that the ML + terms given to realize the axioms do have the expected types. In + fact, the strings containing realizing code are just copied to the + extracted files. The extraction recognizes whether the realized axiom + should become a ML type constant or a ML object declaration. For example: + +.. coqtop:: in + + Axiom X:Set. + Axiom x:X. + Extract Constant X => "int". + Extract Constant x => "0". + +Notice that in the case of type scheme axiom (i.e. whose type is an +arity, that is a sequence of product finished by a sort), then some type +variables have to be given (as quoted strings). The syntax is then: + +.. cmdv:: Extract Constant @qualid @string ... @string => @string. + +The number of type variables is checked by the system. For example: + +.. coqtop:: in + + Axiom Y : Set -> Set -> Set. + Extract Constant Y "'a" "'b" => " 'a * 'b ". + +Realizing an axiom via ``Extract Constant`` is only useful in the +case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom +have no computational content and hence will not appears in extracted +terms. But a warning is nonetheless issued if extraction encounters a +logical axiom. This warning reminds user that inconsistent logical +axioms may lead to incorrect or non-terminating extracted terms. + +If an informative axiom has not been realized before an extraction, a +warning is also issued and the definition of the axiom is filled with +an exception labeled ``AXIOM TO BE REALIZED``. The user must then +search these exceptions inside the extracted file and replace them by +real code. + +Realizing inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~ + +The system also provides a mechanism to specify ML terms for inductive +types and constructors. For instance, the user may want to use the ML +native boolean type instead of |Coq| one. The syntax is the following: + +.. cmd:: Extract Inductive @qualid => @string [ @string ... @string ]. + + Give an ML extraction for the given inductive type. You must specify + extractions for the type itself (first `string`) and all its + constructors (all the `string` between square brackets). In this form, + the ML extraction must be an ML inductive datatype, and the native + pattern-matching of the language will be used. + +.. cmdv:: Extract Inductive @qualid => @string [ @string ... @string ] @string. + + Same as before, with a final extra `string` that indicates how to + perform pattern-matching over this inductive type. In this form, + the ML extraction could be an arbitrary type. + For an inductive type with `k` constructors, the function used to + emulate the pattern-matching should expect `(k+1)` arguments, first the `k` + branches in functional form, and then the inductive element to + destruct. For instance, the match branch ``| S n => foo`` gives the + functional form ``(fun n -> foo)``. Note that a constructor with no + argument is considered to have one unit argument, in order to block + early evaluation of the branch: ``| O => bar`` leads to the functional + form ``(fun () -> bar)``. For instance, when extracting ``nat`` + into |OCaml| ``int``, the code to provide has type: + ``(unit->'a)->(int->'a)->int->'a``. + +.. caution:: As for ``Extract Constant``, this command should be used with care: + + * The ML code provided by the user is currently **not** checked at all by + extraction, even for syntax errors. + + * Extracting an inductive type to a pre-existing ML inductive type + is quite sound. But extracting to a general type (by providing an + ad-hoc pattern-matching) will often **not** be fully rigorously + correct. For instance, when extracting ``nat`` to |OCaml| ``int``, + it is theoretically possible to build ``nat`` values that are + larger than |OCaml| ``max_int``. It is the user's responsibility to + be sure that no overflow or other bad events occur in practice. + + * Translating an inductive type to an arbitrary ML type does **not** + magically improve the asymptotic complexity of functions, even if the + ML type is an efficient representation. For instance, when extracting + ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic. + It might be interesting to associate this translation with + some specific ``Extract Constant`` when primitive counterparts exist. + +Typical examples are the following: + +.. coqtop:: in + + Extract Inductive unit => "unit" [ "()" ]. + Extract Inductive bool => "bool" [ "true" "false" ]. + Extract Inductive sumbool => "bool" [ "true" "false" ]. + +.. note:: + + When extracting to |OCaml|, if an inductive constructor or type has arity 2 and + the corresponding string is enclosed by parentheses, and the string meets + |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is + used as infix constructor or type. + +.. coqtop:: in + + Extract Inductive list => "list" [ "[]" "(::)" ]. + Extract Inductive prod => "(*)" [ "(,)" ]. + +As an example of translation to a non-inductive datatype, let's turn +``nat`` into |OCaml| ``int`` (see caveat above): + +.. coqtop:: in + + Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". + +Avoiding conflicts with existing filenames +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When using ``Extraction Library``, the names of the extracted files +directly depends from the names of the |Coq| files. It may happen that +these filenames are in conflict with already existing files, +either in the standard library of the target language or in other +code that is meant to be linked with the extracted code. +For instance the module ``List`` exists both in |Coq| and in |OCaml|. +It is possible to instruct the extraction not to use particular filenames. + +.. cmd:: Extraction Blacklist @ident ... @ident. + + Instruct the extraction to avoid using these names as filenames + for extracted code. + +.. cmd:: Print Extraction Blacklist. + + Show the current list of filenames the extraction should avoid. + +.. cmd:: Reset Extraction Blacklist. + + Allow the extraction to use any filename. + +For |OCaml|, a typical use of these commands is +``Extraction Blacklist String List``. + +Differences between |Coq| and ML type systems +---------------------------------------------- + +Due to differences between |Coq| and ML type systems, +some extracted programs are not directly typable in ML. +We now solve this problem (at least in |OCaml|) by adding +when needed some unsafe casting ``Obj.magic``, which give +a generic type ``'a`` to any term. + +First, if some part of the program is *very* polymorphic, there +may be no ML type for it. In that case the extraction to ML works +alright but the generated code may be refused by the ML +type-checker. A very well known example is the ``distr-pair`` +function: + +.. coqtop:: in + + Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y). + +In |OCaml|, for instance, the direct extracted term would be:: + + let dp x y f = Pair((f () x),(f () y)) + +and would have type:: + + dp : 'a -> 'a -> (unit -> 'a -> 'b) -> ('b,'b) prod + +which is not its original type, but a restriction. + +We now produce the following correct version:: + + let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) + +Secondly, some |Coq| definitions may have no counterpart in ML. This +happens when there is a quantification over types inside the type +of a constructor; for example: + +.. coqtop:: in + + Inductive anything : Type := dummy : forall A:Set, A -> anything. + +which corresponds to the definition of an ML dynamic type. +In |OCaml|, we must cast any argument of the constructor dummy +(no GADT are produced yet by the extraction). + +Even with those unsafe castings, you should never get error like +``segmentation fault``. In fact even if your program may seem +ill-typed to the |OCaml| type-checker, it can't go wrong : it comes +from a Coq well-typed terms, so for example inductive types will always +have the correct number of arguments, etc. Of course, when launching +manually some extracted function, you should apply it to arguments +of the right shape (from the |Coq| point-of-view). + +More details about the correctness of the extracted programs can be +found in :cite:`Let02`. + +We have to say, though, that in most "realistic" programs, these problems do not +occur. For example all the programs of Coq library are accepted by the |OCaml| +type-checker without any ``Obj.magic`` (see examples below). + +Some examples +------------- + +We present here two examples of extractions, taken from the +|Coq| Standard Library. We choose |OCaml| as target language, +but all can be done in the other dialects with slight modifications. +We then indicate where to find other examples and tests of extraction. + +A detailed example: Euclidean division +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The file ``Euclid`` contains the proof of Euclidean division. +The natural numbers used there are unary integers of type ``nat``, +defined by two constructors ``O`` and ``S``. +This module contains a theorem ``eucl_dev``, whose type is:: + + forall b:nat, b > 0 -> forall a:nat, diveucl a b + +where ``diveucl`` is a type for the pair of the quotient and the +modulo, plus some logical assertions that disappear during extraction. +We can now extract this program to |OCaml|: + +.. coqtop:: none + + Reset Initial. + +.. coqtop:: all + + Require Extraction. + Require Import Euclid Wf_nat. + Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. + Recursive Extraction eucl_dev. + +The inlining of ``gt_wf_rec`` and others is not +mandatory. It only enhances readability of extracted code. +You can then copy-paste the output to a file ``euclid.ml`` or let +|Coq| do it for you with the following command:: + + Extraction "euclid" eucl_dev. + +Let us play the resulting program (in an |OCaml| toplevel):: + + #use "euclid.ml";; + type nat = O | S of nat + type sumbool = Left | Right + val sub : nat -> nat -> nat = <fun> + val le_lt_dec : nat -> nat -> sumbool = <fun> + val le_gt_dec : nat -> nat -> sumbool = <fun> + type diveucl = Divex of nat * nat + val eucl_dev : nat -> nat -> diveucl = <fun> + + # eucl_dev (S (S O)) (S (S (S (S (S O)))));; + - : diveucl = Divex (S (S O), S O) + +It is easier to test on |OCaml| integers:: + + # let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));; + val nat_of_int : int -> nat = <fun> + + # let rec int_of_nat = function O -> 0 | S p -> 1+(int_of_nat p);; + val int_of_nat : nat -> int = <fun> + + # let div a b = + let Divex (q,r) = eucl_dev (nat_of_int b) (nat_of_int a) + in (int_of_nat q, int_of_nat r);; + val div : int -> int -> int * int = <fun> + + # div 173 15;; + - : int * int = (11, 8) + +Note that these ``nat_of_int`` and ``int_of_nat`` are now +available via a mere ``Require Import ExtrOcamlIntConv`` and then +adding these functions to the list of functions to extract. This file +``ExtrOcamlIntConv.v`` and some others in ``plugins/extraction/`` +are meant to help building concrete program via extraction. + +Extraction's horror museum +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Some pathological examples of extraction are grouped in the file +``test-suite/success/extraction.v`` of the sources of |Coq|. + +Users' Contributions +~~~~~~~~~~~~~~~~~~~~ + +Several of the |Coq| Users' Contributions use extraction to produce +certified programs. In particular the following ones have an automatic +extraction test: + + * ``additions`` : https://github.com/coq-contribs/additions + * ``bdds`` : https://github.com/coq-contribs/bdds + * ``canon-bdds`` : https://github.com/coq-contribs/canon-bdds + * ``chinese`` : https://github.com/coq-contribs/chinese + * ``continuations`` : https://github.com/coq-contribs/continuations + * ``coq-in-coq`` : https://github.com/coq-contribs/coq-in-coq + * ``exceptions`` : https://github.com/coq-contribs/exceptions + * ``firing-squad`` : https://github.com/coq-contribs/firing-squad + * ``founify`` : https://github.com/coq-contribs/founify + * ``graphs`` : https://github.com/coq-contribs/graphs + * ``higman-cf`` : https://github.com/coq-contribs/higman-cf + * ``higman-nw`` : https://github.com/coq-contribs/higman-nw + * ``hardware`` : https://github.com/coq-contribs/hardware + * ``multiplier`` : https://github.com/coq-contribs/multiplier + * ``search-trees`` : https://github.com/coq-contribs/search-trees + * ``stalmarck`` : https://github.com/coq-contribs/stalmarck + +Note that ``continuations`` and ``multiplier`` are a bit particular. They are +examples of developments where ``Obj.magic`` are needed. This is +probably due to an heavy use of impredicativity. After compilation, those +two examples run nonetheless, thanks to the correction of the +extraction :cite:`Let02`. diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst new file mode 100644 index 0000000000..d60387f4f6 --- /dev/null +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -0,0 +1,841 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. _generalizedrewriting: + +Generalized rewriting +===================== + +:Author: Matthieu Sozeau + +This chapter presents the extension of several equality related +tactics to work over user-defined structures (called setoids) that are +equipped with ad-hoc equivalence relations meant to behave as +equalities. Actually, the tactics have also been generalized to +relations weaker then equivalences (e.g. rewriting systems). The +toolbox also extends the automatic rewriting capabilities of the +system, allowing the specification of custom strategies for rewriting. + +This documentation is adapted from the previous setoid documentation +by Claudio Sacerdoti Coen (based on previous work by Clément Renard). +The new implementation is a drop-in replacement for the old one +[#tabareau]_, hence most of the documentation still applies. + +The work is a complete rewrite of the previous implementation, based +on the type class infrastructure. It also improves on and generalizes +the previous implementation in several ways: + + ++ User-extensible algorithm. The algorithm is separated in two parts: + generations of the rewriting constraints (done in ML) and solving of + these constraints using type class resolution. As type class + resolution is extensible using tactics, this allows users to define + general ways to solve morphism constraints. ++ Sub-relations. An example extension to the base algorithm is the + ability to define one relation as a subrelation of another so that + morphism declarations on one relation can be used automatically for + the other. This is done purely using tactics and type class search. ++ Rewriting under binders. It is possible to rewrite under binders in + the new implementation, if one provides the proper morphisms. Again, + most of the work is handled in the tactics. ++ First-class morphisms and signatures. Signatures and morphisms are + ordinary Coq terms, hence they can be manipulated inside Coq, put + inside structures and lemmas about them can be proved inside the + system. Higher-order morphisms are also allowed. ++ Performance. The implementation is based on a depth-first search for + the first solution to a set of constraints which can be as fast as + linear in the size of the term, and the size of the proof term is + linear in the size of the original term. Besides, the extensibility + allows the user to customize the proof search if necessary. + +.. [#tabareau] Nicolas Tabareau helped with the gluing. + +Introduction to generalized rewriting +------------------------------------- + + +Relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~ + +A parametric *relation* ``R`` is any term of type +``forall (x1 :T1 ) ... (xn :Tn ), relation A``. +The expression ``A``, which depends on ``x1 ... xn`` , is called the *carrier* +of the relation and ``R`` is said to be a relation over ``A``; the list +``x1,...,xn`` is the (possibly empty) list of parameters of the relation. + +**Example 1 (Parametric relation):** + +It is possible to implement finite sets of elements of type ``A`` as +unordered list of elements of type ``A``. +The function ``set_eq: forall (A: Type), relation (list A)`` +satisfied by two lists with the same elements is a parametric relation +over ``(list A)`` with one parameter ``A``. The type of ``set_eq`` +is convertible with ``forall (A: Type), list A -> list A -> Prop.`` + +An *instance* of a parametric relation ``R`` with n parameters is any term +``(R t1 ... tn )``. + +Let ``R`` be a relation over ``A`` with ``n`` parameters. A term is a parametric +proof of reflexivity for ``R`` if it has type +``forall (x1 :T1 ) ... (xn :Tn), reflexive (R x1 ... xn )``. +Similar definitions are given for parametric proofs of symmetry and transitivity. + +**Example 2 (Parametric relation (cont.)):** + +The ``set_eq`` relation of the previous example can be proved to be +reflexive, symmetric and transitive. A parametric unary function ``f`` of type +``forall (x1 :T1 ) ... (xn :Tn ), A1 -> A2`` covariantly respects two parametric relation instances +``R1`` and ``R2`` if, whenever ``x``, ``y`` satisfy ``R1 x y``, their images (``f x``) and (``f y``) +satisfy ``R2 (f x) (f y)``. An ``f`` that respects its input and output +relations will be called a unary covariant *morphism*. We can also say +that ``f`` is a monotone function with respect to ``R1`` and ``R2`` . The +sequence ``x1 ... xn`` represents the parameters of the morphism. + +Let ``R1`` and ``R2`` be two parametric relations. The *signature* of a +parametric morphism of type ``forall (x1 :T1 ) ... (xn :Tn ), A1 -> A2`` +that covariantly respects two instances :math:`I_{R_1}` and :math:`I_{R_2}` of ``R1`` and ``R2`` +is written :math:`I_{R_1} ++> I_{R_2}`. Notice that the special arrow ++>, which +reminds the reader of covariance, is placed between the two relation +instances, not between the two carriers. The signature relation +instances and morphism will be typed in a context introducing +variables for the parameters. + +The previous definitions are extended straightforwardly to n-ary +morphisms, that are required to be simultaneously monotone on every +argument. + +Morphisms can also be contravariant in one or more of their arguments. +A morphism is contravariant on an argument associated to the relation +instance :math`R` if it is covariant on the same argument when the inverse +relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` +is used in signatures for contravariant morphisms. + +Functions having arguments related by symmetric relations instances +are both covariant and contravariant in those arguments. The special +arrow ``==>`` is used in signatures for morphisms that are both +covariant and contravariant. + +An instance of a parametric morphism :math:`f` with :math:`n` +parameters is any term :math:`f \, t_1 \ldots t_n`. + +**Example 3 (Morphisms):** + +Continuing the previous example, let ``union: forall (A: Type), list A -> list A -> list A`` +perform the union of two sets by appending one list to the other. ``union` is a binary +morphism parametric over ``A`` that respects the relation instance +``(set_eq A)``. The latter condition is proved by showing: + +.. coqtop:: in + + forall (A: Type) (S1 S1’ S2 S2’: list A), + set_eq A S1 S1’ -> + set_eq A S2 S2’ -> + set_eq A (union A S1 S2) (union A S1’ S2’). + +The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` +for all ``A``. + +**Example 4 (Contravariant morphism):** + +The division function ``Rdiv: R -> R -> R`` is a morphism of signature +``le ++> le --> le`` where ``le`` is the usual order relation over +real numbers. Notice that division is covariant in its first argument +and contravariant in its second argument. + +Leibniz equality is a relation and every function is a morphism that +respects Leibniz equality. Unfortunately, Leibniz equality is not +always the intended equality for a given structure. + +In the next section we will describe the commands to register terms as +parametric relations and morphisms. Several tactics that deal with +equality in Coq can also work with the registered relations. The exact +list of tactic will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. +For instance, the tactic reflexivity can be used to close a goal ``R n n`` whenever ``R`` +is an instance of a registered reflexive relation. However, the +tactics that replace in a context ``C[]`` one term with another one +related by ``R`` must verify that ``C[]`` is a morphism that respects the +intended relation. Currently the verification consists in checking +whether ``C[]`` is a syntactic composition of morphism instances that respects some obvious +compatibility constraints. + + +**Example 5 (Rewriting):** + +Continuing the previous examples, suppose that the user must prove +``set_eq int (union int (union int S1 S2) S2) (f S1 S2)`` under the +hypothesis ``H: set_eq int S2 (@nil int)``. It +is possible to use the ``rewrite`` tactic to replace the first two +occurrences of ``S2`` with ``@nil int`` in the goal since the +context ``set_eq int (union int (union int S1 nil) nil) (f S1 S2)``, +being a composition of morphisms instances, is a morphism. However the +tactic will fail replacing the third occurrence of ``S2`` unless ``f`` +has also been declared as a morphism. + + +Adding new relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`, +:g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be +declared with the following command: + +.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident. + +after having required the ``Setoid`` module with the ``Require Setoid`` +command. + +The :g:`@ident` gives a unique name to the morphism and it is used +by the command to generate fresh names for automatically provided +lemmas used internally. + +Notice that the carrier and relation parameters may refer to the +context of variables introduced at the beginning of the declaration, +but the instances need not be made only of variables. Also notice that +``A`` is *not* required to be a term having the same parameters as ``Aeq``, +although that is often the case in practice (this departs from the +previous implementation). + + +.. cmd:: Add Relation + +In case the carrier and relations are not parametric, one can use this command +instead, whose syntax is the same except there is no local context. + +The proofs of reflexivity, symmetry and transitivity can be omitted if +the relation is not an equivalence relation. The proofs must be +instances of the corresponding relation definitions: e.g. the proof of +reflexivity must have a type convertible to +:g:`reflexive (A t1 ... tn) (Aeq t′ 1 …t′ n )`. +Each proof may refer to the introduced variables as well. + +**Example 6 (Parametric relation):** + +For Leibniz equality, we may declare: + +.. coqtop:: in + + Add Parametric Relation (A : Type) : A (@eq A) + [reflexivity proved by @refl_equal A] + ... + +Some tactics (``reflexivity``, ``symmetry``, ``transitivity``) work only on +relations that respect the expected properties. The remaining tactics +(``replace``, ``rewrite`` and derived tactics such as ``autorewrite``) do not +require any properties over the relation. However, they are able to +replace terms with related ones only in contexts that are syntactic +compositions of parametric morphism instances declared with the +following command. + +.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident. + +The command declares ``f`` as a parametric morphism of signature ``sig``. The +identifier ``id`` gives a unique name to the morphism and it is used as +the base name of the type class instance definition and as the name of +the lemma that proves the well-definedness of the morphism. The +parameters of the morphism as well as the signature may refer to the +context of variables. The command asks the user to prove interactively +that ``f`` respects the relations identified from the signature. + +**Example 7:** + +We start the example by assuming a small theory over +homogeneous sets and we declare set equality as a parametric +equivalence relation and union of two sets as a parametric morphism. + +.. coqtop:: in + + Require Export Setoid. + Require Export Relation_Definitions. + + Set Implicit Arguments. + + Parameter set: Type -> Type. + Parameter empty: forall A, set A. + Parameter eq_set: forall A, set A -> set A -> Prop. + Parameter union: forall A, set A -> set A -> set A. + + Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)). + Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)). + Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)). + Axiom empty_neutral: forall A (S: set A), eq_set (union S (empty A)) S. + + Axiom union_compat: forall (A : Type), + forall x x' : set A, eq_set x x' -> + forall y y' : set A, eq_set y y' -> + eq_set (union x y) (union x' y'). + + Add Parametric Relation A : (set A) (@eq_set A) + reflexivity proved by (eq_set_refl (A:=A)) + symmetry proved by (eq_set_sym (A:=A)) + transitivity proved by (eq_set_trans (A:=A)) + as eq_set_rel. + + Add Parametric Morphism A : (@union A) with + signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. + Proof. + exact (@union_compat A). + Qed. + +It is possible to reduce the burden of specifying parameters using +(maximally inserted) implicit arguments. If ``A`` is always set as +maximally implicit in the previous example, one can write: + +.. coqtop:: in + + Add Parametric Relation A : (set A) eq_set + reflexivity proved by eq_set_refl + symmetry proved by eq_set_sym + transitivity proved by eq_set_trans + as eq_set_rel. + +.. coqtop:: in + + Add Parametric Morphism A : (@union A) with + signature eq_set ==> eq_set ==> eq_set as union_mor. + +.. coqtop:: in + + Proof. exact (@union_compat A). Qed. + +We proceed now by proving a simple lemma performing a rewrite step and +then applying reflexivity, as we would do working with Leibniz +equality. Both tactic applications are accepted since the required +properties over ``eq_set`` and ``union`` can be established from the two +declarations above. + +.. coqtop:: in + + Goal forall (S: set nat), + eq_set (union (union S empty) S) (union S S). + +.. coqtop:: in + + Proof. intros. rewrite empty_neutral. reflexivity. Qed. + +The tables of relations and morphisms are managed by the type class +instance mechanism. The behavior on section close is to generalize the +instances by the variables of the section (and possibly hypotheses +used in the proofs of instance declarations) but not to export them in +the rest of the development for proof search. One can use the +``Existing Instance`` command to do so outside the section, using the name of the +declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier +for the corresponding class instance declaration +(see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at +definition time. When loading a compiled file or importing a module, +all the declarations of this module will be loaded. + + +Rewriting and non reflexive relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To replace only one argument of an n-ary morphism it is necessary to +prove that all the other arguments are related to themselves by the +respective relation instances. + +**Example 8:** + +To replace ``(union S empty)`` with ``S`` in ``(union (union S empty) S) (union S S)`` +the rewrite tactic must exploit the monotony of ``union`` (axiom ``union_compat`` +in the previous example). Applying ``union_compat`` by hand we are left with the +goal ``eq_set (union S S) (union S S)``. + +When the relations associated to some arguments are not reflexive, the +tactic cannot automatically prove the reflexivity goals, that are left +to the user. + +Setoids whose relation are partial equivalence relations (PER) are +useful to deal with partial functions. Let ``R`` be a PER. We say that an +element ``x`` is defined if ``R x x``. A partial function whose domain +comprises all the defined elements only is declared as a morphism that +respects ``R``. Every time a rewriting step is performed the user must +prove that the argument of the morphism is defined. + +**Example 9:** + +Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the +smaller PER over non zero elements). Division can be declared as a +morphism of signature ``eq ==> eq0 ==> eq``. Replace ``x`` with +``y`` in ``div x n = div y n`` opens the additional goal ``eq0 n n`` +that is equivalent to ``n = n /\ n <> 0``. + + +Rewriting and non symmetric relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When the user works up to relations that are not symmetric, it is no +longer the case that any covariant morphism argument is also +contravariant. As a result it is no longer possible to replace a term +with a related one in every context, since the obtained goal implies +the previous one if and only if the replacement has been performed in +a contravariant position. In a similar way, replacement in an +hypothesis can be performed only if the replaced term occurs in a +covariant position. + +**Example 10 (Covariance and contravariance):** + +Suppose that division over real numbers has been defined as a morphism of signature +``Z.div: Z.lt ++> Z.lt --> Z.lt`` (i.e. ``Z.div`` is increasing in +its first argument, but decreasing on the second one). Let ``<`` +denotes ``Z.lt``. Under the hypothesis ``H: x < y`` we have +``k < x / y -> k < x / x``, but not ``k < y / x -> k < x / x``. Dually, +under the same hypothesis ``k < x / y -> k < y / y`` holds, but +``k < y / x -> k < y / y`` does not. Thus, if the current goal is +``k < x / x``, it is possible to replace only the second occurrence of +``x`` (in contravariant position) with ``y`` since the obtained goal +must imply the current one. On the contrary, if ``k < x / x`` is an +hypothesis, it is possible to replace only the first occurrence of +``x`` (in covariant position) with ``y`` since the current +hypothesis must imply the obtained one. + +Contrary to the previous implementation, no specific error message +will be raised when trying to replace a term that occurs in the wrong +position. It will only fail because the rewriting constraints are not +satisfiable. However it is possible to use the at modifier to specify +which occurrences should be rewritten. + +As expected, composing morphisms together propagates the variance +annotations by switching the variance every time a contravariant +position is traversed. + +**Example 11:** + +Let us continue the previous example and let us consider +the goal ``x / (x / x) < k``. The first and third occurrences of +``x`` are in a contravariant position, while the second one is in +covariant position. More in detail, the second occurrence of ``x`` +occurs covariantly in ``(x / x)`` (since division is covariant in +its first argument), and thus contravariantly in ``x / (x / x)`` +(since division is contravariant in its second argument), and finally +covariantly in ``x / (x / x) < k`` (since ``<``, as every +transitive relation, is contravariant in its first argument with +respect to the relation itself). + + +Rewriting in ambiguous setoid contexts +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +One function can respect several different relations and thus it can +be declared as a morphism having multiple signatures. + +**Example 12:** + + +Union over homogeneous lists can be given all the +following signatures: ``eq ==> eq ==> eq`` (``eq`` being the +equality over ordered lists) ``set_eq ==> set_eq ==> set_eq`` +(``set_eq`` being the equality over unordered lists up to duplicates), +``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq`` +being the equality over unordered lists). + +To declare multiple signatures for a morphism, repeat the ``Add Morphism`` +command. + +When morphisms have multiple signatures it can be the case that a +rewrite request is ambiguous, since it is unclear what relations +should be used to perform the rewriting. Contrary to the previous +implementation, the tactic will always choose the first possible +solution to the set of constraints generated by a rewrite and will not +try to find *all* possible solutions to warn the user about. + + +Commands and tactics +-------------------- + + +.. _first-class-setoids-and-morphisms: + +First class setoids and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + + +The implementation is based on a first-class representation of +properties of relations and morphisms as type classes. That is, the +various combinations of properties on relations and morphisms are +represented as records and instances of theses classes are put in a +hint database. For example, the declaration: + +.. coqtop:: in + + Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) + [reflexivity proved by refl] + [symmetry proved by sym] + [transitivity proved by trans] + as id. + + +is equivalent to an instance declaration: + +.. coqtop:: in + + Instance (x1 : T1) ... (xn : Tk) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := + [Equivalence_Reflexive := refl] + [Equivalence_Symmetric := sym] + [Equivalence_Transitive := trans]. + +The declaration itself amounts to the definition of an object of the +record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added +to the ``typeclass_instances`` hint database. Morphism declarations are +also instances of a type class defined in ``Classes.Morphisms``. See the +documentation on type classes :ref:`typeclasses` +and the theories files in Classes for further explanations. + +One can inform the rewrite tactic about morphisms and relations just +by using the typeclass mechanism to declare them using Instance and +Context vernacular commands. Any object of type Proper (the type of +morphism declarations) in the local context will also be automatically +used by the rewriting tactic to solve constraints. + +Other representations of first class setoids and morphisms can also be +handled by encoding them as records. In the following example, the +projections of the setoid relation and of the morphism function can be +registered as parametric relations and morphisms. + +**Example 13 (First class setoids):** + +.. coqtop:: in + + Require Import Relation_Definitions Setoid. + + Record Setoid: Type := + { car: Type; + eq: car -> car -> Prop; + refl: reflexive _ eq; + sym: symmetric _ eq; + trans: transitive _ eq + }. + + Add Parametric Relation (s : Setoid) : (@car s) (@eq s) + reflexivity proved by (refl s) + symmetry proved by (sym s) + transitivity proved by (trans s) as eq_rel. + + Record Morphism (S1 S2:Setoid): Type := + { f: car S1 -> car S2; + compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) + }. + + Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : + (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. + Proof. apply (compat S1 S2 M). Qed. + + Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2) + (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). + Proof. intros. rewrite H. reflexivity. Qed. + +.. _tactics-enabled-on-user-provided-relations: + +Tactics enabled on user provided relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following tactics, all prefixed by ``setoid_``, deal with arbitrary +registered relations and morphisms. Moreover, all the corresponding +unprefixed tactics (i.e. ``reflexivity``, ``symmetry``, ``transitivity``, +``replace``, ``rewrite``) have been extended to fall back to their prefixed +counterparts when the relation involved is not Leibniz equality. +Notice, however, that using the prefixed tactics it is possible to +pass additional arguments such as ``using relation``. + +.. tacv:: setoid_reflexivity + +.. tacv:: setoid_symmetry [in @ident] + +.. tacv:: setoid_transitivity + +.. tacv:: setoid_rewrite [@orientation] @term [at @occs] [in @ident] + +.. tacv:: setoid_replace @term with @term [in @ident] [using relation @term] [by @tactic] + + +The ``using relation`` arguments cannot be passed to the unprefixed form. +The latter argument tells the tactic what parametric relation should +be used to replace the first tactic argument with the second one. If +omitted, it defaults to the ``DefaultRelation`` instance on the type of +the objects. By default, it means the most recent ``Equivalence`` instance +in the environment, but it can be customized by declaring +new ``DefaultRelation`` instances. As Leibniz equality is a declared +equivalence, it will fall back to it if no other relation is declared +on a given type. + +Every derived tactic that is based on the unprefixed forms of the +tactics considered above will also work up to user defined relations. +For instance, it is possible to register hints for ``autorewrite`` that +are not proof of Leibniz equalities. In particular it is possible to +exploit ``autorewrite`` to simulate normalization in a term rewriting +system up to user defined equalities. + + +Printing relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ``Print Instances`` command can be used to show the list of currently +registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric`` +or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms +(implemented as ``Proper`` instances). When the rewriting tactics refuse +to replace a term in a context because the latter is not a composition +of morphisms, the ``Print Instances`` commands can be useful to understand +what additional morphisms should be registered. + + +Deprecated syntax and backward incompatibilities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Due to backward compatibility reasons, the following syntax for the +declaration of setoids and morphisms is also accepted. + +.. tacv:: Add Setoid @A @Aeq @ST as @ident + +where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier +and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record +packing together the reflexivity, symmetry and transitivity lemmas). +Notice that the syntax is not completely backward compatible since the +identifier was not required. + +.. cmd:: Add Morphism f : @ident. + +The latter command also is restricted to the declaration of morphisms +without parameters. It is not fully backward compatible since the +property the user is asked to prove is slightly different: for n-ary +morphisms the hypotheses of the property are permuted; moreover, when +the morphism returns a proposition, the property is now stated using a +bi-implication in place of a simple implication. In practice, porting +an old development to the new semantics is usually quite simple. + +Notice that several limitations of the old implementation have been +lifted. In particular, it is now possible to declare several relations +with the same carrier and several signatures for the same morphism. +Moreover, it is now also possible to declare several morphisms having +the same signature. Finally, the replace and rewrite tactics can be +used to replace terms in contexts that were refused by the old +implementation. As discussed in the next section, the semantics of the +new ``setoid_rewrite`` command differs slightly from the old one and +``rewrite``. + + +Extensions +---------- + + +Rewriting under binders +~~~~~~~~~~~~~~~~~~~~~~~ + +warning:: Due to compatibility issues, this feature is enabled only +when calling the ``setoid_rewrite`` tactics directly and not ``rewrite``. + +To be able to rewrite under binding constructs, one must declare +morphisms with respect to pointwise (setoid) equivalence of functions. +Example of such morphisms are the standard ``all`` and ``ex`` combinators for +universal and existential quantification respectively. They are +declared as morphisms in the ``Classes.Morphisms_Prop`` module. For +example, to declare that universal quantification is a morphism for +logical equivalence: + +.. coqtop:: in + + Instance all_iff_morphism (A : Type) : + Proper (pointwise_relation A iff ==> iff) (@all A). + +.. coqtop:: all + + Proof. simpl_relation. + +One then has to show that if two predicates are equivalent at every +point, their universal quantifications are equivalent. Once we have +declared such a morphism, it will be used by the setoid rewriting +tactic each time we try to rewrite under an ``all`` application (products +in ``Prop`` are implicitly translated to such applications). + +Indeed, when rewriting under a lambda, binding variable ``x``, say from ``P x`` +to ``Q x`` using the relation iff, the tactic will generate a proof of +``pointwise_relation A iff (fun x => P x) (fun x => Q x)`` from the proof +of ``iff (P x) (Q x)`` and a constraint of the form Proper +``(pointwise_relation A iff ==> ?) m`` will be generated for the +surrounding morphism ``m``. + +Hence, one can add higher-order combinators as morphisms by providing +signatures using pointwise extension for the relations on the +functional arguments (or whatever subrelation of the pointwise +extension). For example, one could declare the ``map`` combinator on lists +as a morphism: + +.. coqtop:: in + + Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : + Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). + +where ``list_equiv`` implements an equivalence on lists parameterized by +an equivalence on the elements. + +Note that when one does rewriting with a lemma under a binder using +``setoid_rewrite``, the application of the lemma may capture the bound +variable, as the semantics are different from rewrite where the lemma +is first matched on the whole term. With the new ``setoid_rewrite``, +matching is done on each subterm separately and in its local +environment, and all matches are rewritten *simultaneously* by +default. The semantics of the previous ``setoid_rewrite`` implementation +can almost be recovered using the ``at 1`` modifier. + + +Sub-relations +~~~~~~~~~~~~~ + +Sub-relations can be used to specify that one relation is included in +another, so that morphisms signatures for one can be used for the +other. If a signature mentions a relation ``R`` on the left of an +arrow ``==>``, then the signature also applies for any relation ``S`` that is +smaller than ``R``, and the inverse applies on the right of an arrow. One +can then declare only a few morphisms instances that generate the +complete set of signatures for a particular constant. By default, the +only declared subrelation is ``iff``, which is a subrelation of ``impl`` and +``inverse impl`` (the dual of implication). That’s why we can declare only +two morphisms for conjunction: ``Proper (impl ==> impl ==> impl) and`` and +``Proper (iff ==> iff ==> iff) and``. This is sufficient to satisfy any +rewriting constraints arising from a rewrite using ``iff``, ``impl`` or +``inverse impl`` through ``and``. + +Sub-relations are implemented in ``Classes.Morphisms`` and are a prime +example of a mostly user-space extension of the algorithm. + + +Constant unfolding +~~~~~~~~~~~~~~~~~~ + +The resolution tactic is based on type classes and hence regards user- +defined constants as transparent by default. This may slow down the +resolution due to a lot of unifications (all the declared ``Proper`` +instances are tried at each node of the search tree). To speed it up, +declare your constant as rigid for proof search using the command +``Typeclasses Opaque`` (see :ref:`TypeclassesTransparent`). + +Strategies for rewriting +------------------------ + +Definitions +~~~~~~~~~~~ + +The generalized rewriting tactic is based on a set of strategies that can be +combined to obtain custom rewriting procedures. Its set of strategies is based +on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting +strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a +strategy expression. Strategies are defined inductively as described by the +following grammar: + +.. productionlist:: rewriting + s, t, u : `strategy` + : | `lemma` + : | `lemma_right_to_left` + : | `failure` + : | `identity` + : | `reflexivity` + : | `progress` + : | `failure_catch` + : | `composition` + : | `left_biased_choice` + : | `iteration_one_or_more` + : | `iteration_zero_or_more` + : | `one_subterm` + : | `all_subterms` + : | `innermost_first` + : | `outermost_first` + : | `bottom_up` + : | `top_down` + : | `apply_hint` + : | `any_of_the_terms` + : | `apply_reduction` + : | `fold_expression` + +.. productionlist:: rewriting + strategy : "(" `s` ")" + lemma : `c` + lemma_right_to_left : "<-" `c` + failure : `fail` + identity : `id` + reflexivity : `refl` + progress : `progress` `s` + failure_catch : `try` `s` + composition : `s` ";" `u` + left_biased_choice : choice `s` `t` + iteration_one_or_more : `repeat` `s` + iteration_zero_or_more : `any` `s` + one_subterm : subterm `s` + all_subterms : subterms `s` + innermost_first : `innermost` `s` + outermost_first : `outermost` `s` + bottom_up : `bottomup` `s` + top_down : `topdown` `s` + apply_hint : hints `hintdb` + any_of_the_terms : terms (`c`)+ + apply_reduction : eval `redexpr` + fold_expression : fold `c` + + +Actually a few of these are defined in term of the others using a +primitive fixpoint operator: + +.. productionlist:: rewriting + try `s` : choice `s` `id` + any `s` : fix `u`. try (`s` ; `u`) + repeat `s` : `s` ; `any` `s` + bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu + topdown s : fix `td`. (choice s (progress (subterms td))) ; try td + innermost s : fix `i`. (choice (subterm i) s) + outermost s : fix `o`. (choice s (subterm o)) + +The basic control strategy semantics are straightforward: strategies +are applied to subterms of the term to rewrite, starting from the root +of the term. The lemma strategies unify the left-hand-side of the +lemma with the current subterm and on success rewrite it to the right- +hand-side. Composition can be used to continue rewriting on the +current subterm. The fail strategy always fails while the identity +strategy succeeds without making progress. The reflexivity strategy +succeeds, making progress using a reflexivity proof of rewriting. +Progress tests progress of the argument strategy and fails if no +progress was made, while ``try`` always succeeds, catching failures. +Choice is left-biased: it will launch the first strategy and fall back +on the second one in case of failure. One can iterate a strategy at +least 1 time using ``repeat`` and at least 0 times using ``any``. + +The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to +respectively one or all subterms of the current term under +consideration, left-to-right. ``subterm`` stops at the first subterm for +which ``s`` made progress. The composite strategies ``innermost`` and ``outermost`` +perform a single innermost or outermost rewrite using their argument +strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many +rewritings as possible, starting from the bottom or the top of the +term. + +Hint databases created for ``autorewrite`` can also be used +by ``rewrite_strat`` using the ``hints`` strategy that applies any of the +lemmas at the current subterm. The ``terms`` strategy takes the lemma +names directly as arguments. The ``eval`` strategy expects a reduction +expression (see :ref:`performingcomputations`) and succeeds +if it reduces the subterm under consideration. The ``fold`` strategy takes +a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` +on success, it is stronger than the tactic ``fold``. + + +Usage +~~~~~ + + +.. tacv:: rewrite_strat @s [in @ident] + + Rewrite using the strategy s in hypothesis ident or the conclusion. + + .. exn:: Nothing to rewrite. + + If the strategy failed. + + .. exn:: No progress made. + + If the strategy succeeded but made no progress. + + .. exn:: Unable to satisfy the rewriting constraints. + + If the strategy succeeded and made progress but the + corresponding rewriting constraints are not satisfied. + + + The ``setoid_rewrite c`` tactic is basically equivalent to + ``rewrite_strat (outermost c)``. + diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst new file mode 100644 index 0000000000..ec1b942e02 --- /dev/null +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -0,0 +1,469 @@ +.. include:: ../replaces.rst + +.. _implicitcoercions: + +Implicit Coercions +==================== + +:Author: Amokrane Saïbi + +General Presentation +--------------------- + +This section describes the inheritance mechanism of |Coq|. In |Coq| with +inheritance, we are not interested in adding any expressive power to +our theory, but only convenience. Given a term, possibly not typable, +we are interested in the problem of determining if it can be well +typed modulo insertion of appropriate coercions. We allow to write: + + * :g:`f a` where :g:`f:(forall x:A,B)` and :g:`a:A'` when ``A'`` can + be seen in some sense as a subtype of ``A``. + * :g:`x:A` when ``A`` is not a type, but can be seen in + a certain sense as a type: set, group, category etc. + * :g:`f a` when ``f`` is not a function, but can be seen in a certain sense + as a function: bijection, functor, any structure morphism etc. + + +Classes +------- + +A class with `n` parameters is any defined name with a type +:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort. Thus a class with +parameters is considered as a single class and not as a family of +classes. An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`. +In addition to these user-classes, we have two abstract classes: + + + * ``Sortclass``, the class of sorts; its objects are the terms whose type is a + sort (e.g. :g:`Prop` or :g:`Type`). + * ``Funclass``, the class of functions; its objects are all the terms with a functional + type, i.e. of form :g:`forall x:A,B`. + +Formally, the syntax of a classes is defined as: + +.. productionlist:: + class: qualid + : | `Sortclass` + : | `Funclass` + + +Coercions +--------- + +A name ``f`` can be declared as a coercion between a source user-class +``C`` with `n` parameters and a target class ``D`` if one of these +conditions holds: + + * ``D`` is a user-class, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m` + is the number of parameters of ``D``. + * ``D`` is ``Funclass``, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`. + * ``D`` is ``Sortclass``, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), s` with ``s`` a sort. + +We then write :g:`f : C >-> D`. The restriction on the type +of coercions is called *the uniform inheritance condition*. + +.. note:: The abstract classe ``Sortclass`` can be used as a source class, but + the abstract class ``Funclass`` cannot. + +To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to +apply the coercion ``f`` to it; the obtained term :g:`f t₁..tₙ t` is +then an object of ``D``. + + +Identity Coercions +------------------- + +Identity coercions are special cases of coercions used to go around +the uniform inheritance condition. Let ``C`` and ``D`` be two classes +with respectively `n` and `m` parameters and +:g:`f:forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘ` a function which +does not verify the uniform inheritance condition. To declare ``f`` as +coercion, one has first to declare a subclass ``C'`` of ``C``: + + :g:`C' := fun (x₁:T₁)..(xₖ:Tₖ) => C u₁..uₙ` + +We then define an *identity coercion* between ``C'`` and ``C``: + + :g:`Id_C'_C := fun (x₁:T₁)..(xₖ:Tₖ)(y:C' x₁..xₖ) => (y:C u₁..uₙ)` + +We can now declare ``f`` as coercion from ``C'`` to ``D``, since we can +"cast" its type as +:g:`forall (x₁:T₁)..(xₖ:Tₖ)(y:C' x₁..xₖ),D v₁..vₘ`. + +The identity coercions have a special status: to coerce an object +:g:`t:C' t₁..tₖ` +of ``C'`` towards ``C``, we does not have to insert explicitly ``Id_C'_C`` +since :g:`Id_C'_C t₁..tₖ t` is convertible with ``t``. However we +"rewrite" the type of ``t`` to become an object of ``C``; in this case, +it becomes :g:`C uₙ'..uₖ'` where each ``uᵢ'`` is the result of the +substitution in ``uᵢ`` of the variables ``xⱼ`` by ``tⱼ``. + +Inheritance Graph +------------------ + +Coercions form an inheritance graph with classes as nodes. We call +*coercion path* an ordered list of coercions between two nodes of +the graph. A class ``C`` is said to be a subclass of ``D`` if there is a +coercion path in the graph from ``C`` to ``D``; we also say that ``C`` +inherits from ``D``. Our mechanism supports multiple inheritance since a +class may inherit from several classes, contrary to simple inheritance +where a class inherits from at most one class. However there must be +at most one path between two classes. If this is not the case, only +the *oldest* one is valid and the others are ignored. So the order +of declaration of coercions is important. + +We extend notations for coercions to coercion paths. For instance +:g:`[f₁;..;fₖ] : C >-> D` is the coercion path composed +by the coercions ``f₁..fₖ``. The application of a coercion path to a +term consists of the successive application of its coercions. + + +Declaration of Coercions +------------------------- + +.. cmd:: Coercion @qualid : @class >-> @class. + + Declares the construction denoted by `qualid` as a coercion between + the two given classes. + + .. exn:: @qualid not declared + .. exn:: @qualid is already a coercion + .. exn:: Funclass cannot be a source class + .. exn:: @qualid is not a function + .. exn:: Cannot find the source class of @qualid + .. exn:: Cannot recognize @class as a source class of @qualid + .. exn:: @qualid does not respect the uniform inheritance condition + .. exn:: Found target class ... instead of ... + + .. warn:: Ambigous path: + + When the coercion `qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + + .. cmdv:: Local Coercion @qualid : @class >-> @class. + + Declares the construction denoted by `qualid` as a coercion local to + the current section. + + .. cmdv:: Coercion @ident := @term. + + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. + + .. cmdv:: Coercion @ident := @term : @type. + + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. + + .. cmdv:: Local Coercion @ident := @term. + + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. + +Assumptions can be declared as coercions at declaration time. +This extends the grammar of assumptions from +Figure :ref:`vernacular` as follows: + +.. + FIXME: + \comindex{Variable \mbox{\rm (and coercions)}} + \comindex{Axiom \mbox{\rm (and coercions)}} + \comindex{Parameter \mbox{\rm (and coercions)}} + \comindex{Hypothesis \mbox{\rm (and coercions)}} + +.. productionlist:: + assumption : assumption_keyword assums . + assums : simple_assums + : | (simple_assums) ... (simple_assums) + simple_assums : ident ... ident :[>] term + +If the extra ``>`` is present before the type of some assumptions, these +assumptions are declared as coercions. + +Similarly, constructors of inductive types can be declared as coercions at +definition time of the inductive type. This extends and modifies the +grammar of inductive types from Figure :ref:`vernacular` as follows: + +.. + FIXME: + \comindex{Inductive \mbox{\rm (and coercions)}} + \comindex{CoInductive \mbox{\rm (and coercions)}} + +.. productionlist:: + inductive : `Inductive` ind_body `with` ... `with` ind_body + : | `CoInductive` ind_body `with` ... `with` ind_body + ind_body : ident [binders] : term := [[|] constructor | ... | constructor] + constructor : ident [binders] [:[>] term] + +Especially, if the extra ``>`` is present in a constructor +declaration, this constructor is declared as a coercion. + +.. cmd:: Identity Coercion @ident : @class >-> @class. + + If ``C`` is the source `class` and ``D`` the destination, we check + that ``C`` is a constant with a body of the form + :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the + number of parameters of ``D``. Then we define an identity + function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`, + and we declare it as an identity coercion between ``C`` and ``D``. + + .. exn:: @class must be a transparent constant + + .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident. + + Idem but locally to the current section. + + .. cmdv:: SubClass @ident := @type. + + If `type` is a class `ident'` applied to some arguments then + `ident` is defined and an identity coercion of name + `Id_ident_ident'` is + declared. Otherwise said, this is an abbreviation for + + ``Definition`` `ident` ``:=`` `type`. + + ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`. + + .. cmdv:: Local SubClass @ident := @type. + + Same as before but locally to the current section. + + +Displaying Available Coercions +------------------------------- + +.. cmd:: Print Classes. + + Print the list of declared classes in the current context. + +.. cmd:: Print Coercions. + + Print the list of declared coercions in the current context. + +.. cmd:: Print Graph. + + Print the list of valid coercion paths in the current context. + +.. cmd:: Print Coercion Paths @class @class. + + Print the list of valid coercion paths between the two given classes. + +Activating the Printing of Coercions +------------------------------------- + +.. cmd:: Set Printing Coercions. + + This command forces all the coercions to be printed. + Conversely, to skip the printing of coercions, use + ``Unset Printing Coercions``. By default, coercions are not printed. + +.. cmd:: Add Printing Coercion @qualid. + + This command forces coercion denoted by `qualid` to be printed. + To skip the printing of coercion `qualid`, use + ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed. + +.. _coercions-classes-as-records: + +Classes as Records +------------------ + +We allow the definition of *Structures with Inheritance* (or classes as records) +by extending the existing :cmd:`Record` macro. Its new syntax is: + +.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. + + The first identifier `ident` is the name of the defined record and + `sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be ``Build_``\ `ident` if not given). + The other identifiers are the names of the fields, and the `term` + are their respective types. If ``:>`` is used instead of ``:`` in + the declaration of a field, then the name of this field is automatically + declared as a coercion from the record name to the class of this + field type. Remark that the fields always verify the uniform + inheritance condition. If the optional ``>`` is given before the + record name, then the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). + +.. note:: + + The keyword ``Structure`` is a synonym of ``Record``. + +.. + FIXME: \comindex{Structure} + + +Coercions and Sections +---------------------- + +The inheritance mechanism is compatible with the section +mechanism. The global classes and coercions defined inside a section +are redefined after its closing, using their new value and new +type. The classes and coercions which are local to the section are +simply forgotten. +Coercions with a local source class or a local target class, and +coercions which do not verify the uniform inheritance condition any longer +are also forgotten. + +Coercions and Modules +--------------------= + +From |Coq| version 8.3, the coercions present in a module are activated +only when the module is explicitly imported. Formerly, the coercions +were activated as soon as the module was required, whatever it was +imported or not. + +To recover the behavior of the versions of |Coq| prior to 8.3, use the +following command: + +.. cmd:: Set Automatic Coercions Import. + +To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``. + + +Examples +-------- + +There are three situations: + +Coercion at function application +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +:g:`f a` is ill-typed where :g:`f:forall x:A,B` and :g:`a:A'`. If there is a +coercion path between ``A'`` and ``A``, then :g:`f a` is transformed into +:g:`f a'` where ``a'`` is the result of the application of this +coercion path to ``a``. + +We first give an example of coercion between atomic inductive types + +.. coqtop:: all + + Definition bool_in_nat (b:bool) := if b then 0 else 1. + Coercion bool_in_nat : bool >-> nat. + Check (0 = true). + Set Printing Coercions. + Check (0 = true). + Unset Printing Coercions. + + +.. warning:: + + Note that ``Check true=O`` would fail. This is "normal" behaviour of + coercions. To validate ``true=O``, the coercion is searched from + ``nat`` to ``bool``. There is none. + +We give an example of coercion between classes with parameters. + +.. coqtop:: all + + Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set). + Parameter f : forall n:nat, C n -> D (S n) true. + Coercion f : C >-> D. + Parameter g : forall (n:nat) (b:bool), D n b -> E b. + Coercion g : D >-> E. + Parameter c : C 0. + Parameter T : E true -> nat. + Check (T c). + Set Printing Coercions. + Check (T c). + Unset Printing Coercions. + +We give now an example using identity coercions. + +.. coqtop:: all + + Definition D' (b:bool) := D 1 b. + Identity Coercion IdD'D : D' >-> D. + Print IdD'D. + Parameter d' : D' true. + Check (T d'). + Set Printing Coercions. + Check (T d'). + Unset Printing Coercions. + + +In the case of functional arguments, we use the monotonic rule of +sub-typing. Approximatively, to coerce :g:`t:forall x:A,B` towards +:g:`forall x:A',B'`, one have to coerce ``A'`` towards ``A`` and ``B`` +towards ``B'``. An example is given below: + +.. coqtop:: all + + Parameters (A B : Set) (h : A -> B). + Coercion h : A >-> B. + Parameter U : (A -> E true) -> nat. + Parameter t : B -> C 0. + Check (U t). + Set Printing Coercions. + Check (U t). + Unset Printing Coercions. + +Remark the changes in the result following the modification of the +previous example. + +.. coqtop:: all + + Parameter U' : (C 0 -> B) -> nat. + Parameter t' : E true -> A. + Check (U' t'). + Set Printing Coercions. + Check (U' t'). + Unset Printing Coercions. + + +Coercion to a type +~~~~~~~~~~~~~~~~~~ + +An assumption ``x:A`` when ``A`` is not a type, is ill-typed. It is +replaced by ``x:A'`` where ``A'`` is the result of the application to +``A`` of the coercion path between the class of ``A`` and +``Sortclass`` if it exists. This case occurs in the abstraction +:g:`fun x:A => t`, universal quantification :g:`forall x:A,B`, global +variables and parameters of (co-)inductive definitions and +functions. In :g:`forall x:A,B`, such a coercion path may be applied +to ``B`` also if necessary. + +.. coqtop:: all + + Parameter Graph : Type. + Parameter Node : Graph -> Type. + Coercion Node : Graph >-> Sortclass. + Parameter G : Graph. + Parameter Arrows : G -> G -> Type. + Check Arrows. + Parameter fg : G -> G. + Check fg. + Set Printing Coercions. + Check fg. + Unset Printing Coercions. + + +Coercion to a function +~~~~~~~~~~~~~~~~~~~~~~ + +``f a`` is ill-typed because ``f:A`` is not a function. The term +``f`` is replaced by the term obtained by applying to ``f`` the +coercion path between ``A`` and ``Funclass`` if it exists. + +.. coqtop:: all + + Parameter bij : Set -> Set -> Set. + Parameter ap : forall A B:Set, bij A B -> A -> B. + Coercion ap : bij >-> Funclass. + Parameter b : bij nat nat. + Check (b 0). + Set Printing Coercions. + Check (b 0). + Unset Printing Coercions. + +Let us see the resulting graph after all these examples. + +.. coqtop:: all + + Print Graph. diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst new file mode 100644 index 0000000000..80ea8a1166 --- /dev/null +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -0,0 +1,59 @@ +.. include:: ../replaces.rst + +.. _miscellaneousextensions: + +Miscellaneous extensions +======================== + +Program derivation +------------------ + +|Coq| comes with an extension called ``Derive``, which supports program +derivation. Typically in the style of Bird and Meertens or derivations +of program refinements. To use the Derive extension it must first be +required with ``Require Coq.Derive.Derive``. When the extension is loaded, +it provides the following command: + +.. cmd:: Derive @ident SuchThat @term As @ident + +The first `ident` can appear in `term`. This command opens a new proof +presenting the user with a goal for term in which the name `ident` is +bound to an existential variable `?x` (formally, there are other goals +standing for the existential variables but they are shelved, as +described in :tacn:`shelve`). + +When the proof ends two constants are defined: + ++ The first one is named using the first `ident` and is defined as the proof of the + shelved goal (which is also the value of `?x`). It is always + transparent. ++ The second one is named using the second `ident`. It has type `term`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with ``Qed``, and transparent if the proof ends with ``Defined``. + +.. example:: + .. coqtop:: all + + Require Coq.derive.Derive. + Require Import Coq.Numbers.Natural.Peano.NPeano. + + Section P. + + Variables (n m k:nat). + + Derive p SuchThat ((k*n)+(k*m) = p) As h. + Proof. + rewrite <- Nat.mul_add_distr_l. + subst p. + reflexivity. + Qed. + + End P. + + Print p. + Check h. + +Any property can be used as `term`, not only an equation. In particular, +it could be an order relation specifying some form of program +refinement or a non-executable property from which deriving a program +is convenient. diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst new file mode 100644 index 0000000000..387d614956 --- /dev/null +++ b/doc/sphinx/addendum/nsatz.rst @@ -0,0 +1,101 @@ +.. include:: ../preamble.rst + +.. _nsatz: + +Nsatz: tactics for proving equalities in integral domains +=========================================================== + +:Author: Loïc Pottier + +The tactic `nsatz` proves goals of the form + +:math:`\begin{array}{l} +\forall X_1,\ldots,X_n \in A,\\ +P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) , \ldots , P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ +\vdash P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\ +\end{array}` + +where :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is an integral +domain, i.e. a commutative ring with no zero divisor. For example, :math:`A` +can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. +Note that the equality :math:`=` used in these goals can be +any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibnitz equality. + +It also proves formulas + +:math:`\begin{array}{l} +\forall X_1,\ldots,X_n \in A,\\ +P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) \wedge \ldots \wedge P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ +\rightarrow P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\ +\end{array}` + +doing automatic introductions. + + +Using the basic tactic `nsatz` +------------------------------ + + +Load the Nsatz module: + +.. coqtop:: all + + Require Import Nsatz. + +and use the tactic `nsatz`. + +More about `nsatz` +--------------------- + +Hilbert’s Nullstellensatz theorem shows how to reduce proofs of +equalities on polynomials on a commutative ring :math:`A` with no zero divisor +to algebraic computations: it is easy to see that if a polynomial :math:`P` in +:math:`A[X_1,\ldots,X_n]` verifies :math:`c P^r = \sum_{i=1}^{s} S_i P_i`, with +:math:`c \in A`, :math:`c \not = 0`, +:math:`r` a positive integer, and the :math:`S_i` s in :math:`A[X_1,\ldots,X_n ]`, +then :math:`P` is zero whenever polynomials :math:`P_1,\ldots,P_s` are zero +(the converse is also true when :math:`A` is an algebraic closed field: the method is +complete). + +So, proving our initial problem can reduce into finding :math:`S_1,\ldots,S_s`, +:math:`c` and :math:`r` such that :math:`c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)`, +which will be proved by the tactic ring. + +This is achieved by the computation of a Gröbner basis of the ideal +generated by :math:`P_1-Q_1,...,P_s-Q_s`, with an adapted version of the +Buchberger algorithm. + +This computation is done after a step of *reification*, which is +performed using :ref:`typeclasses`. + +The ``Nsatz`` module defines the tactic `nsatz`, which can be used without +arguments, or with the syntax: + +| nsatz with radicalmax:=num%N strategy:=num%Z parameters:= :n:`{* var}` variables:= :n:`{* var}` + +where: + +* `radicalmax` is a bound when for searching r s.t. + :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)` + +* `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy + used in Buchberger algorithm (see :cite:`sugar` for details): + + * strategy = 0: reverse lexicographic order and newest s-polynomial. + * strategy = 1: reverse lexicographic order and sugar strategy. + * strategy = 2: pure lexicographic order and newest s-polynomial. + * strategy = 3: pure lexicographic order and sugar strategy. + +* `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among + :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with + rational fractions in these variables, i.e. polynomials are considered + with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient + :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic + produces a goal which states that :math:`c` is not zero. + +* `variables` is the list of the variables in the decreasing order in + which they will be used in Buchberger algorithm. If `variables` = `(@nil R)`, + then `lvar` is replaced by all the variables which are not in + `parameters`. + +See file `Nsatz.v` for many examples, especially in geometry. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst new file mode 100644 index 0000000000..edb8676a5b --- /dev/null +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -0,0 +1,229 @@ +.. include:: ../replaces.rst + +.. _asynchronousandparallelproofprocessing: + +Asynchronous and Parallel Proof Processing +========================================== + +:Author: Enrico Tassi + +This chapter explains how proofs can be asynchronously processed by +|Coq|. This feature improves the reactivity of the system when used in +interactive mode via |CoqIDE|. In addition, it allows |Coq| to take +advantage of parallel hardware when used as a batch compiler by +decoupling the checking of statements and definitions from the +construction and checking of proofs objects. + +This feature is designed to help dealing with huge libraries of +theorems characterized by long proofs. In the current state, it may +not be beneficial on small sets of short files. + +This feature has some technical limitations that may make it +unsuitable for some use cases. + +For example, in interactive mode, some errors coming from the kernel +of |Coq| are signaled late. The type of errors belonging to this +category are universe inconsistencies. + +At the time of writing, only opaque proofs (ending with ``Qed`` or +``Admitted``) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running |CoqIDE| in +Windows. The current implementation of the feature is not stable on +Windows. It can be enabled, as described below at :ref:`interactive-mode`, +though doing so is not recommended. + +Proof annotations +---------------------- + +To process a proof asynchronously |Coq| needs to know the precise +statement of the theorem without looking at the proof. This requires +some annotations if the theorem is proved inside a Section (see +Section :ref:`section-mechanism`). + +When a section ends, |Coq| looks at the proof object to decide which +section variables are actually used and hence have to be quantified in +the statement of the theorem. To avoid making the construction of +proofs mandatory when ending a section, one can start each proof with +the ``Proof using`` command (Section :ref:`proof-editing-mode`) that +declares which section variables the theorem uses. + +The presence of ``Proof`` using is needed to process proofs asynchronously +in interactive mode. + +It is not strictly mandatory in batch mode if it is not the first time +the file is compiled and if the file itself did not change. When the +proof does not begin with Proof using, the system records in an +auxiliary file, produced along with the `.vo` file, the list of section +variables used. + +Automatic suggestion of proof annotations +````````````````````````````````````````` + +The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +command is processed, a correct proof annotation. It is up to the user +to modify the proof script accordingly. + + +Proof blocks and error resilience +-------------------------------------- + +|Coq| 8.6 introduced a mechanism for error resiliency: in interactive +mode |Coq| is able to completely check a document containing errors +instead of bailing out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular +commands and errors occurring in proofs. + +To properly recover from a failing tactic, |Coq| needs to recognize the +structure of the proof in order to confine the error to a sub proof. +Proof block detection is performed by looking at the syntax of the +proof script (i.e. also looking at indentation). |Coq| comes with four +kind of proof blocks, and an ML API to add new ones. + +:curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling` +:par: blocks are atomic, i.e. just one tactic introduced by the `par:` + goal selector +:indent: blocks end with a tactic indented less than the previous one +:bullet: blocks are delimited by two equal bullet signs at the same + indentation level + +Caveats +```````` + +When a vernacular command fails the subsequent error messages may be +bogus, i.e. caused by the first error. Error resiliency for vernacular +commands can be switched off by passing ``-async-proofs-command-error-resilience off`` +to |CoqIDE|. + +An incorrect proof block detection can result into an incorrect error +recovery and hence in bogus errors. Proof block detection cannot be +precise for bullets or any other non well parenthesized proof +structure. Error resiliency can be turned off or selectively activated +for any set of block kind passing to |CoqIDE| one of the following +options: + +- ``-async-proofs-tactic-error-resilience off`` +- ``-async-proofs-tactic-error-resilience all`` +- ``-async-proofs-tactic-error-resilience`` :n:`{*, blocktype}` + +Valid proof block types are: “curly”, “par”, “indent”, and “bullet”. + +.. _interactive-mode: + +Interactive mode +--------------------- + +At the time of writing the only user interface supporting asynchronous +proof processing is |CoqIDE|. + +When |CoqIDE| is started, two |Coq| processes are created. The master one +follows the user, giving feedback as soon as possible by skipping +proofs, which are delegated to the worker process. The worker process, +whose state can be seen by clicking on the button in the lower right +corner of the main |CoqIDE| window, asynchronously processes the proofs. +If a proof contains an error, it is reported in red in the label of +the very same button, that can also be used to see the list of errors +and jump to the corresponding line. + +If a proof is processed asynchronously the corresponding Qed command +is colored using a lighter color that usual. This signals that the +proof has been delegated to a worker process (or will be processed +lazily if the ``-async-proofs lazy`` option is used). Once finished, the +worker process will provide the proof object, but this will not be +automatically checked by the kernel of the main process. To force the +kernel to check all the proof objects, one has to click the button +with the gears. Only then are all the universe constraints checked. + +Caveats +``````` + +The number of worker processes can be increased by passing |CoqIDE| +the ``-async-proofs-j n`` flag. Note that the memory consumption increases too, +since each worker requires the same amount of memory as the master +process. Also note that increasing the number of workers may reduce +the reactivity of the master process to user commands. + +To disable this feature, one can pass the ``-async-proofs off`` flag to +|CoqIDE|. Conversely, on Windows, where the feature is disabled by +default, pass the ``-async-proofs on`` flag to enable it. + +Proofs that are known to take little time to process are not delegated +to a worker process. The threshold can be configure with +``-async-proofs-delegation-threshold``. Default is 0.03 seconds. + +Batch mode +--------------- + +When |Coq| is used as a batch compiler by running `coqc` or `coqtop` +-compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, +among other things, theorems statements and proofs. Hence to produce a +.vo |Coq| need to process all the proofs of the `.v` file. + +The asynchronous processing of proofs can decouple the generation of a +compiled file (like the `.vo` one) that can be loaded by ``Require`` from the +generation and checking of the proof objects. The ``-quick`` flag can be +passed to `coqc` or `coqtop` to produce, quickly, `.vio` files. +Alternatively, when using a Makefile produced by `coq_makefile`, +the ``quick`` target can be used to compile all files using the ``-quick`` flag. + +A `.vio` file can be loaded using ``Require`` exactly as a `.vo` file but +proofs will not be available (the Print command produces an error). +Moreover, some universe constraints might be missing, so universes +inconsistencies might go unnoticed. A `.vio` file does not contain proof +objects, but proof tasks, i.e. what a worker process can transform +into a proof object. + +Compiling a set of files with the ``-quick`` flag allows one to work, +interactively, on any file without waiting for all the proofs to be +checked. + +When working interactively, one can fully check all the `.v` files by +running `coqc` as usual. + +Alternatively one can turn each `.vio` into the corresponding `.vo`. All +.vio files can be processed in parallel, hence this alternative might +be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +obtain a good scheduling for two workers to produce `a.vo`, `b.vo`, and +`c.vo`. When using a Makefile produced by `coq_makefile`, the ``vio2vo`` target +can be used for that purpose. Variable `J` should be set to the number +of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the +.vo files obtained from `.vio` files are complete (they contain all proof +terms and universe constraints), the satisfiability of all universe +constraints has not been checked globally (they are checked to be +consistent for every single proof). Constraints will be checked when +these `.vo` files are (recursively) loaded with ``Require``. + +There is an extra, possibly even faster, alternative: just check the +proof tasks stored in `.vio` files without producing the `.vo` files. This +is possibly faster because all the proof tasks are independent, hence +one can further partition the job to be done between workers. The +``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +good scheduling for 6 workers to check all the proof tasks of `a.vio`, +`b.vio`, and `c.vio`. Auxiliary files are used to predict how long a proof +task will take, assuming it will take the same amount of time it took +last time. When using a Makefile produced by coq_makefile, the +``checkproofs`` target can be used to check all `.vio` files. Variable `J` +should be set to the number of workers, e.g. ``make checkproofs J=6``. As +when converting `.vio` files to `.vo` files, universe constraints are not +checked to be globally consistent. Hence this compilation mode is only +useful for quick regression testing and on developments not making +heavy use of the `Type` hierarchy. + +Limiting the number of parallel workers +-------------------------------------------- + +Many |Coq| processes may run on the same computer, and each of them may +start many additional worker processes. The `coqworkmgr` utility lets +one limit the number of workers, globally. + +The utility accepts the ``-j`` argument to specify the maximum number of +workers (defaults to 2). `coqworkmgr` automatically starts in the +background and prints an environment variable assignment +like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable +in all the shells from which |Coq| processes will be started. If one +uses just one terminal running the bash shell, then +``export ‘coqworkmgr -j 4‘`` will do the job. + +After that, all |Coq| processes, e.g. `coqide` and `coqc`, will honor the +limit, globally. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst new file mode 100644 index 0000000000..1c3fdeb430 --- /dev/null +++ b/doc/sphinx/addendum/program.rst @@ -0,0 +1,381 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. this should be just "_program", but refs to it don't work + +.. _programs: + +Program +======== + +:Author: Matthieu Sozeau + +We present here the |Program| tactic commands, used to build +certified |Coq| programs, elaborating them from their algorithmic +skeleton and a rich specification :cite:`sozeau06`. It can be thought of as a +dual of :ref:`Extraction <extraction>`. The goal of |Program| is to +program as in a regular functional programming language whilst using +as rich a specification as desired and proving that the code meets the +specification using the whole |Coq| proof apparatus. This is done using +a technique originating from the “Predicate subtyping” mechanism of +PVS :cite:`Rushby98`, which generates type-checking conditions while typing a +term constrained to a particular type. Here we insert existential +variables in the term, which must be filled with proofs to get a +complete |Coq| term. |Program| replaces the |Program| tactic by Catherine +Parent :cite:`Parent95b` which had a similar goal but is no longer maintained. + +The languages available as input are currently restricted to |Coq|’s +term language, but may be extended to OCaml, Haskell and +others in the future. We use the same syntax as |Coq| and permit to use +implicit arguments and the existing coercion mechanism. Input terms +and types are typed in an extended system (Russell) and interpreted +into |Coq| terms. The interpretation process may produce some proof +obligations which need to be resolved to create the final term. + + +.. _elaborating-programs: + +Elaborating programs +--------------------- + +The main difference from |Coq| is that an object in a type T : Set can +be considered as an object of type { x : T | P} for any wellformed P : +Prop. If we go from T to the subset of T verifying property P, we must +prove that the object under consideration verifies it. Russell will +generate an obligation for every such coercion. In the other +direction, Russell will automatically insert a projection. + +Another distinction is the treatment of pattern-matching. Apart from +the following differences, it is equivalent to the standard match +operation (see :ref:`extendedpatternmatching`). + + ++ Generation of equalities. A match expression is always generalized + by the corresponding equality. As an example, the expression: + + :: + + match x with + | 0 => t + | S n => u + end. + + will be first rewritten to: + + :: + + (match x as y return (x = y -> _) with + | 0 => fun H : x = 0 -> t + | S n => fun H : x = S n -> u + end) (eq_refl n). + + This permits to get the proper equalities in the context of proof + obligations inside clauses, without which reasoning is very limited. + ++ Generation of inequalities. If a pattern intersects with a previous + one, an inequality is added in the context of the second branch. See + for example the definition of div2 below, where the second branch is + typed in a context where ∀ p, _ <> S (S p). ++ Coercion. If the object being matched is coercible to an inductive + type, the corresponding coercion will be automatically inserted. This + also works with the previous mechanism. + + +There are options to control the generation of equalities and +coercions. + +.. opt:: Program Cases + + This controls the special treatment of pattern-matching generating equalities + and inequalities when using |Program| (it is on by default). All + pattern-matchings and let-patterns are handled using the standard algorithm + of |Coq| (see :ref:`extendedpatternmatching`) when this option is + deactivated. + +.. opt:: Program Generalized Coercion + + This controls the coercion of general inductive types when using |Program| + (the option is on by default). Coercion of subset types and pairs is still + active in this case. + +.. _syntactic_control: + +Syntactic control over equalities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To give more control over the generation of equalities, the +typechecker will fall back directly to |Coq|’s usual typing of dependent +pattern-matching if a return or in clause is specified. Likewise, the +if construct is not treated specially by |Program| so boolean tests in +the code are not automatically reflected in the obligations. One can +use the dec combinator to get the correct hypotheses as in: + +.. coqtop:: none + + Require Import Program Arith. + +.. coqtop:: all + + Program Definition id (n : nat) : { x : nat | x = n } := + if dec (leb n 0) then 0 + else S (pred n). + +The let tupling construct :g:`let (x1, ..., xn) := t in b` does not +produce an equality, contrary to the let pattern construct :g:`let ’(x1, +..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +coerce term to its support type. It can be useful in notations, for +example: + +.. coqtop:: all + + Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). + +This notation denotes equality on subset types using equality on their +support types, avoiding uses of proof-irrelevance that would come up +when reasoning with equality on the subset types themselves. + +The next two commands are similar to their standard counterparts +:cmd:`Definition` and :cmd:`Fixpoint` +in that they define constants. However, they may require the user to +prove some goals to construct the final definitions. + + +.. _program_definition: + +Program Definition +~~~~~~~~~~~~~~~~~~ + +.. cmd:: Program Definition @ident := @term. + + This command types the value term in Russell and generates proof + obligations. Once solved using the commands shown below, it binds the + final |Coq| term to the name ``ident`` in the environment. + + .. exn:: ident already exists + + .. cmdv:: Program Definition @ident : @type := @term + + It interprets the type ``type``, potentially generating proof + obligations to be resolved. Once done with them, we have a |Coq| + type |type_0|. It then elaborates the preterm ``term`` into a |Coq| + term |term_0|, checking that the type of |term_0| is coercible to + |type_0|, and registers ``ident`` as being of type |type_0| once the + set of obligations generated during the interpretation of |term_0| + and the aforementioned coercion derivation are solved. + + .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... + + + .. cmdv:: Program Definition @ident @binders : @type := @term. + + This is equivalent to: + + :g:`Program Definition ident : forall binders, type := fun binders => term`. + + .. TODO refer to production in alias + +See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` + +.. _program_fixpoint: + +Program Fixpoint +~~~~~~~~~~~~~~~~ + +.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term. + +The optional order annotation follows the grammar: + +.. productionlist:: orderannot + order : measure `term` (`term`)? | wf `term` `term` + ++ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional (parenthesised) term + ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` + to ``lt``. + ++ :g:`wf R x` which is equivalent to :g:`measure x (R)`. + +The structural fixpoint operator behaves just like the one of |Coq| (see +:cmd:`Fixpoint`), except it may also generate obligations. It works +with mutually recursive definitions too. + +.. coqtop:: reset none + + Require Import Program Arith. + +.. coqtop:: all + + Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. + +Here we have one obligation for each branch (branches for :g:`0` and +``(S 0)`` are automatically generated by the pattern-matching +compilation algorithm). + +.. coqtop:: all + + Obligation 1. + +.. coqtop:: reset none + + Require Import Program Arith. + +One can use a well-founded order or a measure as termination orders +using the syntax: + +.. coqtop:: in + + Program Fixpoint div2 (n : nat) {measure n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. + + + +.. caution:: When defining structurally recursive functions, the generated + obligations should have the prototype of the currently defined + functional in their context. In this case, the obligations should be + transparent (e.g. defined using :g:`Defined`) so that the guardedness + condition on recursive calls can be checked by the kernel’s type- + checker. There is an optimization in the generation of obligations + which gets rid of the hypothesis corresponding to the functional when + it is not necessary, so that the obligation can be declared opaque + (e.g. using :g:`Qed`). However, as soon as it appears in the context, the + proof of the obligation is *required* to be declared transparent. + + No such problems arise when using measures or well-founded recursion. + +.. _program_lemma: + +Program Lemma +~~~~~~~~~~~~~ + +.. cmd:: Program Lemma @ident : @type. + + The Russell language can also be used to type statements of logical + properties. It will generate obligations, try to solve them + automatically and fail if some unsolved obligations remain. In this + case, one can first define the lemma’s statement using :g:`Program + Definition` and use it as the goal afterwards. Otherwise the proof + will be started with the elaborated version as a goal. The + :g:`Program` prefix can similarly be used as a prefix for + :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc... + +.. _solving_obligations: + +Solving obligations +-------------------- + +The following commands are available to manipulate obligations. The +optional identifier is used when multiple functions have unsolved +obligations (e.g. when defining mutually recursive blocks). The +optional tactic is replaced by the default one if not specified. + +.. cmd:: {? Local|Global} Obligation Tactic := @tactic + + Sets the default obligation solving tactic applied to all obligations + automatically, whether to solve them or when starting to prove one, + e.g. using :g:`Next`. :g:`Local` makes the setting last only for the current + module. Inside sections, local is the default. + +.. cmd:: Show Obligation Tactic + + Displays the current default tactic. + +.. cmd:: Obligations {? of @ident} + + Displays all remaining obligations. + +.. cmd:: Obligation num {? of @ident} + + Start the proof of obligation num. + +.. cmd:: Next Obligation {? of @ident} + + Start the proof of the next unsolved obligation. + +.. cmd:: Solve Obligations {? of @ident} {? with @tactic} + + Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one. + +.. cmd:: Solve All Obligations {? with @tactic} + + Tries to solve each obligation of every program using the given + tactic or the default one (useful for mutually recursive definitions). + +.. cmd:: Admit Obligations {? of @ident} + + Admits all obligations (of ``ident``). + + .. note:: Does not work with structurally recursive programs. + +.. cmd:: Preterm {? of @ident} + + Shows the term that will be fed to the kernel once the obligations + are solved. Useful for debugging. + +.. opt:: Transparent Obligations + + Control whether all obligations should be declared as transparent + (the default), or if the system should infer which obligations can be + declared opaque. + +.. opt:: Hide Obligations + + Control whether obligations appearing in the + term should be hidden as implicit arguments of the special + constantProgram.Tactics.obligation. + +.. opt:: Shrink Obligations + + *Deprecated since 8.7* + + This option (on by default) controls whether obligations should have + their context minimized to the set of variables used in the proof of + the obligation, to avoid unnecessary dependencies. + +The module :g:`Coq.Program.Tactics` defines the default tactic for solving +obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also +adds some useful notations, as documented in the file itself. + +.. _program-faq: + +Frequently Asked Questions +--------------------------- + + +.. exn:: Ill-formed recursive definition + + This error can happen when one tries to define a function by structural + recursion on a subset object, which means the |Coq| function looks like: + + :: + + Program Fixpoint f (x : A | P) := match x with A b => f b end. + + Supposing ``b : A``, the argument at the recursive call to ``f`` is not a + direct subterm of ``x`` as ``b`` is wrapped inside an ``exist`` constructor to + build an object of type ``{x : A | P}``. Hence the definition is + rejected by the guardedness condition checker. However one can use + wellfounded recursion on subset objects like this: + + :: + + Program Fixpoint f (x : A | P) { measure (size x) } := + match x with A b => f b end. + + One will then just have to prove that the measure decreases at each + recursive call. There are three drawbacks though: + + #. A measure function has to be defined; + #. The reduction is a little more involved, although it works well + using lazy evaluation; + #. Mutual recursion on the underlying inductive type isn’t possible + anymore, but nested mutual recursion is always possible. + +.. bibliography:: ../biblio.bib + :keyprefix: p- diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst new file mode 100644 index 0000000000..ae666a0d45 --- /dev/null +++ b/doc/sphinx/addendum/ring.rst @@ -0,0 +1,770 @@ +.. include:: ../replaces.rst +.. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` +.. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` +.. |eq| replace:: `=`:sub:`(by the main correctness theorem)` +.. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` +.. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` + + +.. _theringandfieldtacticfamilies: + +The ring and field tactic families +==================================== + +:Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_ + +This chapter presents the tactics dedicated to deal with ring and +field equations. + +What does this tactic do? +------------------------------ + +``ring`` does associative-commutative rewriting in ring and semi-ring +structures. Assume you have two binary functions :math:`\oplus` and +:math:`\otimes` that are associative and commutative, with :math:`\oplus` +distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for +:math:`\oplus` and :math:`\otimes`. A polynomial is an expression built on +variables :math:`V_0`, :math:`V_1`, :math:`\dots` and constants by application +of :math:`\oplus` and :math:`\otimes`. + +Let an ordered product be a product of variables :math:`V_{i_1} \otimes \dots +\otimes V_{i_n}` verifying :math:`i_1 ≤ i_2 ≤ \dots ≤ i_n` . Let a monomial be +the product of a constant and an ordered product. We can order the monomials by +the lexicographic order on products of variables. Let a canonical sum be an +ordered sum of monomials that are all different, i.e. each monomial in the sum +is strictly less than the following monomial according to the lexicographic +order. It is an easy theorem to show that every polynomial is equivalent (modulo +the ring properties) to exactly one canonical sum. This canonical sum is called +the normal form of the polynomial. In fact, the actual representation shares +monomials with same prefixes. So what does ring? It normalizes polynomials over +any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring +expressions, so that the user does not have to deal manually with the theorems +of associativity and commutativity. + + +.. example:: + + In the ring of integers, the normal form of + :math:`x (3 + yx + 25(1 − z)) + zx` + is + :math:`28x + (−24)xz + xxy`. + + +``ring`` is also able to compute a normal form modulo monomial equalities. +For example, under the hypothesis that :math:`2x^2 = yz+1`, the normal form of +:math:`2(x + 1)x − x − zy` is :math:`x+1`. + +The variables map +---------------------- + +It is frequent to have an expression built with :math:`+` and :math:`\times`, +but rarely on variables only. Let us associate a number to each subterm of a +ring expression in the Gallina language. For example in the ring |nat|, consider +the expression: + + +:: + + (plus (mult (plus (f (5)) x) x) + (mult (if b then (4) else (f (3))) (2))) + + +As a ring expression, it has 3 subterms. Give each subterm a number in +an arbitrary order: + +===== =============== ========================= +0 :math:`\mapsto` if b then (4) else (f (3)) +1 :math:`\mapsto` (f (5)) +2 :math:`\mapsto` x +===== =============== ========================= + +Then normalize the “abstract” polynomial +:math:`((V_1 \otimes V_2 ) \oplus V_2) \oplus (V_0 \otimes 2)` +In our example the normal form is: +:math:`(2 \otimes V_0 ) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2 )`. +Then substitute the variables by their values in the variables map to +get the concrete normal polynomial: + +:: + + (plus (mult (2) (if b then (4) else (f (3)))) + (plus (mult (f (5)) x) (mult x x))) + + +Is it automatic? +--------------------- + +Yes, building the variables map and doing the substitution after +normalizing is automatically done by the tactic. So you can just +forget this paragraph and use the tactic according to your intuition. + +Concrete usage in Coq +-------------------------- + +.. tacn:: ring + +The ``ring`` tactic solves equations upon polynomial expressions of a ring +(or semi-ring) structure. It proceeds by normalizing both hand sides +of the equation (w.r.t. associativity, commutativity and +distributivity, constant propagation, rewriting of monomials) and +comparing syntactically the results. + +.. tacn:: ring_simplify + +``ring_simplify`` applies the normalization procedure described above to +the terms given. The tactic then replaces all occurrences of the terms +given in the conclusion of the goal by their normal forms. If no term +is given, then the conclusion should be an equation and both hand +sides are normalized. The tactic can also be applied in a hypothesis. + +The tactic must be loaded by ``Require Import Ring``. The ring structures +must be declared with the ``Add Ring`` command (see below). The ring of +booleans is predefined; if one wants to use the tactic on |nat| one must +first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do +``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do +``Require Import NArithRing`` or ``Require Import NArith``. + + +.. example:: + + .. coqtop:: all + + Require Import ZArith. + Open Scope Z_scope. + Goal forall a b c:Z, + (a + b + c) ^ 2 = + a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c. + intros; ring. + Abort. + Goal forall a b:Z, + 2 * a * b = 30 -> (a + b) ^ 2 = a ^ 2 + b ^ 2 + 30. + intros a b H; ring [H]. + Abort. + + +.. tacv:: ring [{* @term }] + +decides the equality of two terms modulo ring operations and +the equalities defined by the :n:`@term`\ s. +Each :n:`@term` has to be a proof of some equality `m = p`, where `m` is a monomial (after “abstraction”), `p` a polynomial and `=` the corresponding equality of the ring structure. + +.. tacv:: ring_simplify [{* @term }] {* @term } in @ident + +performs the simplification in the hypothesis named :n:`@ident`. + + +.. note:: + + .. tacn:: ring_simplify @term1; ring_simplify @term2 + + is not equivalent to + + .. tacn:: ring_simplify @term1 @term2 + + In the latter case the variables map + is shared between the two terms, and common subterm `t` of :n:`@term1` and :n:`@term2` + will have the same associated variable number. So the first + alternative should be avoided for terms belonging to the same ring + theory. + + +Error messages: + + +.. exn:: not a valid ring equation + + The conclusion of the goal is not provable in the corresponding ring theory. + +.. exn:: arguments of ring_simplify do not have all the same type + + ``ring_simplify`` cannot simplify terms of several rings at the same + time. Invoke the tactic once per ring structure. + +.. exn:: cannot find a declared ring structure over @term + + No ring has been declared for the type of the terms to be simplified. + Use ``Add Ring`` first. + +.. exn:: cannot find a declared ring structure for equality @term + + Same as above is the case of the ``ring`` tactic. + + +Adding a ring structure +---------------------------- + +Declaring a new ring consists in proving that a ring signature (a +carrier set, an equality, and ring operations: ``Ring_theory.ring_theory`` +and ``Ring_theory.semi_ring_theory``) satisfies the ring axioms. Semi- +rings (rings without + inverse) are also supported. The equality can +be either Leibniz equality, or any relation declared as a setoid (see +:ref:`tactics-enabled-on-user-provided-relations`). The definition of ring and semi-rings (see module +``Ring_theory``) is: + +.. coqtop:: in + + Record ring_theory : Prop := mk_rt { + Radd_0_l : forall x, 0 + x == x; + Radd_sym : forall x y, x + y == y + x; + Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; + Rmul_1_l : forall x, 1 * x == x; + Rmul_sym : forall x y, x * y == y * x; + Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + Rsub_def : forall x y, x - y == x + -y; + Ropp_def : forall x, x + (- x) == 0 + }. + + Record semi_ring_theory : Prop := mk_srt { + SRadd_0_l : forall n, 0 + n == n; + SRadd_sym : forall n m, n + m == m + n ; + SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; + SRmul_1_l : forall n, 1*n == n; + SRmul_0_l : forall n, 0*n == 0; + SRmul_sym : forall n m, n*m == m*n; + SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; + SRdistr_l : forall n m p, (n + m)*p == n*p + m*p + }. + + +This implementation of ``ring`` also features a notion of constant that +can be parameterized. This can be used to improve the handling of +closed expressions when operations are effective. It consists in +introducing a type of *coefficients* and an implementation of the ring +operations, and a morphism from the coefficient type to the ring +carrier type. The morphism needs not be injective, nor surjective. + +As an example, one can consider the real numbers. The set of +coefficients could be the rational numbers, upon which the ring +operations can be implemented. The fact that there exists a morphism +is defined by the following properties: + +.. coqtop:: in + + Record ring_morph : Prop := mkmorph { + morph0 : [cO] == 0; + morph1 : [cI] == 1; + morph_add : forall x y, [x +! y] == [x]+[y]; + morph_sub : forall x y, [x -! y] == [x]-[y]; + morph_mul : forall x y, [x *! y] == [x]*[y]; + morph_opp : forall x, [-!x] == -[x]; + morph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + + Record semi_morph : Prop := mkRmorph { + Smorph0 : [cO] == 0; + Smorph1 : [cI] == 1; + Smorph_add : forall x y, [x +! y] == [x]+[y]; + Smorph_mul : forall x y, [x *! y] == [x]*[y]; + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + + +where ``c0`` and ``cI`` denote the 0 and 1 of the coefficient set, ``+!``, ``*!``, ``-!`` +are the implementations of the ring operations, ``==`` is the equality of +the coefficients, ``?+!`` is an implementation of this equality, and ``[x]`` +is a notation for the image of ``x`` by the ring morphism. + +Since |Z| is an initial ring (and |N| is an initial semi-ring), it can +always be considered as a set of coefficients. There are basically +three kinds of (semi-)rings: + +abstract rings + to be used when operations are not effective. The set + of coefficients is |Z| (or |N| for semi-rings). + +computational rings + to be used when operations are effective. The + set of coefficients is the ring itself. The user only has to provide + an implementation for the equality. + +customized ring + for other cases. The user has to provide the + coefficient set and the morphism. + + +This implementation of ring can also recognize simple power +expressions as ring expressions. A power function is specified by the +following property: + +.. coqtop:: in + + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) + }. + + End POWER. + + +The syntax for adding a new ring is + +.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}. + +The :n:`@ident` is not relevant. It is just used for error messages. The +:n:`@term` is a proof that the ring signature satisfies the (semi-)ring +axioms. The optional list of modifiers is used to tailor the behavior +of the tactic. The following list describes their syntax and effects: + +.. prodn:: + ring_mod ::= abstract %| decidable @term %| morphism @term + %| setoid @term @term + %| constants [@ltac] + %| preprocess [@ltac] + %| postprocess [@ltac] + %| power_tac @term [@ltac] + %| sign @term + %| div @term + + +abstract + declares the ring as abstract. This is the default. + +decidable :n:`@term` + declares the ring as computational. The expression + :n:`@term` is the correctness proof of an equality test ``?=!`` + (which hould be evaluable). Its type should be of the form + ``forall x y, x ?=! y = true → x == y``. + +morphism :n:`@term` + declares the ring as a customized one. The expression + :n:`@term` is a proof that there exists a morphism between a set of + coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and + ``Ring_theory.semi_morph``). + +setoid :n:`@term` :n:`@term` + forces the use of given setoid. The first + :n:`@term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and + ``Ring_theory.sring_eq_ext``). + This modifier needs not be used if the setoid and morphisms have been + declared. + +constants [:n:`@ltac`] + specifies a tactic expression :n:`@ltac` that, given a + term, returns either an object of the coefficient set that is mapped + to the expression via the morphism, or returns + ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 + to their counterpart in the coefficient set. This is generally not + desirable for non trivial computational rings. + +preprocess [:n:`@ltac`] + specifies a tactic :n:`@ltac` that is applied as a + preliminary step for ``ring`` and ``ring_simplify``. It can be used to + transform a goal so that it is better recognized. For instance, ``S n`` + can be changed to ``plus 1 n``. + +postprocess [:n:`@ltac`] + specifies a tactic :n:`@ltac` that is applied as a final + step for ``ring_simplify``. For instance, it can be used to undo + modifications of the preprocessor. + +power_tac :n:`@term` [:n:`@ltac`] + allows ``ring`` and ``ring_simplify`` to recognize + power expressions with a constant positive integer exponent (example: + ::math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies + the specification of a power function (term has to be a proof of + ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + that, given a term, “abstracts” it into an object of type |N| whose + interpretation via ``Cp_phi`` (the evaluation function of power + coefficient) is the original term, or returns ``InitialRing.NotConstant`` + if not a constant coefficient (i.e. |L_tac| is the inverse function of + ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v`` + and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic + does not recognize power expressions as ring expressions. + +sign :n:`@term` + allows ``ring_simplify`` to use a minus operation when + outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The + term `:n:`@term` is a proof that a given sign function indicates expressions + that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See + ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. + +div :n:`@term` + allows ``ring`` and ``ring_simplify`` to use monomials with + coefficient other than 1 in the rewriting. The term :n:`@term` is a proof + that a given division function satisfies the specification of an + euclidean division function (:n:`@term` has to be a proof of + ``Ring_theory.div_theory``). For example, this function is called when + trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See + ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + +Error messages: + +.. exn:: bad ring structure + + The proof of the ring structure provided is not + of the expected type. + +.. exn:: bad lemma for decidability of equality + + The equality function + provided in the case of a computational ring has not the expected + type. + +.. exn:: ring operation should be declared as a morphism + + A setoid associated to the carrier of the ring structure has been found, + but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`. + +How does it work? +---------------------- + +The code of ring is a good example of tactic written using *reflection*. +What is reflection? Basically, it is writing |Coq| tactics in |Coq|, rather +than in |OCaml|. From the philosophical point of view, it is +using the ability of the Calculus of Constructions to speak and reason +about itself. For the ring tactic we used Coq as a programming +language and also as a proof environment to build a tactic and to +prove it correctness. + +The interested reader is strongly advised to have a look at the +file ``Ring_polynom.v``. Here a type for polynomials is defined: + + +.. coqtop:: in + + Inductive PExpr : Type := + | PEc : C -> PExpr + | PEX : positive -> PExpr + | PEadd : PExpr -> PExpr -> PExpr + | PEsub : PExpr -> PExpr -> PExpr + | PEmul : PExpr -> PExpr -> PExpr + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. + + +Polynomials in normal form are defined as: + + +.. coqtop:: in + + Inductive Pol : Type := + | Pc : C -> Pol + | Pinj : positive -> Pol -> Pol + | PX : Pol -> positive -> Pol -> Pol. + + +where ``Pinj n P`` denotes ``P`` in which :math:`V_i` is replaced by :math:`V_{i+n}` , +and ``PX P n Q`` denotes :math:`P \otimes V_1^n \oplus Q'`, `Q'` being `Q` where :math:`V_i` is replaced by :math:`V_{i+1}`. + +Variables maps are represented by list of ring elements, and two +interpretation functions, one that maps a variables map and a +polynomial to an element of the concrete ring, and the second one that +does the same for normal forms: + + +.. coqtop:: in + + + Definition PEeval : list R -> PExpr -> R := [...]. + Definition Pphi_dev : list R -> Pol -> R := [...]. + + +A function to normalize polynomials is defined, and the big theorem is +its correctness w.r.t interpretation, that is: + + +.. coqtop:: in + + Definition norm : PExpr -> Pol := [...]. + Lemma Pphi_dev_ok : + forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. + + +So now, what is the scheme for a normalization proof? Let p be the +polynomial expression that the user wants to normalize. First a little +piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an +abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|- +equivalent to ``(PEeval`` `v` `ap`\ ``)``. Then we replace it by ``(Pphi_dev`` `v` +``(norm`` `ap`\ ``))``, using the main correctness theorem and we reduce it to a +concrete expression `p’`, which is the concrete normal form of `p`. This is summarized in this diagram: + +========= ====== ==== +`p` |ra| |re| +\ |eq| \ +`p’` |la| |le| +========= ====== ==== + +The user do not see the right part of the diagram. From outside, the +tactic behaves like a |bdi| simplification extended with AC rewriting +rules. Basically, the proof is only the application of the main +correctness theorem to well-chosen arguments. + +Dealing with fields +------------------------ + +.. tacn:: field + +The ``field`` tactic is an extension of the ``ring`` to deal with rational +expression. Given a rational expression :math:`F = 0`. It first reduces the +expression `F` to a common denominator :math:`N/D = 0` where `N` and `D` +are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this +gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve +:math:`N = 0`. +Note that ``field`` also generates non-zero conditions for all the +denominators it encounters in the reduction. In our example, it +generates the condition :math:`x \neq 0`. These conditions appear as one subgoal +which is a conjunction if there are several denominators. Non-zero +conditions are always polynomial expressions. For example when +reducing the expression :math:`1/(1 + 1/x)`, two side conditions are +generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since +a field is an integral domain, and when the equality test on +coefficients is complete w.r.t. the equality of the target field, +constants can be proven different from zero automatically. + +The tactic must be loaded by ``Require Import Field``. New field +structures can be declared to the system with the ``Add Field`` command +(see below). The field of real numbers is defined in module ``RealField`` +(in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so +that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on +real numbers. Rational numbers in canonical form are also declared as +a field in module ``Qcanon``. + + +.. example:: + + .. coqtop:: all + + Require Import Reals. + Open Scope R_scope. + Goal forall x, + x <> 0 -> (1 - 1 / x) * x - x + 1 = 0. + intros; field; auto. + Abort. + Goal forall x y, + y <> 0 -> y = x -> x / y = 1. + intros x y H H1; field [H1]; auto. + Abort. + +.. tacv:: field [{* @term}] + + decides the equality of two terms modulo + field operations and the equalities defined + by the :n:`@term`\ s. Each :n:`@term` has to be a proof of some equality + `m` ``=`` `p`, where `m` is a monomial (after “abstraction”), `p` a polynomial + and ``=`` the corresponding equality of the field structure. + +.. note:: + + rewriting works with the equality `m` ``=`` `p` only if `p` is a polynomial since + rewriting is handled by the underlying ring tactic. + +.. tacv:: field_simplify + + performs the simplification in the conclusion of the + goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step + (the same as the one for rings) is then applied to :math:`N_1`, :math:`D_1`, + :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during the + fraction simplifications. This yields smaller expressions when + reducing to the same denominator since common factors can be canceled. + +.. tacv:: field_simplify [{* @term }] + + performs the simplification in the conclusion of the goal using the equalities + defined by the :n:`@term`\ s. + +.. tacv:: field_simplify [{* @term }] {* @term } + + performs the simplification in the terms :n:`@terms` of the conclusion of the goal + using the equalities defined by :n:`@term`\ s inside the brackets. + +.. tacv :: field_simplify in @ident + + performs the simplification in the assumption :n:`@ident`. + +.. tacv :: field_simplify [{* @term }] in @ident + + performs the simplification + in the assumption :n:`@ident` using the equalities defined by the :n:`@term`\ s. + +.. tacv:: field_simplify [{* @term }] {* @term } in @ident + + performs the simplification in the :n:`@term`\ s of the assumption :n:`@ident` using the + equalities defined by the :n:`@term`\ s inside the brackets. + +.. tacv:: field_simplify_eq + + performs the simplification in the conclusion of + the goal removing the denominator. :math:`F_1 = F_2` becomes :math:`N_1 D_2 = N_2 D_1`. + +.. tacv:: field_simplify_eq [ {* @term }] + + performs the simplification in + the conclusion of the goal using the equalities defined by + :n:`@term`\ s. + +.. tacv:: field_simplify_eq in @ident + + performs the simplification in the assumption :n:`@ident`. + +.. tacv:: field_simplify_eq [{* @term}] in @ident + + performs the simplification in the assumption :n:`@ident` using the equalities defined by + :n:`@terms`\ s and removing the denominator. + + +Adding a new field structure +--------------------------------- + +Declaring a new field consists in proving that a field signature (a +carrier set, an equality, and field operations: +``Field_theory.field_theory`` and ``Field_theory.semi_field_theory``) +satisfies the field axioms. Semi-fields (fields without + inverse) are +also supported. The equality can be either Leibniz equality, or any +relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of +fields and semi-fields is: + +.. coqtop:: in + + Record field_theory : Prop := mk_field { + F_R : ring_theory rO rI radd rmul rsub ropp req; + F_1_neq_0 : ~ 1 == 0; + Fdiv_def : forall p q, p / q == p * / q; + Finv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + + Record semi_field_theory : Prop := mk_sfield { + SF_SR : semi_ring_theory rO rI radd rmul req; + SF_1_neq_0 : ~ 1 == 0; + SFdiv_def : forall p q, p / q == p * / q; + SFinv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + + +The result of the normalization process is a fraction represented by +the following type: + +.. coqtop:: in + + Record linear : Type := mk_linear { + num : PExpr C; + denum : PExpr C; + condition : list (PExpr C) + }. + + +where ``num`` and ``denum`` are the numerator and denominator; ``condition`` is a +list of expressions that have appeared as a denominator during the +normalization process. These expressions must be proven different from +zero for the correctness of the algorithm. + +The syntax for adding a new field is + +.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}. + +The :n:`@ident` is not relevant. It is just used for error +messages. :n:`@term` is a proof that the field signature satisfies the +(semi-)field axioms. The optional list of modifiers is used to tailor +the behavior of the tactic. + +.. prodn:: + field_mod := @ring_mod %| completeness @term + +Since field tactics are built upon ``ring`` +tactics, all modifiers of the ``Add Ring`` apply. There is only one +specific modifier: + +completeness :n:`@term` + allows the field tactic to prove automatically + that the image of non-zero coefficients are mapped to non-zero + elements of the field. :n:`@term` is a proof of + + ``forall x y, [x] == [y] -> x ?=! y = true``, + + which is the completeness of equality on coefficients + w.r.t. the field equality. + + +History of ring +-------------------- + +First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot +of rewriting. But the proofs terms generated by rewriting were too big +for |Coq|’s type-checker. Let us see why: + +.. coqtop:: all + + Require Import ZArith. + Open Scope Z_scope. + Goal forall x y z : Z, + x + 3 + y + y * z = x + 3 + y + z * y. + intros; rewrite (Zmult_comm y z); reflexivity. + Save foo. + Print foo. + +At each step of rewriting, the whole context is duplicated in the +proof term. Then, a tactic that does hundreds of rewriting generates +huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote +it using reflection (see :cite:`Bou97`). Later, it +was rewritten by Patrick Loiseleur: the new tactic does not any +more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not +only to replace the rewriting steps, but also to achieve the +interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote a +few |ML| code for the ``Add Ring`` command, that allow to register new rings +dynamically. + +Proofs terms generated by ring are quite small, they are linear in the +number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking +those terms requires some time because it makes a large use of the +conversion rule, but memory requirements are much smaller. + + +.. _discussion_reflection: + + +Discussion +---------------- + + +Efficiency is not the only motivation to use reflection here. ``ring`` +also deals with constants, it rewrites for example the expression +``34 + 2 * x − x + 12`` to the expected result ``x + 46``. +For the tactic ``ACDSimpl``, the only constants were 0 and 1. +So the expression ``34 + 2 * (x − 1) + 12`` +is interpreted as :math:`V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3`\ , +with the variables mapping +:math:`\{V_0 \mapsto 34; V_1 \mapsto 2; V_2 \mapsto x; V_3 \mapsto 12\}`\ . +Then it is rewritten to ``34 − x + 2 * x + 12``, very far from the expected result. +Here rewriting is not sufficient: you have to do some kind of reduction +(some kind of computation) to achieve the normalization. + +The tactic ``ring`` is not only faster than a classical one: using +reflection, we get for free integration of computation and reasoning +that would be very complex to implement in the classic fashion. + +Is it the ultimate way to write tactics? The answer is: yes and no. +The ``ring`` tactic uses intensively the conversion rule of |Cic|, that is +replaces proof by computation the most as it is possible. It can be +useful in all situations where a classical tactic generates huge proof +terms. Symbolic Processing and Tautologies are in that case. But there +are also tactics like ``auto`` or ``linear`` that do many complex computations, +using side-effects and backtracking, and generate a small proof term. +Clearly, it would be significantly less efficient to replace them by +tactics using reflection. + +Another idea suggested by Benjamin Werner: reflection could be used to +couple an external tool (a rewriting program or a model checker) +with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and +prove a correction theorem that states that *replaying traces* is safe +w.r.t some interpretation. Then we let the external tool do every +computation (using side-effects, backtracking, exception, or others +features that are not available in pure lambda calculus) to produce +the trace: now we can check in |Coq| that the trace has the expected +semantic by applying the correction lemma. + + + + + + +.. rubric:: Footnotes +.. [#f1] based on previous work from Patrick Loiseleur and Samuel Boutin + + + diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index becebb421b..8861cac8af 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -5,9 +5,6 @@ Type Classes ============ -:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html -:Author: Matthieu Sozeau - This chapter presents a quick reference of the commands related to type classes. For an actual introduction to type classes, there is a description of the system :cite:`sozeau08` and the literature on type @@ -151,11 +148,10 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we -provide a new way to introduce variables into section contexts, -compatible with the implicit argument mechanism. The new command works -similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it -accepts any binding context as argument. For example: +To ease the parametrization of developments by type classes, we provide a new +way to introduce variables into section contexts, compatible with the implicit +argument mechanism. The new command works similarly to the :cmd:`Variables` +vernacular, except it accepts any binding context as argument. For example: .. coqtop:: all @@ -336,7 +332,7 @@ Variants: .. cmd:: Program Instance - Switches the type-checking to Program (chapter :ref:`program`) and + Switches the type-checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. .. cmd:: Declare Instance diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst new file mode 100644 index 0000000000..c791fc906b --- /dev/null +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -0,0 +1,445 @@ +.. include:: ../replaces.rst + +.. _polymorphicuniverses: + +Polymorphic Universes +====================== + +:Author: Matthieu Sozeau + +General Presentation +--------------------- + +.. warning:: + + The status of Universe Polymorphism is experimental. + +This section describes the universe polymorphic extension of |Coq|. +Universe polymorphism makes it possible to write generic definitions +making use of universes and reuse them at different and sometimes +incompatible universe levels. + +A standard example of the difference between universe *polymorphic* +and *monomorphic* definitions is given by the identity function: + +.. coqtop:: in + + Definition identity {A : Type} (a : A) := a. + +By default, constant declarations are monomorphic, hence the identity +function declares a global universe (say ``Top.1``) for its domain. +Subsequently, if we try to self-apply the identity, we will get an +error: + +.. coqtop:: all + + Fail Definition selfid := identity (@identity). + +Indeed, the global level ``Top.1`` would have to be strictly smaller than +itself for this self-application to typecheck, as the type of +:g:`(@identity)` is :g:`forall (A : Type@{Top.1}), A -> A` whose type is itself +:g:`Type@{Top.1+1}`. + +A universe polymorphic identity function binds its domain universe +level at the definition level instead of making it global. + +.. coqtop:: in + + Polymorphic Definition pidentity {A : Type} (a : A) := a. + +.. coqtop:: all + + About pidentity. + +It is then possible to reuse the constant at different levels, like +so: + +.. coqtop:: in + + Definition selfpid := pidentity (@pidentity). + +Of course, the two instances of :g:`pidentity` in this definition are +different. This can be seen when the :opt:`Printing Universes` option is on: + +.. coqtop:: none + + Set Printing Universes. + +.. coqtop:: all + + Print selfpid. + +Now :g:`pidentity` is used at two different levels: at the head of the +application it is instantiated at ``Top.3`` while in the argument position +it is instantiated at ``Top.4``. This definition is only valid as long as +``Top.4`` is strictly smaller than ``Top.3``, as show by the constraints. Note +that this definition is monomorphic (not universe polymorphic), so the +two universes (in this case ``Top.3`` and ``Top.4``) are actually global +levels. + +When printing :g:`pidentity`, we can see the universes it binds in +the annotation :g:`@{Top.2}`. Additionally, when +:g:`Set Printing Universes` is on we print the "universe context" of +:g:`pidentity` consisting of the bound universes and the +constraints they must verify (for :g:`pidentity` there are no constraints). + +Inductive types can also be declared universes polymorphic on +universes appearing in their parameters or fields. A typical example +is given by monoids: + +.. coqtop:: in + + Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car; + mon_op : mon_car -> mon_car -> mon_car }. + +.. coqtop:: in + + Print Monoid. + +The Monoid's carrier universe is polymorphic, hence it is possible to +instantiate it for example with :g:`Monoid` itself. First we build the +trivial unit monoid in :g:`Set`: + +.. coqtop:: in + + Definition unit_monoid : Monoid := + {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. + +From this we can build a definition for the monoid of :g:`Set`\-monoids +(where multiplication would be given by the product of monoids). + +.. coqtop:: in + + Polymorphic Definition monoid_monoid : Monoid. + refine (@Build_Monoid Monoid unit_monoid (fun x y => x)). + Defined. + +.. coqtop:: all + + Print monoid_monoid. + +As one can see from the constraints, this monoid is “large”, it lives +in a universe strictly higher than :g:`Set`. + +Polymorphic, Monomorphic +------------------------- + +.. cmd:: Polymorphic @definition + + As shown in the examples, polymorphic definitions and inductives can be + declared using the ``Polymorphic`` prefix. + +.. opt:: Universe Polymorphism + + Once enabled, this option will implicitly prepend ``Polymorphic`` to any + definition of the user. + +.. cmd:: Monomorphic @definition + + When the :opt:`Universe Polymorphism` option is set, to make a definition + producing global universe constraints, one can use the ``Monomorphic`` prefix. + +Many other commands support the ``Polymorphic`` flag, including: + +.. TODO add links on each of these? + +- ``Lemma``, ``Axiom``, and all the other “definition” keywords support + polymorphism. + +- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support + polymorphism. This means that the universe variables (and associated + constraints) are discharged polymorphically over definitions that use + them. In other words, two definitions in the section sharing a common + variable will both get parameterized by the universes produced by the + variable declaration. This is in contrast to a “mononorphic” variable + which introduces global universes and constraints, making the two + definitions depend on the *same* global universes associated to the + variable. + +- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint + polymorphically, not at a single instance. + +Cumulative, NonCumulative +------------------------- + +Polymorphic inductive types, coinductive types, variants and records can be +declared cumulative using the :g:`Cumulative` prefix. + +.. cmd:: Cumulative @inductive + + Declares the inductive as cumulative + +Alternatively, there is an option :g:`Set Polymorphic Inductive +Cumulativity` which when set, makes all subsequent *polymorphic* +inductive definitions cumulative. When set, inductive types and the +like can be enforced to be non-cumulative using the :g:`NonCumulative` +prefix. + +.. cmd:: NonCumulative @inductive + + Declares the inductive as non-cumulative + +.. opt:: Polymorphic Inductive Cumulativity + + When this option is on, it sets all following polymorphic inductive + types as cumulative (it is off by default). + +Consider the examples below. + +.. coqtop:: in + + Polymorphic Cumulative Inductive list {A : Type} := + | nil : list + | cons : A -> list -> list. + +.. coqtop:: all + + Print list. + +When printing :g:`list`, the universe context indicates the subtyping +constraints by prefixing the level names with symbols. + +Because inductive subtypings are only produced by comparing inductives +to themselves with universes changed, they amount to variance +information: each universe is either invariant, covariant or +irrelevant (there are no contravariant subtypings in Coq), +respectively represented by the symbols `=`, `+` and `*`. + +Here we see that :g:`list` binds an irrelevant universe, so any two +instances of :g:`list` are convertible: :math:`E[Γ] ⊢ \mathsf{list}@\{i\}~A +=_{βδιζη} \mathsf{list}@\{j\}~B` whenever :math:`E[Γ] ⊢ A =_{βδιζη} B` and +this applies also to their corresponding constructors, when +they are comparable at the same type. + +See :ref:`Conversion-rules` for more details on convertibility and subtyping. +The following is an example of a record with non-trivial subtyping relation: + +.. coqtop:: all + + Polymorphic Cumulative Record packType := {pk : Type}. + +:g:`packType` binds a covariant universe, i.e. + +.. math:: + + E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} + \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j + +Cumulative inductive types, coninductive types, variants and records +only make sense when they are universe polymorphic. Therefore, an +error is issued whenever the user uses the :g:`Cumulative` or +:g:`NonCumulative` prefix in a monomorphic context. +Notice that this is not the case for the option :g:`Set Polymorphic Inductive Cumulativity`. +That is, this option, when set, makes all subsequent *polymorphic* +inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) +but has no effect on *monomorphic* inductive declarations. + +Consider the following examples. + +.. coqtop:: all reset + + Monomorphic Cumulative Inductive Unit := unit. + +.. coqtop:: all reset + + Monomorphic NonCumulative Inductive Unit := unit. + +.. coqtop:: all reset + + Set Polymorphic Inductive Cumulativity. + Inductive Unit := unit. + +An example of a proof using cumulativity +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. coqtop:: in + + Set Universe Polymorphism. + Set Polymorphic Inductive Cumulativity. + + Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + + Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + + Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B. + Proof. + exact H. + Defined. + End down. + +Cumulativity Weak Constraints +----------------------------- + +.. opt:: Cumulativity Weak Constraints + +This option, on by default, causes "weak" constraints to be produced +when comparing universes in an irrelevant position. Processing weak +constraints is delayed until minimization time. A weak constraint +between `u` and `v` when neither is smaller than the other and +one is flexible causes them to be unified. Otherwise the constraint is +silently discarded. + +This heuristic is experimental and may change in future versions. +Disabling weak constraints is more predictable but may produce +arbitrary numbers of universes. + + +Global and local universes +--------------------------- + +Each universe is declared in a global or local environment before it +can be used. To ensure compatibility, every *global* universe is set +to be strictly greater than :g:`Set` when it is introduced, while every +*local* (i.e. polymorphically quantified) universe is introduced as +greater or equal to :g:`Set`. + + +Conversion and unification +--------------------------- + +The semantics of conversion and unification have to be modified a +little to account for the new universe instance arguments to +polymorphic references. The semantics respect the fact that +definitions are transparent, so indistinguishable from their bodies +during conversion. + +This is accomplished by changing one rule of unification, the first- +order approximation rule, which applies when two applicative terms +with the same head are compared. It tries to short-cut unfolding by +comparing the arguments directly. In case the constant is universe +polymorphic, we allow this rule to fire only when unifying the +universes results in instantiating a so-called flexible universe +variables (not given by the user). Similarly for conversion, if such +an equation of applicative terms fail due to a universe comparison not +being satisfied, the terms are unfolded. This change implies that +conversion and unification can have different unfolding behaviors on +the same development with universe polymorphism switched on or off. + + +Minimization +------------- + +Universe polymorphism with cumulativity tends to generate many useless +inclusion constraints in general. Typically at each application of a +polymorphic constant :g:`f`, if an argument has expected type :g:`Type@{i}` +and is given a term of type :g:`Type@{j}`, a :math:`j ≤ i` constraint will be +generated. It is however often the case that an equation :math:`j = i` would +be more appropriate, when :g:`f`\'s universes are fresh for example. +Consider the following example: + +.. coqtop:: none + + Polymorphic Definition pidentity {A : Type} (a : A) := a. + Set Printing Universes. + +.. coqtop:: in + + Definition id0 := @pidentity nat 0. + +.. coqtop:: all + + Print id0. + +This definition is elaborated by minimizing the universe of :g:`id0` to +level :g:`Set` while the more general definition would keep the fresh level +:g:`i` generated at the application of :g:`id` and a constraint that :g:`Set` :math:`≤ i`. +This minimization process is applied only to fresh universe variables. +It simply adds an equation between the variable and its lower bound if +it is an atomic universe (i.e. not an algebraic max() universe). + +.. opt:: Universe Minimization ToSet + + Turning this option off (it is on by default) disallows minimization + to the sort :g:`Set` and only collapses floating universes between + themselves. + + +Explicit Universes +------------------- + +The syntax has been extended to allow users to explicitly bind names +to universes and explicitly instantiate polymorphic definitions. + +.. cmd:: Universe @ident. + + In the monorphic case, this command declares a new global universe + named :g:`ident`, which can be referred to using its qualified name + as well. Global universe names live in a separate namespace. The + command supports the polymorphic flag only in sections, meaning the + universe quantification will be discharged on each section definition + independently. One cannot mix polymorphic and monomorphic + declarations in the same section. + + +.. cmd:: Constraint @ident @ord @ident. + + This command declares a new constraint between named universes. The + order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint + is then enforced in the global environment. Like ``Universe``, it can be + used with the ``Polymorphic`` prefix in sections only to declare + constraints discharged at section closing time. One cannot declare a + global constraint on polymorphic universes. + + .. exn:: Undeclared universe @ident. + + .. exn:: Universe inconsistency. + + +Polymorphic definitions +~~~~~~~~~~~~~~~~~~~~~~~ + +For polymorphic definitions, the declaration of (all) universe levels +introduced by a definition uses the following syntax: + +.. coqtop:: in + + Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. + +.. coqtop:: all + + Print le. + +During refinement we find that :g:`j` must be larger or equal than :g:`i`, as we +are using :g:`A : Type@{i} <= Type@{j}`, hence the generated constraint. At the +end of a definition or proof, we check that the only remaining +universes are the ones declared. In the term and in general in proof +mode, introduced universe names can be referred to in terms. Note that +local universe names shadow global universe names. During a proof, one +can use :ref:`Show Universes <ShowUniverses>` to display the current context of universes. + +Definitions can also be instantiated explicitly, giving their full +instance: + +.. coqtop:: all + + Check (pidentity@{Set}). + Monomorphic Universes k l. + Check (le@{k l}). + +User-named universes and the anonymous universe implicitly attached to +an explicit :g:`Type` are considered rigid for unification and are never +minimized. Flexible anonymous universes can be produced with an +underscore or by omitting the annotation to a polymorphic definition. + +.. coqtop:: all + + Check (fun x => x) : Type -> Type. + Check (fun x => x) : Type -> Type@{_}. + + Check le@{k _}. + Check le. + +.. opt:: Strict Universe Declaration. + + The command ``Unset Strict Universe Declaration`` allows one to freely use + identifiers for universes without declaring them first, with the + semantics that the first use declares it. In this mode, the universe + names are not associated with the definition or proof once it has been + defined. This is meant mainly for debugging purposes. |