diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 41 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 35 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 10 |
4 files changed, 62 insertions, 29 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 98e81ebc65..3d3a1b11b1 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -96,8 +96,9 @@ constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the acyclicity of the graph of constraints -results in a Universe inconsistency error (see also Section -:ref:`printing-universes`). +results in a Universe inconsistency error. + +.. seealso:: Section :ref:`printing-universes`. .. _Terms: @@ -723,6 +724,7 @@ each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{ the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). .. example:: + The declaration for parameterized lists is: .. math:: @@ -741,11 +743,12 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is | cons : A -> list A -> list A. .. example:: + The declaration for a mutual inductive definition of tree and forest is: .. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + \ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} {\left[\begin{array}{rcl} \node &:& \forest → \tree\\ \emptyf &:& \forest\\ @@ -763,10 +766,11 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is | consf : tree -> forest -> forest. .. example:: + The declaration for a mutual inductive definition of even and odd is: .. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ @@ -778,7 +782,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is .. coqtop:: in - Inductive even : nat -> prop := + Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) with odd : nat -> prop := @@ -811,6 +815,7 @@ contains an inductive declaration. E[Γ] ⊢ c : C .. example:: + Provided that our environment :math:`E` contains inductive definitions we showed before, these two inference rules above enable us to conclude that: @@ -919,6 +924,7 @@ condition* for a constant :math:`X` in the following cases: .. example:: + For instance, if one considers the following variant of a tree type branching over the natural numbers: @@ -961,7 +967,7 @@ 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[Γ_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}}{Γ} @@ -985,6 +991,7 @@ the Type hierarchy. .. example:: + It is well known that the existential quantifier can be encoded as an inductive definition. The following declaration introduces the second- order existential quantifier :math:`∃ X.P(X)`. @@ -1019,7 +1026,7 @@ Template polymorphism +++++++++++++++++++++ Inductive types declared in :math:`\Type` are polymorphic over their arguments -in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +in :math:`\Type`. 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`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the @@ -1102,6 +1109,7 @@ sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). A an example, let us consider the following definition: .. example:: + .. coqtop:: in Inductive option (A:Type) : Type := @@ -1118,6 +1126,7 @@ if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not se if set in :math:`\Prop`. .. example:: + .. coqtop:: all Check (fun A:Set => option A). @@ -1126,6 +1135,7 @@ if set in :math:`\Prop`. Here is another example. .. example:: + .. coqtop:: in Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. @@ -1136,6 +1146,7 @@ none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three k eliminations schemes are allowed. .. example:: + .. coqtop:: all Check (fun A:Set => prod A). @@ -1242,7 +1253,7 @@ In this expression, if :math:`m` eventually happens to evaluate to and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the :math:`u_1 … u_{p_i}` according to the ι-reduction. -Actually, for type-checking a :math:`\Match…\with…\endkw` expression we also need +Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need to know the predicate P to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` @@ -1324,6 +1335,7 @@ the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, a logical disjunction :math:`A ∨ B` is defined inductively by: .. example:: + .. coqtop:: in Inductive or (A B:Prop) : Prop := @@ -1334,6 +1346,7 @@ The following definition which computes a boolean value by case over the proof of :g:`or A B` is not accepted: .. example:: + .. coqtop:: all Fail Definition choice (A B: Prop) (x:or A B) := @@ -1357,6 +1370,7 @@ property which are provably different, contradicting the proof- irrelevance property which is sometimes a useful axiom: .. example:: + .. coqtop:: all Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -1385,11 +1399,12 @@ arguments of this constructor have type :math:`\Prop`. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort :math:`s` is legal. Typical examples are the conjunction of non-informative propositions and the -equality. If there is an hypothesis :math:`h:a=b` in the local context, it can +equality. If there is a hypothesis :math:`h:a=b` in the local context, it can be used for rewriting not only in logical propositions but also in any type. .. example:: + .. coqtop:: all Print eq_rec. @@ -1421,6 +1436,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: .. example:: + The following term in concrete syntax:: match t as l return P' with @@ -1485,6 +1501,7 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_ .. example:: + Below is a typing rule for the term shown in the previous example: .. inference:: list example @@ -1634,6 +1651,7 @@ The following definitions are correct, we enter them using the :cmd:`Fixpoint` command and show the internal representation. .. example:: + .. coqtop:: all Fixpoint plus (n m:nat) {struct n} : nat := @@ -1804,17 +1822,18 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`. The Calculus of Inductive Constructions with impredicative Set ----------------------------------------------------------------- -|Coq| can be used as a type-checker for the Calculus of Inductive +|Coq| can be used as a type checker for the Calculus of Inductive Constructions with an impredicative sort :math:`\Set` by using the compiler option ``-impredicative-set``. For example, using the ordinary `coqtop` command, the following is rejected, .. example:: + .. coqtop:: all Fail Definition id: Set := forall X:Set,X->X. -while it will type-check, if one uses instead the `coqtop` +while it will type check, if one uses instead the `coqtop` ``-impredicative-set`` option.. The major change in the theory concerns the rule for product formation diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 52c56d2bd2..9de30e2190 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -848,6 +848,7 @@ Notation Interpretation Precedence Associativity .. example:: + .. coqtop:: all reset Require Import ZArith. @@ -887,6 +888,7 @@ Notation Interpretation =============== =================== .. example:: + .. coqtop:: all reset Require Import Reals. @@ -906,6 +908,7 @@ tactics (see Chapter :ref:`tactics`), there are also: Proves that two real integer constants are different. .. example:: + .. coqtop:: all reset Require Import DiscrR. @@ -919,6 +922,7 @@ tactics (see Chapter :ref:`tactics`), there are also: Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions. .. example:: + .. coqtop:: all reset Require Import Reals. @@ -933,6 +937,7 @@ tactics (see Chapter :ref:`tactics`), there are also: corresponding to the condition on each operand of the product. .. example:: + .. coqtop:: all reset Require Import Reals. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 394b928ada..0fbe7ac70b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -70,7 +70,9 @@ generates a variant type definition with just one constructor: To build an object of type :n:`@ident`, one should provide the constructor :n:`@ident₀` with the appropriate number of terms filling the fields of the record. -.. example:: Let us define the rational :math:`1/2`: +.. example:: + + Let us define the rational :math:`1/2`: .. coqtop:: in @@ -210,7 +212,7 @@ During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section :ref:`gallina-inductive-definitions`, may also occur. -**See also** Coercions and records in Section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. +.. seealso:: Coercions and records in section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. .. _primitive_projections: @@ -227,7 +229,7 @@ term constructor `r.(p)` representing a primitive projection `p` applied to a record object `r` (i.e., primitive projections are always applied). Even if the record type has parameters, these do not appear at applications of the projection, considerably reducing the sizes of -terms when manipulating parameterized records and typechecking time. +terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement for the usual defined ones, although there are a few notable differences. @@ -326,7 +328,7 @@ into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed under its expanded form (see :opt:`Printing Matching`). -See also: :ref:`extendedpatternmatching`. +.. seealso:: :ref:`extendedpatternmatching`. .. _if-then-else: @@ -709,7 +711,7 @@ terminating functions. `functional inversion` will not be available for the function. -See also: :ref:`functional-scheme` and :tacn:`function induction` +.. seealso:: :ref:`functional-scheme` and :tacn:`function induction` Depending on the ``{…}`` annotation, different definition mechanisms are used by ``Function``. A more precise description is given below. @@ -1258,7 +1260,7 @@ identifiers qualid, i.e. as list of identifiers separated by dots (see |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts the name of a library is called a *library root*. All library files of the standard library of |Coq| have the reserved root |Coq| but library -file names based on other roots can be obtained by using |Coq| commands +filenames based on other roots can be obtained by using |Coq| commands (coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`). Also, when an interactive |Coq| session starts, a library of root ``Top`` is started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`). @@ -1292,7 +1294,7 @@ short name (or even same partially qualified names as soon as the full names are different). Notice that the notion of absolute, partially qualified and short -names also applies to library file names. +names also applies to library filenames. **Visibility** @@ -1326,7 +1328,7 @@ accessible, absolute names can never be hidden. Locate nat. -See also: Commands :cmd:`Locate` and :cmd:`Locate Library`. +.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`. .. _libraries-and-filesystem: @@ -1512,7 +1514,8 @@ says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non maximally. This can be governed argument per argument by the command :cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. -See also :ref:`displaying-implicit-args`. + +.. seealso:: :ref:`displaying-implicit-args`. Casual use of implicit arguments @@ -1849,15 +1852,15 @@ are named as expected. .. example:: (continued) -.. coqtop:: all + .. coqtop:: all - Arguments p [s t] _ [u] _: rename. + Arguments p [s t] _ [u] _: rename. - Check (p r1 (u:=c)). + Check (p r1 (u:=c)). - Check (p (s:=a) (t:=b) r1 (u:=c) r2). + Check (p (s:=a) (t:=b) r1 (u:=c) r2). - Fail Arguments p [s t] _ [w] _ : assert. + Fail Arguments p [s t] _ [w] _ : assert. .. _displaying-implicit-args: @@ -1885,7 +1888,7 @@ arguments that are not detected as strict implicit arguments. This “defensive” mode can quickly make the display cumbersome so this can be deactivated by turning this option off. -See also: :opt:`Printing All`. +.. seealso:: :opt:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1935,7 +1938,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. 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|. Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be - solved during the type-checking process, :token:`qualid` is used as a solution. + solved during the type checking process, :token:`qualid` is used as a solution. Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| into a complete structure built on |c_i|. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8250b4b3d6..075235a8e2 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -758,6 +758,7 @@ Simple inductive types the case of annotated inductive types — cf. next section). .. example:: + The set of natural numbers is defined as: .. coqtop:: all @@ -919,7 +920,7 @@ Parametrized inductive types When this option is set (it is off by default), inductive definitions are abstracted over their parameters - before typechecking constructors, allowing to write: + before type checking constructors, allowing to write: .. coqtop:: all undo @@ -976,6 +977,7 @@ Mutually defined inductive types reason, the parameters must be strictly the same for each inductive types. .. example:: + The typical example of a mutual inductive data type is the one for trees and forests. We assume given two types :g:`A` and :g:`B` as variables. It can be declared the following way. @@ -1048,6 +1050,7 @@ of the type. For co-inductive types, the only elimination principle is case analysis. .. example:: + An example of a co-inductive type is the type of infinite sequences of natural numbers, usually called streams. @@ -1067,6 +1070,7 @@ Definition of co-inductive predicates and blocks of mutually co-inductive definitions are also allowed. .. example:: + An example of a co-inductive predicate is the extensional equality on streams: @@ -1120,7 +1124,7 @@ constructions. arguments, and this choice influences the reduction of the fixpoint. Hence an explicit annotation must be used if the leftmost decreasing argument is not the desired one. Writing explicit annotations can also - speed up type-checking of large mutual fixpoints. + speed up type checking of large mutual fixpoints. + In order to keep the strong normalization property, the fixed point reduction will only be performed when the argument in position of the @@ -1129,6 +1133,7 @@ constructions. .. example:: + One can define the addition function as : .. coqtop:: all @@ -1201,6 +1206,7 @@ constructions. inductive types. .. example:: + The size of trees and forests can be defined the following way: .. coqtop:: all |