diff options
Diffstat (limited to 'doc/sphinx')
27 files changed, 1187 insertions, 688 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index e4f078c1d6..881f7a310d 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -214,17 +214,17 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Example:: - .. coqtop:: in reset undo + .. coqtop:: in reset Print nat. Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -234,8 +234,10 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after - running all the commands in this block + - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both) + - ``warn``: Don't die if a command emits a warning + - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) + - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per @@ -509,7 +511,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -519,7 +521,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 81f25bf274..78803a927f 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -265,7 +265,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -275,7 +275,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. coqtop:: all +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 7b8a86d1ab..3ec6c118af 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -59,7 +59,7 @@ pattern matching. Consider for example the function that computes the maximum of two natural numbers. We can write it in primitive syntax by: -.. coqtop:: in undo +.. coqtop:: in Fixpoint max (n m:nat) {struct m} : nat := match n with @@ -75,7 +75,7 @@ Multiple patterns Using multiple patterns in the definition of ``max`` lets us write: -.. coqtop:: in undo +.. coqtop:: in reset Fixpoint max (n m:nat) {struct m} : nat := match n, m with @@ -103,7 +103,7 @@ Aliasing subpatterns We can also use :n:`as @ident` to associate a name to a sub-pattern: -.. coqtop:: in undo +.. coqtop:: in reset Fixpoint max (n m:nat) {struct n} : nat := match n, m with @@ -128,18 +128,22 @@ Here is now an example of nested patterns: This is compiled into: -.. coqtop:: all undo +.. coqtop:: all Unset Printing Matching. Print even. +.. coqtop:: none + + Set Printing Matching. + In the previous examples patterns do not conflict with, but sometimes it is comfortable to write patterns that admit a non trivial superposition. Consider the boolean function :g:`lef` that given two natural numbers yields :g:`true` if the first one is less or equal than the second one and :g:`false` otherwise. We can write it as follows: -.. coqtop:: in undo +.. coqtop:: in Fixpoint lef (n m:nat) {struct m} : bool := match n, m with @@ -158,7 +162,7 @@ is matched by the first pattern, and so :g:`(lef O O)` yields true. Another way to write this function is: -.. coqtop:: in +.. coqtop:: in reset Fixpoint lef (n m:nat) {struct m} : bool := match n, m with @@ -191,7 +195,7 @@ Multiple patterns that share the same right-hand-side can be factorized using the notation :n:`{+| @mult_pattern}`. For instance, :g:`max` can be rewritten as follows: -.. coqtop:: in undo +.. coqtop:: in reset Fixpoint max (n m:nat) {struct m} : nat := match n, m with @@ -269,7 +273,7 @@ When we use parameters in patterns there is an error message: Set Asymmetric Patterns. Check (fun l:List nat => match l with - | nil => nil + | nil => nil _ | cons _ l' => l' end). Unset Asymmetric Patterns. @@ -291,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write: end). But the possibility to use all the arguments is given by “``@``” implicit -explicitations (as for terms 2.7.11). +explicitations (as for terms, see :ref:`explicit-applications`). .. coqtop:: all @@ -325,7 +329,7 @@ Understanding dependencies in patterns We can define the function length over :g:`listn` by: -.. coqtop:: in +.. coqdoc:: Definition length (n:nat) (l:listn n) := n. @@ -367,6 +371,10 @@ different types and we need to provide the elimination predicate: | consn n' a y => consn (n' + m) a (concat n' y m l') end. +.. coqtop:: none + + Reset concat. + The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`. In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr` are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`. @@ -503,7 +511,7 @@ can also be caught in the matching. .. example:: - .. coqtop:: in + .. coqtop:: in reset Inductive list : nat -> Set := | nil : list 0 diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b606fb4dd2..b474c51f17 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -121,7 +121,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. morphism parametric over ``A`` that respects the relation instance ``(set_eq A)``. The latter condition is proved by showing: - .. coqtop:: in + .. coqdoc:: forall (A: Type) (S1 S1' S2 S2': list A), set_eq A S1 S1' -> @@ -205,7 +205,7 @@ Adding new relations and morphisms For Leibniz equality, we may declare: - .. coqtop:: in + .. coqdoc:: Add Parametric Relation (A : Type) : A (@eq A) [reflexivity proved by @refl_equal A] @@ -274,7 +274,7 @@ following command. (maximally inserted) implicit arguments. If ``A`` is always set as maximally implicit in the previous example, one can write: - .. coqtop:: in + .. coqdoc:: Add Parametric Relation A : (set A) eq_set reflexivity proved by eq_set_refl @@ -282,13 +282,8 @@ following command. 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 @@ -300,7 +295,7 @@ following command. .. coqtop:: in Goal forall (S : set nat), - eq_set (union (union S empty) S) (union S S). + eq_set (union (union S (empty nat)) S) (union S S). .. coqtop:: in @@ -486,7 +481,7 @@ registered as parametric relations and morphisms. .. example:: First class setoids - .. coqtop:: in + .. coqtop:: in reset Require Import Relation_Definitions Setoid. @@ -623,12 +618,16 @@ declared as morphisms in the ``Classes.Morphisms_Prop`` module. For example, to declare that universal quantification is a morphism for logical equivalence: +.. coqtop:: none + + Require Import Morphisms. + .. coqtop:: in Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all +.. coqtop:: all abort Proof. simpl_relation. @@ -650,7 +649,7 @@ functional arguments (or whatever subrelation of the pointwise extension). For example, one could declare the ``map`` combinator on lists as a morphism: -.. coqtop:: in +.. coqdoc:: Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index e5b41be691..d15aacad44 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,7 +37,7 @@ In addition to these user-defined classes, we have two built-in classes: * ``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: +Formally, the syntax of classes is defined as: .. productionlist:: class: `qualid` @@ -289,7 +289,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be :n:`Build_@ident` if not given). + of the constructor (it will be :n:`Build_@ident` if not given). The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically @@ -365,7 +365,7 @@ We first give an example of coercion between atomic inductive types .. warning:: - Note that ``Check true=O`` would fail. This is "normal" behavior of + Note that ``Check (true = O)`` would fail. This is "normal" behavior of coercions. To validate ``true=O``, the coercion is searched from ``nat`` to ``bool``. There is none. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index b076aac1ed..e56b36caad 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -124,7 +124,7 @@ and checked to be :math:`-1`. that :tacn:`omega` does not solve, such as the following so-called *omega nightmare* :cite:`TheOmegaPaper`. -.. coqtop:: in +.. coqdoc:: Goal forall x y, 27 <= 11 * x + 13 * y <= 45 -> @@ -234,7 +234,8 @@ proof by abstracting monomials by variables. To illustrate the working of the tactic, consider we wish to prove the following Coq goal: -.. coqtop:: all +.. needs csdp +.. coqdoc:: Require Import ZArith Psatz. Open Scope Z_scope. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 8204d93fa7..20e4c6a3d6 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -197,7 +197,7 @@ be either Leibniz equality, or any relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definitions of ring and semiring (see module ``Ring_theory``) are: -.. coqtop:: in +.. coqdoc:: Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; @@ -235,7 +235,7 @@ 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 +.. coqdoc:: Record ring_morph : Prop := mkmorph { morph0 : [cO] == 0; @@ -285,13 +285,14 @@ following property: .. coqtop:: in + Require Import Reals. 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) + rpow_pow_N : forall r n, rpow r (Cp_phi n) = pow_N 1%R Rmult r n }. End POWER. @@ -422,7 +423,7 @@ 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 +.. coqdoc:: Inductive PExpr : Type := | PEc : C -> PExpr @@ -437,7 +438,7 @@ file ``Ring_polynom.v``. Here a type for polynomials is defined: Polynomials in normal form are defined as: -.. coqtop:: in +.. coqdoc:: Inductive Pol : Type := | Pc : C -> Pol @@ -454,7 +455,7 @@ polynomial to an element of the concrete ring, and the second one that does the same for normal forms: -.. coqtop:: in +.. coqdoc:: Definition PEeval : list R -> PExpr -> R := [...]. @@ -465,7 +466,7 @@ A function to normalize polynomials is defined, and the big theorem is its correctness w.r.t interpretation, that is: -.. coqtop:: in +.. coqdoc:: Definition norm : PExpr -> Pol := [...]. Lemma Pphi_dev_ok : @@ -616,7 +617,7 @@ 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 semifields is: -.. coqtop:: in +.. coqdoc:: Record field_theory : Prop := mk_field { F_R : ring_theory rO rI radd rmul rsub ropp req; @@ -636,7 +637,7 @@ fields and semifields is: The result of the normalization process is a fraction represented by the following type: -.. coqtop:: in +.. coqdoc:: Record linear : Type := mk_linear { num : PExpr C; @@ -690,7 +691,7 @@ for |Coq|’s type checker. Let us see why: x + 3 + y + y * z = x + 3 + y + z * y. intros; rewrite (Zmult_comm y z); reflexivity. Save foo. - Print 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 diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 43d302114e..c7ea7e326f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is: eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end }. -If one does not give all the members in the Instance declaration, Coq -enters the proof-mode and the user is asked to build inhabitants of -the remaining fields, e.g.: +Using :cmd:`Program Instance`, if one does not give all the members in +the Instance declaration, Coq generates obligations for the remaining +fields, e.g.: .. coqtop:: in - Instance eq_bool : EqDec bool := + Require Import Program.Tactics. + Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }. .. coqtop:: all - Proof. intros x y H. - -.. coqtop:: all - - destruct x ; destruct y ; (discriminate || reflexivity). - -.. coqtop:: all - + Next Obligation. + destruct x ; destruct y ; (discriminate || reflexivity). Defined. One has to take care that the transparency of every field is @@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.: .. coqtop:: in - Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := + Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) end }. .. coqtop:: none - Abort. + Admit Obligations. These instances are used just as well as lemmas in the instance hint database. @@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example: Context `{EA : EqDec A}. - Global Instance option_eqb : EqDec (option A) := + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }. - Admitted. + Admit Obligations. End EqDec_defs. @@ -564,12 +559,12 @@ Settings This flag allows to switch the behavior of instance declarations made through the Instance command. - + When it is on (the default), instances that have unsolved holes in + + When it is off (the default), they fail with an error instead. + + + When it is on, instances that have unsolved holes in their proof-term silently open the proof mode with the remaining obligations to prove. - + When it is off, they fail with an error instead. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 04aedd0cf6..6b10b7c0b3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -223,7 +223,7 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -Cumulative inductive types, coninductive types, variants and records +Cumulative inductive types, coinductive 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. @@ -236,11 +236,11 @@ Consider the following examples. .. coqtop:: all reset - Monomorphic Cumulative Inductive Unit := unit. + Fail Monomorphic Cumulative Inductive Unit := unit. .. coqtop:: all reset - Monomorphic NonCumulative Inductive Unit := unit. + Fail Monomorphic NonCumulative Inductive Unit := unit. .. coqtop:: all reset diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index d9eaa2c6c6..0467852b19 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -45,6 +45,58 @@ s}, year = {1972} } +@inproceedings{CH85, + title={Constructions: a higher order proof system for mechanizing mathematics}, + author={Coquand, Thierry and Huet, Gérard}, + booktitle={European Conference on Computer Algebra}, + pages={151--184}, + year={1985}, + issn = {1611-3349}, + doi = {10.1007/3-540-15983-5_13}, + url = {http://dx.doi.org/10.1007/3-540-15983-5_13}, + isbn = 9783540396840, + publisher = {Springer Berlin Heidelberg} +} + +@techreport{CH88 + TITLE = {{The calculus of constructions}}, + AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, + URL = {https://hal.inria.fr/inria-00076024}, + NUMBER = {RR-0530}, + INSTITUTION = {{INRIA}}, + YEAR = {1986}, + MONTH = May, + PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf}, + HAL_ID = {inria-00076024}, + HAL_VERSION = {v1}, +} + +@techreport{CH87, + TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}}, + AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, + URL = {https://hal.inria.fr/inria-00076039}, + NUMBER = {RR-0515}, + INSTITUTION = {{INRIA}}, + YEAR = {1986}, + MONTH = Apr, + PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf}, + HAL_ID = {inria-00076039}, + HAL_VERSION = {v1}, +} + +@techreport{C90, + TITLE = {{Metamathematical investigations of a calculus of constructions}}, + AUTHOR = {Coquand, T.}, + URL = {https://hal.inria.fr/inria-00075471}, + NUMBER = {RR-1088}, + INSTITUTION = {{INRIA}}, + YEAR = {1989}, + MONTH = Sep, + PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf}, + HAL_ID = {inria-00075471}, + HAL_VERSION = {v1}, +} + @PhDThesis{Coq85, author = {Th. Coquand}, month = jan, @@ -80,6 +132,19 @@ s}, bibsource = {DBLP, http://dblp.uni-trier.de} } +@inproceedings{CP90, + title={Inductively defined types}, + author={Coquand, Thierry and Paulin, Christine}, + booktitle={COLOG-88}, + pages={50--66}, + year={1990}, + issn = {1611-3349}, + doi = {10.1007/3-540-52335-9_47}, + url = {http://dx.doi.org/10.1007/3-540-52335-9_47}, + isbn = 9783540469636, + publisher = {Springer Berlin Heidelberg} +} + @Book{Cur58, author = {Haskell B. Curry and Robert Feys and William Craig}, title = {Combinatory Logic}, @@ -216,7 +281,19 @@ s}, year = {1980} } -@InProceedings{Hue88, +@inproceedings{H88, + title={Induction principles formalized in the Calculus of Constructions}, + author={Huet, G{\'e}rard}, + booktitle={Programming of Future Generation Computers. Elsevier Science}, + year={1988}, + issn = {1611-3349}, + doi = {10.1007/3-540-17660-8_62}, + url = {http://dx.doi.org/10.1007/3-540-17660-8_62}, + isbn = 9783540477464, + publisher = {Springer Berlin Heidelberg} +} + +@InProceedings{H89, author = {G. Huet}, booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, editor = {R. Narasimhan}, @@ -305,6 +382,50 @@ s}, url = {http://www.xmailserver.org/diff2.pdf} } +@inproceedings{P86, + title={Algorithm development in the calculus of constructions}, + author={Mohring, Christine}, + booktitle={LICS}, + pages={84--91}, + year={1986} +} + +@inproceedings{P89, + title={Extracting $\Omega$'s programs from proofs in the calculus of constructions}, + author={Paulin-Mohring, Christine}, + booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + pages={89--104}, + year={1989}, + doi = {10.1145/75277.75285}, + url = {http://dx.doi.org/10.1145/75277.75285}, + isbn = 0897912942, + organization = {ACM Press} +} + +@inproceedings{P93, + title={Inductive definitions in the system coq rules and properties}, + author={Paulin-Mohring, Christine}, + booktitle={International Conference on Typed Lambda Calculi and Applications}, + pages={328--345}, + year={1993}, + doi = {10.1007/bfb0037116}, + url = {http://dx.doi.org/10.1007/bfb0037116}, + isbn = 3540565175, + organization = {Springer-Verlag} +} + +@inproceedings{PP90, + title={Inductively defined types in the Calculus of Constructions}, + author={Pfenning, Frank and Paulin-Mohring, Christine}, + booktitle={International Conference on Mathematical Foundations of Programming Semantics}, + pages={209--228}, + year={1989}, + doi = {10.1007/bfb0040259}, + url = {http://dx.doi.org/10.1007/bfb0040259}, + isbn = 0387973753, + organization = {Springer-Verlag} +} + @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 39047f4f23..48ad60c6dd 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -28,7 +28,7 @@ from shutil import copyfile import sphinx # Increase recursion limit for sphinx -sys.setrecursionlimit(1500) +sys.setrecursionlimit(3000) # If extensions (or modules to document with autodoc) are in another directory, # add these directories to sys.path here. If the directory is relative to the @@ -142,6 +142,7 @@ exclude_patterns = [ 'introduction.rst', 'refman-preamble.rst', 'README.rst', + 'README.gen.rst', 'README.template.rst' ] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS] diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 909af6e2f2..5873096523 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -2,10 +2,13 @@ Credits ------- +Historical roots +---------------- + Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal -specification. It is the result of about ten years of research of the -Coq project. We shall briefly survey here three main aspects: the +specification. It is the result of about ten years [#years]_ of research +of the Coq project. We shall briefly survey here three main aspects: the *logical language* in which we write our axiomatizations and specifications, the *proof assistant* which allows the development of verified mathematical proofs, and the *program extractor* which @@ -21,8 +24,8 @@ prompted Russell to restrict predicate calculus with a stratification of *types*. This effort culminated with *Principia Mathematica*, the first systematic attempt at a formal foundation of mathematics. A simplification of this system along the lines of simply typed -:math:`\lambda`-calculus occurred with Church’s *Simple Theory of -Types*. The :math:`\lambda`-calculus notation, originally used for +λ-calculus occurred with Church’s *Simple Theory of +Types*. The λ-calculus notation, originally used for expressing functionality, could also be used as an encoding of natural deduction proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the *Automath* project, the first full-scale attempt to develop and @@ -32,7 +35,7 @@ Exploiting this Curry-Howard isomorphism, notable achievements in proof theory saw the emergence of two type-theoretic frameworks; the first one, Martin-Löf’s *Intuitionistic Theory of Types*, attempts a new foundation of mathematics on constructive principles. The second one, -Girard’s polymorphic :math:`\lambda`-calculus :math:`F_\omega`, is a +Girard’s polymorphic λ-calculus :math:`F_\omega`, is a very strong functional system in which we may represent higher-order logic proof structures. Combining both systems in a higher-order extension of the Automath language, T. Coquand presented in 1985 the @@ -107,15 +110,27 @@ advantage of special hardware, debuggers, and the like. We hope that |Coq| can be of use to researchers interested in experimenting with this new methodology. +.. [#years] At the time of writting, i.e. 1995. + +Brief summary of the versions up to 5.10 +---------------------------------------- + +.. note:: + This summary was written in 1995 together with the previous + section and formed the initial version of the Credits chapter + (that has since then been appended to, at each new release). + A more comprehensive description of these early versions is + available in the next few sections, which were written in 2015. + A first implementation of CoC was started in 1984 by G. Huet and T. Coquand. Its implementation language was CAML, a functional programming language from the ML family designed at INRIA in Rocquencourt. The core of this system was a proof-checker for CoC seen as a typed -:math:`\lambda`-calculus, called the *Constructive Engine*. This engine +λ-calculus, called the *Constructive Engine*. This engine was operated through a high-level notation permitting the declaration of axioms and parameters, the definition of mathematical types and objects, and the explicit construction of proof objects encoded as -:math:`\lambda`-terms. A section mechanism, designed and implemented by +λ-terms. A section mechanism, designed and implemented by G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental @@ -189,8 +204,324 @@ definitions of “inversion predicates”. | Gérard Huet | -Credits: addendum for version 6.1 ---------------------------------- +Version 1 +--------- + +.. note:: + + These additional notes come from a document written + in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin + to accompany their public release of the archive of versions 1.10 to 6.2 + of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and + implemented in the Formel team, joint between the INRIA Rocquencourt + laboratory and the Ecole Normale Supérieure of Paris, from 1984 + onwards. + +This software is a prototype type-checker for a higher-order logical +formalism known as the Theory of Constructions, presented in his PhD +thesis by Thierry Coquand, with influences from Girard's system F and +de Bruijn's Automath. The metamathematical analysis of the system is +the PhD work of Thierry Coquand. The software is mostly the work of +Gérard Huet. Most of the mathematical examples verified with the +software are due to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at +the time) was a version of ML adapted from the Edinburgh LCF system +and running on a LISP backend. The main improvements from the original +LCF ML were that ML was compiled rather than interpreted (Gérard Huet +building on the original translator by Lockwood Morris), and that it +was enriched by recursively defined types (work of Guy +Cousineau). This ancestor of CAML was used and improved by Larry +Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to +early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used +for the examples in Thierry Coquand's thesis, defended on January 31st +1985. There was a unique binding operator, used both for universal +quantification (dependent product) at the level of types and +functional abstraction (λ) at the level of terms/proofs, in the manner +of Automath. Substitution (λ-reduction) was implemented using de +Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used +for the examples in the paper: T. Coquand, G. Huet. *Constructions: A +Higher Order Proof System for Mechanizing Mathematics* :cite:`CH85`. + +Christine Paulin joined the team at this point, for her DEA research +internship. In her DEA memoir (August 1985) she presents developments +for the *lambo* function – :math:`\text{lambo}(f)(n)` computes the minimal +:math:`m` such that :math:`f(m)` is greater than :math:`n`, for :math:`f` +an increasing integer function, a challenge for constructive mathematics. +She also encoded the majority voting algorithm of Boyer and Moore. + +Version 2 +--------- + +The formal system, now renamed as the *Calculus of Constructions*, was +presented with a proof of consistency and comparisons with proof +systems of Per Martin Löf, Girard, and the Automath family of N. de +Bruijn, in the paper: T. Coquand and G. Huet. *The Calculus of +Constructions* :cite:`CH88`. + +An abstraction of the software design, in the form of an abstract +machine for proof checking, and a fuller sequence of mathematical +developments was presented in: T. Coquand, G. Huet. *Concepts +Mathématiques et Informatiques Formalisés dans le Calcul des +Constructions* :cite:`CH87`. + +Version 2.8 was frozen on December 16th, 1985, and served for +developing the examples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative +hierarchy of universes. Universe levels were initially explicit +natural numbers. Another improvement was the possibility of automatic +synthesis of implicit type arguments, relieving the user of tedious +redundant declarations. + +Christine Paulin wrote an article *Algorithm development in the +Calculus of Constructions* :cite:`P86`. Besides *lambo* and *majority*, +she presents *quicksort* and a text formatting algorithm. + +Version 2.13 of the Calculus of Constructions with universes was +frozen on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with +ML algorithms was given by Gérard Huet in his May 1986 CMU course +notes *Formal Structures for Computation and Deduction*. Its chapter +*Induction and Recursion in the Theory of Constructions* was presented +as an invited paper at the Joint Conference on Theory and Practice of +Software Development TAPSOFT’87 at Pise in March 1987, and published +as *Induction Principles Formalized in the Calculus of +Constructions* :cite:`H88`. + +Version 3 +--------- + +This version saw the beginning of proof automation, with a search +algorithm inspired from PROLOG and the applicative logic programming +programs of the course notes *Formal structures for computation and +deduction*. The search algorithm was implemented in ML by Thierry +Coquand. The proof system could thus be used in two modes: proof +verification and proof synthesis, with tactics such as ``AUTO``. + +The implementation language was now called CAML, for Categorical +Abstract Machine Language. It used as backend the LLM3 virtual machine +of Le Lisp by Jérôme Chailloux. The main developers of CAML were +Michel Mauny, Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of +November 1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University +in 1986-87, where he developed a variant implementation in SML, with +which he wrote some developments on fixpoints in Scott's domains. + +Version 4 +--------- + +This version saw the beginning of program extraction from proofs, with +two varieties of the type ``Prop`` of propositions, indicating +constructive intent. The proof extraction algorithms were implemented +by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library +of mathematical developments (directory ``exemples``), with libraries +``Logic`` (containing impredicative encodings of intuitionistic logic and +algebraic primitives for booleans, natural numbers and list), ``Peano`` +developing second-order Peano arithmetic, ``Arith`` defining addition, +multiplication, euclidean division and factorial. Typical developments +were the Knaster-Tarski theorem and Newman's lemma from rewriting +theory. + +V4.2 was a joint development of a team consisting of Thierry Coquand, +Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the +log of changes. It was frozen on September 1987 as the last version +implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable +development system. + +V4.3 saw the first top-level of the system. Instead of evaluating +explicit quotations, the user could develop his mathematics in a +high-level language called the mathematical vernacular (following +Automath terminology). The user could develop files in the vernacular +notation (with ``.v`` extension) which were now separate from the ``ml`` +sources of the implementation. Gilles Dowek joined the team to +develop the vernacular language as his DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of +lemmas when local hypotheses of proofs were discharged. This gave a +notion of global mathematical environment with local sections. + +Another significant practical change was that the system, originally +developped on the VAX central computer of our lab, was transferred on +SUN personal workstations, allowing a level of distributed +development. The extraction algorithm was modified, with three +annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop`` +and ``Type``. + +Version 4.3 was frozen at the end of November 1987, and was +distributed to an early community of users (among those were Hugo +Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. Now natural +numbers could be defined as:: + + [source, coq] + Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. + +These inductive types were encoded impredicatively in the calculus, +using a subsystem *rec* due to Christine Paulin. V4.4 was frozen on +March 6th 1988. + +Version 4.5 was the first one to support inductive types and program +extraction. Its banner was *Calcul des Constructions avec +Réalisations et Synthèse*. The vernacular language was enriched to +accommodate extraction commands. + +The verification engine design was presented as: G. Huet. *The +Constructive Engine*. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. The final paper, +describing the V4.9 implementation, appeared in: A perspective in +Theoretical Computer Science, Commemorative Volume in memory of Gift +Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on +Logical Foundations of Functional Programming organized by Gérard Huet +at Austin, Texas. + +Version 4.6 was started during the summer of 1988. Its main +improvement was the complete rehaul of the proof synthesis engine by +Thierry Coquand, with a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd +1988. It evolved progressively into LEGO, proof system for Luo's +formalism of Extended Calculus of Constructions. + +The discharge tactic was modified by Gérard Huet to allow for +inter-dependencies in discharged lemmas. Christine Paulin improved the +inductive definition scheme in order to accommodate predicates of any +arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to +improve the modularity of the implementation. Now the term verifier is +identified as a proper module Machine, which the structure of its +internal data structures being hidden and thus accessible only through +the legitimate operations. This machine (the constructive engine) was +the trusted core of the implementation. The proof synthesis mechanism +was a separate proof term generator. Once a complete proof term was +synthesized with the help of tactics, it was entirely re-checked by +the engine. Thus there was no need to certify the tactics, and the +system took advantage of this fact by having tactics ignore the +universe levels, universe consistency check being relegated to the +final type-checking pass. This induced a certain puzzlement in early +users who saw, after a successful proof search, their ``QED`` followed +by silence, followed by a failure message due to a universe +inconsistency… + +The set of examples comprise set theory experiments by Hugo Herbelin, +and notably the Schroeder-Bernstein theorem. + +Version 4.8, started on October 8th, 1988, saw a major +re-implementation of the abstract syntax type ``constr``, separating +variables of the formalism and metavariables denoting incomplete terms +managed by the search mechanism. A notion of level (with three values +``TYPE``, ``OBJECT`` and ``PROOF``) is made explicit and a type judgement +clarifies the constructions, whose implementation is now fully +explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof +synthesis to the new representation, and simplifies pattern matching +to first-order predicate calculus matching, with important performance +gain. + +A new representation of the universe hierarchy is then defined by +Gérard Huet. Universe levels are now implemented implicitly, through +a hidden graph of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the +ordering, and thus consistency. This was documented in a memo *Adding +Type:Type to the Calculus of Constructions* which was never published. + +The development version is released as a stable 4.8 at the end of +1988. + +Version 4.9 is released on March 1st 1989, with the new "elastic" +universe hierarchy. + +The spring of 1989 saw the first attempt at documenting the system +usage, with a number of papers describing the formalism: + +- *Metamathematical Investigations of a Calculus of Constructions*, by + Thierry Coquand :cite:`C90`, + +- *Inductive definitions in the Calculus of Constructions*, by + Christine Paulin-Mohrin, + +- *Extracting Fω's programs from proofs in the Calculus of + Constructions*, by Christine Paulin-Mohring* :cite:`P89`, + +- *The Constructive Engine*, by Gérard Huet :cite:`H89`, + +as well as a number of user guides: + +- *A short user's guide for the Constructions*, Version 4.10, by Gérard Huet +- *A Vernacular Syllabus*, by Gilles Dowek. +- *The Tactics Theorem Prover, User's guide*, Version 4.10, by Thierry + Coquand. + +Stable V4.10, released on May 1st, 1989, was then a mature system, +distributed with CAML V2.6. + +In the mean time, Thierry Coquand and Christine Paulin-Mohring had +been investigating how to add native inductive types to the Calculus +of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. *Inductively defined types in the +Calculus of Constructions* :cite:`PP90`. An extension of the calculus +with primitive inductive types appeared in: T. Coquand and +C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`. + +This led to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules +and Properties* :cite:`P93`. + +The last version of CONSTR is Version 4.11, which was last distributed +in the spring of 1990. It was demonstrated at the first workshop of +the European Basic Research Action Logical Frameworks In Sophia +Antipolis in May 1990. + +Version 5 +--------- + +At the end of 1989, Version 5.1 was started, and renamed as the system +Coq for the Calculus of Inductive Constructions. It was then ported to +the new stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers +University in Göteborg. Christine Paulin-Mohring took a CNRS +researcher position at the LIP laboratory of École Normale Supérieure +de Lyon. Project Formel was terminated, and gave rise to two teams: +Cristal at INRIA-Roquencourt, that continued developments in +functional programming with Caml-light then OCaml, and Coq, continuing +the type theory research, with a joint team headed by Gérard Huet at +INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory +of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software +architect of Version 5. He completely rehauled the implementation for +efficiency. Versions 5.6 and 5.8 were major distributed versions, +with complete documentation and a library of users' developements. The +use of the RCS revision control system, and systematic ChangeLog +files, allow a more precise tracking of the software developments. + +| September 2015 + +| Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. +| + +Version 6.1 +----------- The present version 6.1 of |Coq| is based on the V5.10 architecture. It was ported to the new language Objective Caml by Bruno Barras. The @@ -226,8 +557,8 @@ Barras. | Christine Paulin | -Credits: addendum for version 6.2 ---------------------------------- +Version 6.2 +----------- In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA. @@ -271,8 +602,8 @@ Loiseleur. | Christine Paulin | -Credits: addendum for version 6.3 ---------------------------------- +Version 6.3 +----------- The main changes in version V6.3 were the introduction of a few new tactics and the extension of the guard condition for fixpoint @@ -304,8 +635,8 @@ Monin from CNET Lannion. | Christine Paulin | -Credits: versions 7 -------------------- +Versions 7 +---------- The version V7 is a new implementation started in September 1999 by Jean-Christophe Filliâtre. This is a major revision with respect to the @@ -393,8 +724,8 @@ J.-F. Monin from France Telecom R & D. | Hugo Herbelin & Christine Paulin | -Credits: version 8.0 --------------------- +Version 8.0 +----------- Coq version 8 is a major revision of the |Coq| proof assistant. First, the underlying logic is slightly different. The so-called *impredicativity* @@ -495,8 +826,8 @@ under the responsibility of Christine Paulin. | (updated Apr. 2006) | -Credits: version 8.1 --------------------- +Version 8.1 +----------- Coq version 8.1 adds various new functionalities. @@ -574,8 +905,8 @@ and Yale University. | Hugo Herbelin | -Credits: version 8.2 --------------------- +Version 8.2 +----------- Coq version 8.2 adds new features, new libraries and improves on many various aspects. @@ -668,8 +999,8 @@ the Coq-Club mailing list. | Hugo Herbelin | -Credits: version 8.3 --------------------- +Version 8.3 +----------- Coq version 8.3 is before all a transition version with refinements or extensions of the existing features and libraries and a new tactic nsatz @@ -742,8 +1073,8 @@ Pierce for the excellent teaching materials they provided. | Hugo Herbelin | -Credits: version 8.4 --------------------- +Version 8.4 +----------- Coq version 8.4 contains the result of three long-term projects: a new modular library of arithmetic by Pierre Letouzey, a new proof engine by @@ -898,8 +1229,8 @@ Eelis van der Weegen. | Hugo Herbelin | -Credits: version 8.5 --------------------- +Version 8.5 +----------- Coq version 8.5 contains the result of five specific long-term projects: @@ -916,7 +1247,7 @@ Coq version 8.5 contains the result of five specific long-term projects: Matthieu Sozeau. - An implementation of primitive projections with - :math:`\eta`-conversion bringing significant performance improvements + :math:`\eta`\-conversion bringing significant performance improvements when using records by Matthieu Sozeau. The full integration of the proof engine, by Arnaud Spiwack and @@ -967,10 +1298,10 @@ messages in case of inconsistencies and allowing higher-level algorithms like unification to be entirely type safe. The internal representation of universes has been modified but this is invisible to the user. -The underlying logic has been extended with :math:`\eta`-conversion for +The underlying logic has been extended with :math:`\eta`\-conversion for records defined with primitive projections by Matthieu Sozeau. This -additional form of :math:`\eta`-conversion is justified using the same -principle than the previously added :math:`\eta`-conversion for function +additional form of :math:`\eta`\-conversion is justified using the same +principle than the previously added :math:`\eta`\-conversion for function types, based on formulations of the Calculus of Inductive Constructions with typed equality. Primitive projections, which do not carry the parameters of the record and are rigid names (not defined as a @@ -1052,8 +1383,8 @@ Tankink. Maxime Dénès coordinated the release process. | Hugo Herbelin, Matthieu Sozeau and the |Coq| development team | -Credits: version 8.6 --------------------- +Version 8.6 +----------- Coq version 8.6 contains the result of refinements, stabilization of 8.5’s features and cleanups of the internals of the system. Over the @@ -1192,8 +1523,8 @@ Dénès to put together a |Coq| consortium. | Matthieu Sozeau and the |Coq| development team | -Credits: version 8.7 --------------------- +Version 8.7 +----------- |Coq| version 8.7 contains the result of refinements, stabilization of features and cleanups of the internals of the system along with a few new features. The @@ -1298,8 +1629,8 @@ system, is now upcoming and will rely on Inria’s newly created Foundation. | Matthieu Sozeau and the |Coq| development team | -Credits: version 8.8 --------------------- +Version 8.8 +----------- |Coq| version 8.8 contains the result of refinements and stabilization of features and deprecations, cleanups of the internals of the system along @@ -1405,8 +1736,8 @@ The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. | Matthieu Sozeau for the |Coq| development team | -Credits: version 8.9 --------------------- +Version 8.9 +----------- |Coq| version 8.9 contains the result of refinements and stabilization of features and deprecations or removals of deprecated features, diff --git a/doc/sphinx/dune b/doc/sphinx/dune index fff025c919..353d58c676 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1 +1,8 @@ (dirs :standard _static) + +(rule (targets README.gen.rst) + (deps (source_tree ../tools/coqrst) README.template.rst) + (action (run ../tools/coqrst/regen_readme.py %{targets}))) + +(alias (name refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 962d2a94e3..e05df65c63 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -20,9 +20,9 @@ There are types for functions (or programs), there are atomic types (especially datatypes)... but also types for proofs and types for the types themselves. Especially, any object handled in the formalism must belong to a type. For instance, universal quantification is relative -to a type and takes the form "*for all x of type T, P* ". The expression -“x of type T” is written :g:`x:T`. Informally, :g:`x:T` can be thought as -“x belongs to T”. +to a type and takes the form “*for all x of type* :math:`T`, :math:`P`”. The expression +“:math:`x` *of type* :math:`T`” is written “:math:`x:T`”. Informally, “:math:`x:T`” can be thought as +“:math:`x` *belongs to* :math:`T`”. The types of types are *sorts*. Types and sorts are themselves terms so that terms, types and sorts are all components of a common @@ -132,7 +132,7 @@ the following rules. which maps elements of :math:`T` to the expression :math:`u`. #. if :math:`t` and :math:`u` are terms then :math:`(t~u)` is a term (:g:`t u` in |Coq| concrete - syntax). The term :math:`(t~u)` reads as “t applied to u”. + syntax). The term :math:`(t~u)` reads as “:math:`t` applied to :math:`u`”. #. if :math:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are terms then :math:`\letin{x}{t:T}{u}` is a term which denotes the term :math:`u` where the variable :math:`x` is locally bound @@ -216,7 +216,7 @@ For the rest of the chapter, :math:`Γ::(y:T)` denotes the local context :math:` enriched with the local assumption :math:`y:T`. Similarly, :math:`Γ::(y:=t:T)` denotes the local context :math:`Γ` enriched with the local definition :math:`(y:=t:T)`. The notation :math:`[]` denotes the empty local context. By :math:`Γ_1 ; Γ_2` we mean -concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2` . +concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2`. .. _Global-environment: @@ -542,10 +542,10 @@ exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangle … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and :math:`u_2` are identical, or they are convertible up to η-expansion, i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is -recursively convertible to :math:`u_1'` , or, symmetrically, +recursively convertible to :math:`u_1'`, or, symmetrically, :math:`u_2` is :math:`λx:T.~u_2'` and :math:`u_1 x` is recursively convertible to :math:`u_2'`. We then write -:math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2` . +:math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2`. Apart from this we consider two instances of polymorphic and cumulative (see Chapter :ref:`polymorphicuniverses`) inductive types @@ -782,7 +782,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) - with odd : nat -> prop := + with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n). @@ -793,7 +793,7 @@ Types of inductive objects ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We have to give the type of constants in a global environment :math:`E` which -contains an inductive declaration. +contains an inductive definition. .. inference:: Ind @@ -833,7 +833,7 @@ contains an inductive declaration. Well-formed inductive definitions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We cannot accept any inductive declaration because some of them lead +We cannot accept any inductive definition because some of them lead to inconsistent systems. We restrict ourselves to definitions which satisfy a syntactic criterion of positivity. Before giving the formal rules, we need a few definitions: @@ -898,7 +898,7 @@ cases: + :math:`T` converts to :math:`∀ x:U,~V` and :math:`X` does not occur in type :math:`U` but occurs strictly positively in type :math:`V` + :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an - inductive declaration of the form + inductive definition of the form .. math:: \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n} @@ -914,7 +914,7 @@ Nested Positivity The type of constructor :math:`T` of :math:`I` *satisfies the nested positivity condition* for a constant :math:`X` in the following cases: -+ :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive definition with :math:`m` ++ :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive type with :math:`m` parameters and :math:`X` does not occur in any :math:`u_i` + :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the nested positivity condition for :math:`X` @@ -929,7 +929,7 @@ condition* for a constant :math:`X` in the following cases: Inductive nattree (A:Type) : Type := | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A. + | natnode : A -> (nat -> nattree A) -> nattree A. Then every instantiated constructor of ``nattree A`` satisfies the nested positivity condition for ``nattree``: @@ -939,7 +939,7 @@ condition* for a constant :math:`X` in the following cases: type of that constructor (primarily because ``nattree`` does not have any (real) arguments) ... (bullet 1) - + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``natnode`` satisfies the positivity condition for ``nattree`` because: - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 1) @@ -963,10 +963,9 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]` .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ - \WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ} + \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} provided that the following side conditions hold: @@ -976,13 +975,13 @@ provided that the following side conditions hold: context of parameters, + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`, + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which - satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ ∪ E`. + satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ E`. One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sort :math:`\Prop` but may fail to define inductive definition on sort :math:`\Set` and -generate constraints between universes for inductive definitions in +sort :math:`\Prop` but may fail to define inductive type on sort :math:`\Set` and +generate constraints between universes for inductive types in the Type hierarchy. @@ -1062,9 +1061,9 @@ longest prefix of parameters such that the :math:`m` first arguments of all occurrences of all :math:`I_j` in all :math:`C_k` (even the occurrences in the hypotheses of :math:`C_k`) are exactly applied to :math:`p_1 … p_m` (:math:`m` is the number of *recursively uniform parameters* and the :math:`p−m` remaining parameters -are the *recursively non-uniform parameters*). Let :math:`q_1 , …, q_r` , with +are the *recursively non-uniform parameters*). Let :math:`q_1 , …, q_r`, with :math:`0≤ r≤ m`, be a (possibly) partial instantiation of the recursively -uniform parameters of :math:`Γ_P` . We have: +uniform parameters of :math:`Γ_P`. We have: .. inference:: Ind-Family @@ -1083,7 +1082,7 @@ provided that the following side conditions hold: + :math:`Γ_{P′}` is the context obtained from :math:`Γ_P` by replacing each :math:`P_l` that is an arity with :math:`P_l'` for :math:`1≤ l ≤ r` (notice that :math:`P_l` arity implies :math:`P_l'` arity since :math:`E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}`); - + there are sorts :math:`s_i` , for :math:`1 ≤ i ≤ k` such that, for + + there are sorts :math:`s_i`, for :math:`1 ≤ i ≤ k` such that, for :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ; + the sorts :math:`s_i` are such that all eliminations, to @@ -1214,7 +1213,7 @@ recognized implicitly and taken into account in the conversion rule. From the logical point of view, we have built a type family by giving a set of constructors. We want to capture the fact that we do not have any other way to build an object in this type. So when trying to prove -a property about an object :math:`m` in an inductive definition it is enough +a property about an object :math:`m` in an inductive type it is enough to enumerate all the cases where :math:`m` starts with a different constructor. @@ -1320,7 +1319,7 @@ and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that **Notations.** The :math:`[I:A|B]` is defined as the smallest relation satisfying the following rules: We write :math:`[I|B]` for :math:`[I:A|B]` where :math:`A` is the type of :math:`I`. -The case of inductive definitions in sorts :math:`\Set` or :math:`\Type` is simple. +The case of inductive types in sorts :math:`\Set` or :math:`\Type` is simple. There is no restriction on the sort of the predicate to be eliminated. .. inference:: Prod @@ -1396,7 +1395,7 @@ proof-irrelevance property which is sometimes a useful axiom: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. -The elimination of an inductive definition of type :math:`\Prop` on a predicate +The elimination of an inductive type of sort :math:`\Prop` on a predicate :math:`P` of type :math:`I→ \Type` leads to a paradox when applied to impredicative inductive definition like the second-order existential quantifier :g:`exProp` defined above, because it gives access to the two projections on @@ -1441,7 +1440,7 @@ elimination on any sort is allowed. **Type of branches.** Let :math:`c` be a term of type :math:`C`, we assume :math:`C` is a type of constructor for an inductive type :math:`I`. Let :math:`P` be a term that represents the property to be -proved. We assume :math:`r` is the number of parameters and :math:`p` is the number of +proved. We assume :math:`r` is the number of parameters and :math:`s` is the number of arguments. We define a new type :math:`\{c:C\}^P` which represents the type of the branch @@ -1449,7 +1448,7 @@ corresponding to the :math:`c:C` constructor. .. math:: \begin{array}{ll} - \{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)\}^P &\equiv (P~t_1\ldots ~t_p~c) \\ + \{c:(I~q_1\ldots q_r\ t_1 \ldots t_s)\}^P &\equiv (P~t_1\ldots ~t_s~c) \\ \{c:∀ x:T,~C\}^P &\equiv ∀ x:T,~\{(c~x):C\}^P \end{array} @@ -1496,7 +1495,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: & ≡∀ n:\nat,~∀ l:\List~\nat,~(P~(\cons~\nat~n~l)). \end{array} - Given some :math:`P` then :math:`\{(\Nil~\nat)\}^P` represents the expected type of :math:`f_1` , + Given some :math:`P` then :math:`\{(\Nil~\nat)\}^P` represents the expected type of :math:`f_1`, and :math:`\{(\cons~\nat)\}^P` represents the expected type of :math:`f_2`. @@ -1628,15 +1627,15 @@ Before accepting a fixpoint definition as being correctly typed, we check that the definition is “guarded”. A precise analysis of this notion can be found in :cite:`Gim94`. The first stage is to precise on which argument the fixpoint will be decreasing. The type of this argument -should be an inductive definition. For doing this, the syntax of +should be an inductive type. For doing this, the syntax of fixpoints is extended and becomes .. math:: - \Fix~f_i\{f_1/k_1 :A_1':=t_1' … f_n/k_n :A_n':=t_n'\} + \Fix~f_i\{f_1/k_1 :A_1:=t_1 … f_n/k_n :A_n:=t_n\} where :math:`k_i` are positive integers. Each :math:`k_i` represents the index of -parameter of :math:`f_i` , on which :math:`f_i` is decreasing. Each :math:`A_i` should be a +parameter of :math:`f_i`, on which :math:`f_i` is decreasing. Each :math:`A_i` should be a type (reducible to a term) starting with at least :math:`k_i` products :math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'` and :math:`B_{k_i}` an inductive type. @@ -1648,7 +1647,7 @@ The definition of being structurally smaller is a bit technical. One needs first to define the notion of *recursive arguments of a constructor*. For an inductive definition :math:`\ind{r}{Γ_I}{Γ_C}`, if the type of a constructor :math:`c` has the form -:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r :T_r,~(I_j~p_1 … p_r~t_1 … t_s )`, +:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_m :T_m,~(I_j~p_1 … p_r~t_1 … t_s )`, then the recursive arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs. @@ -1661,13 +1660,13 @@ Given a variable :math:`y` of an inductively defined type in a declaration + :math:`(t~u)` and :math:`λ x:U .~t` when :math:`t` is structurally smaller than :math:`y`. + :math:`\case(c,P,f_1 … f_n)` when each :math:`f_i` is structurally smaller than :math:`y`. If :math:`c` is :math:`y` or is structurally smaller than :math:`y`, its type is an inductive - definition :math:`I_p` part of the inductive declaration corresponding to :math:`y`. + type :math:`I_p` part of the inductive definition corresponding to :math:`y`. Each :math:`f_i` corresponds to a type of constructor - :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_k :B_k ,~(I~a_1 … a_k )` - and can consequently be written :math:`λ y_1 :B_1' .~… λ y_k :B_k'.~g_i`. (:math:`B_i'` is + :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_m :B_m ,~(I_p~p_1 … p_r~t_1 … t_s )` + and can consequently be written :math:`λ y_1 :B_1' .~… λ y_m :B_m'.~g_i`. (:math:`B_i'` is obtained from :math:`B_i` by substituting parameters for variables) the variables :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the - ones in which one of the :math:`I_l` occurs) are structurally smaller than y. + ones in which one of the :math:`I_l` occurs) are structurally smaller than :math:`y`. The following definitions are correct, we enter them using the :cmd:`Fixpoint` @@ -1750,7 +1749,7 @@ One can modify a global declaration by generalizing it over a previously assumed constant :math:`c`. For doing that, we need to modify the reference to the global declaration in the subsequent global environment and local context by explicitly applying this constant to -the constant :math:`c'`. +the constant :math:`c`. Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write :math:`∀x:U,~\subst{Γ}{c}{x}` to mean @@ -1780,7 +1779,7 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}} One can similarly modify a global declaration by generalizing it over -a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of the form +a previously defined constant :math:`c`. Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write :math:`\subst{Γ}{c}{u}` to mean :math:`[y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]`. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index b82b3b0e80..d1b95e6203 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -146,7 +146,7 @@ Propositional Connectives First, we find propositional calculus connectives: -.. coqtop:: in +.. coqdoc:: Inductive True : Prop := I. Inductive False : Prop := . @@ -236,7 +236,7 @@ Finally, a few easy lemmas are provided. single: eq_rect (term) single: eq_rect_r (term) -.. coqtop:: in +.. coqdoc:: Theorem absurd : forall A C:Prop, A -> ~ A -> C. Section equality. @@ -264,7 +264,7 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. -.. coqtop:: in +.. coqtop:: in abort Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) @@ -465,7 +465,7 @@ Intuitionistic Type Theory. single: Choice2 (term) single: bool_choice (term) -.. coqtop:: in +.. coqdoc:: Lemma Choice : forall (S S':Set) (R:S -> S' -> Prop), @@ -506,7 +506,7 @@ realizability interpretation. single: absurd_set (term) single: and_rect (term) -.. coqtop:: in +.. coqdoc:: Definition except := False_rec. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. @@ -531,7 +531,7 @@ section :tacn:`refine`). This scope is opened by default. The following example is not part of the standard library, but it shows the usage of the notations: - .. coqtop:: in + .. coqtop:: in reset Fixpoint even (n:nat) : bool := match n with @@ -558,7 +558,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: -.. coqtop:: in +.. coqdoc:: Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := @@ -606,11 +606,14 @@ Finally, it gives the definition of the usual orderings ``le``, single: ge (term) single: gt (term) -.. coqtop:: in +.. This emits a notation already used warning but it won't be shown to + the user. + +.. coqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n - | le_S : forall m:nat, n <= m -> n <= (S m). + | le_S : forall m:nat, n <= m -> n <= (S m) where "n <= m" := (le n m) : nat_scope. Definition lt (n m:nat) := S n <= m. Definition ge (n m:nat) := m <= n. @@ -625,7 +628,7 @@ induction principle. single: nat_case (term) single: nat_double_ind (term) -.. coqtop:: in +.. coqdoc:: Theorem nat_case : forall (n:nat) (P:nat -> Prop), @@ -652,7 +655,7 @@ well-founded induction, in module ``Wf.v``. single: Acc_rect (term) single: well_founded (term) -.. coqtop:: in +.. coqdoc:: Section Well_founded. Variable A : Type. @@ -681,7 +684,7 @@ fixpoint equation can be proved. single: Fix_F_inv (term) single: Fix_F_eq (term) -.. coqtop:: in +.. coqdoc:: Section FixPoint. Variable P : A -> Type. @@ -715,7 +718,7 @@ of equality: .. coqtop:: in Inductive identity (A:Type) (a:A) : A -> Type := - identity_refl : identity a a. + identity_refl : identity A a a. Some properties of ``identity`` are proved in the module ``Logic_Type``, which also provides the definition of ``Type`` level negation: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 50a56f1d51..f1733a5ebf 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -247,11 +247,6 @@ Primitive Projections printing time (even though they are absent in the actual AST manipulated by the kernel). -.. flag:: Printing Primitive Projection Compatibility - - This compatibility option (on by default) governs the - printing of pattern matching over primitive records. - Primitive Record Types ++++++++++++++++++++++ @@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` -to display unfolded primitive projections as matches and distinguish them from folded ones. +user-level, and there is no way to display unfolded projections differently +from folded ones. Compatibility Projections and :g:`match` @@ -1924,9 +1919,10 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical Structure @qualid +.. cmd:: Canonical {? Structure } @qualid - This command declares :token:`qualid` as a canonical structure. + This command declares :token:`qualid` as a canonical instance of a + structure (a record). Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -1961,12 +1957,12 @@ in :ref:`canonicalstructures`; here only a simple example is given. Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Canonical Structure nat_setoid. + Canonical nat_setoid. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. - .. coqtop:: all + .. coqtop:: all abort Lemma is_law_S : is_law S. @@ -1974,11 +1970,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. cmdv:: Canonical Structure @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical Structure @ident`. - + declaration :n:`Canonical @ident`. .. cmd:: Print Canonical Projections @@ -2019,10 +2014,10 @@ or :g:`m` to the type :g:`nat` of natural numbers). Implicit Types m n : nat. Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. - - intros m n. + Proof. intros m n. Abort. Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. + Abort. .. cmdv:: Implicit Type @ident : @type @@ -2265,3 +2260,52 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. + +.. _primitive-integers: + +Primitive Integers +-------------------------------- + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Uint63` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5ecf007eff..9bd41d79b7 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -434,6 +434,10 @@ the identifier :g:`b` being used to represent the dependency. the return type. For instance, the following alternative definition is accepted and has the same meaning as the previous one. + .. coqtop:: none + + Reset bool_case. + .. coqtop:: in Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := @@ -471,7 +475,7 @@ For instance, in the following example: Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with - | eq_refl _ => eq_refl A x + | eq_refl _ _ => eq_refl A x end. the type of the branch is :g:`eq A x x` because the third argument of @@ -826,6 +830,10 @@ Simple inductive types .. example:: + .. coqtop:: none + + Reset nat. + .. coqtop:: in Inductive nat : Set := O | S (_:nat). @@ -904,6 +912,10 @@ Parametrized inductive types Once again, it is possible to specify only the type of the arguments of the constructors, and to omit the type of the conclusion: + .. coqtop:: none + + Reset list. + .. coqtop:: in Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). @@ -949,7 +961,7 @@ Parametrized inductive types inductive definitions are abstracted over their parameters before type checking constructors, allowing to write: - .. coqtop:: all undo + .. coqtop:: all Set Uniform Inductive Parameters. Inductive list3 (A:Set) : Set := @@ -960,7 +972,7 @@ Parametrized inductive types and using :cmd:`Context` to give the uniform parameters, like so (cf. :ref:`section-mechanism`): - .. coqtop:: all undo + .. coqtop:: all reset Section list3. Context (A:Set). @@ -1011,7 +1023,7 @@ Mutually defined inductive types .. coqtop:: in - Variables A B : Set. + Parameters A B : Set. Inductive tree : Set := node : A -> forest -> tree @@ -1038,7 +1050,7 @@ Mutually defined inductive types two type variables :g:`A` and :g:`B`, the declaration should be done the following way: - .. coqtop:: in + .. coqdoc:: Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B @@ -1130,6 +1142,10 @@ found in e.g. Agda, and preserves subject reduction. The above example can be rewritten in the following way. +.. coqtop:: none + + Reset Stream. + .. coqtop:: all Set Primitive Projections. @@ -1147,7 +1163,7 @@ axiom. .. coqtop:: all - Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s). + Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s). More generally, as in the case of positive coinductive types, it is consistent to further identify extensional equality of coinductive types with propositional @@ -1517,7 +1533,7 @@ the following attributes names are recognized: .. example:: - .. coqtop:: all reset + .. coqtop:: all reset warn From Coq Require Program. #[program] Definition one : nat := S _. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 1b4d2315aa..eebf1f11e1 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -34,6 +34,11 @@ allow dynamic linking of tactics). You can switch to the OCaml toplevel with the command ``Drop.``, and come back to the |Coq| toplevel with the command ``Coqloop.loop();;``. +.. flag:: Coqtop Exit On Error + + This option, off by default, causes coqtop to exit with status code + ``1`` if a command produces an error instead of recovering from it. + Batch compilation (coqc) ------------------------ diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 9455228e7d..8b7fe20191 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -230,10 +230,12 @@ mathematical symbols ∀ and ∃, you may define: .. coqtop:: in - Notation "∀ x : T, P" := - (forall x : T, P) (at level 200, x ident). - Notation "∃ x : T, P" := - (exists x : T, P) (at level 200, x ident). + Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. + Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. There exists a small set of such notations already defined, in the file `utf8.v` of Coq library, so you may enable them just by diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index bd16b70d02..b629d15b11 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -33,7 +33,7 @@ example, revisiting the first example of the inversion documentation: | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. + Parameter P : nat -> nat -> Prop. Goal forall n m:nat, Le (S n) m -> P n m. @@ -53,7 +53,7 @@ rule of thumb, all the variables that appear inside constructors in the indices of the hypothesis should be generalized. This is exactly what the ``generalize_eqs_vars`` variant does: -.. coqtop:: all +.. coqtop:: all abort generalize_eqs_vars H. induction H. @@ -65,11 +65,11 @@ as well in this case, e.g.: .. coqtop:: none - Abort. + Require Import Coq.Program.Equality. .. coqtop:: in - Variable Q : forall (n m : nat), Le n m -> Prop. + Parameter Q : forall (n m : nat), Le n m -> Prop. Goal forall n m (p : Le (S n) m), Q (S n) m p. .. coqtop:: all @@ -88,11 +88,7 @@ automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality`` does. For example, we might simplify the previous goals considerably: -.. coqtop:: all - - Require Import Coq.Program.Equality. - -.. coqtop:: all +.. coqtop:: all abort induction p ; simplify_dep_elim. @@ -105,10 +101,6 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we’ve done manually with dependent destruction: -.. coqtop:: none - - Abort. - .. coqtop:: in Lemma ex : forall n m:nat, Le (S n) m -> P n m. @@ -117,7 +109,7 @@ redo what we’ve done manually with dependent destruction: intros n m H. -.. coqtop:: all +.. coqtop:: all abort dependent destruction H. @@ -126,17 +118,13 @@ destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors: -.. coqtop:: none - - Abort. - .. coqtop:: in Set Implicit Arguments. .. coqtop:: in - Variable A : Set. + Parameter A : Set. .. coqtop:: in @@ -230,29 +218,21 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. -.. coqtop:: none - - Abort. - The problem here is that we can’t just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau. -.. coqtop:: none - - Abort. - With this proper separation of the index from the instance and the right induction loading (putting ``G`` and ``D`` after the inducted-on hypothesis), the proof will go through, but it is a very tedious @@ -349,7 +329,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Variable Ack : nat -> nat -> nat. + Parameter Ack : nat -> nat -> nat. .. coqtop:: in @@ -377,7 +357,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Variable g : nat -> nat -> nat. + Parameter g : nat -> nat -> nat. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 442077616f..52e3029b8f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -200,7 +200,7 @@ following form: :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for - i = 0, ..., n and all have to be tactics. The :n:`v__i` is applied to the + i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. @@ -602,7 +602,7 @@ Failing .. example:: - .. coqtop:: all + .. coqtop:: all fail Goal True. Proof. fail. Abort. @@ -701,7 +701,7 @@ tactic .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac time_constr1 tac := let eval_early := match goal with _ => restart_timer "(depth 1)" end in @@ -716,7 +716,6 @@ tactic let y := time_constr1 ltac:(fun _ => eval compute in x) in y) in pose v. - Abort. Local definitions ~~~~~~~~~~~~~~~~~ @@ -847,7 +846,7 @@ We can carry out pattern matching on terms with: .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac f x := match x with @@ -1022,7 +1021,7 @@ Counting the goals Goal True /\ True /\ True. split;[|split]. - .. coqtop:: all + .. coqtop:: all abort all:pr_numgoals. @@ -1154,6 +1153,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ @@ -1301,10 +1309,10 @@ performance issue. .. coqtop:: all - Set Ltac Profiling. - tac. - Show Ltac Profile. - Show Ltac Profile "omega". + Set Ltac Profiling. + tac. + Show Ltac Profile. + Show Ltac Profile "omega". .. coqtop:: in diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 24645a8cc3..27360f02d3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -30,7 +30,7 @@ When a proof is completed, the message ``Proof completed`` is displayed. One can then register this proof as a defined constant in the environment. Because there exists a correspondence between proofs and terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those +:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those terms are called *proof terms*. @@ -529,16 +529,12 @@ Requesting information .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal exists n, n = 0. eexists ?[n]. Show n. - .. coqtop:: none - - Abort. - .. cmdv:: Show Script :name: Show Script @@ -739,14 +735,10 @@ Notes: split. - .. coqtop:: all + .. coqtop:: all abort 2: split. - .. coqtop:: none - - Abort. - .. .. coqtop:: none @@ -759,14 +751,10 @@ Notes: intros n. - .. coqtop:: all + .. coqtop:: all abort intros m. - .. coqtop:: none - - Abort. - This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after the split because it has not changed. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 483dbd311d..b240cef40c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -215,7 +215,7 @@ construct differs from the latter in that .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -233,7 +233,7 @@ construct differs from the latter in that .. coqtop:: reset all - Definition f u := let (m, n) := u in m + n. + Fail Definition f u := let (m, n) := u in m + n. The ``let:`` construct is just (more legible) notation for the primitive @@ -275,7 +275,7 @@ example, the null and all list function(al)s can be defined as follows: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -376,7 +376,7 @@ expressions such as .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -401,7 +401,7 @@ each point of use, e.g., the above definition can be written: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -413,7 +413,7 @@ each point of use, e.g., the above definition can be written: Variable all : (T -> bool) -> list T -> bool. - .. coqtop:: all undo + .. coqtop:: all Prenex Implicits null. Definition all_null (s : list T) := all null s. @@ -436,7 +436,7 @@ The syntax of the new declaration is a ``Set Printing All`` command). All |SSR| library files thus start with the incantation - .. coqtop:: all undo + .. coqdoc:: Set Implicit Arguments. Unset Strict Implicit. @@ -464,7 +464,7 @@ defined by the following declaration: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -505,7 +505,7 @@ Definitions |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: -.. coqtop:: in +.. coqdoc:: pose t := x + y. @@ -518,7 +518,7 @@ For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -534,7 +534,7 @@ The |SSR| pose tactic also supports (co)fixpoints, by providing the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …`` constructs. For instance, the following tactic: -.. coqtop:: in +.. coqdoc:: pose fix f (x y : nat) {struct x} : nat := if x is S p then S (f p y) else 0. @@ -544,7 +544,7 @@ on natural numbers. Similarly, local cofixpoints can be defined by a tactic of the form: -.. coqtop:: in +.. coqdoc:: pose cofix f (arg : T) := … . @@ -553,26 +553,26 @@ offers a smooth way of defining local abstractions. The type of “holes” is guessed by type inference, and the holes are abstracted. For instance the tactic: -.. coqtop:: in +.. coqdoc:: pose f := _ + 1. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n := n + 1. When the local definition of a function involves both arguments and holes, hole abstractions appear first. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x := x + _. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n x := x + n. @@ -580,13 +580,13 @@ The interaction of the pose tactic with the interpretation of implicit arguments results in a powerful and concise syntax for local definitions involving dependent types. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x y := (x, y). adds to the context the local definition: -.. coqtop:: in +.. coqdoc:: pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). @@ -639,7 +639,7 @@ The tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -652,11 +652,7 @@ The tactic: Lemma test x : f x + f x = f x. set t := f _. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart set t := {2}(f _). @@ -694,7 +690,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -715,7 +711,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -736,7 +732,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -756,7 +752,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -766,7 +762,7 @@ Moreover: .. coqtop:: all Lemma test : forall x : nat, x + 1 = 0. - set t := _ + 1. + Fail set t := _ + 1. + Typeclass inference should fill in any residual hole, but matching should never assign a value to a global existential variable. @@ -789,7 +785,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -810,7 +806,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -831,7 +827,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -862,7 +858,7 @@ selection. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -879,7 +875,7 @@ only one occurrence of the selected term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -889,7 +885,7 @@ only one occurrence of the selected term. .. coqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. - set a := {2}(_ + _). + Fail set a := {2}(_ + _). .. _basic_localization_ssr: @@ -910,7 +906,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -926,7 +922,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -1042,7 +1038,7 @@ constants to the goal. For example, the proof of [#3]_ - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1079,7 +1075,7 @@ constants to the goal. Because they are tacticals, ``:`` and ``=>`` can be combined, as in -.. coqtop:: in +.. coqdoc:: move: m le_n_m => p le_n_p. @@ -1104,7 +1100,7 @@ The ``:`` tactical is used to operate on an element in the context. to encapsulate the inductive step in a single command: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1139,7 +1135,7 @@ Basic tactics like apply and elim can also be used without the ’:’ tactical: for example we can directly start a proof of ``subnK`` by induction on the top variable ``m`` with -.. coqtop:: in +.. coqdoc:: elim=> [|m IHm] n le_n. @@ -1150,7 +1146,7 @@ explained in terms of the goal stack:: is basically equivalent to -.. coqtop:: in +.. coqdoc:: move: a H1 H2; tactic => a H1 H2. @@ -1163,13 +1159,13 @@ temporary abbreviation to hide the statement of the goal from The general form of the in tactical can be used directly with the ``move``, ``case`` and ``elim`` tactics, so that one can write -.. coqtop:: in +.. coqdoc:: elim: n => [|n IHn] in m le_n_m *. instead of -.. coqtop:: in +.. coqdoc:: elim: n m le_n_m => [|n IHn] m le_n_m. @@ -1257,7 +1253,7 @@ The elim tactic .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1297,7 +1293,7 @@ existential metavariables of sort :g:`Prop`. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1398,7 +1394,7 @@ Switches affect the discharging of a :token:`d_item` as follows: For example, the tactic: -.. coqtop:: in +.. coqdoc:: move: n {2}n (refl_equal n). @@ -1409,7 +1405,7 @@ For example, the tactic: Therefore this tactic changes any goal ``G`` into -.. coqtop:: +.. coqdoc:: forall n n0 : nat, n = n0 -> G. @@ -1477,7 +1473,7 @@ context to interpret wildcards; in particular it can accommodate the .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1752,7 +1748,7 @@ Clears are deferred until the end of the intro pattern. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -1813,7 +1809,7 @@ Block introduction .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1843,7 +1839,7 @@ Generation of equations The generation of named equations option stores the definition of a new constant as an equation. The tactic: -.. coqtop:: in +.. coqdoc:: move En: (size l) => n. @@ -1851,7 +1847,7 @@ where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and adds the fact ``En : size l = n`` to the context. This is quite different from: -.. coqtop:: in +.. coqdoc:: pose n := (size l). @@ -1866,7 +1862,7 @@ deal with the possible parameters of the constants introduced. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1885,7 +1881,7 @@ under fresh |SSR| names. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1936,7 +1932,7 @@ be substituted. inferred looking at the type of the top assumption. This allows for the compact syntax: - .. coqtop:: in + .. coqdoc:: case: {2}_ / eqP. @@ -1952,7 +1948,7 @@ be substituted. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1989,19 +1985,17 @@ be substituted. Lemma test l : (length l) * 2 = length (l ++ l). case: (lastP l). - Applied to the same goal, the command: - ``case: l / (lastP l).`` - generates the same subgoals but ``l`` has been cleared from both contexts. + Applied to the same goal, the tactc ``case: l / (lastP l)`` + generates the same subgoals but ``l`` has been cleared from both contexts: - Again applied to the same goal, the command. + .. coqtop:: all restart - .. coqtop:: none + case: l / (lastP l). - Abort. + Again applied to the same goal: - .. coqtop:: all + .. coqtop:: all restart abort - Lemma test l : (length l) * 2 = length (l ++ l). case: {1 3}l / (lastP l). Note that selected occurrences on the left of the ``/`` @@ -2015,10 +2009,6 @@ be substituted. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). @@ -2104,15 +2094,15 @@ into a closing one (similar to :tacn:`now`). Its general syntax is: :name: by :undocumented: -The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to -:n:`[by @tactic | by @tactic | ...]` and this form should be preferred -to the former. +The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to +:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the +standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed with a ``by``, like in: -.. coqtop:: in +.. coqdoc:: by apply/eqP; rewrite -dvdn1. @@ -2147,13 +2137,13 @@ A natural and common way of closing a goal is to apply a lemma which is the exact one needed for the goal to be solved. The defective form of the tactic: -.. coqtop:: in +.. coqdoc:: exact. is equivalent to: -.. coqtop:: in +.. coqdoc:: do [done | by move=> top; apply top]. @@ -2161,13 +2151,13 @@ where ``top`` is a fresh name assigned to the top assumption of the goal. This applied form is supported by the ``:`` discharge tactical, and the tactic: -.. coqtop:: in +.. coqdoc:: exact: MyLemma. is equivalent to: -.. coqtop:: in +.. coqdoc:: by apply: MyLemma. @@ -2179,19 +2169,19 @@ is equivalent to: follows the ``by`` keyword is considered to be a parenthesized block applied to the current goal. Hence for example if the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1. succeeds, then the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1; apply my_lemma2. usually fails since it is equivalent to: - .. coqtop:: in + .. coqdoc:: by (rewrite my_lemma1; apply my_lemma2). @@ -2247,7 +2237,7 @@ Finally, the tactics ``last`` and ``first`` combine with the branching syntax of Ltac: if the tactic generates n subgoals on a given goal, then the tactic -.. coqtop:: in +.. coqdoc:: tactic ; last k [ tactic1 |…| tacticm ] || tacticn. @@ -2260,9 +2250,8 @@ to the others. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none - Abort. From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. @@ -2296,13 +2285,13 @@ Iteration A tactic of the form: -.. coqtop:: in +.. coqdoc:: do [ tactic 1 | … | tactic n ]. is equivalent to the standard Ltac expression: -.. coqtop:: in +.. coqdoc:: first [ tactic 1 | … | tactic n ]. @@ -2327,14 +2316,14 @@ Their meaning is: For instance, the tactic: -.. coqtop:: in +.. coqdoc:: tactic; do 1? rewrite mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals generated by tactic , whereas the tactic: -.. coqtop:: in +.. coqdoc:: tactic; do 2! rewrite mult_comm. @@ -2380,7 +2369,7 @@ between standard Ltac in and the |SSR| tactical in. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2455,7 +2444,7 @@ the holes are abstracted in term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2469,7 +2458,7 @@ the holes are abstracted in term. The invokation of ``have`` is equivalent to: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2487,7 +2476,7 @@ tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2518,7 +2507,7 @@ tactics of the form: which behave like: -.. coqtop:: in +.. coqdoc:: have: term ; first by tactic. move=> clear_switch i_item. @@ -2531,7 +2520,7 @@ to introduce the new assumption itself. The ``by`` feature is especially convenient when the proof script of the statement is very short, basically when it fits in one line like in: -.. coqtop:: in +.. coqdoc:: have H23 : 3 + 2 = 2 + 3 by rewrite addnC. @@ -2540,7 +2529,7 @@ the further use of the intermediate step. For instance, .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2559,7 +2548,7 @@ the further use of the intermediate step. For instance, Thanks to the deferred execution of clears, the following idiom is also supported (assuming x occurs in the goal only): -.. coqtop:: in +.. coqdoc:: have {x} -> : x = y. @@ -2568,7 +2557,7 @@ destruction of existential assumptions like in the tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2595,7 +2584,7 @@ term for the intermediate lemma, using tactics of the form: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2616,7 +2605,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. From Coq Require Import Omega. @@ -2635,7 +2624,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity, bound variables can be surrounded with parentheses even if no type is specified: -.. coqtop:: in +.. coqtop:: all restart have (x) : 2 * x = x + x by omega. @@ -2649,13 +2638,8 @@ copying the goal itself. .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all restart abort - Lemma test : True. have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2676,10 +2660,9 @@ context entry name. .. coqtop:: none - Abort All. Set Printing Depth 15. - .. coqtop:: all + .. coqtop:: all abort Inductive Ord n := Sub x of x < n. Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). @@ -2695,11 +2678,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega. @@ -2712,11 +2691,7 @@ with have and an explicit term, they must be used as follows: .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. @@ -2735,11 +2710,7 @@ makes use of it). .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega. @@ -2756,21 +2727,21 @@ typeclass inference. .. coqtop:: none - Abort All. - Axiom ty : Type. Axiom t : ty. Goal True. -+ .. coqtop:: in undo + .. coqtop:: all have foo : ty. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. -+ .. coqdoc:: + .. A strange bug prevents using the coqtop directive here + + .. coqdoc:: have foo : ty := . @@ -2779,13 +2750,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``, hence two subgoals are generated. -+ .. coqtop:: in undo + .. coqtop:: all restart have foo : ty := t. No inference for ``ty`` and ``t``. -+ .. coqtop:: in undo + .. coqtop:: all restart abort have foo := t. @@ -2816,7 +2787,7 @@ The + but the optional clear item is still performed in the *second* branch. This means that the tactic: - .. coqtop:: in + .. coqdoc:: suff {H} H : forall x : nat, x >= 0. @@ -2834,10 +2805,9 @@ The ``have`` modifier can follow the ``suff`` tactic. .. coqtop:: none - Abort All. Axioms G P : Prop. - .. coqtop:: all + .. coqtop:: all abort Lemma test : G. suff have H : P. @@ -2888,7 +2858,7 @@ name of the local definition with the ``@`` character. In the second subgoal, the tactic: -.. coqtop:: in +.. coqdoc:: move=> clear_switch i_item. @@ -2902,10 +2872,6 @@ are unique. .. example:: - .. coqtop:: none - - Abort All. - .. coqtop:: all Lemma quo_rem_unicity d q1 q2 r1 r2 : @@ -2927,7 +2893,7 @@ pattern will be used to process its instance. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -2936,6 +2902,7 @@ pattern will be used to process its instance. Axiom P : nat -> Prop. Axioms eqn leqn : nat -> nat -> bool. + Declare Scope this_scope. Notation "a != b" := (eqn a b) (at level 70) : this_scope. Notation "a <= b" := (leqn a b) (at level 70) : this_scope. Open Scope this_scope. @@ -2976,7 +2943,7 @@ illustrated in the following example. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2995,10 +2962,13 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: none + .. coqtop:: reset none + + From Coq Require Import ssreflect Omega. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - Abort All. - From Coq Require Import Omega. Section Test. Variable x : nat. Definition addx z := z + x. @@ -3126,14 +3096,14 @@ An :token:`r_item` can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all abort Definition double x := x + x. Definition ddouble x := double (double x). @@ -3145,21 +3115,16 @@ An :token:`r_item` can be: The |SSR| terms containing holes are *not* typed as abstractions in this context. Hence the following script fails. - .. coqtop:: none - - Abort. - .. coqtop:: all Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - rewrite -[f y]/(y + _). - but the following script succeeds + .. coqtop:: all fail - .. coqtop:: none + rewrite -[f y]/(y + _). - Restart. + but the following script succeeds .. coqtop:: all @@ -3192,7 +3157,7 @@ tactics. In a rewrite tactic of the form: -.. coqtop:: in +.. coqdoc:: rewrite occ_switch [term1]term2. @@ -3235,7 +3200,7 @@ Performing rewrite and simplification operations in a single tactic enhances significantly the concision of scripts. For instance the tactic: -.. coqtop:: in +.. coqdoc:: rewrite /my_def {2}[f _]/= my_eq //=. @@ -3250,7 +3215,7 @@ proof of basic results on natural numbers arithmetic. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3286,7 +3251,7 @@ side of the equality the user wants to rewrite. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3306,7 +3271,7 @@ the equality. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3316,7 +3281,7 @@ the equality. .. coqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. - rewrite [x + _]H. + Fail rewrite [x + _]H. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. @@ -3329,7 +3294,7 @@ Occurrence switches and redex switches .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3358,7 +3323,7 @@ repetition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3388,7 +3353,7 @@ rewrite operations prescribed by the rules on the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3397,7 +3362,7 @@ rewrite operations prescribed by the rules on the current goal. Section Test. - .. coqtop:: all + .. coqtop:: all abort Variables (a b c : nat). Hypothesis eqab : a = b. @@ -3411,10 +3376,6 @@ rewrite operations prescribed by the rules on the current goal. ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a definition: - .. coqtop:: none - - Abort. - .. coqtop:: all Definition multi1 := (eqab, eqac). @@ -3431,7 +3392,7 @@ literal matches have priority. .. example:: - .. coqtop:: all + .. coqtop:: all abort Definition d := a. Hypotheses eqd0 : d = 0. @@ -3448,11 +3409,7 @@ repeated anew. .. example:: - .. coqtop:: none - - Abort. - - .. coqtop:: all + .. coqtop:: all abort Hypothesis eq_adda_b : forall x, x + a = b. Hypothesis eq_adda_c : forall x, x + a = c. @@ -3475,10 +3432,6 @@ tactic rewrite ``(=~ multi1)`` is equivalent to ``rewrite multi1_rev``. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Hypothesis eqba : b = a. @@ -3498,7 +3451,7 @@ reasoning purposes. The library also provides one lemma per such operation, stating that both versions return the same values when applied to the same arguments: -.. coqtop:: in +.. coqdoc:: Lemma addE : add =2 addn. Lemma doubleE : double =1 doublen. @@ -3514,7 +3467,7 @@ hand side. In order to reason conveniently on expressions involving the efficient operations, we gather all these rules in the definition ``trecE``: -.. coqtop:: in +.. coqdoc:: Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). @@ -3534,7 +3487,7 @@ Anyway this tactic is *not* equivalent to .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3550,11 +3503,7 @@ Anyway this tactic is *not* equivalent to while the other tactic results in - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart abort rewrite (_ : forall x, x * 0 = 0). @@ -3572,14 +3521,14 @@ cases: + |SSR| never accepts to rewrite indeterminate patterns like: - .. coqtop:: in + .. coqdoc:: Lemma foo (x : unit) : x = tt. |SSR| will however accept the ηζ expansion of this rule: - .. coqtop:: in + .. coqdoc:: Lemma fubar (x : unit) : (let u := x in u) = tt. @@ -3588,7 +3537,7 @@ cases: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3611,11 +3560,7 @@ cases: there is no occurrence of the head symbol ``f`` of the rewrite rule in the goal. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart fail rewrite H. @@ -3625,21 +3570,13 @@ cases: occurrence), using tactic ``rewrite /f`` (for a global replacement of f by g) or ``rewrite pattern/f``, for a finer selection. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite /f H. alternatively one can override the pattern inferred from ``H`` - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite [f _]H. @@ -3658,7 +3595,7 @@ corresponding new goals will be generated. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -3666,7 +3603,7 @@ corresponding new goals will be generated. Unset Printing Implicit Defensive. Set Warnings "-notation-overridden". - .. coqtop:: all + .. coqtop:: all abort Axiom leq : nat -> nat -> bool. Notation "m <= n" := (leq m n) : nat_scope. @@ -3689,10 +3626,6 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. @@ -3729,7 +3662,7 @@ copy of any term t. However this copy is (on purpose) *not convertible* to t in the |Coq| system [#8]_. The job is done by the following construction: -.. coqtop:: in +.. coqdoc:: Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. @@ -3741,7 +3674,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require Import List. @@ -3765,7 +3698,7 @@ definition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3793,14 +3726,14 @@ some functions by the partial evaluation switch ``/=``, unless this allowed the evaluation of a condition. This is possible thanks to another mechanism of term tagging, resting on the following *Notation*: -.. coqtop:: in +.. coqdoc:: Notation "'nosimpl' t" := (let: tt := tt in t). The term ``(nosimpl t)`` simplifies to ``t`` *except* in a definition. More precisely, given: -.. coqtop:: in +.. coqdoc:: Definition foo := (nosimpl bar). @@ -3816,7 +3749,7 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to The ``nosimpl`` trick only works if no reduction is apparent in ``t``; in particular, the declaration: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl (bar x). @@ -3824,14 +3757,14 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to function, and to use the following definition, which blocks the reduction as expected: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: -.. coqtop:: in +.. coqdoc:: Definition addn := nosimpl plus. @@ -3851,7 +3784,7 @@ Congruence Because of the way matching interferes with parameters of type families, the tactic: -.. coqtop:: in +.. coqdoc:: apply: my_congr_property. @@ -3875,7 +3808,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3902,7 +3835,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3925,7 +3858,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3946,7 +3879,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4047,7 +3980,7 @@ For a quick glance at what can be expressed with the last :token:`r_pattern` consider the goal ``a = b`` and the tactic -.. coqtop:: in +.. coqdoc:: rewrite [in X in _ = X]rule. @@ -4126,7 +4059,7 @@ parentheses are required around more complex patterns. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4148,14 +4081,14 @@ patterns over simple terms, but to interpret a pattern with double parentheses as a simple term. For example, the following tactic would capture any occurrence of the term ``a in A``. -.. coqtop:: in +.. coqdoc:: set t := ((a in A)). Contextual patterns can also be used as arguments of the ``:`` tactical. For example: -.. coqtop:: in +.. coqdoc:: elim: n (n in _ = n) (refl_equal n). @@ -4165,7 +4098,7 @@ Contextual patterns in rewrite .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4246,7 +4179,7 @@ context shortcuts. The following example is taken from ``ssreflect.v`` where the ``LHS`` and ``RHS`` shortcuts are defined. -.. coqtop:: in +.. coqdoc:: Notation RHS := (X in _ = X)%pattern. Notation LHS := (X in X = _)%pattern. @@ -4254,7 +4187,7 @@ The following example is taken from ``ssreflect.v`` where the Shortcuts defined this way can be freely used in place of the trailing ``ident in term`` part of any contextual pattern. Some examples follow: -.. coqtop:: in +.. coqdoc:: set rhs := RHS. rewrite [in RHS]rule. @@ -4287,13 +4220,13 @@ The view syntax combined with the ``elim`` tactic specifies an elimination scheme to be used instead of the default, generated, one. Hence the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V. is a synonym for: -.. coqtop:: in +.. coqdoc:: intro top; elim top using V; clear top. @@ -4303,13 +4236,13 @@ Since an elimination view supports the two bookkeeping tacticals of discharge and introduction (see section :ref:`basic_tactics_ssr`), the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V: x => y. is a synonym for: -.. coqtop:: in +.. coqdoc:: elim x using V; clear x; intro y. @@ -4329,7 +4262,7 @@ generation (see section :ref:`generation_of_equations_ssr`). The following script illustrates a toy example of this feature. Let us define a function adding an element at the end of a list: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect List. Set Implicit Arguments. @@ -4367,13 +4300,13 @@ command) can be combined with the type family switches described in section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: -.. coqtop:: in +.. coqdoc:: foo_ind : forall …, forall x : T, P p1 … pm. and consider the tactic: -.. coqtop:: in +.. coqdoc:: elim/foo_ind: e1 … / en. @@ -4404,7 +4337,7 @@ Here is an example of a regular, but nontrivial, eliminator. Here is a toy example illustrating this feature. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4424,14 +4357,14 @@ Here is an example of a regular, but nontrivial, eliminator. The following tactics are all valid and perform the same elimination on this goal. - .. coqtop:: in + .. coqdoc:: elim/plus_ind: z / (plus _ z). elim/plus_ind: {z}(plus _ z). elim/plus_ind: {z}_. elim/plus_ind: z / _. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4456,7 +4389,7 @@ Here is an example of a regular, but nontrivial, eliminator. ``plus (plus x y) z`` thus instantiating the last ``_`` with ``z``. Note that the tactic: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4473,7 +4406,7 @@ Here is an example of a regular, but nontrivial, eliminator. .. coqtop:: all - elim/plus_ind: y / _. + Fail elim/plus_ind: y / _. triggers an error: in the conclusion of the ``plus_ind`` eliminator, the first argument of the predicate @@ -4486,7 +4419,7 @@ Here is an example of a truncated eliminator: Consider the goal: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4494,7 +4427,7 @@ Here is an example of a truncated eliminator: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqdoc:: Lemma test p n (n_gt0 : 0 < n) (pr_p : prime p) : p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 -> @@ -4505,7 +4438,7 @@ Here is an example of a truncated eliminator: where the type of the ``big_prop`` eliminator is - .. coqtop:: in + .. coqdoc:: big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R), Pb idx -> @@ -4518,7 +4451,7 @@ Here is an example of a truncated eliminator: inferred one is used instead: ``big[_/_]_(i <- _ | _ i) _ i``, and after the introductions, the following goals are generated: - .. coqtop:: in + .. coqdoc:: subgoal 1 is: p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 @@ -4550,7 +4483,7 @@ disjunction. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4571,7 +4504,7 @@ disjunction. This operation is so common that the tactic shell has specific syntax for it. The following scripts: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4584,13 +4517,13 @@ disjunction. Lemma test a : P (a || a) -> True. - .. coqtop:: all undo + .. coqtop:: all move=> HPa; move/P2Q: HPa => HQa. or more directly: - .. coqtop:: all undo + .. coqtop:: all restart move/P2Q=> HQa. @@ -4606,7 +4539,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4624,7 +4557,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss This view tactic performs: - .. coqtop:: in + .. coqdoc:: move=> HQ; case: {HQ}(Q2P HQ) => [HPa | HPb]. @@ -4639,7 +4572,7 @@ relevant for the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4661,14 +4594,14 @@ relevant for the current goal. the double implication into the expected simple implication. The last script is in fact equivalent to: - .. coqtop:: in + .. coqdoc:: Lemma test a b : P (a || b) -> True. move/(iffLR (PQequiv _ _)). where: - .. coqtop:: in + .. coqdoc:: Lemma iffLR P Q : (P <-> Q) -> P -> Q. @@ -4683,7 +4616,7 @@ assumption to some given arguments. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4712,7 +4645,7 @@ bookkeeping steps. The following example use the ``~~`` prenex notation for boolean negation: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4768,7 +4701,7 @@ analysis: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4785,7 +4718,7 @@ analysis .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4810,7 +4743,7 @@ decidable predicate to its boolean version. First, booleans are injected into propositions using the coercion mechanism: -.. coqtop:: in +.. coqdoc:: Coercion is_true (b : bool) := b = true. @@ -4827,7 +4760,7 @@ To get all the benefits of the boolean reflection, it is in fact convenient to introduce the following inductive predicate ``reflect`` to relate propositions and booleans: -.. coqtop:: in +.. coqdoc:: Inductive reflect (P: Prop): bool -> Type := | Reflect_true : P -> reflect P true @@ -4838,9 +4771,9 @@ logically equivalent propositions. For instance, the following lemma: -.. coqtop:: in +.. coqdoc:: - Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). + Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). relates the boolean conjunction to the logical one ``/\``. Note that in ``andP``, ``b1`` and ``b2`` are two boolean variables and the @@ -4853,20 +4786,20 @@ to the case analysis of |Coq|’s inductive types. Since the equivalence predicate is defined in |Coq| as: -.. coqtop:: in +.. coqdoc:: Definition iff (A B:Prop) := (A -> B) /\ (B -> A). where ``/\`` is a notation for ``and``: -.. coqtop:: in +.. coqdoc:: Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B. This make case analysis very different according to the way an equivalence property has been defined. -.. coqtop:: in +.. coqdoc:: Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). @@ -4875,7 +4808,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4888,11 +4821,15 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). - .. coqtop:: all undo + .. coqtop:: all case: (@andE b1 b2). - .. coqtop:: all undo + .. coqtop:: none + + Restart. + + .. coqtop:: all case: (@andP b1 b2). @@ -4912,7 +4849,7 @@ The view mechanism is compatible with reflect predicates. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4920,17 +4857,13 @@ The view mechanism is compatible with reflect predicates. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. coqtop:: all abort Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. apply/andP. Conversely - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (a b : bool) : a /\ b -> a. @@ -4950,13 +4883,13 @@ Specializing assumptions The |SSR| tactic: -.. coqtop:: in +.. coqdoc:: move/(_ term1 … termn). is equivalent to the tactic: -.. coqtop:: in +.. coqdoc:: intro top; generalize (top term1 … termn); clear top. @@ -5013,13 +4946,13 @@ If ``term`` is a double implication, then the view hint will be one of the defined view hints for implication. These hints are by default the ones present in the file ``ssreflect.v``: -.. coqtop:: in +.. coqdoc:: Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q. which transforms a double implication into the left-to-right one, or: -.. coqtop:: in +.. coqdoc:: Lemma iffRL : forall P Q, (P <-> Q) -> Q -> P. @@ -5034,7 +4967,7 @@ but they also allow complex transformation, involving negations. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5067,7 +5000,7 @@ actually uses its propositional interpretation. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5123,13 +5056,13 @@ equality, while the second term is the one applied to the right hand side. In this context, the identity view can be used when no view has to be applied: -.. coqtop:: in +.. coqdoc:: Lemma idP : reflect b1 b1. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5145,7 +5078,7 @@ In this context, the identity view can be used when no view has to be applied: The same goal can be decomposed in several ways, and the user may choose the most convenient interpretation. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5198,7 +5131,7 @@ in sequence. Both move and apply can be followed by an arbitrary number of ``/term``. The main difference between the following two tactics -.. coqtop:: in +.. coqdoc:: apply/v1/v2/v3. apply/v1; apply/v2; apply/v3. @@ -5210,7 +5143,7 @@ line would apply the view ``v2`` to all the goals generated by ``apply/v1``. Note that the NO-OP intro pattern ``-`` can be used to separate two views, making the two following examples equivalent: -.. coqtop:: in +.. coqdoc:: move=> /v1; move=> /v2. move=> /v1 - /v2. @@ -5221,7 +5154,7 @@ pass a given hypothesis to a lemma. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5280,7 +5213,7 @@ equivalences are indeed taken into account, otherwise only single looks for any notation that contains fragment as a substring. If the ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 081fef07b9..7b395900e9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -378,7 +378,7 @@ Examples: .. coqtop:: reset none - Variables (A : Prop) (B: nat -> Prop) (C: Prop). + Parameters (A : Prop) (B: nat -> Prop) (C: Prop). .. coqtop:: out @@ -730,15 +730,15 @@ Applying theorems .. coqtop:: reset in - Variable R : nat -> nat -> Prop. + Parameter R : nat -> nat -> Prop. - Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z. + Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z. - Variables n m p : nat. + Parameters n m p : nat. - Hypothesis Rnm : R n m. + Axiom Rnm : R n m. - Hypothesis Rmp : R m p. + Axiom Rmp : R m p. Consider the goal ``(R n p)`` provable using the transitivity of ``R``: @@ -749,39 +749,39 @@ Applying theorems The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: - .. coqtop:: all + .. coqtop:: all fail - Fail apply Rtrans. + apply Rtrans. A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - .. coqtop:: all undo + .. coqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: in undo + .. coqtop:: in restart apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: in undo + .. coqtop:: in restart apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: all undo + .. coqtop:: all restart apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. - .. coqtop:: all undo + .. coqtop:: all restart apply Rtrans with (2 := Rmp). @@ -789,7 +789,7 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. - .. coqtop:: all + .. coqtop:: all restart abort eapply Rtrans. @@ -2332,6 +2332,7 @@ and an explanation of the underlying technique. where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident + :name: inversion_clear This behaves as :n:`inversion` and then erases :n:`@ident` from the context. @@ -2490,47 +2491,51 @@ and an explanation of the underlying technique. *Non-dependent inversion*. - Let us consider the relation Le over natural numbers and the following - variables: + Let us consider the relation :g:`Le` over natural numbers: - .. coqtop:: all + .. coqtop:: reset in Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Let us consider the following goal: .. coqtop:: none + Section Section. + Variable P : nat -> nat -> Prop. + Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. - intros. - .. coqtop:: all + .. coqtop:: out - Show. + intros. - To prove the goal, we may need to reason by cases on H and to derive - that m is necessarily of the form (S m 0 ) for certain m 0 and that - (Le n m 0 ). Deriving these conditions corresponds to proving that the - only possible constructor of (Le (S n) m) isLeS and that we can invert - the-> in the type of LeS. This inversion is possible because Le is the - smallest set closed by the constructors LeO and LeS. + To prove the goal, we may need to reason by cases on :g:`H` and to derive + that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that + :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only + possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert + the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` + is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - .. coqtop:: undo all + .. coqtop:: all inversion_clear H. - Note that m has been substituted in the goal for (S m0) and that the - hypothesis (Le n m0) has been added to the context. + Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the + hypothesis :g:`(Le n m0)` has been added to the context. - Sometimes it is interesting to have the equality m=(S m0) in the - context to use it after. In that case we can use inversion that does + Sometimes it is interesting to have the equality :g:`m = (S m0)` in the + context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: undo all + .. coqtop:: none restart + + intros. + + .. coqtop:: all inversion H. @@ -2540,31 +2545,26 @@ and an explanation of the underlying technique. Let us consider the following goal: - .. coqtop:: reset none + .. coqtop:: none - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. - intros. - .. coqtop:: all + .. coqtop:: out - Show. + intros. - As H occurs in the goal, we may want to reason by cases on its - structure and so, we would like inversion tactics to substitute H by + As :g:`H` occurs in the goal, we may want to reason by cases on its + structure and so, we would like inversion tactics to substitute :g:`H` by the corresponding @term in constructor form. Neither :tacn:`inversion` nor - :n:`inversion_clear` do such a substitution. To have such a behavior we + :tacn:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all dependent inversion_clear H. - Note that H has been substituted by (LeS n m0 l) andm by (S m0). + Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`. .. example:: @@ -2933,6 +2933,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3315,7 +3321,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal ~0=0. unfold not. @@ -3323,10 +3329,6 @@ the conversion in hypotheses :n:`{+ @ident}`. pattern (0 = 0). fold not. - .. coqtop:: none - - Abort. - .. tacv:: fold {+ @term} Equivalent to :n:`fold @term ; ... ; fold @term`. @@ -3406,129 +3408,140 @@ Automation This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the :tacn:`assumption` - tactic, then it reduces the goal to an atomic one using intros and + tactic, then it reduces the goal to an atomic one using :tacn:`intros` and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals. - By default, auto only uses the hypotheses of the current goal and the - hints of the database named core. + By default, :tacn:`auto` only uses the hypotheses of the current goal and + the hints of the database named ``core``. + + .. warning:: + + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. + + .. tacv:: auto @num + + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. + + .. tacv:: auto with {+ @ident} + + Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. -.. tacv:: auto @num + .. note:: - Forces the search depth to be :token:`num`. The maximal search depth - is 5 by default. + Use the fake database `nocore` if you want to *not* use the `core` + database. -.. tacv:: auto with {+ @ident} + .. tacv:: auto with * - Uses the hint databases :n:`{+ @ident}` in addition to the database core. + Uses all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than the variant + where the required databases are explicitly listed. .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. -.. tacv:: auto with * + .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses all existing hint databases. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. note:: -.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + The hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @ident` + may fail where :n:`apply @ident` succeeds. - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an - inductive type, it is the collection of its constructors which are added - as hints. + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! -.. tacv:: info_auto + .. tacv:: info_auto - Behaves like auto but shows the tactics it uses to solve the goal. This - variant is very useful for getting a better understanding of automation, or - to know what lemmas/assumptions were used. + Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This + variant is very useful for getting a better understanding of automation, or + to know what lemmas/assumptions were used. -.. tacv:: debug auto - :name: debug auto + .. tacv:: debug auto + :name: debug auto - Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, - including failing paths. + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. -.. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - This is the most general form, combining the various options. + This is the most general form, combining the various options. .. tacv:: trivial :name: trivial - This tactic is a restriction of auto that is not recursive + This tactic is a restriction of :tacn:`auto` that is not recursive and tries only hints that cost `0`. Typically it solves trivial equalities like :g:`X=X`. -.. tacv:: trivial with {+ @ident} - :undocumented: - -.. tacv:: trivial with * - :undocumented: - -.. tacv:: trivial using {+ @lemma} - :undocumented: - -.. tacv:: debug trivial - :name: debug trivial - :undocumented: - -.. tacv:: info_trivial - :name: info_trivial - :undocumented: - -.. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} - :undocumented: + .. tacv:: trivial with {+ @ident} + trivial with * + trivial using {+ @lemma} + debug trivial + info_trivial + {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: .. note:: - :tacn:`auto` either solves completely the goal or else leaves it - intact. :tacn:`auto` and :tacn:`trivial` never fail. - -The following options enable printing of informative or debug information for -the :tacn:`auto` and :tacn:`trivial` tactics: + :tacn:`auto` and :tacn:`trivial` either solve completely the goal or + else succeed without changing the goal. Use :g:`solve [ auto ]` and + :g:`solve [ trivial ]` if you would prefer these tactics to fail when + they do not manage to solve the goal. .. flag:: Info Auto Debug Auto Info Trivial Debug Trivial - :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + These options enable printing of informative or debug information for + the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto :name: eauto This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, - :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` - where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + :tacn:`eauto` does try them (informally speaking, it internally uses a tactic + close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` + in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: .. coqtop:: all - Hint Resolve ex_intro. + Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. Note that ``ex_intro`` should be declared as a hint. -.. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. -:tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following options: -.. flag:: Info Eauto - Debug Eauto - :undocumented: + .. flag:: Info Eauto + Debug Eauto + :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} @@ -3670,11 +3683,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Local is useless since hints do not survive anyway to the closure of sections. - .. cmdv:: Local Hint @hint_definition - - Idem for the core database. - - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} + .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve This command adds :n:`simple apply @term` to the hint list with the head @@ -3693,16 +3702,16 @@ The general command to add a hint to some databases :n:`{+ @ident}` is typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @term cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable such that - this tactic cannot be associated to a constant. + The head symbol of the type of :n:`@term` is a bound variable + such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} + .. cmdv:: Hint Resolve {+ @term} : @ident Adds each :n:`Hint Resolve @term`. - .. cmdv:: Hint Resolve -> @term + .. cmdv:: Hint Resolve -> @term : @ident Adds the left-to-right implication of an equivalence as a hint (informally the hint will be used as :n:`apply <- @term`, although as mentionned @@ -3713,7 +3722,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term + .. cmdv:: Hint Immediate @term : @ident :name: Hint Immediate This command adds :n:`simple apply @term; trivial` to the hint list associated @@ -3729,37 +3738,37 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. exn:: @term cannot be used as a hint :undocumented: - .. cmdv:: Immediate {+ @term} + .. cmdv:: Immediate {+ @term} : @ident Adds each :n:`Hint Immediate @term`. - .. cmdv:: Hint Constructors @ident + .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors - If :n:`@ident` is an inductive type, this command adds all its constructors as + If :token:`qualid` is an inductive type, this command adds all its constructors as hints of type ``Resolve``. Then, when the conclusion of current goal has the form - :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. + :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. - .. exn:: @ident is not an inductive type - :undocumented: + .. exn:: @qualid is not an inductive type + :undocumented: - .. cmdv:: Hint Constructors {+ @ident} + .. cmdv:: Hint Constructors {+ @qualid} : @ident - Adds each :n:`Hint Constructors @ident`. + Extends the previous command for several inductive types. - .. cmdv:: Hint Unfold @qualid + .. cmdv:: Hint Unfold @qualid : @ident :name: Hint Unfold This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :n:`@ident`. + used when the head constant of the goal is :token:`qualid`. Its cost is 4. - .. cmdv:: Hint Unfold {+ @ident} + .. cmdv:: Hint Unfold {+ @qualid} - Adds each :n:`Hint Unfold @ident`. + Extends the previous command for several defined constants. - .. cmdv:: Hint Transparent {+ @qualid} - Hint Opaque {+ @qualid} + .. cmdv:: Hint Transparent {+ @qualid} : @ident + Hint Opaque {+ @qualid} : @ident :name: Hint Transparent; Hint Opaque This adds transparency hints to the database, making :n:`@qualid` @@ -3768,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) - Hint Constants %( Transparent %| Opaque %) + .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident + Hint Constants %( Transparent %| Opaque %) : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3777,7 +3786,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is overwritting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @num {? @pattern} => @tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and @@ -3788,7 +3797,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. coqtop:: in - Hint Extern 4 (~(_ = _)) => discriminate. + Hint Extern 4 (~(_ = _)) => discriminate : core. Now, when the head of the goal is a disequality, ``auto`` will try discriminate if it does not manage to solve the goal with hints with a @@ -3807,7 +3816,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Goal forall a b:list (nat * nat), {a = b} + {a <> b}. Info 1 auto with eqdec. - .. cmdv:: Hint Cut @regexp + .. cmdv:: Hint Cut @regexp : @ident :name: Hint Cut .. warning:: @@ -3841,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a98a46ba21..3e8dd25ee0 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1213,10 +1213,19 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _internal-registration-commands: + +Internal registration commands +-------------------------------- + +Due to their internal nature, the commands that are presented in this section +are not for general use. They are meant to appear only in standard libraries and +in support libraries of plug-ins. + .. _exposing-constants-to-ocaml-libraries: Exposing constants to OCaml libraries ----------------------------------------------------------------- +```````````````````````````````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 @@ -1225,5 +1234,35 @@ Exposing constants to OCaml libraries calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known where is the constant defined (file, module, library, etc.). - Due to its internal nature, this command is not for general use. It is meant - to appear only in standard libraries and in support libraries of plug-ins. + As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, + the constant is exposed to the kernel. For instance, the `Int63` module + features the following declaration: + + .. coqdoc:: + + Register bool as kernel.ind_bool. + + This makes the kernel aware of what is the type of boolean values. This + information is used for instance to define the return type of the + :g:`#int63_eq` primitive. + + .. seealso:: :ref:`primitive-integers` + +Inlining hints for the fast reduction machines +```````````````````````````````````````````````````````````````` + +.. cmd:: Register Inline @qualid + + This command gives as a hint to the reduction machines (VM and native) that + the body of the constant :n:`@qualid` should be inlined in the generated code. + +Registering primitive operations +```````````````````````````````` + +.. cmd:: Primitive @ident__1 := #@ident__2. + + Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When + running this command, the type of the primitive should be already known by + the kernel (this is achieved through this command for primitive types and + through the :cmd:`Register` command with the :g:`kernel` name-space for other + types). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 105b0445fd..e5eb7eb4f5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -181,7 +181,7 @@ rules. Some simple left factorization work has to be done. Here is an example. .. coqtop:: all Notation "x < y" := (lt x y) (at level 70). - Notation "x < y < z" := (x < y /\ y < z) (at level 70). + Fail Notation "x < y < z" := (x < y /\ y < z) (at level 70). In order to factorize the left part of the rules, the subexpression referred to by ``y`` has to be at the same level in both rules. However the @@ -486,7 +486,7 @@ Sometimes, for the sake of factorization of rules, a binder has to be parsed as a term. This is typically the case for a notation such as the following: -.. coqtop:: in +.. coqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0, x at level 99 as ident). @@ -788,9 +788,9 @@ main grammar, or from another custom entry as is the case in to indicate that ``e`` has to be parsed at level ``2`` of the grammar associated to the custom entry ``expr``. The level can be omitted, as in -.. coqtop:: in +.. coqdoc:: - Notation "[ e ]" := e (e custom expr)`. + Notation "[ e ]" := e (e custom expr). in which case Coq tries to infer it. @@ -1058,7 +1058,7 @@ Binding arguments of a constant to an interpretation scope in the scope delimited by the key ``F`` (``Rfun_scope``) and the last argument in the scope delimited by the key ``R`` (``R_scope``). - .. coqtop:: in + .. coqdoc:: Arguments plus_fct (f1 f2)%F x%R. @@ -1066,7 +1066,7 @@ Binding arguments of a constant to an interpretation scope parentheses. In the following example arguments A and B are marked as maximally inserted implicit arguments and are put into the type_scope scope. - .. coqtop:: in + .. coqdoc:: Arguments respectful {A B}%type (R R')%signature _ _. @@ -1115,6 +1115,8 @@ Binding arguments of a constant to an interpretation scope .. coqtop:: all Parameter g : bool -> bool. + Declare Scope mybool_scope. + Notation "@@" := true (only parsing) : bool_scope. Notation "@@" := false (only parsing): mybool_scope. @@ -1148,9 +1150,10 @@ Binding types of arguments to an interpretation scope can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` - .. coqtop:: in + .. coqtop:: in reset Parameter U : Set. + Declare Scope U_scope. Bind Scope U_scope with U. Parameter Uplus : U -> U -> U. Parameter P : forall T:Set, T -> U -> Prop. @@ -1575,7 +1578,7 @@ Numeral notations For example - .. coqtop:: all + .. coqtop:: all warn Check 90000. |