diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 93 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 68 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 160 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 1 |
7 files changed, 257 insertions, 117 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e56b36caad..238106b2e7 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -9,9 +9,11 @@ Short description of the tactics -------------------------------- The Psatz module (``Require Import Psatz.``) gives access to several -tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_. -It also possible to get the tactics for integers by a ``Require Import Lia``, -rationals ``Require Import Lqa`` and reals ``Require Import Lra``. +tactics for solving arithmetic goals over :math:`\mathbb{Q}`, +:math:`\mathbb{R}`, and :math:`\mathbb{Z}` but also :g:`nat` and +:g:`N`. It also possible to get the tactics for integers by a +``Require Import Lia``, rationals ``Require Import Lqa`` and reals +``Require Import Lra``. + :tacn:`lia` is a decision procedure for linear integer arithmetic; + :tacn:`nia` is an incomplete proof procedure for integer non-linear @@ -23,7 +25,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. ``n`` is an optional integer limiting the proof search depth, is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light - driver to the external prover `csdp` [#]_. Note that the `csdp` driver is + driver to the external prover `csdp` [#csdp]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts even without `csdp`. @@ -78,7 +80,7 @@ closed under the following rules: \end{array}` The following theorem provides a proof principle for checking that a -set of polynomial inequalities does not have solutions [#]_. +set of polynomial inequalities does not have solutions [#fnpsatz]_. .. _psatz_thm: @@ -111,32 +113,21 @@ and checked to be :math:`-1`. The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. - `lia`: a tactic for linear integer arithmetic --------------------------------------------- .. tacn:: lia :name: lia - This tactic offers an alternative to the :tacn:`omega` tactic. Roughly - speaking, the deductive power of lia is the combined deductive power of - :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals - that :tacn:`omega` does not solve, such as the following so-called *omega - nightmare* :cite:`TheOmegaPaper`. - -.. coqdoc:: - - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. + This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. + :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof -principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, +principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this @@ -249,21 +240,55 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. -.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with - the ``zify`` tactic. -.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by - pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may - need to manually run ``zify`` first). -.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing - the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually - run ``zify`` first). -.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and - :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the - ``Z.to_euclidean_division_equations`` tactic (you may need to manually run - ``zify`` first). -.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp -.. [#] Variants deal with equalities and strict inequalities. -.. [#] In practice, the oracle might fail to produce such a refutation. +`zify`: pre-processing of arithmetic goals +------------------------------------------ + +.. tacn:: zify + :name: zify + + This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. + By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. + :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`. + + + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + +.. cmd:: Show Zify InjTyp + :name: Show Zify InjTyp + + This command shows the list of types that can be injected into :g:`Z`. + +.. cmd:: Show Zify BinOp + :name: Show Zify BinOp + + This command shows the list of binary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify BinRel + :name: Show Zify BinRel + + This command shows the list of binary relations processed by :tacn:`zify`. + + +.. cmd:: Show Zify UnOp + :name: Show Zify UnOp + + This command shows the list of unary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify CstOp + :name: Show Zify CstOp + + This command shows the list of constants processed by :tacn:`zify`. + +.. cmd:: Show Zify Spec + :name: Show Zify Spec + + This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`. + +.. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#fnpsatz] Variants deal with equalities and strict inequalities. +.. [#mayfail] In practice, the oracle might fail to produce such a refutation. .. comment in original TeX: .. %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e698bfb66..1d0b732e7d 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including: - :cmd:`Section` will locally set the polymorphism flag inside the section. - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. This means that the universe variables (and associated - constraints) are discharged polymorphically over definitions that use - them. In other words, two definitions in the section sharing a common - variable will both get parameterized by the universes produced by the - variable declaration. This is in contrast to a “mononorphic” variable - which introduces global universes and constraints, making the two - definitions depend on the *same* global universes associated to the - variable. + polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint polymorphically, not at a single instance. @@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions. as well. Global universe names live in a separate namespace. The command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition - independently. One cannot mix polymorphic and monomorphic - declarations in the same section. - + independently. .. cmd:: Constraint @universe_constraint Polymorphic Constraint @universe_constraint @@ -510,3 +501,23 @@ underscore or by omitting the annotation to a polymorphic definition. Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. About baz. + +.. _universe-polymorphism-in-sections: + +Universe polymorphism and sections +---------------------------------- + +The universe polymorphic or monomorphic status is +attached to each individual section, and all term or universe declarations +contained inside must respect it, as described below. It is possible to nest a +polymorphic section inside a monomorphic one, but the converse is not allowed. + +:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and :cmd:`Constraint` in a section support +polymorphism. This means that the universe variables and their associated +constraints are discharged polymorphically over definitions that use +them. In other words, two definitions in the section sharing a common +variable will both get parameterized by the universes produced by the +variable declaration. This is in contrast to a “mononorphic” variable +which introduces global universes and constraints, making the two +definitions depend on the *same* global universes associated to the +variable. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index c591a1f1de..38b3c34209 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -649,6 +649,74 @@ Many bug fixes and documentation improvements, in particular: (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle). +Changes in 8.10+beta3 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + +- Fix soundness issue with template polymorphism (`#9294 + <https://github.com/coq/coq/issues/9294>`_). + + Declarations of template-polymorphic inductive types ignored the + provenance of the universes they were abstracting on and did not + detect if they should be greater or equal to :math:`\Set` in + general. Previous universes and universes introduced by the inductive + definition could have constraints that prevented their instantiation + with e.g. :math:`\Prop`, resulting in unsound instantiations later. The + implemented fix only allows abstraction over universes introduced by + the inductive declaration, and properly records all their constraints + by making them by default only :math:`>= \Prop`. It is also checked + that a template polymorphic inductive actually is polymorphic on at + least one universe. + + This prevents inductive declarations in sections to be universe + polymorphic over section parameters. For a backward compatible fix, + simply hoist the inductive definition out of the section. + An alternative is to declare the inductive as universe-polymorphic and + cumulative in a universe-polymorphic section: all universes and + constraints will be properly gathered in this case. + See :ref:`Template-polymorphism` for a detailed exposition of the + rules governing template-polymorphic types. + + To help users incrementally fix this issue, a command line option + `-no-template-check` and a global flag :flag:`Template Check` are + available to selectively disable the new check. Use at your own risk. + + (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau + and Maxime Dénès). + +**User messages** + +- Improve the ambiguous paths warning to indicate which path is ambiguous with + new one + (`#10336 <https://github.com/coq/coq/pull/10336>`_, + closes `#3219 <https://github.com/coq/coq/issues/3219>`_, + by Kazuhiko Sakaguchi). + +**Extraction** + +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). +- Fix a printing bug of OCaml extraction on dependent record projections, which + produced improper `assert false`. This change makes the OCaml extractor + internally inline record projections by default; thus the monolithic OCaml + extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not + produce record projection constants anymore except for record projections + explicitly instructed to extract, and records declared in opaque modules + (`#10577 <https://github.com/coq/coq/pull/10577>`_, + fixes `#7348 <https://github.com/coq/coq/issues/7348>`_, + by Kazuhiko Sakaguchi). + +**Standard library** + +- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons`` + (`#9379 <https://github.com/coq/coq/pull/9379>`_, + by Yishuai Li, with help of Konstantinos Kallas, + follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_, + which added ``uncons`` in 8.10+beta1). Version 8.9 ----------- diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index ef183174d7..1611e9dd52 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -70,7 +70,7 @@ and function types over these sorts. Formally, we call :math:`\Sort` the set of sorts which is defined by: .. math:: - + \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and @@ -436,7 +436,7 @@ instance the identity function over a given type :math:`T` can be written this a *reduction* (or a *conversion*) rule we call :math:`β`: .. math:: - + E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u} We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of @@ -474,14 +474,14 @@ with its value, that is to expand (or unfold) it into its value. This reduction is called δ-reduction and shows as follows. .. inference:: Delta-Local - + \WFE{\Gamma} (x:=t:T) ∈ Γ -------------- E[Γ] ⊢ x~\triangleright_Δ~t .. inference:: Delta-Global - + \WFE{\Gamma} (c:=t:T) ∈ E -------------- @@ -499,7 +499,7 @@ destroyed, this reduction differs from δ-reduction. It is called ζ-reduction and shows as follows. .. inference:: Zeta - + \WFE{\Gamma} \WTEG{u}{U} \WTE{\Gamma::(x:=u:U)}{t}{T} @@ -533,17 +533,17 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. .. math:: f ~:~ ∀ x:\Type(2),~\Type(1) - + then .. math:: λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1) - + We could not allow .. math:: λ x:\Type(1).~(f~x) ~\triangleright_η~ f - + because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. @@ -665,7 +665,7 @@ a *subtyping* relation inductively defined by: .. math:: [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ] - + respectively then .. math:: @@ -695,7 +695,7 @@ a *subtyping* relation inductively defined by: The conversion rule up to subtyping is now exactly: .. inference:: Conv - + E[Γ] ⊢ U : s E[Γ] ⊢ t : T E[Γ] ⊢ T ≤_{βδιζη} U @@ -716,13 +716,13 @@ that :math:`t_0` is :math:`λ x:T.~u_0` then one step of β-head reduction of :m .. math:: λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~ λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n ) - + Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the *β-head normal form* of :math:`t`: .. math:: t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m ) - + where :math:`v` is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some :math:`u_i` can be reducible. Similar notions of head-normal forms involving δ, ι @@ -828,7 +828,7 @@ We have to give the type of constants in a global environment :math:`E` which contains an inductive definition. .. inference:: Ind - + \WFE{Γ} \ind{p}{Γ_I}{Γ_C} ∈ E (a:A)∈Γ_I @@ -836,7 +836,7 @@ contains an inductive definition. E[Γ] ⊢ a : A .. inference:: Constr - + \WFE{Γ} \ind{p}{Γ_I}{Γ_C} ∈ E (c:C)∈Γ_C @@ -917,7 +917,7 @@ condition* for a constant :math:`X` in the following cases: + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i` + :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the positivity condition for :math:`X`. - + Strict positivity +++++++++++++++++ @@ -931,10 +931,10 @@ cases: 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 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} - + (in particular, it is not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in any of the :math:`t_i`, and the (instantiated) types of constructor @@ -998,7 +998,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]` (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} - + provided that the following side conditions hold: @@ -1052,30 +1052,10 @@ between universes for inductive types in the Type hierarchy. Template polymorphism +++++++++++++++++++++ -Inductive types can be made polymorphic over their arguments -in :math:`\Type`. - -.. flag:: Auto Template Polymorphism - - This option, enabled by default, makes every inductive type declared - at level :math:`\Type` (without annotations or hiding it behind a - definition) template polymorphic. - - This can be prevented using the ``notemplate`` attribute. - - An inductive type can be forced to be template polymorphic using the - ``template`` attribute. - - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. - -.. warn:: Automatically declaring @ident as template polymorphic. - - Warning ``auto-template`` can be used to find which types are - implicitly declared template polymorphic by :flag:`Auto Template - Polymorphism`. +Inductive types can be made polymorphic over the universes introduced by +their parameters in :math:`\Type`, if the minimal inferred sort of the +inductive declarations either mention some of those parameter universes +or is computed to be :math:`\Prop` or :math:`\Set`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. @@ -1117,10 +1097,11 @@ provided that the following side conditions hold: + 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 - :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed - (see Section :ref:`Destructors`). - + + the sorts :math:`s_i` are all introduced by the inductive + declaration and have no universe constraints beside being greater + than or equal to :math:`\Prop`, and such that all + eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, + are allowed (see Section :ref:`Destructors`). Notice that if :math:`I_j~q_1 … q_r` is typable using the rules **Ind-Const** and @@ -1141,6 +1122,61 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or :math:`C_i~q_1 … q_r` is mapped to the names chosen in the specific instance of :math:`\ind{p}{Γ_I}{Γ_C}`. +.. warning:: + + The restriction that sorts are introduced by the inductive + declaration prevents inductive types declared in sections to be + template-polymorphic on universes introduced previously in the + section: they cannot parameterize over the universes introduced with + section variables that become parameters at section closing time, as + these may be shared with other definitions from the same section + which can impose constraints on them. + +.. flag:: Auto Template Polymorphism + + This option, enabled by default, makes every inductive type declared + at level :math:`\Type` (without annotations or hiding it behind a + definition) template polymorphic if possible. + + This can be prevented using the ``notemplate`` attribute. + +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + + An inductive type can be forced to be template polymorphic using the + ``template`` attribute: it should then fullfill the criterion to + be template polymorphic or an error is raised. + +.. exn:: Inductive @ident cannot be made template polymorphic. + + This error is raised when the `#[universes(template)]` attribute is + on but the inductive cannot be made polymorphic on any universe or be + inferred to live in :math:`\Prop` or :math:`\Set`. + + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. + +.. flag:: Template Check + + Unsetting option :flag:`Template Check` disables the check of + locality of the sorts when abstracting the inductive over its + parameters. This is a deprecated and *unsafe* flag that can introduce + inconsistencies, it is only meant to help users incrementally update + code from Coq versions < 8.10 which did not implement this check. + The `Coq89.v` compatibility file sets this flag globally. A global + ``-no-template-check`` command line option is also available. Use at + your own risk. Use of this flag is recorded in the typing flags + associated to a definition but is *not* supported by the |Coq| + checker (`coqchk`). It will appear in :g:`Print Assumptions` and + :g:`About @ident` output involving inductive declarations that were + (potentially unsoundly) assumed to be template polymorphic. + + In practice, the rule **Ind-Family** is used by |Coq| only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over @@ -1154,10 +1190,10 @@ inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicativ Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_), and otherwise in the Type hierarchy. -Note that the side-condition about allowed elimination sorts in the -rule **Ind-Family** is just to avoid to recompute the allowed elimination -sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As -an example, let us consider the following definition: +Note that the side-condition about allowed elimination sorts in the rule +**Ind-Family** avoids to recompute the allowed elimination sorts at each +instance of a pattern matching (see Section :ref:`Destructors`). As an +example, let us consider the following definition: .. example:: @@ -1320,7 +1356,7 @@ using the syntax: \Match~m~\as~x~\In~I~\_~a~\return~P~\with~ (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend - + The :math:`\as` part can be omitted if either the result type does not depend on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m` can occur in :math:`P` where it is considered a bound variable). The :math:`\In` part @@ -1360,7 +1396,7 @@ There is no restriction on the sort of the predicate to be eliminated. ----------------------- [I:∀ x:A,~A′|∀ x:A,~B′] - + .. inference:: Set & Type s_1 ∈ \{\Set,\Type(j)\} @@ -1376,7 +1412,7 @@ is also of sort :math:`\Prop` or is of the morally smaller sort :math:`\SProp`. .. inference:: Prop - + s ∈ \{\SProp,\Prop\} -------------------- [I:\Prop|I→s] @@ -1404,7 +1440,7 @@ the proof of :g:`or A B` is not accepted: Fail Definition choice (A B: Prop) (x:or A B) := match x with or_introl _ _ a => true | or_intror _ _ b => false end. - + From the computational point of view, the structure of the proof of :g:`(or A B)` in this term is needed for computing the boolean value. @@ -1441,7 +1477,7 @@ this type. :math:`\Prop` for which more eliminations are allowed. .. inference:: Prop-extended - + I~\kw{is an empty or singleton definition} s ∈ \Sort ------------------------------------- @@ -1589,7 +1625,7 @@ An ι-redex is a term of the following form: .. math:: \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) - + with :math:`c_{p_i}` the :math:`i`-th constructor of the inductive type :math:`I` with :math:`r` parameters. @@ -1636,7 +1672,7 @@ Typing rule The typing rule is the expected one for a fixpoint. .. inference:: Fix - + (E[Γ] ⊢ A_i : s_i )_{i=1… n} (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} ------------------------------------------------------- @@ -1749,7 +1785,7 @@ The reduction for fixpoints is: .. math:: (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} - + when :math:`a_{k_i}` starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction for primitive recursive operators. The following reductions are now @@ -1808,11 +1844,11 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} {\subst{Γ}{c′}{(c′~c)}}} - + .. math:: \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}} - + .. math:: \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ @@ -1853,7 +1889,7 @@ One can consequently derive the following property. .. _First-pruning-property: .. inference:: First pruning property: - + \WF{E;~c:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- @@ -1933,5 +1969,3 @@ impredicative system for sort :math:`\Set` become: s ∈ \{\Type(i)\} ---------------- [I:\Set|I→ s] - - diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 7d6171285e..b1f392c337 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -179,10 +179,13 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -Notice that these settings are saved in the file `.coqiderc` of your -home directory. +Notice that these settings are saved in the file ``coqiderc`` in the +``coq`` subdirectory of the user configuration directory which +is the value of ``$XDG_CONFIG_HOME`` if this environment variable is +set and which otherwise is ``$HOME/.config/``. -A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It +A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in +the same ``coq`` subdirectory of the user configuration directory. It is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release @@ -259,8 +262,9 @@ Adding custom bindings ~~~~~~~~~~~~~~~~~~~~~~ To extend the default set of bindings, create a file named ``coqide.bindings`` -and place it in the same folder as ``coqide.keys``. On Linux, this would be -the folder ``~/.config/coq``. The file `coqide.bindings` should contain one +and place it in the same folder as ``coqide.keys``. This would be +the folder ``$XDG_CONFIG_HOME/coq``, defaulting to ``~/.config/coq`` +if ``XDG_CONFIG_HOME`` is unset. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 554f6bf230..47ecfb9db0 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -522,10 +522,7 @@ of your project. (flags :standard -warn-error -3-9-27-32-33-50) (libraries coq.plugins.cc coq.plugins.extraction)) - (rule - (targets g_equations.ml) - (deps (:pp-file g_equations.mlg)) - (action (run coqpp %{pp-file}))) + (coq.pp (modules g_equations)) And a Coq-specific part that depends on it via the ``libraries`` field: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c391cc949d..2885d6dc33 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -627,6 +627,7 @@ file is a particular case of module called *library file*. as ``Export``. .. cmdv:: From @dirpath Require @qualid + :name: From ... Require ... This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` |