From 068dfb13db8b8801a1b5f7694a3fe90d640c7577 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 29 Mar 2018 18:20:33 +0200 Subject: [Sphinx] Move chapter 29 to new infrastructure --- Makefile.doc | 3 +- doc/refman/Reference-Manual.tex | 1 - doc/refman/Universes.tex | 393 -------------------------- doc/sphinx/addendum/universe-polymorphism.rst | 393 ++++++++++++++++++++++++++ 4 files changed, 394 insertions(+), 396 deletions(-) delete mode 100644 doc/refman/Universes.tex create mode 100644 doc/sphinx/addendum/universe-polymorphism.rst diff --git a/Makefile.doc b/Makefile.doc index e52da403a..b9443f723 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -58,8 +58,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ - RefMan-ltac.v.tex \ - Universes.v.tex) + RefMan-ltac.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex) \ diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 061686e12..d373f76bf 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -109,7 +109,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{Universes.v}% Universe polymorphes %BEGIN LATEX \RefManCutCommand{ENDADDENDUM=\thepage} %END LATEX diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex deleted file mode 100644 index c7d39c0f3..000000000 --- a/doc/refman/Universes.tex +++ /dev/null @@ -1,393 +0,0 @@ -\achapter{Polymorphic Universes} -%HEVEA\cutname{universes.html} -\aauthor{Matthieu Sozeau} - -\label{Universes-full} -\index{Universes!presentation} - -\asection{General Presentation} - -\begin{flushleft} - \em The status of Universe Polymorphism is experimental. -\end{flushleft} - -This section describes the universe polymorphic extension of Coq. -Universe polymorphism makes it possible to write generic definitions making use of -universes and reuse them at different and sometimes incompatible universe levels. - -A standard example of the difference between universe \emph{polymorphic} and -\emph{monomorphic} definitions is given by the identity function: - -\begin{coq_example*} -Definition identity {A : Type} (a : A) := a. -\end{coq_example*} - -By default, constant declarations are monomorphic, hence the identity -function declares a global universe (say \texttt{Top.1}) for its -domain. Subsequently, if we try to self-apply the identity, we will get -an error: - -\begin{coq_eval} -Set Printing Universes. -\end{coq_eval} -\begin{coq_example} -Fail Definition selfid := identity (@identity). -\end{coq_example} - -Indeed, the global level \texttt{Top.1} would have to be strictly smaller than itself -for this self-application to typecheck, as the type of \texttt{(@identity)} is -\texttt{forall (A : Type@{Top.1}), A -> A} whose type is itself \texttt{Type@{Top.1+1}}. - -A universe polymorphic identity function binds its domain universe level -at the definition level instead of making it global. - -\begin{coq_example} -Polymorphic Definition pidentity {A : Type} (a : A) := a. -About pidentity. -\end{coq_example} - -It is then possible to reuse the constant at different levels, like so: - -\begin{coq_example} -Definition selfpid := pidentity (@pidentity). -\end{coq_example} - -Of course, the two instances of \texttt{pidentity} in this definition -are different. This can be seen when \texttt{Set Printing Universes} is -on: - -\begin{coq_example} -Print selfpid. -\end{coq_example} - -Now \texttt{pidentity} is used at two different levels: at the head of -the application it is instantiated at \texttt{Top.3} while in the -argument position it is instantiated at \texttt{Top.4}. This definition -is only valid as long as \texttt{Top.4} is strictly smaller than -\texttt{Top.3}, as show by the constraints. Note that this definition is -monomorphic (not universe polymorphic), so the two universes -(in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels. - -When printing \texttt{pidentity}, we can see the universes it binds in -the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set - Printing Universes} is on we print the ``universe context'' of -\texttt{pidentity} consisting of the bound universes and the -constraints they must verify (for \texttt{pidentity} there are no -constraints). - -Inductive types can also be declared universes polymorphic on universes -appearing in their parameters or fields. A typical example is given by -monoids: - -\begin{coq_example} -Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car; - mon_op : mon_car -> mon_car -> mon_car }. -Print Monoid. -\end{coq_example} - -The \texttt{Monoid}'s carrier universe is polymorphic, hence it is -possible to instantiate it for example with \texttt{Monoid} itself. -First we build the trivial unit monoid in \texttt{Set}: -\begin{coq_example} -Definition unit_monoid : Monoid := - {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. -\end{coq_example} - -From this we can build a definition for the monoid of -\texttt{Set}-monoids (where multiplication would be given by the product -of monoids). - -\begin{coq_example*} -Polymorphic Definition monoid_monoid : Monoid. - refine (@Build_Monoid Monoid unit_monoid (fun x y => x)). -Defined. -\end{coq_example*} -\begin{coq_example} -Print monoid_monoid. -\end{coq_example} - -As one can see from the constraints, this monoid is ``large'', it lives -in a universe strictly higher than \texttt{Set}. - -\asection{\tt Polymorphic, Monomorphic} -\comindex{Polymorphic} -\comindex{Monomorphic} -\optindex{Universe Polymorphism} - -As shown in the examples, polymorphic definitions and inductives can be -declared using the \texttt{Polymorphic} prefix. There also exists an -option \texttt{Set Universe Polymorphism} which will implicitly prepend -it to any definition of the user. In that case, to make a definition -producing global universe constraints, one can use the -\texttt{Monomorphic} prefix. Many other commands support the -\texttt{Polymorphic} flag, including: - -\begin{itemize} -\item \texttt{Lemma}, \texttt{Axiom}, and all the other ``definition'' - keywords support polymorphism. -\item \texttt{Variables}, \texttt{Context}, \texttt{Universe} and - \texttt{Constraint} in a section support polymorphism. This means - that the universe variables (and associated constraints) are - discharged polymorphically over definitions that use them. In other - words, two definitions in the section sharing a common variable will - both get parameterized by the universes produced by the variable - declaration. This is in contrast to a ``mononorphic'' variable which - introduces global universes and constraints, making the two - definitions depend on the \emph{same} global universes associated to - the variable. -\item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint - polymorphically, not at a single instance. -\end{itemize} - -\asection{{\tt Cumulative, NonCumulative}} -\comindex{Cumulative} -\comindex{NonCumulative} -\optindex{Polymorphic Inductive Cumulativity} - -Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the \texttt{Cumulative} prefix. Alternatively, -there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set, -makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set, -inductive types and the like can be enforced to be -\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below. -\begin{coq_example*} -Polymorphic Cumulative Inductive list {A : Type} := -| nil : list -| cons : A -> list -> list. -\end{coq_example*} -\begin{coq_example} -Print list. -\end{coq_example} -When printing \texttt{list}, the universe context indicates the -subtyping constraints by prefixing the level names with symbols. - -Because inductive subtypings are only produced by comparing inductives -to themselves with universes changed, they amount to variance -information: each universe is either invariant, covariant or -irrelevant (there are no contravariant subtypings in Coq), -respectively represented by the symbols \texttt{=}, \texttt{+} and -\texttt{*}. - -Here we see that \texttt{list} binds an irrelevant universe, so any -two instances of \texttt{list} are convertible: -$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever -$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully -applied to convertible arguments) constructors. - -See Chapter~\ref{Cic} for more details on convertibility and subtyping. -The following is an example of a record with non-trivial subtyping relation: -\begin{coq_example*} -Polymorphic Cumulative Record packType := {pk : Type}. -\end{coq_example*} -\begin{coq_example} -Print packType. -\end{coq_example} -\texttt{packType} binds a covariant universe, i.e. -$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever -\texttt{i $\leq$ j}. - -Cumulative inductive types, coninductive types, variants and records -only make sense when they are universe polymorphic. Therefore, an -error is issued whenever the user uses the \texttt{Cumulative} or -\texttt{NonCumulative} prefix in a monomorphic context. -Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}. -That is, this option, when set, makes all subsequent \emph{polymorphic} -inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used) -but has no effect on \emph{monomorphic} inductive declarations. -Consider the following examples. -\begin{coq_example} -Monomorphic Cumulative Inductive Unit := unit. -\end{coq_example} -\begin{coq_example} -Monomorphic NonCumulative Inductive Unit := unit. -\end{coq_example} -\begin{coq_example*} -Set Polymorphic Inductive Cumulativity. -Inductive Unit := unit. -\end{coq_example*} -\begin{coq_example} -Print Unit. -\end{coq_example} - -\subsection*{An example of a proof using cumulativity} - -\begin{coq_example} -Set Universe Polymorphism. -Set Polymorphic Inductive Cumulativity. - -Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. - -Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) - := forall f g : (forall a, B a), - (forall x, eq@{e} (f x) (g x)) - -> eq@{e} f g. - -Section down. - Universes a b e e'. - Constraint e' < e. - Lemma funext_down {A B} - (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B. - Proof. - exact H. - Defined. -\end{coq_example} - -\subsection{\tt Cumulativity Weak Constraints} -\optindex{Cumulativity Weak Constraints} - -This option, on by default, causes ``weak'' constraints to be produced -when comparing universes in an irrelevant position. Processing weak -constraints is delayed until minimization time. A weak constraint -between {\tt u} and {\tt v} when neither is smaller than the other and -one is flexible causes them to be unified. Otherwise the constraint is -silently discarded. - -This heuristic is experimental and may change in future versions. -Disabling weak constraints is more predictable but may produce -arbitrary numbers of universes. - -\asection{Global and local universes} - -Each universe is declared in a global or local environment before it can -be used. To ensure compatibility, every \emph{global} universe is set to -be strictly greater than \Set~when it is introduced, while every -\emph{local} (i.e. polymorphically quantified) universe is introduced as -greater or equal to \Set. - -\asection{Conversion and unification} - -The semantics of conversion and unification have to be modified a little -to account for the new universe instance arguments to polymorphic -references. The semantics respect the fact that definitions are -transparent, so indistinguishable from their bodies during conversion. - -This is accomplished by changing one rule of unification, the -first-order approximation rule, which applies when two applicative terms -with the same head are compared. It tries to short-cut unfolding by -comparing the arguments directly. In case the constant is universe -polymorphic, we allow this rule to fire only when unifying the universes -results in instantiating a so-called flexible universe variables (not -given by the user). Similarly for conversion, if such an equation of -applicative terms fail due to a universe comparison not being satisfied, -the terms are unfolded. This change implies that conversion and -unification can have different unfolding behaviors on the same -development with universe polymorphism switched on or off. - -\asection{Minimization} -\optindex{Universe Minimization ToSet} - -Universe polymorphism with cumulativity tends to generate many useless -inclusion constraints in general. Typically at each application of a -polymorphic constant $f$, if an argument has expected type -\verb|Type@{i}| and is given a term of type \verb|Type@{j}|, a $j \le i$ -constraint will be generated. It is however often the case that an -equation $j = i$ would be more appropriate, when $f$'s -universes are fresh for example. Consider the following example: - -\begin{coq_eval} -Set Printing Universes. -\end{coq_eval} -\begin{coq_example} -Definition id0 := @pidentity nat 0. -Print id0. -\end{coq_example} - -This definition is elaborated by minimizing the universe of id to level -\Set~while the more general definition would keep the fresh level i -generated at the application of id and a constraint that $\Set \le i$. -This minimization process is applied only to fresh universe -variables. It simply adds an equation between the variable and its lower -bound if it is an atomic universe (i.e. not an algebraic \texttt{max()} -universe). - -The option \texttt{Unset Universe Minimization ToSet} disallows -minimization to the sort $\Set$ and only collapses floating universes -between themselves. - -\asection{Explicit Universes} - -The syntax has been extended to allow users to explicitly bind names to -universes and explicitly instantiate polymorphic definitions. - -\subsection{\tt Universe {\ident}. - \comindex{Universe} - \label{UniverseCmd}} - -In the monorphic case, this command declares a new global universe named -{\ident}, which can be referred to using its qualified name as -well. Global universe names live in a separate namespace. The command -supports the polymorphic flag only in sections, meaning the universe -quantification will be discharged on each section definition -independently. One cannot mix polymorphic and monomorphic declarations -in the same section. - -\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. - \comindex{Constraint} - \label{ConstraintCmd}} - -This command declares a new constraint between named universes. -The order relation can be one of $<$, $\le$ or $=$. If consistent, -the constraint is then enforced in the global environment. Like -\texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix -in sections only to declare constraints discharged at section closing time. -One cannot declare a global constraint on polymorphic universes. - -\begin{ErrMsgs} -\item \errindex{Undeclared universe {\ident}}. -\item \errindex{Universe inconsistency} -\end{ErrMsgs} - -\subsection{Polymorphic definitions} -For polymorphic definitions, the declaration of (all) universe levels -introduced by a definition uses the following syntax: - -\begin{coq_example*} -Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. -\end{coq_example*} -\begin{coq_example} -Print le. -\end{coq_example} - -During refinement we find that $j$ must be larger or equal than $i$, as -we are using $A : Type@{i} <= Type@{j}$, hence the generated -constraint. At the end of a definition or proof, we check that the only -remaining universes are the ones declared. In the term and in general in -proof mode, introduced universe names can be referred to in -terms. Note that local universe names shadow global universe names. -During a proof, one can use \texttt{Show Universes} to display -the current context of universes. - -Definitions can also be instantiated explicitly, giving their full instance: -\begin{coq_example} -Check (pidentity@{Set}). -Universes k l. -Check (le@{k l}). -\end{coq_example} - -User-named universes and the anonymous universe implicitly attached to -an explicit $Type$ are considered rigid for unification and are never -minimized. Flexible anonymous universes can be produced with an -underscore or by omitting the annotation to a polymorphic definition. - -\begin{coq_example} - Check (fun x => x) : Type -> Type. - Check (fun x => x) : Type -> Type@{_}. - - Check le@{k _}. - Check le. -\end{coq_example} - -\subsection{\tt Unset Strict Universe Declaration. - \optindex{Strict Universe Declaration} - \label{StrictUniverseDeclaration}} - -The command \texttt{Unset Strict Universe Declaration} allows one to -freely use identifiers for universes without declaring them first, with -the semantics that the first use declares it. In this mode, the universe -names are not associated with the definition or proof once it has been -defined. This is meant mainly for debugging purposes. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst new file mode 100644 index 000000000..c7d39c0f3 --- /dev/null +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -0,0 +1,393 @@ +\achapter{Polymorphic Universes} +%HEVEA\cutname{universes.html} +\aauthor{Matthieu Sozeau} + +\label{Universes-full} +\index{Universes!presentation} + +\asection{General Presentation} + +\begin{flushleft} + \em The status of Universe Polymorphism is experimental. +\end{flushleft} + +This section describes the universe polymorphic extension of Coq. +Universe polymorphism makes it possible to write generic definitions making use of +universes and reuse them at different and sometimes incompatible universe levels. + +A standard example of the difference between universe \emph{polymorphic} and +\emph{monomorphic} definitions is given by the identity function: + +\begin{coq_example*} +Definition identity {A : Type} (a : A) := a. +\end{coq_example*} + +By default, constant declarations are monomorphic, hence the identity +function declares a global universe (say \texttt{Top.1}) for its +domain. Subsequently, if we try to self-apply the identity, we will get +an error: + +\begin{coq_eval} +Set Printing Universes. +\end{coq_eval} +\begin{coq_example} +Fail Definition selfid := identity (@identity). +\end{coq_example} + +Indeed, the global level \texttt{Top.1} would have to be strictly smaller than itself +for this self-application to typecheck, as the type of \texttt{(@identity)} is +\texttt{forall (A : Type@{Top.1}), A -> A} whose type is itself \texttt{Type@{Top.1+1}}. + +A universe polymorphic identity function binds its domain universe level +at the definition level instead of making it global. + +\begin{coq_example} +Polymorphic Definition pidentity {A : Type} (a : A) := a. +About pidentity. +\end{coq_example} + +It is then possible to reuse the constant at different levels, like so: + +\begin{coq_example} +Definition selfpid := pidentity (@pidentity). +\end{coq_example} + +Of course, the two instances of \texttt{pidentity} in this definition +are different. This can be seen when \texttt{Set Printing Universes} is +on: + +\begin{coq_example} +Print selfpid. +\end{coq_example} + +Now \texttt{pidentity} is used at two different levels: at the head of +the application it is instantiated at \texttt{Top.3} while in the +argument position it is instantiated at \texttt{Top.4}. This definition +is only valid as long as \texttt{Top.4} is strictly smaller than +\texttt{Top.3}, as show by the constraints. Note that this definition is +monomorphic (not universe polymorphic), so the two universes +(in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels. + +When printing \texttt{pidentity}, we can see the universes it binds in +the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set + Printing Universes} is on we print the ``universe context'' of +\texttt{pidentity} consisting of the bound universes and the +constraints they must verify (for \texttt{pidentity} there are no +constraints). + +Inductive types can also be declared universes polymorphic on universes +appearing in their parameters or fields. A typical example is given by +monoids: + +\begin{coq_example} +Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car; + mon_op : mon_car -> mon_car -> mon_car }. +Print Monoid. +\end{coq_example} + +The \texttt{Monoid}'s carrier universe is polymorphic, hence it is +possible to instantiate it for example with \texttt{Monoid} itself. +First we build the trivial unit monoid in \texttt{Set}: +\begin{coq_example} +Definition unit_monoid : Monoid := + {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. +\end{coq_example} + +From this we can build a definition for the monoid of +\texttt{Set}-monoids (where multiplication would be given by the product +of monoids). + +\begin{coq_example*} +Polymorphic Definition monoid_monoid : Monoid. + refine (@Build_Monoid Monoid unit_monoid (fun x y => x)). +Defined. +\end{coq_example*} +\begin{coq_example} +Print monoid_monoid. +\end{coq_example} + +As one can see from the constraints, this monoid is ``large'', it lives +in a universe strictly higher than \texttt{Set}. + +\asection{\tt Polymorphic, Monomorphic} +\comindex{Polymorphic} +\comindex{Monomorphic} +\optindex{Universe Polymorphism} + +As shown in the examples, polymorphic definitions and inductives can be +declared using the \texttt{Polymorphic} prefix. There also exists an +option \texttt{Set Universe Polymorphism} which will implicitly prepend +it to any definition of the user. In that case, to make a definition +producing global universe constraints, one can use the +\texttt{Monomorphic} prefix. Many other commands support the +\texttt{Polymorphic} flag, including: + +\begin{itemize} +\item \texttt{Lemma}, \texttt{Axiom}, and all the other ``definition'' + keywords support polymorphism. +\item \texttt{Variables}, \texttt{Context}, \texttt{Universe} and + \texttt{Constraint} in a section support polymorphism. This means + that the universe variables (and associated constraints) are + discharged polymorphically over definitions that use them. In other + words, two definitions in the section sharing a common variable will + both get parameterized by the universes produced by the variable + declaration. This is in contrast to a ``mononorphic'' variable which + introduces global universes and constraints, making the two + definitions depend on the \emph{same} global universes associated to + the variable. +\item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint + polymorphically, not at a single instance. +\end{itemize} + +\asection{{\tt Cumulative, NonCumulative}} +\comindex{Cumulative} +\comindex{NonCumulative} +\optindex{Polymorphic Inductive Cumulativity} + +Polymorphic inductive types, coinductive types, variants and records can be +declared cumulative using the \texttt{Cumulative} prefix. Alternatively, +there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set, +makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set, +inductive types and the like can be enforced to be +\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below. +\begin{coq_example*} +Polymorphic Cumulative Inductive list {A : Type} := +| nil : list +| cons : A -> list -> list. +\end{coq_example*} +\begin{coq_example} +Print list. +\end{coq_example} +When printing \texttt{list}, the universe context indicates the +subtyping constraints by prefixing the level names with symbols. + +Because inductive subtypings are only produced by comparing inductives +to themselves with universes changed, they amount to variance +information: each universe is either invariant, covariant or +irrelevant (there are no contravariant subtypings in Coq), +respectively represented by the symbols \texttt{=}, \texttt{+} and +\texttt{*}. + +Here we see that \texttt{list} binds an irrelevant universe, so any +two instances of \texttt{list} are convertible: +$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever +$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully +applied to convertible arguments) constructors. + +See Chapter~\ref{Cic} for more details on convertibility and subtyping. +The following is an example of a record with non-trivial subtyping relation: +\begin{coq_example*} +Polymorphic Cumulative Record packType := {pk : Type}. +\end{coq_example*} +\begin{coq_example} +Print packType. +\end{coq_example} +\texttt{packType} binds a covariant universe, i.e. +$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever +\texttt{i $\leq$ j}. + +Cumulative inductive types, coninductive types, variants and records +only make sense when they are universe polymorphic. Therefore, an +error is issued whenever the user uses the \texttt{Cumulative} or +\texttt{NonCumulative} prefix in a monomorphic context. +Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}. +That is, this option, when set, makes all subsequent \emph{polymorphic} +inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used) +but has no effect on \emph{monomorphic} inductive declarations. +Consider the following examples. +\begin{coq_example} +Monomorphic Cumulative Inductive Unit := unit. +\end{coq_example} +\begin{coq_example} +Monomorphic NonCumulative Inductive Unit := unit. +\end{coq_example} +\begin{coq_example*} +Set Polymorphic Inductive Cumulativity. +Inductive Unit := unit. +\end{coq_example*} +\begin{coq_example} +Print Unit. +\end{coq_example} + +\subsection*{An example of a proof using cumulativity} + +\begin{coq_example} +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. + +Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + +Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + +Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B. + Proof. + exact H. + Defined. +\end{coq_example} + +\subsection{\tt Cumulativity Weak Constraints} +\optindex{Cumulativity Weak Constraints} + +This option, on by default, causes ``weak'' constraints to be produced +when comparing universes in an irrelevant position. Processing weak +constraints is delayed until minimization time. A weak constraint +between {\tt u} and {\tt v} when neither is smaller than the other and +one is flexible causes them to be unified. Otherwise the constraint is +silently discarded. + +This heuristic is experimental and may change in future versions. +Disabling weak constraints is more predictable but may produce +arbitrary numbers of universes. + +\asection{Global and local universes} + +Each universe is declared in a global or local environment before it can +be used. To ensure compatibility, every \emph{global} universe is set to +be strictly greater than \Set~when it is introduced, while every +\emph{local} (i.e. polymorphically quantified) universe is introduced as +greater or equal to \Set. + +\asection{Conversion and unification} + +The semantics of conversion and unification have to be modified a little +to account for the new universe instance arguments to polymorphic +references. The semantics respect the fact that definitions are +transparent, so indistinguishable from their bodies during conversion. + +This is accomplished by changing one rule of unification, the +first-order approximation rule, which applies when two applicative terms +with the same head are compared. It tries to short-cut unfolding by +comparing the arguments directly. In case the constant is universe +polymorphic, we allow this rule to fire only when unifying the universes +results in instantiating a so-called flexible universe variables (not +given by the user). Similarly for conversion, if such an equation of +applicative terms fail due to a universe comparison not being satisfied, +the terms are unfolded. This change implies that conversion and +unification can have different unfolding behaviors on the same +development with universe polymorphism switched on or off. + +\asection{Minimization} +\optindex{Universe Minimization ToSet} + +Universe polymorphism with cumulativity tends to generate many useless +inclusion constraints in general. Typically at each application of a +polymorphic constant $f$, if an argument has expected type +\verb|Type@{i}| and is given a term of type \verb|Type@{j}|, a $j \le i$ +constraint will be generated. It is however often the case that an +equation $j = i$ would be more appropriate, when $f$'s +universes are fresh for example. Consider the following example: + +\begin{coq_eval} +Set Printing Universes. +\end{coq_eval} +\begin{coq_example} +Definition id0 := @pidentity nat 0. +Print id0. +\end{coq_example} + +This definition is elaborated by minimizing the universe of id to level +\Set~while the more general definition would keep the fresh level i +generated at the application of id and a constraint that $\Set \le i$. +This minimization process is applied only to fresh universe +variables. It simply adds an equation between the variable and its lower +bound if it is an atomic universe (i.e. not an algebraic \texttt{max()} +universe). + +The option \texttt{Unset Universe Minimization ToSet} disallows +minimization to the sort $\Set$ and only collapses floating universes +between themselves. + +\asection{Explicit Universes} + +The syntax has been extended to allow users to explicitly bind names to +universes and explicitly instantiate polymorphic definitions. + +\subsection{\tt Universe {\ident}. + \comindex{Universe} + \label{UniverseCmd}} + +In the monorphic case, this command declares a new global universe named +{\ident}, which can be referred to using its qualified name as +well. Global universe names live in a separate namespace. The command +supports the polymorphic flag only in sections, meaning the universe +quantification will be discharged on each section definition +independently. One cannot mix polymorphic and monomorphic declarations +in the same section. + +\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. + \comindex{Constraint} + \label{ConstraintCmd}} + +This command declares a new constraint between named universes. +The order relation can be one of $<$, $\le$ or $=$. If consistent, +the constraint is then enforced in the global environment. Like +\texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix +in sections only to declare constraints discharged at section closing time. +One cannot declare a global constraint on polymorphic universes. + +\begin{ErrMsgs} +\item \errindex{Undeclared universe {\ident}}. +\item \errindex{Universe inconsistency} +\end{ErrMsgs} + +\subsection{Polymorphic definitions} +For polymorphic definitions, the declaration of (all) universe levels +introduced by a definition uses the following syntax: + +\begin{coq_example*} +Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. +\end{coq_example*} +\begin{coq_example} +Print le. +\end{coq_example} + +During refinement we find that $j$ must be larger or equal than $i$, as +we are using $A : Type@{i} <= Type@{j}$, hence the generated +constraint. At the end of a definition or proof, we check that the only +remaining universes are the ones declared. In the term and in general in +proof mode, introduced universe names can be referred to in +terms. Note that local universe names shadow global universe names. +During a proof, one can use \texttt{Show Universes} to display +the current context of universes. + +Definitions can also be instantiated explicitly, giving their full instance: +\begin{coq_example} +Check (pidentity@{Set}). +Universes k l. +Check (le@{k l}). +\end{coq_example} + +User-named universes and the anonymous universe implicitly attached to +an explicit $Type$ are considered rigid for unification and are never +minimized. Flexible anonymous universes can be produced with an +underscore or by omitting the annotation to a polymorphic definition. + +\begin{coq_example} + Check (fun x => x) : Type -> Type. + Check (fun x => x) : Type -> Type@{_}. + + Check le@{k _}. + Check le. +\end{coq_example} + +\subsection{\tt Unset Strict Universe Declaration. + \optindex{Strict Universe Declaration} + \label{StrictUniverseDeclaration}} + +The command \texttt{Unset Strict Universe Declaration} allows one to +freely use identifiers for universes without declaring them first, with +the semantics that the first use declares it. In this mode, the universe +names are not associated with the definition or proof once it has been +defined. This is meant mainly for debugging purposes. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3