1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
|
.. _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 :flag:`Allow StrictProp`.
.. flag:: 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``.
.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
:undocumented:
.. 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.
.. flag:: Elaboration StrictProp Cumulativity
:name: Elaboration StrictProp Cumulativity
Unset this flag (it is 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.
|
