Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Ngcd_def.v
Sprache: Coq
Untersuchungsergebnis.rst Download desText {Text[90] Latech[112] Haskell[212]}zum Wurzelverzeichnis wechseln
.. _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.
[ zur Elbe Produktseite wechseln0.107Quellennavigators
]
|
|
