diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 236 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 155 |
4 files changed, 323 insertions, 78 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. coqtop:: all +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 3ec6c118af..e882ce6e88 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -285,7 +285,7 @@ By default, implicit arguments are omitted in patterns. So we write: .. coqtop:: all - Arguments nil [A]. + Arguments nil {A}. Arguments cons [A] _ _. Check (fun l:List nat => diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst new file mode 100644 index 0000000000..015b84c530 --- /dev/null +++ b/doc/sphinx/addendum/sprop.rst @@ -0,0 +1,236 @@ +.. _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 :opt:`Allow StrictProp`. + +.. opt:: 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``. + +.. 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. + +.. opt:: Elaboration StrictProp Cumulativity + :name: Elaboration StrictProp Cumulativity + + Unset this option (it's 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. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index c7ea7e326f..e6a5b3972c 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,7 +1,7 @@ .. _typeclasses: -Type Classes -============ +Typeclasses +=========== This chapter presents a quick reference of the commands related to type classes. For an actual introduction to typeclasses, there is a @@ -15,24 +15,25 @@ Class and Instance declarations The syntax for class and instance declarations is the same as the record syntax of Coq: -``Class Id (`` |p_1| ``:`` |t_1| ``) ⋯ (`` |p_n| ``:`` |t_n| ``) [: -sort] := {`` |f_1| ``:`` |u_1| ``; ⋮`` |f_m| ``:`` |u_m| ``}.`` +.. coqdoc:: -``Instance ident : Id`` |p_1| ``⋯`` |p_n| ``:= {`` |f_1| ``:=`` |t_1| ``; ⋮`` |f_m| ``:=`` |t_m| ``}.`` + Class classname (p1 : t1) ⋯ (pn : tn) [: sort] := { f1 : u1 ; ⋯ ; fm : um }. -The |p_i| ``:`` |t_i| variables are called the *parameters* of the class and -the |f_i| ``:`` |t_i| are called the *methods*. Each class definition gives + Instance instancename q1 ⋯ qm : classname p1 ⋯ pn := { f1 := t1 ; ⋯ ; fm := tm }. + +The ``pi : ti`` variables are called the *parameters* of the class and +the ``fi : ti`` are called the *methods*. Each class definition gives rise to a corresponding record declaration and each instance is a -regular definition whose name is given by ident and type is an +regular definition whose name is given by `instancename` and type is an instantiation of the record type. We’ll use the following example class in the rest of the chapter: .. coqtop:: in - Class EqDec (A : Type) := { - eqb : A -> A -> bool ; - eqb_leibniz : forall x y, eqb x y = true -> x = y }. + Class EqDec (A : Type) := + { eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true -> x = y }. This class implements a boolean equality test which is compatible with Leibniz equality on some type. An example implementation is: @@ -40,9 +41,11 @@ Leibniz equality on some type. An example implementation is: .. coqtop:: in Instance unit_EqDec : EqDec unit := - { eqb x y := true ; - eqb_leibniz x y H := - match x, y return x = y with tt, tt => eq_refl tt end }. + { eqb x y := true ; + eqb_leibniz x y H := + match x, y return x = y with + | tt, tt => eq_refl tt + end }. Using :cmd:`Program Instance`, if one does not give all the members in the Instance declaration, Coq generates obligations for the remaining @@ -52,7 +55,7 @@ fields, e.g.: Require Import Program.Tactics. Program Instance eq_bool : EqDec bool := - { eqb x y := if x then y else negb y }. + { eqb x y := if x then y else negb y }. .. coqtop:: all @@ -127,9 +130,9 @@ the constraints as a binding context before the instance, e.g.: .. coqtop:: in Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := - { eqb x y := match x, y with - | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) - end }. + { eqb x y := match x, y with + | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) + end }. .. coqtop:: none @@ -138,21 +141,27 @@ the constraints as a binding context before the instance, e.g.: These instances are used just as well as lemmas in the instance hint database. +.. _contexts: + Sections and contexts --------------------- -To ease the parametrization of developments by typeclasses, we provide a new -way to introduce variables into section contexts, compatible with the implicit -argument mechanism. The new command works similarly to the :cmd:`Variables` -vernacular, except it accepts any binding context as argument. For example: +To ease developments parameterized by many instances, one can use the +:cmd:`Context` command to introduce these parameters into section contexts, +it works similarly to the command :cmd:`Variable`, except it accepts any +binding context as an argument, so variables can be implicit, and +:ref:`implicit-generalization` can be used. +For example: .. coqtop:: all Section EqDec_defs. - Context `{EA : EqDec A}. + Context `{EA : EqDec A}. - Global Program Instance option_eqb : EqDec (option A) := +.. coqtop:: in + + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true @@ -160,14 +169,17 @@ vernacular, except it accepts any binding context as argument. For example: end }. Admit Obligations. +.. coqtop:: all + End EqDec_defs. About option_eqb. -Here the Global modifier redeclares the instance at the end of the +Here the :cmd:`Global` modifier redeclares the instance at the end of the section, once it has been generalized by the context variables it uses. +.. seealso:: Section :ref:`section-mechanism` Building hierarchies -------------------- @@ -188,7 +200,7 @@ superclasses as a binding context: Contrary to Haskell, we have no special syntax for superclasses, but this declaration is equivalent to: -:: +.. coqdoc:: Class `(E : EqDec A) => Ord A := { le : A -> A -> bool }. @@ -248,8 +260,8 @@ explanation). These may be used as parts of other classes: .. coqtop:: all Class PreOrder (A : Type) (R : relation A) := - { PreOrder_Reflexive :> Reflexive A R ; - PreOrder_Transitive :> Transitive A R }. + { PreOrder_Reflexive :> Reflexive A R ; + PreOrder_Transitive :> Transitive A R }. The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a ``Reflexive`` relation. So each time a reflexive relation is needed, a @@ -273,33 +285,31 @@ Summary of the commands .. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } The :cmd:`Class` command is used to declare a typeclass with parameters - ``binders`` and fields the declared record fields. - -Variants: + :token:`binders` and fields the declared record fields. -.. _singleton-class: + .. _singleton-class: -.. cmd:: Class @ident {? @binders} : {? @sort} := @ident : @term + .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term - This variant declares a *singleton* class with a single method. This - singleton class is a so-called definitional class, represented simply - as a definition ``ident binders := term`` and whose instances are - themselves objects of this type. Definitional classes are not wrapped - inside records, and the trivial projection of an instance of such a - class is convertible to the instance itself. This can be useful to - make instances of existing objects easily and to reduce proof size by - not inserting useless projections. The class constant itself is - declared rigid during resolution so that the class abstraction is - maintained. + This variant declares a *singleton* class with a single method. This + singleton class is a so-called definitional class, represented simply + as a definition ``ident binders := term`` and whose instances are + themselves objects of this type. Definitional classes are not wrapped + inside records, and the trivial projection of an instance of such a + class is convertible to the instance itself. This can be useful to + make instances of existing objects easily and to reduce proof size by + not inserting useless projections. The class constant itself is + declared rigid during resolution so that the class abstraction is + maintained. -.. cmd:: Existing Class @ident + .. cmdv:: Existing Class @ident - This variant declares a class a posteriori from a constant or - inductive definition. No methods or instances are defined. + This variant declares a class a posteriori from a constant or + inductive definition. No methods or instances are defined. - .. warn:: @ident is already declared as a typeclass + .. warn:: @ident is already declared as a typeclass - This command has no effect when used on a typeclass. + This command has no effect when used on a typeclass. .. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } @@ -314,32 +324,33 @@ Variants: :tacn:`auto` hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. -.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term - This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type :n:`forall @binders, @class - @term__1 … @term__n`. One need not even mention the unique field name for - singleton classes. + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type :n:`forall @binders, @class + @term__1 … @term__n`. One need not even mention the unique field name for + singleton classes. -.. cmdv:: Global Instance + .. cmdv:: Global Instance + :name: Global Instance - One can use the ``Global`` modifier on instances declared in a - section so that their generalization is automatically redeclared - after the section is closed. + One can use the :cmd:`Global` modifier on instances declared in a + section so that their generalization is automatically redeclared + after the section is closed. -.. cmdv:: Program Instance - :name: Program Instance + .. cmdv:: Program Instance + :name: Program Instance - Switches the type checking to Program (chapter :ref:`programs`) and - uses the obligation mechanism to manage missing fields. + Switches the type checking to `Program` (chapter :ref:`programs`) and + uses the obligation mechanism to manage missing fields. -.. cmdv:: Declare Instance - :name: Declare Instance + .. cmdv:: Declare Instance + :name: Declare Instance - In a Module Type, this command states that a corresponding concrete - instance should exist in any implementation of this Module Type. This - is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or - between :cmd:`Declare Module` and :cmd:`Module`. + In a :cmd:`Module Type`, this command states that a corresponding concrete + instance should exist in any implementation of this :cmd:`Module Type`. This + is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or + between :cmd:`Declare Module` and :cmd:`Module`. Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a @@ -354,11 +365,6 @@ few other commands related to typeclasses. equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. -.. cmd:: Context @binders - - Declares variables according to the given binding context, which might - use :ref:`implicit-generalization`. - .. tacn:: typeclasses eauto :name: typeclasses eauto @@ -449,9 +455,8 @@ By default, all constants and local variables are considered transparent. One should take care not to make opaque any constant that is used to abbreviate a type, like: -:: - - relation A := A -> A -> Prop. +.. coqdoc:: + Definition relation A := A -> A -> Prop. This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. |