Documentation for SProp

7 files changed, 309 insertions, 24 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 927a912fbf..e790d20e00 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -273,6 +273,7 @@
 \newcommand{\nS}{\mbox{\textsf{S}}}
 \newcommand{\node}{\mbox{\textsf{node}}}
 \newcommand{\Nil}{\mbox{\textsf{nil}}}
+\newcommand{\SProp}{\mbox{\textsf{SProp}}}
 \newcommand{\Prop}{\mbox{\textsf{Prop}}}
 \newcommand{\Set}{\mbox{\textsf{Set}}}
 \newcommand{\si}{\mbox{\textsf{if}}}
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
new file mode 100644
index 0000000000..015b84c530
--- /dev/null
+++ b/doc/sphinx/addendum/sprop.rst
@@ -0,0 +1,236 @@
+.. _sprop:
+
+SProp (proof irrelevant propositions)
+=====================================
+
+.. warning::
+
+   The status of strict propositions is experimental.
+
+This section describes the extension of |Coq| with definitionally
+proof irrelevant propositions (types in the sort :math:`\SProp`, also
+known as strict propositions). To use :math:`\SProp` you must pass
+``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`.
+
+.. opt:: Allow StrictProp
+   :name: Allow StrictProp
+
+   Allows using :math:`\SProp` when set and forbids it when unset. The
+   initial value depends on whether you used the command line
+   ``-allow-sprop``.
+
+.. coqtop:: none
+
+   Set Allow StrictProp.
+
+Some of the definitions described in this document are available
+through ``Coq.Logic.StrictProp``, which see.
+
+Basic constructs
+----------------
+
+The purpose of :math:`\SProp` is to provide types where all elements
+are convertible:
+
+.. coqdoc::
+
+   Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.
+
+Since we have definitional :ref:`eta-expansion` for
+functions, the property of being a type of definitionally irrelevant
+values is impredicative, and so is :math:`\SProp`:
+
+.. coqdoc::
+
+   Check fun (A:Type) (B:A -> SProp) => (forall x:A, B x) : SProp.
+
+.. warning::
+
+   Conversion checking through bytecode or native code compilation
+   currently does not understand proof irrelevance.
+
+In order to keep conversion tractable, cumulativity for :math:`\SProp`
+is forbidden:
+
+.. coqtop:: all
+
+   Fail Check (fun (A:SProp) => A : Type).
+
+We can explicitly lift strict propositions into the relevant world by
+using a wrapping inductive type. The inductive stops definitional
+proof irrelevance from escaping.
+
+.. coqtop:: in
+
+   Inductive Box (A:SProp) : Prop := box : A -> Box A.
+   Arguments box {_} _.
+
+.. coqtop:: all
+
+   Fail Check fun (A:SProp) (x y : Box A) => eq_refl : x = y.
+
+.. doesn't get merged with the above if coqdoc
+.. coqtop:: in
+
+   Definition box_irrelevant (A:SProp) (x y : Box A) : x = y
+     := match x, y with box x, box y => eq_refl end.
+
+In the other direction, we can use impredicativity to "squash" a
+relevant type, making an irrelevant approximation.
+
+.. coqdoc::
+
+  Definition iSquash (A:Type) : SProp
+    := forall P : SProp, (A -> P) -> P.
+  Definition isquash A : A -> iSquash A
+    := fun a P f => f a.
+  Definition iSquash_sind A (P : iSquash A -> SProp) (H : forall x : A, P (isquash A x))
+    : forall x : iSquash A, P x
+    := fun x => x (P x) (H : A -> P x).
+
+Or more conveniently (but equivalently)
+
+.. coqdoc::
+
+  Inductive Squash (A:Type) : SProp := squash : A -> Squash A.
+
+Most inductives types defined in :math:`\SProp` are squashed types,
+i.e. they can only be eliminated to construct proofs of other strict
+propositions. Empty types are the only exception.
+
+.. coqtop:: in
+
+   Inductive sEmpty : SProp := .
+
+.. coqtop:: all
+
+   Check sEmpty_rect.
+
+.. note::
+
+   Eliminators to strict propositions are called ``foo_sind``, in the
+   same way that eliminators to propositions are called ``foo_ind``.
+
+Primitive records in :math:`\SProp` are allowed when fields are strict
+propositions, for instance:
+
+.. coqtop:: in
+
+   Set Primitive Projections.
+   Record sProd (A B : SProp) : SProp := { sfst : A; ssnd : B }.
+
+On the other hand, to avoid having definitionally irrelevant types in
+non-:math:`\SProp` sorts (through record η-extensionality), primitive
+records in relevant sorts must have at least one relevant field.
+
+.. coqtop:: all
+
+   Set Warnings "+non-primitive-record".
+   Fail Record rBox (A:SProp) : Prop := rbox { runbox : A }.
+
+.. coqdoc::
+
+   Record ssig (A:Type) (P:A -> SProp) : Type := { spr1 : A; spr2 : P spr1 }.
+
+Note that ``rBox`` works as an emulated record, which is equivalent to
+the Box inductive.
+
+Encodings for strict propositions
+---------------------------------
+
+The elimination for unit types can be encoded by a trivial function
+thanks to proof irrelevance:
+
+.. coqdoc::
+
+   Inductive sUnit : SProp := stt.
+   Definition sUnit_rect (P:sUnit->Type) (v:P stt) (x:sUnit) : P x := v.
+
+By using empty and unit types as base values, we can encode other
+strict propositions. For instance:
+
+.. coqdoc::
+
+  Definition is_true (b:bool) : SProp := if b then sUnit else sEmpty.
+
+  Definition is_true_eq_true b : is_true b -> true = b
+    := match b with
+       | true => fun _ => eq_refl
+       | false => sEmpty_ind _
+       end.
+
+  Definition eq_true_is_true b (H:true=b) : is_true b
+    := match H in _ = x return is_true x with eq_refl => stt end.
+
+Issues with non-cumulativity
+----------------------------
+
+During normal term elaboration, we don't always know that a type is a
+strict proposition early enough. For instance:
+
+.. coqdoc::
+
+   Definition constant_0 : ?[T] -> nat := fun _ : sUnit => 0.
+
+While checking the type of the constant, we only know that ``?[T]``
+must inhabit some sort. Putting it in some floating universe ``u``
+would disallow instantiating it by ``sUnit : SProp``.
+
+In order to make the system usable without having to annotate every
+instance of :math:`\SProp`, we consider :math:`\SProp` to be a subtype
+of every universe during elaboration (i.e. outside the kernel). Then
+once we have a fully elaborated term it is sent to the kernel which
+will check that we didn't actually need cumulativity of :math:`\SProp`
+(in the example above, ``u`` doesn't appear in the final term).
+
+This means that some errors will be delayed until ``Qed``:
+
+.. coqtop:: in
+
+   Lemma foo : Prop.
+   Proof. pose (fun A : SProp => A : Type); exact True.
+
+.. coqtop:: all
+
+   Fail Qed.
+
+.. coqtop:: in
+
+   Abort.
+
+.. opt:: Elaboration StrictProp Cumulativity
+   :name: Elaboration StrictProp Cumulativity
+
+   Unset this option (it's on by default) to be strict with regard to
+   :math:`\SProp` cumulativity during elaboration.
+
+The implementation of proof irrelevance uses inferred "relevance"
+marks on binders to determine which variables are irrelevant. Together
+with non-cumulativity this allows us to avoid retyping during
+conversion. However during elaboration cumulativity is allowed and so
+the algorithm may miss some irrelevance:
+
+.. coqtop:: all
+
+  Fail Definition late_mark := fun (A:SProp) (P:A -> Prop) x y (v:P x) => v : P y.
+
+The binders for ``x`` and ``y`` are created before their type is known
+to be ``A``, so they're not marked irrelevant. This can be avoided
+with sufficient annotation of binders (see ``irrelevance`` at the
+beginning of this chapter) or by bypassing the conversion check in
+tactics.
+
+.. coqdoc::
+
+   Definition late_mark := fun (A:SProp) (P:A -> Prop) x y (v:P x) =>
+     ltac:(exact_no_check v) : P y.
+
+The kernel will re-infer the marks on the fully elaborated term, and
+so correctly converts ``x`` and ``y``.
+
+.. warn:: Bad relevance
+
+  This is a developer warning, disabled by default. It is emitted by
+  the kernel when it is passed a term with incorrect relevance marks.
+  To avoid conversion issues as in ``late_mark`` you may wish to use
+  it to find when your tactics are producing incorrect marks.
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index a652b9e1ca..5a349fcf75 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -74,6 +74,7 @@ Contents
    addendum/parallel-proof-processing
    addendum/miscellaneous-extensions
    addendum/universe-polymorphism
+   addendum/sprop
 
 .. toctree::
    :caption: Reference
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 9e9eb330fe..ff3971aee4 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -81,6 +81,7 @@ Addendum
    addendum/parallel-proof-processing
    addendum/miscellaneous-extensions
    addendum/universe-polymorphism
+   addendum/sprop
 
 .. toctree::
    zebibliography
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,
diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty
index 8f7b1bb1e8..90a63a5a2d 100644
--- a/doc/sphinx/refman-preamble.sty
+++ b/doc/sphinx/refman-preamble.sty
@@ -58,6 +58,7 @@
 \newcommand{\Pair}{\textsf{pair}}
 \newcommand{\plus}{\mathsf{plus}}
 \newcommand{\Prod}{\textsf{prod}}
+\newcommand{\SProp}{\textsf{SProp}}
 \newcommand{\Prop}{\textsf{Prop}}
 \newcommand{\return}{\kw{return}}
 \newcommand{\Set}{\textsf{Set}}