\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \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}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

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 $\SProp$, also known as strict propositions) as described in [GCST19].

To use $\SProp$ you must pass -allow-sprop to the Coq program or use Allow StrictProp.

Flag Allow StrictProp¶: Allows using $\SProp$ when set and forbids it when unset. The initial value depends on whether you used the command line -allow-sprop.

Error SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.¶

Set Allow StrictProp.

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:

Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.

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.

Warning

Conversion checking through bytecode or native code compilation currently does not understand proof irrelevance.

In order to keep conversion tractable, cumulativity for $\SProp$ is forbidden:

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

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.

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)

Inductive Squash (A:Type) : SProp := squash : A -> Squash A.

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 "+non-primitive-record".
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

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:

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:

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:

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 $\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 subgoal ============================ Prop
Proof.
pose (fun A : SProp => A : Type); exact True.: No more subgoals.

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 non-cumulativity 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.

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.

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.