diff options
Diffstat (limited to 'doc')
20 files changed, 323 insertions, 156 deletions
diff --git a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst new file mode 100644 index 0000000000..87e89a70f1 --- /dev/null +++ b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst @@ -0,0 +1,30 @@ +- 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). diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst new file mode 100644 index 0000000000..fba09f5e87 --- /dev/null +++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst @@ -0,0 +1,5 @@ +- White spaces are forbidden in the “&ident” syntax for ltac2 references + that are described in :ref:`ltac2_built-in-quotations` + (`#10324 <https://github.com/coq/coq/pull/10324>`_, + fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, + authored by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst new file mode 100644 index 0000000000..ef7adde801 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst @@ -0,0 +1,4 @@ +- Adding unsafe commands to enable/disable guard checking, positivity checking + and universes checking (providing a local `-type-in-type`). + See :ref:`controlling-typing-flags`. + (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). diff --git a/doc/changelog/08-tools/10577-extraction-dependent-projections.rst b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst new file mode 100644 index 0000000000..4d52355542 --- /dev/null +++ b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst @@ -0,0 +1,9 @@ +- 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). diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst new file mode 100644 index 0000000000..ab625b9e03 --- /dev/null +++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst @@ -0,0 +1,4 @@ +- Removes deprecated modules `Coq.ZArith.Zlogarithm` + and `Coq.ZArith.Zsqrt_compat` + (#9881 <https://github.com/coq/coq/pull/9811> + by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst new file mode 100644 index 0000000000..d69056fc2f --- /dev/null +++ b/doc/changelog/10-standard-library/10445-constructive-reals.rst @@ -0,0 +1,12 @@ +- New module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers. Classical real numbers are now defined + as a quotient of these constructive real numbers, which significantly reduces + the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`), + while preserving backward compatibility. + + Futhermore, the new axioms for classical real numbers include the limited + principle of omniscience (`sig_forall_dec`), which is a logical principle + instead of an ad hoc property of the real numbers. + + See `#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters. diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst new file mode 100644 index 0000000000..864c4e6a7e --- /dev/null +++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst @@ -0,0 +1,6 @@ +- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the + :g:`List` module. + + See `#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash. diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune index 79d561061d..ab9b4dd531 100644 --- a/doc/plugin_tutorial/tuto0/src/dune +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p0) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto0.ml) - (deps (:pp-file g_tuto0.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto0)) diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune index cf9c674b14..054d5ecd26 100644 --- a/doc/plugin_tutorial/tuto1/src/dune +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p1) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto1.ml) - (deps (:pp-file g_tuto1.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto1)) diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index 68ddd13947..8c4b04b1ae 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p2) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto2.ml) - (deps (:pp-file g_tuto2.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto2)) diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune index ba6d8b288f..678dd71328 100644 --- a/doc/plugin_tutorial/tuto3/src/dune +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -4,7 +4,4 @@ (flags :standard -warn-error -3) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto3.ml) - (deps (:pp-file g_tuto3.mlg)) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto3)) diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 903ee115c9..cdb7ea834f 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -162,7 +162,7 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the generation and checking of the proof objects. The ``-quick`` flag can be -passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, the ``quick`` target can be used to compile all files using the ``-quick`` flag. @@ -182,7 +182,7 @@ running ``coqc`` as usual. Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All .vio files can be processed in parallel, hence this alternative might -be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +be faster. The command ``coqc -schedule-vio2vo 2 a b c`` can be used to obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and ``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target can be used for that purpose. Variable ``J`` should be set to the number @@ -197,7 +197,7 @@ There is an extra, possibly even faster, alternative: just check the proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This is possibly faster because all the proof tasks are independent, hence one can further partition the job to be done between workers. The -``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +``coqc -schedule-vio-checking 6 a b c`` command can be used to obtain a good scheduling for 6 workers to check all the proof tasks of ``a.vio``, ``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6ac55e7bf4..c591a1f1de 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -894,8 +894,8 @@ Standard Library and other packages. They are still delimited by `%int` and `%uint`. - Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, - and `int31` are no longer available merely by `Require`ing the files - that define the inductives. You must `Import` `Coq.Strings.String.StringSyntax` + and `int31` are no longer available merely by :cmd:`Require`\ing the files + that define the inductives. You must :cmd:`Import` `Coq.Strings.String.StringSyntax` (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and 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/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index acf68e9fd2..dc4f91e66b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -260,10 +260,7 @@ To eliminate the (co-)inductive type, one must use its defined primitive project For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the -:flag:`Printing Primitive Projection Parameters` flag. Further compatibility -printing can be deactivated thanks to the ``Printing Primitive Projection -Compatibility`` option which governs the printing of pattern matching -over primitive records. +:flag:`Printing Primitive Projection Parameters` flag. There are currently two ways to introduce primitive records types: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 91dfa34494..2cbd41af8b 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -778,7 +778,8 @@ Simple inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. + the inductive definition. The positivity checking can be disabled using + the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. 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/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index ceaa2775bf..045d028d02 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -17,16 +17,16 @@ Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: - is error-prone and fragile - has an intricate implementation -Following the need of users that start developing huge projects relying +Following the need of users who are developing huge projects relying critically on Ltac, we believe that we should offer a proper modern language that features at least the following: - at least informal, predictable semantics -- a typing system -- standard programming facilities (i.e. datatypes) +- a type system +- standard programming facilities (e.g., datatypes) This new language, called Ltac2, is described in this chapter. It is still -experimental but we encourage nonetheless users to start testing it, +experimental but we nonetheless encourage users to start testing it, especially wherever an advanced tactic language is needed. The previous implementation of Ltac, described in the previous chapter, will be referred to as Ltac1. @@ -36,9 +36,9 @@ as Ltac1. General design -------------- -There are various alternatives to Ltac1, such that Mtac or Rtac for instance. -While those alternatives can be quite distinct from Ltac1, we designed -Ltac2 to be closest as reasonably possible to Ltac1, while fixing the +There are various alternatives to Ltac1, such as Mtac or Rtac for instance. +While those alternatives can be quite different from Ltac1, we designed +Ltac2 to be as close as reasonably possible to Ltac1, while fixing the aforementioned defects. In particular, Ltac2 is: @@ -47,11 +47,11 @@ In particular, Ltac2 is: * a call-by-value functional language * with effects - * together with Hindley-Milner type system + * together with the Hindley-Milner type system - a language featuring meta-programming facilities for the manipulation of Coq-side terms -- a language featuring notation facilities to help writing palatable scripts +- a language featuring notation facilities to help write palatable scripts We describe more in details each point in the remainder of this document. @@ -77,7 +77,7 @@ Sticking to a standard ML type system can be considered somewhat weak for a meta-language designed to manipulate Coq terms. In particular, there is no way to statically guarantee that a Coq term resulting from an Ltac2 computation will be well-typed. This is actually a design choice, motivated -by retro-compatibility with Ltac1. Instead, well-typedness is deferred to +by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are provided with an ill-typed term. @@ -92,7 +92,7 @@ Type Syntax ~~~~~~~~~~~ At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. +close to OCaml. Types follow the simply-typed syntax of OCaml. The non-terminal :production:`lident` designates identifiers starting with a lowercase. @@ -122,7 +122,7 @@ Built-in types include: Type declarations ~~~~~~~~~~~~~~~~~ -One can define new types by the following commands. +One can define new types with the following commands. .. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident :name: Ltac2 Type @@ -149,7 +149,7 @@ One can define new types by the following commands. Variants are sum types defined by constructors and eliminated by pattern-matching. They can be recursive, but the `rec` flag must be - explicitly set. Pattern-maching must be exhaustive. + explicitly set. Pattern matching must be exhaustive. Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `rec` flag is set. @@ -158,15 +158,15 @@ One can define new types by the following commands. Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example - is the standard `exn` type. Pattern-matching must always include a catch-all - clause. They can be extended by this command. + is the standard `exn` type. Pattern matching on open variants must always include a catch-all + clause. They can be extended with this command. Term Syntax ~~~~~~~~~~~ The syntax of the functional fragment is very close to the one of Ltac1, except that it adds a true pattern-matching feature, as well as a few standard -constructions from ML. +constructs from ML. .. productionlist:: coq ltac2_var : `lident` @@ -202,7 +202,7 @@ constructions from ML. In practice, there is some additional syntactic sugar that allows e.g. to bind a variable and match on it at the same time, in the usual ML style. -There is a dedicated syntax for list and array literals. +There is dedicated syntax for list and array literals. .. note:: @@ -217,7 +217,7 @@ Ltac Definitions This command defines a new global Ltac2 value. For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, i.e. a function, a constant or a pure constructor recursively applied to + value, that is, a function, a constant or a pure constructor recursively applied to values. If ``rec`` is set, the tactic is expanded into a recursive binding. @@ -247,7 +247,7 @@ if ever we implement native compilation. The expected equations are as follows:: (t any term, V values, C constructor) Note that call-by-value reduction is already a departure from Ltac1 which uses -heuristics to decide when evaluating an expression. For instance, the following +heuristics to decide when to evaluate an expression. For instance, the following expressions do not evaluate the same way in Ltac1. :n:`foo (idtac; let x := 0 in bar)` @@ -255,7 +255,7 @@ expressions do not evaluate the same way in Ltac1. :n:`foo (let x := 0 in bar)` Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk -not to compute the argument, and :n:`foo` would have e.g. type +to not compute the argument, and :n:`foo` would have e.g. type :n:`(unit -> unit) -> unit`. :n:`foo (fun () => let x := 0 in bar)` @@ -263,19 +263,19 @@ not to compute the argument, and :n:`foo` would have e.g. type Typing ~~~~~~ -Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there +Typing is strict and follows the Hindley-Milner system. Unlike Ltac1, there are no type casts at runtime, and one has to resort to conversion functions. See notations though to make things more palatable. -In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but -one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`, +In this setting, all the usual argument-free tactics have type :n:`unit -> unit`, but +one can return a value of type :n:`t` thanks to terms of type :n:`unit -> t`, or take additional arguments. Effects ~~~~~~~ Effects in Ltac2 are straightforward, except that instead of using the -standard IO monad as the ambient effectful world, Ltac2 is going to use the +standard IO monad as the ambient effectful world, Ltac2 is has a tactic monad. Note that the order of evaluation of application is *not* specified and is @@ -288,15 +288,15 @@ Intuitively a thunk of type :n:`unit -> 'a` can do the following: - It can perform non-backtracking IO like printing and setting mutable variables - It can fail in a non-recoverable way -- It can use first-class backtrack. The proper way to figure that is that we - morally have the following isomorphism: +- It can use first-class backtracking. One way to think about this is that + thunks are isomorphic to this type: :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` i.e. thunks can produce a lazy list of results where each tail is waiting for a continuation exception. -- It can access a backtracking proof state, made out amongst other things of +- It can access a backtracking proof state, consisting among other things of the current evar assignation and the list of goals under focus. -We describe more thoroughly the various effects existing in Ltac2 hereafter. +We now describe more thoroughly the various effects in Ltac2. Standard IO +++++++++++ @@ -315,28 +315,28 @@ Fatal errors ++++++++++++ The Ltac2 language provides non-backtracking exceptions, also known as *panics*, -through the following primitive in module `Control`.:: +through the following primitive in module `Control`:: val throw : exn -> 'a Unlike backtracking exceptions from the next section, this kind of error is never caught by backtracking primitives, that is, throwing an exception -destroys the stack. This is materialized by the following equation, where `E` -is an evaluation context.:: +destroys the stack. This is codified by the following equation, where `E` +is an evaluation context:: E[throw e] ≡ throw e (e value) -There is currently no way to catch such an exception and it is a design choice. -There might be at some future point a way to catch it in a brutal way, -destroying all backtrack and return values. +There is currently no way to catch such an exception, which is a deliberate design choice. +Eventually there might be a way to catch it and +destroy all backtrack and return values. -Backtrack -+++++++++ +Backtracking +++++++++++++ In Ltac2, we have the following backtracking primitives, defined in the -`Control` module.:: +`Control` module:: Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. @@ -344,7 +344,7 @@ In Ltac2, we have the following backtracking primitives, defined in the val plus : (unit -> 'a) -> (exn -> 'a) -> 'a val case : (unit -> 'a) -> ('a * (exn -> 'a)) result -If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is +If one views thunks as lazy lists, then `zero` is the empty list and `plus` is list concatenation, while `case` is pattern-matching. The backtracking is first-class, i.e. one can write @@ -376,8 +376,8 @@ represent several goals, including none. Thus, there is no such thing as *the current goal*. Goals are naturally ordered, though. It is natural to do the same in Ltac2, but we must provide a way to get access -to a given goal. This is the role of the `enter` primitive, that applies a -tactic to each currently focused goal in turn.:: +to a given goal. This is the role of the `enter` primitive, which applies a +tactic to each currently focused goal in turn:: val enter : (unit -> unit) -> unit @@ -427,6 +427,8 @@ In general, quotations can be introduced in terms using the following syntax, wh .. prodn:: ltac2_term += @ident : ( @quotentry ) +.. _ltac2_built-in-quotations: + Built-in quotations +++++++++++++++++++ @@ -439,10 +441,11 @@ The current implementation recognizes the following built-in quotations: holes at runtime (type ``Init.constr`` as well). - ``pattern``, which parses Coq patterns and produces a pattern used for term matching (type ``Init.pattern``). -- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names +- ``reference``, which parses either a :n:`@qualid` or :n:`&@ident`. Qualified names are globalized at internalization into the corresponding global reference, while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a - ``Std.reference``. + ``Std.reference``. There shall be no white space between the ampersand + symbol (``&``) and the identifier (:n:`@ident`). The following syntactic sugar is provided for two common cases. @@ -452,9 +455,9 @@ The following syntactic sugar is provided for two common cases. Strict vs. non-strict mode ++++++++++++++++++++++++++ -Depending on the context, quotations producing terms (i.e. ``constr`` or +Depending on the context, quotation-producing terms (i.e. ``constr`` or ``open_constr``) are not internalized in the same way. There are two possible -modes, respectively called the *strict* and the *non-strict* mode. +modes, the *strict* and the *non-strict* mode. - In strict mode, all simple identifiers appearing in a term quotation are required to be resolvable statically. That is, they must be the short name of @@ -467,7 +470,7 @@ modes, respectively called the *strict* and the *non-strict* mode. of the term at runtime will fail if there is no such variable in the dynamic context. -Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict +Strict mode is enforced by default, such as for all Ltac2 definitions. Non-strict mode is only set when evaluating Ltac2 snippets in interactive proof mode. The rationale is that it is cumbersome to explicitly add ``&`` interactively, while it is expected that global tactics enforce more invariants on their code. @@ -490,12 +493,12 @@ for their side-effects. Semantics +++++++++ -Interpretation of a quoted Coq term is done in two phases, internalization and +A quoted Coq term is interpreted in two phases, internalization and evaluation. -- Internalization is part of the static semantics, i.e. it is done at Ltac2 +- Internalization is part of the static semantics, that is, it is done at Ltac2 typing time. -- Evaluation is part of the dynamic semantics, i.e. it is done when +- Evaluation is part of the dynamic semantics, that is, it is done when a term gets effectively computed by Ltac2. Note that typing of Coq terms is a *dynamic* process occurring at Ltac2 @@ -672,7 +675,7 @@ at parsing time. Scopes are described using a form of S-expression. .. prodn:: ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } -A few scopes contain antiquotation features. For sake of uniformity, all +A few scopes contain antiquotation features. For the sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. The following scopes are built-in. @@ -713,15 +716,15 @@ The following scopes are built-in. - :n:`self`: - + parses a Ltac2 expression at the current level and return it as is. + + parses a Ltac2 expression at the current level and returns it as is. - :n:`next`: - + parses a Ltac2 expression at the next level and return it as is. + + parses a Ltac2 expression at the next level and returns it as is. - :n:`tactic(n = @int)`: - + parses a Ltac2 expression at the provided level :n:`n` and return it as is. + + parses a Ltac2 expression at the provided level :n:`n` and returns it as is. - :n:`thunk(@ltac2_scope)`: @@ -747,7 +750,7 @@ The following scopes are built-in. out of the parsed values in the same order. As an optimization, all subscopes of the form :n:`STRING` are left out of the returned tuple, instead of returning a useless unit value. It is forbidden for the various - subscopes to refer to the global entry using self or next. + subscopes to refer to the global entry using :n:`self` or :n:`next`. A few other specific scopes exist to handle Ltac1-like syntax, but their use is discouraged and they are thus not documented. @@ -758,7 +761,7 @@ planned. Notations ~~~~~~~~~ -The Ltac2 parser can be extended by syntactic notations. +The Ltac2 parser can be extended with syntactic notations. .. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation @@ -793,10 +796,10 @@ Abbreviations .. cmdv:: Ltac2 Notation @lident := @ltac2_term - This command introduces a special kind of notations, called abbreviations, + This command introduces a special kind of notation, called an abbreviation, that is designed so that it does not add any parsing rules. It is similar in spirit to Coq abbreviations, insofar as its main purpose is to give an - absolute name to a piece of pure syntax, which can be transparently referred + absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition. The abbreviation can then be manipulated just as a normal Ltac2 definition, @@ -851,7 +854,7 @@ corresponding code for its side effects. In particular, it cannot return values, and the quotation has type :n:`unit`. Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can -be done via an explicit annotation to the :n:`ltac1` quotation. +be done with an explicit annotation on the :n:`ltac1` quotation. .. productionlist:: coq ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` ) @@ -888,7 +891,7 @@ Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation instead. Note that the tactic expression is evaluated eagerly, if one wants to use it as -an argument to a Ltac1 function, she has to resort to the good old +an argument to a Ltac1 function, one has to resort to the good old :n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately and won't print anything. @@ -923,8 +926,8 @@ Due to conflicts, a few syntactic rules have changed. - The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`. - Levels of a few operators have been revised. Some tacticals now parse as if - they were a normal function, i.e. one has to put parentheses around the - argument when it is complex, e.g an abstraction. List of affected tacticals: + they were normal functions. Parentheses are now required around complex + arguments, such as abstractions. The tacticals affected are: :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`. - :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen, :n:`(fun () => ())` if you want a thunk (see next section), or use printing @@ -1010,4 +1013,4 @@ Exception catching Ltac2 features a proper exception-catching mechanism. For this reason, the Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it, has been removed. Now exceptions are preserved by all tacticals, and it is -your duty to catch them and reraise them depending on your use. +your duty to catch them and re-raise them as needed. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 774732825a..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` @@ -1204,6 +1205,79 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _controlling-typing-flags: + +Controlling Typing Flags +---------------------------- + +.. flag:: Guard Checking + + This option can be used to enable/disable the guard checking of + fixpoints. Warning: this can break the consistency of the system, use at your + own risk. Decreasing argument can still be specified: the decrease is not checked + anymore but it still affects the reduction of the term. Unchecked fixpoints are + printed by :cmd:`Print Assumptions`. + +.. flag:: Positivity Checking + + This option can be used to enable/disable the positivity checking of inductive + types and the productivity checking of coinductive types. Warning: this can + break the consistency of the system, use at your own risk. Unchecked + (co)inductive types are printed by :cmd:`Print Assumptions`. + +.. flag:: Universe Checking + + This option can be used to enable/disable the checking of universes, providing a + form of "type in type". Warning: this breaks the consistency of the system, use + at your own risk. Constants relying on "type in type" are printed by + :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line + argument (see :ref:`command-line-options`). + +.. cmd:: Print Typing Flags + + Print the status of the three typing flags: guard checking, positivity checking + and universe checking. + +.. example:: + + .. coqtop:: all reset + + Unset Guard Checking. + + Print Typing Flags. + + Fixpoint f (n : nat) : False + := f n. + + Fixpoint ackermann (m n : nat) {struct m} : nat := + match m with + | 0 => S n + | S m => + match n with + | 0 => ackermann m 1 + | S n => ackermann m (ackermann (S m) n) + end + end. + + Print Assumptions ackermann. + + Note that the proper way to define the Ackermann function is to use + an inner fixpoint: + + .. coqtop:: all reset + + Fixpoint ack m := + fix ackm n := + match m with + | 0 => S n + | S m' => + match n with + | 0 => ack m' 1 + | S n' => ack m' (ackm n') + end + end. + + .. _internal-registration-commands: Internal registration commands diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a561de1d0c..cc91776a4d 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -181,14 +181,12 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v - theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v @@ -516,7 +514,11 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Reals/Rdefinitions.v + theories/Reals/ConstructiveReals.v + theories/Reals/ConstructiveCauchyReals.v theories/Reals/Raxioms.v + theories/Reals/ConstructiveRIneq.v + theories/Reals/ConstructiveRealsLUB.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -561,6 +563,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v + theories/Reals/ConstructiveRcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v |