\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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}{\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{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \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{\Type}{\textsf{Type}} \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}]} \end{split}\]

# 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 Rocq 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 `-disallow-sprop` to the Rocq program or by turning the `Allow StrictProp` flag off.

Flag Allow StrictProp

  This flag enables or disables the use of \(\SProp\). It is enabled by default. The command-line flag `-disallow-sprop` disables \(\SProp\) at startup.

  Error SProp is disallowed because the "Allow StrictProp" flag is off.

Some of the definitions described in this document are available through `Stdlib.Logic.StrictProp`.

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

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" (universe inconsistency: Cannot enforce SProp <= Top.22).

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

Primitive records in relevant sorts with fields that are only strict propositions are allowed but do not have η-conversion. This is in order to avoid having definitionally irrelevant types in non-\(\SProp\) sorts (through record η-extensionality).

Record rBox (A : SProp) : Prop := rbox { runbox : A }.
  rBox is defined runbox is defined
Goal forall (A : SProp) (r : rBox A), r = {| runbox := r.(runbox A) |}.
  1 goal ============================ forall (A : SProp) (r : rBox A), r = {| runbox := runbox _ r |}
Proof. intros A r. Fail reflexivity. Abort.
  1 goal A : SProp r : rBox A ============================ r = {| runbox := runbox _ r |} The command has indeed failed with message: In environment A : SProp r : rBox A Unable to unify "{| runbox := runbox _ r |}" with "r".

In contrast, primitive records in relevant sorts with at least one relevant field are allowed and have η-conversion.

Record ssig (A : Type) (P : A -> SProp) : Type := { spr1 : A; spr2 : P spr1 }. Goal forall (A : Type) (P : A -> SProp) (s : ssig A P), s = {| spr1 := s.(spr1 A P); spr2 := s.(spr2 A P) |}. Proof. intros A P s. reflexivity. Qed.

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

## Definitional UIP

Flag Definitional UIP

  This flag, off by default, allows the declaration of non-squashed inductive types in \(\SProp\) with 1 constructor which takes no non-parameter arguments. Since this includes equality types, it provides definitional uniqueness of identity proofs.

  Because squashing is a universe restriction, unsetting `Universe Checking` is stronger than setting `Definitional 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 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.

## Debugging \(\SProp\) issues

Every binder in a term (such as `fun x` or `forall x`) caches information called the relevance mark indicating whether its type is in \(\SProp\) or not. This is used to efficiently implement proof irrelevance.

The user should usually not be concerned with relevance marks, so by default they are not displayed. However code outside the kernel may generate incorrect marks resulting in bugs. Typically this means a conversion will incorrectly fail as a variable was incorrectly marked proof relevant.

Warning Bad relevance

  This is a developer warning, which is treated as an error by default. It is emitted by the kernel when it is passed a term with incorrect relevance marks. This is always caused by a bug in Rocq (or a plugin), which should thus be reported and fixed. In order to allow the user to work around such bugs, we leave the ability to unset the `bad-relevance` warning for the time being, so that the kernel will silently repair the proof term instead of failing.

Flag Printing Relevance Marks

  This flag enables debug printing of relevance marks. It is off by default. Note that `Printing All` does not affect printing of relevance marks.

  Set Printing Relevance Marks.
  Check fun x : nat => x.
    fun x : (* Relevant *) nat => x : nat -> nat
  Check fun (P:SProp) (p:P) => p.
    fun (P : (* Relevant *) SProp) (p : (* Irrelevant *) P) => p : forall P : (* Relevant *) SProp, P -> P

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF