SProp (proof irrelevant propositions)¶
Warning
The status of strict propositions is experimental.
In particular, conversion checking through bytecode or native code compilation currently does not understand proof irrelevance.
This section describes the extension of Coq with definitionally proof irrelevant propositions (types in the sort \(\SProp\), also known as strict propositions) as described in [GCST19].
Use of \(\SProp\) may be disabled by passing disallowsprop
to the
Coq program or by turning the Allow StrictProp
flag off.

Flag
Allow StrictProp
¶ Enables or disables the use of \(\SProp\). It is enabled by default. The commandline flag
disallowsprop
disables \(\SProp\) at startup.
Error
SProp is disallowed because the "Allow StrictProp" flag is off.
¶

Error
Some of the definitions described in this document are available
through Coq.Logic.StrictProp
, which see.
Basic constructs¶
The purpose of \(\SProp\) is to provide types where all elements are convertible:
 Theorem irrelevance (A : SProp) (P : A > Prop) : forall x : A, P x > forall y : A, P y.
 1 goal A : SProp P : A > Prop ============================ forall x : A, P x > forall y : A, P y
 Proof.
 intros * Hx *.
 1 goal A : SProp P : A > Prop x : A Hx : P x y : A ============================ P y
 exact Hx.
 No more goals.
 Qed.
Since we have definitional ηexpansion for functions, the property of being a type of definitionally irrelevant values is impredicative, and so is \(\SProp\):
 Check fun (A:Type) (B:A > SProp) => (forall x:A, B x) : SProp.
 fun (A : Type) (B : A > SProp) => (forall x : A, B x) : SProp : forall A : Type, (A > SProp) > SProp
In order to keep conversion tractable, cumulativity for \(\SProp\)
is forbidden, unless the Cumulative StrictProp
flag is turned
on:
 Fail Check (fun (A:SProp) => A : Type).
 The command has indeed failed with message: In environment A : SProp The term "A" has type "SProp" while it is expected to have type "Type".
 Set Cumulative StrictProp.
 Check (fun (A:SProp) => A : Type).
 fun A : SProp => A : Type : SProp > Type
 Unset Cumulative StrictProp.
We can explicitly lift strict propositions into the relevant world by using a wrapping inductive type. The inductive stops definitional proof irrelevance from escaping.
 Inductive Box (A:SProp) : Prop := box : A > Box A.
 Box is defined Box_rect is defined Box_ind is defined Box_rec is defined Box_sind is defined
 Arguments box {_} _.
 Fail Check fun (A:SProp) (x y : Box A) => eq_refl : x = y.
 The command has indeed failed with message: In environment A : SProp x : Box A y : Box A The term "eq_refl" has type "x = x" while it is expected to have type "x = y" (cannot unify "x" and "y").
 Definition box_irrelevant (A:SProp) (x y : Box A) : x = y := match x, y with box x, box y => eq_refl end.
 box_irrelevant is defined
In the other direction, we can use impredicativity to "squash" a relevant type, making an irrelevant approximation.
Or more conveniently (but equivalently)
Most inductives types defined in \(\SProp\) are squashed types, i.e. they can only be eliminated to construct proofs of other strict propositions. Empty types are the only exception.
 Inductive sEmpty : SProp := .
 sEmpty is defined sEmpty_rect is defined sEmpty_ind is defined sEmpty_rec is defined sEmpty_sind is defined
 Check sEmpty_rect.
 sEmpty_rect : forall (P : sEmpty > Type) (s : sEmpty), P s
Note
Eliminators to strict propositions are called foo_sind
, in the
same way that eliminators to propositions are called foo_ind
.
Primitive records in \(\SProp\) are allowed when fields are strict propositions, for instance:
 Set Primitive Projections.
 Record sProd (A B : SProp) : SProp := { sfst : A; ssnd : B }.
 sProd is defined sfst is defined ssnd is defined
On the other hand, to avoid having definitionally irrelevant types in non\(\SProp\) sorts (through record ηextensionality), primitive records in relevant sorts must have at least one relevant field.
 Set Warnings "+nonprimitiverecord".
 Fail Record rBox (A:SProp) : Prop := rbox { runbox : A }.
 The command has indeed failed with message: The record rBox could not be defined as a primitive record [nonprimitiverecord,record]
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:
By using empty and unit types as base values, we can encode other strict propositions. For instance:
Definitional UIP¶

Flag
Definitional UIP
¶ This flag, off by default, allows the declaration of nonsquashed inductive types with 1 constructor which takes no argument in \(\SProp\). Since this includes equality types, it provides definitional uniqueness of identity proofs.
Because squashing is a universe restriction, unsetting
Universe Checking
is stronger than settingDefinitional UIP
.
Definitional UIP involves a special reduction rule through which reduction depends on conversion. Consider the following code:
 Set Definitional UIP.
 Inductive seq {A} (a:A) : A > SProp := srefl : seq a a.
 seq is defined seq_rect is defined seq_ind is defined seq_rec is defined seq_sind is defined
 Axiom e : seq 0 0.
 e is declared
 Definition hidden_arrow := match e return Set with srefl _ => nat > nat end.
 hidden_arrow is defined
 Check (fun (f : hidden_arrow) (x:nat) => (f : nat > nat) x).
 fun (f : hidden_arrow) (x : nat) => (f : nat > nat) x : hidden_arrow > nat > nat
By the usual reduction rules hidden_arrow
is a stuck match, but
by proof irrelevance e
is convertible to srefl 0
and then by
congruence hidden_arrow
is convertible to nat > nat
.
The special reduction reduces any match on a type which uses
definitional UIP when the indices are convertible to those of the
constructor. For seq
, this means a match on a value of type seq x
y
reduces if and only if x
and y
are convertible.
Such matches are indicated in the printed representation by inserting a cast around the discriminee:
 Print hidden_arrow.
 hidden_arrow = match e : seq 0 0 with  srefl _ => nat > nat end : Set
Non Termination with UIP¶
The special reduction rule of UIP combined with an impredicative sort breaks termination of reduction [AC19]:
 Axiom all_eq : forall (P Q:Prop), P > Q > seq P Q.
 all_eq is declared
 Definition transport (P Q:Prop) (x:P) (y:Q) : Q := match all_eq P Q x y with srefl _ => x end.
 transport is defined
 Definition top : Prop := forall P : Prop, P > P.
 top is defined
 Definition c : top := fun P p => transport (top > top) P (fun x : top => x (top > top) (fun x => x) x) p.
 c is defined
 Fail Timeout 1 Eval lazy in c (top > top) (fun x => x) c.
 The command has indeed failed with message: Timeout!
The term c (top > top) (fun x => x) c
infinitely reduces to itself.
Issues with noncumulativity¶
During normal term elaboration, we don't always know that a type is a strict proposition early enough. For instance:
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 \(\SProp\), we consider \(\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 \(\SProp\)
(in the example above, u
doesn't appear in the final term).
This means that some errors will be delayed until Qed
:
 Lemma foo : Prop.
 1 goal ============================ Prop
 Proof. pose (fun A : SProp => A : Type); exact True.
 No more goals.
 Fail Qed.
 The command has indeed failed with message: In environment A : SProp The term "A" has type "SProp" while it is expected to have type "Type".
 Abort.

Flag
Elaboration StrictProp Cumulativity
¶ Unset this flag (it is on by default) to be strict with regard to \(\SProp\) cumulativity during elaboration.
The implementation of proof irrelevance uses inferred "relevance" marks on binders to determine which variables are irrelevant. Together with noncumulativity this allows us to avoid retyping during conversion. However during elaboration cumulativity is allowed and so the algorithm may miss some irrelevance:
 Fail Definition late_mark := fun (A:SProp) (P:A > Prop) x y (v:P x) => v : P y.
 The command has indeed failed with message: In environment A : SProp P : A > Prop x : A y : A v : P x The term "v" has type "P x" while it is expected to have type "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.
The kernel will reinfer the marks on the fully elaborated term, and
so correctly converts x
and y
.

Warning
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.

Flag
Cumulative StrictProp
¶ Set this flag (it is off by default) to make the kernel accept cumulativity between \(\SProp\) and other universes. This makes typechecking incomplete.