Documentation for SProp

2 files changed, 69 insertions, 24 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-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,