diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 81 |
3 files changed, 74 insertions, 19 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..cc5d9d6205 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -533,10 +533,10 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and @@ -678,7 +678,7 @@ form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as :math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an -application. We say then that :math:`t~0` is the *head of* :math:`t`. If we assume +application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: .. math:: @@ -771,8 +771,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \evenS &:& \forall n, \odd~n → \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n → \odd~(\kw{S}~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 636144e0c8..9dae7fd102 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -606,7 +606,7 @@ for several ways of defining a function *and other useful related objects*, namely: an induction principle that reflects the recursive structure of the function (see :tacn:`function induction`) and its fixpoint equality. The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must +similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not necessarily be *structurally* decreasing. The point of the {} annotation is to name the decreasing argument *and* to describe which kind of diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index daf34500bf..1a33a9a46e 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -522,7 +522,7 @@ The Vernacular ============== .. productionlist:: coq - decorated-sentence : [`decoration`] `sentence` + decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` : | `definition` : | `inductive` @@ -1112,6 +1112,59 @@ co-inductive definitions are also allowed. object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in Section :ref:`cofixpoint`. +Caveat +++++++ + +The ability to define co-inductive types by constructors, hereafter called +*positive co-inductive types*, is known to break subject reduction. The story is +a bit long: this is due to dependent pattern-matching which implies +propositional η-equality, which itself would require full η-conversion for +subject reduction to hold, but full η-conversion is not acceptable as it would +make type-checking undecidable. + +Since the introduction of primitive records in Coq 8.5, an alternative +presentation is available, called *negative co-inductive types*. This consists +in defining a co-inductive type as a primitive record type through its +projections. Such a technique is akin to the *co-pattern* style that can be +found in e.g. Agda, and preserves subject reduction. + +The above example can be rewritten in the following way. + +.. coqtop:: all + + Set Primitive Projections. + CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. + CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_hd : hd s1 = hd s2; + eqst_tl : EqSt (tl s1) (tl s2); + }. + +Some properties that hold over positive streams are lost when going to the +negative presentation, typically when they imply equality over streams. +For instance, propositional η-equality is lost when going to the negative +presentation. It is nonetheless logically consistent to recover it through an +axiom. + +.. coqtop:: all + + Axiom Stream_eta : forall s: Stream, s = cons (hs 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 +equality: + +.. coqtop:: all + + Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. + +As of Coq 8.9, it is now advised to use negative co-inductive types rather than +their positive counterparts. + +.. seealso:: + :ref:`primitive_projections` for more information about negative + records and primitive projections. + + Definition of recursive functions --------------------------------- @@ -1422,15 +1475,6 @@ using the keyword :cmd:`Qed`. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the current asserted statement into an axiom and exit the proof editing mode. -.. [1] - This is similar to the expression “*entry* :math:`\{` sep *entry* - :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* - :math:`)`\ \*” in the syntax of regular expressions. - -.. [2] - Except if the inductive type is empty in which case there is no - equation that can be used to infer the return type. - .. _gallina-attributes: Attributes @@ -1438,7 +1482,7 @@ Attributes Any vernacular command can be decorated with a list of attributes, enclosed between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) -and separated by commas ``,``. +and separated by commas ``,``. Multiple space-separated blocks may be provided. Each attribute has a name (an identifier) and may have a value. A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), @@ -1466,12 +1510,14 @@ the following attributes names are recognized: This attribute can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string. @string. + :undocumented: .. warn:: Tactic Notation @qualid is deprecated since @string. @string. + :undocumented: -Here are a few examples: +.. example:: -.. coqtop:: all reset + .. coqtop:: all reset From Coq Require Program. #[program] Definition one : nat := S _. @@ -1486,3 +1532,12 @@ Here are a few examples: Proof. now foo. Abort. + +.. [1] + This is similar to the expression “*entry* :math:`\{` sep *entry* + :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* + :math:`)`\ \*” in the syntax of regular expressions. + +.. [2] + Except if the inductive type is empty in which case there is no + equation that can be used to infer the return type. |