Documentation for SProp

1 files changed, 236 insertions, 0 deletions

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.