diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 73 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 35 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 20 |
3 files changed, 89 insertions, 39 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index e05df65c63..ef183174d7 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -36,21 +36,29 @@ Sorts ~~~~~~~~~~~ All sorts have a type and there is an infinite well-founded typing -hierarchy of sorts whose base sorts are :math:`\Prop` and :math:`\Set`. +hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` +and :math:`\Set`. The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a logical proposition then it denotes the class of terms representing proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is provable. An object of type :math:`\Prop` is called a proposition. +The sort :math:`\SProp` is like :math:`\Prop` but the propositions in +:math:`\SProp` are known to have irrelevant proofs (all proofs are +equal). Objects of type :math:`\SProp` are called strict propositions. +:math:`\SProp` is rejected except when using the compiler option +``-allow-sprop``. See :ref:`sprop` for information about using +:math:`\SProp`. + The sort :math:`\Set` intends to be the type of small sets. This includes data types such as booleans and naturals, but also products, subsets, and function types over these data types. -:math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. +:math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of -|Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` +|Cic| has infinitely many sorts. There are, in addition to the base sorts, a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as @@ -63,7 +71,7 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by: .. math:: - \Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} + \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and :math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`. @@ -113,7 +121,7 @@ language of the *Calculus of Inductive Constructions* is built from the following rules. -#. the sorts :math:`\Set`, :math:`\Prop`, :math:`\Type(i)` are terms. +#. the sorts :math:`\SProp`, :math:`\Prop`, :math:`\Set`, :math:`\Type(i)` are terms. #. variables, hereafter ranged over by letters :math:`x`, :math:`y`, etc., are terms #. constants, hereafter ranged over by letters :math:`c`, :math:`d`, etc., are terms. #. if :math:`x` is a variable and :math:`T`, :math:`U` are terms then @@ -293,6 +301,12 @@ following rules. --------------- \WF{E;~c:=t:T}{} +.. inference:: Ax-SProp + + \WFE{\Gamma} + ---------------------- + \WTEG{\SProp}{\Type(1)} + .. inference:: Ax-Prop \WFE{\Gamma} @@ -325,6 +339,14 @@ following rules. ---------------------------------------------------------- \WTEG{c}{T} +.. inference:: Prod-SProp + + \WTEG{T}{s} + s \in {\Sort} + \WTE{\Gamma::(x:T)}{U}{\SProp} + ----------------------------- + \WTEG{\forall~x:T,U}{\SProp} + .. inference:: Prod-Prop \WTEG{T}{s} @@ -336,14 +358,15 @@ following rules. .. inference:: Prod-Set \WTEG{T}{s} - s \in \{\Prop, \Set\} + s \in \{\SProp, \Prop, \Set\} \WTE{\Gamma::(x:T)}{U}{\Set} ---------------------------- \WTEG{∀ x:T,~U}{\Set} .. inference:: Prod-Type - \WTEG{T}{\Type(i)} + \WTEG{T}{s} + s \in \{\SProp, \Type{i}\} \WTE{\Gamma::(x:T)}{U}{\Type(i)} -------------------------------- \WTEG{∀ x:T,~U}{\Type(i)} @@ -524,6 +547,14 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. 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)`. +.. _proof-irrelevance: + +Proof Irrelevance +~~~~~~~~~~~~~~~~~ + +It is legal to identify any two terms whose common type is a strict +proposition :math:`A : \SProp`. Terms in a strict propositions are +therefore called *irrelevant*. .. _convertibility: @@ -540,7 +571,7 @@ We say that two terms :math:`t_1` and :math:`t_2` are 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 -:math:`u_2` are identical, or they are convertible up to η-expansion, +:math:`u_2` are identical up to irrelevant subterms, or they are convertible up to η-expansion, i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is recursively convertible to :math:`u_1'`, or, symmetrically, :math:`u_2` is :math:`λx:T.~u_2'` @@ -612,6 +643,7 @@ a *subtyping* relation inductively defined by: #. for any :math:`i`, :math:`E[Γ] ⊢ \Set ≤_{βδιζη} \Type(i)`, #. :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Set`, hence, by transitivity, :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Type(i)`, for any :math:`i` + (note: :math:`\SProp` is not related by cumulativity to any other term) #. if :math:`E[Γ] ⊢ T =_{βδιζη} U` and :math:`E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'` then :math:`E[Γ] ⊢ ∀x:T,~T′ ≤_{βδιζη} ∀ x:U,~U′`. @@ -980,9 +1012,9 @@ provided that the following side conditions hold: One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sort :math:`\Prop` but may fail to define inductive type on sort :math:`\Set` and -generate constraints between universes for inductive types in -the Type hierarchy. +sorts :math:`\SProp` and :math:`\Prop` but may fail to define +inductive type on sort :math:`\Set` and generate constraints +between universes for inductive types in the Type hierarchy. .. example:: @@ -1339,14 +1371,15 @@ There is no restriction on the sort of the predicate to be eliminated. The case of Inductive definitions of sort :math:`\Prop` is a bit more complicated, because of our interpretation of this sort. The only -harmless allowed elimination, is the one when predicate :math:`P` is also of -sort :math:`\Prop`. +harmless allowed eliminations, are the ones when predicate :math:`P` +is also of sort :math:`\Prop` or is of the morally smaller sort +:math:`\SProp`. .. inference:: Prop - ~ - --------------- - [I:\Prop|I→\Prop] + s ∈ \{\SProp,\Prop\} + -------------------- + [I:\Prop|I→s] :math:`\Prop` is the type of logical propositions, the proofs of properties :math:`P` in @@ -1434,6 +1467,14 @@ type. An empty definition has no constructors, in that case also, elimination on any sort is allowed. +.. _Eliminaton-for-SProp: + +Inductive types in :math:`\SProp` must have no constructors (i.e. be +empty) to be eliminated to produce relevant values. + +Note that thanks to proof irrelevance elimination functions can be +produced for other types, for instance the elimination for a unit type +is the identity. .. _Type-of-branches: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f1733a5ebf..59506a6ff2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1575,7 +1575,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | @ident } +.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1592,20 +1592,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident } +.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident } +.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } } +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1621,7 +1621,7 @@ Declaring Implicit Arguments .. coqtop:: reset all - Inductive list (A:Type) : Type := + Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. @@ -1629,13 +1629,15 @@ Declaring Implicit Arguments Arguments cons [A] _ _. - Arguments nil [A]. + Arguments nil {A}. Check (cons 3 nil). - Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end. + Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := + match l with nil => nil | cons a t => cons (f a) (map A B f t) end. - Fixpoint length (A:Type) (l:list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end. + Fixpoint length (A : Type) (l : list A) : nat := + match l with nil => 0 | cons _ m => S (length A m) end. Arguments map [A B] f l. @@ -1651,6 +1653,13 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). +.. warn:: Argument number @num is a trailing implicit so must be maximal. + + For instance in + + .. coqtop:: all warn + + Arguments prod _ [_]. Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1704,19 +1713,15 @@ of constants. For instance, the variable ``p`` below has type ``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z`` appear strictly in the body of the type, they are implicit. -.. coqtop:: reset none - - Set Warnings "-local-declaration". - .. coqtop:: all - Variable X : Type. + Parameter X : Type. Definition Relation := X -> X -> Prop. Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z. - Variables (R : Relation) (p : Transitivity R). + Parameters (R : Relation) (p : Transitivity R). Arguments p : default implicits. @@ -1724,7 +1729,7 @@ appear strictly in the body of the type, they are implicit. Print Implicit p. - Variables (a b c : X) (r1 : R a b) (r2 : R b c). + Parameters (a b c : X) (r1 : R a b) (r2 : R b c). Check (p r1 r2). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 9bd41d79b7..02fb9d84ce 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -94,8 +94,8 @@ Keywords employed otherwise:: _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod Prop return - Set then Type using where with + forall fun if IF in let match mod return + SProp Prop Set Type then using where with Special tokens The following sequences of characters are special tokens:: @@ -159,7 +159,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : ' `pattern` name : `ident` | _ qualid : `ident` | `qualid` `access_ident` - sort : Prop | Set | Type + sort : SProp | Prop | Set | Type fix_bodies : `fix_body` : `fix_body` with `fix_body` with … with `fix_body` for `ident` cofix_bodies : `cofix_body` @@ -218,13 +218,17 @@ numbers (see :ref:`datatypes`). .. index:: single: Set (sort) + single: SProp single: Prop single: Type Sorts ----- -There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. +There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. + +- :g:`SProp` is the universe of *definitionally irrelevant + propositions* (also called *strict propositions*). - :g:`Prop` is the universe of *logical propositions*. The logical propositions themselves are typing the proofs. We denote propositions by :production:`form`. @@ -235,7 +239,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Type` is the type of :g:`Prop` and :g:`Set` +- :g:`Type` is the type of sorts. More on sorts can be found in Section :ref:`sorts`. @@ -767,9 +771,9 @@ Simple inductive types are the names of its constructors and :token:`type` their respective types. Depending on the universe where the inductive type :token:`ident` lives (e.g. its type :token:`sort`), Coq provides a number of destructors. - Destructors are named :token:`ident`\ ``_ind``, :token:`ident`\ ``_rec`` - or :token:`ident`\ ``_rect`` which respectively correspond to elimination - principles on :g:`Prop`, :g:`Set` and :g:`Type`. + Destructors are named :token:`ident`\ ``_sind``,:token:`ident`\ ``_ind``, + :token:`ident`\ ``_rec`` or :token:`ident`\ ``_rect`` which respectively + correspond to elimination principles on :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. The type of the destructors expresses structural induction/recursion principles over objects of type :token:`ident`. The constant :token:`ident`\ ``_ind`` is always provided, |