diff options
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/Extraction.tex | 7 | ||||
-rw-r--r-- | doc/refman/RefMan-cic.tex | 24 | ||||
-rw-r--r-- | doc/refman/RefMan-ext.tex | 10 | ||||
-rw-r--r-- | doc/refman/RefMan-pro.tex | 16 | ||||
-rw-r--r-- | doc/refman/RefMan-sch.tex | 7 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 46 | ||||
-rw-r--r-- | doc/refman/Universes.tex | 46 |
7 files changed, 125 insertions, 31 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 01dbcfb1c..fa3d61b1c 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -19,6 +19,12 @@ be used (abusively) to refer to any of the three. %% the one in previous versions of \Coq: there is no more %% an explicit toplevel for the language (formerly called \textsc{Fml}). +Before using any of the commands or options described in this chapter, +the extraction framework should first be loaded explicitly +via {\tt Require Extraction}. Note that in earlier versions of Coq, these +commands and options were directly available without any preliminary +{\tt Require}. + \asection{Generating ML code} \comindex{Extraction} \comindex{Recursive Extraction} @@ -501,6 +507,7 @@ We can now extract this program to \ocaml: Reset Initial. \end{coq_eval} \begin{coq_example} +Require Extraction. Require Import Euclid Wf_nat. Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. Recursive Extraction eucl_dev. diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index fdd272581..96fb1eb75 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -461,6 +461,13 @@ recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$. We then write $\WTEGCONV{t_1}{t_2}$. +Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below) +convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e., +$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$. +Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$ +and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels) +such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$. + The convertibility relation allows introducing a new typing rule which says that two convertible well-formed types have the same inhabitants. @@ -480,6 +487,17 @@ convertibility into a {\em subtyping} relation inductively defined by: \item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity, $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$ \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T, T'}{\forall~x:U, U'}$. +\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full}) + inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$ + and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$ + are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors + \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\] + and + \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\] + respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type) + if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have + \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\] + where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$. \end{enumerate} The conversion rule up to subtyping is now exactly: @@ -530,8 +548,12 @@ Formally, we can represent any {\em inductive definition\index{definition!induct These inductive definitions, together with global assumptions and global definitions, then form the global environment. % Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$ -such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as: +such that each $T$ in $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as: $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}. +Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as: +$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the +{\em Arity} of the inductive type\index{arity of inductive type} $t$ and +$\Sort$ is called the sort of the inductive type $t$. \paragraph{Examples} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 6dd0ddf81..939fc87a6 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -721,18 +721,20 @@ a given type. See Section~\ref{Show}. \section{Advanced recursive functions} -The \emph{experimental} command +The following \emph{experimental} command is available +when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: \begin{center} \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} \{decrease\_annot\} : type$_0$ := \term$_0$} \comindex{Function} \label{Function} \end{center} -can be seen as a generalization of {\tt Fixpoint}. It is actually a -wrapper for several ways of defining a function \emph{and other useful +This command can be seen as a generalization of {\tt Fixpoint}. It is actually +a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the recursive structure of the function (see \ref{FunInduction}), and its -fixpoint equality. The meaning of this +fixpoint equality. + The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be given (unless the function is not recursive), but it must not diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 0760d716e..b66659dc8 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -427,22 +427,6 @@ This command displays the current goals. This tactics script may contain some holes (subgoals not yet proved). They are printed under the form \verb!<Your Tactic Text here>!. -%% \item {\tt Show Tree.}\comindex{Show Tree}\\ -%% This command can be seen as a more structured way of -%% displaying the state of the proof than that -%% provided by {\tt Show Script}. Instead of just giving -%% the list of tactics that have been applied, it -%% shows the derivation tree constructed by then. -%% Each node of the tree contains the conclusion -%% of the corresponding sub-derivation (i.e. a -%% goal with its corresponding local context) and -%% the tactic that has generated all the -%% sub-derivations. The leaves of this tree are -%% the goals which still remain to be proved. - -%\item {\tt Show Node}\comindex{Show Node}\\ -% Not yet documented - \item {\tt Show Proof.}\comindex{Show Proof}\\ It displays the proof term generated by the tactics that have been applied. diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 53aa6b86a..d3719bed4 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -196,8 +196,10 @@ Check tree_forest_mutind. The {\tt Functional Scheme} command is a high-level experimental tool for generating automatically induction principles -corresponding to (possibly mutually recursive) functions. Its -syntax follows the schema: +corresponding to (possibly mutually recursive) functions. +First, it must be made available via {\tt Require Import FunInd}. + Its +syntax then follows the schema: \begin{quote} {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ with\\ @@ -319,6 +321,7 @@ of a tree or a forest. Note that we use \texttt{Function} which generally produces better principles. \begin{coq_example*} +Require Import FunInd. Function tree_size (t:tree) : nat := match t with | node A f => S (forest_size f) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 253eb7f01..be75dc9d5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1053,21 +1053,31 @@ dependencies. This tactic is the inverse of {\tt intro}. \label{move} This moves the hypothesis named {\ident$_1$} in the local context -after the hypothesis named {\ident$_2$}. The proof term is not changed. +after the hypothesis named {\ident$_2$}, where ``after'' is in +reference to the direction of the move. The proof term is not changed. -If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies, -then all the hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) depend on {\ident$_1$} are moved too. +If {\ident$_1$} comes before {\ident$_2$} in the order of +dependencies, then all the hypotheses between {\ident$_1$} and +{\ident$_2$} that (possibly indirectly) depend on {\ident$_1$} are +moved too, and all of them are thus moved after {\ident$_2$} in the +order of dependencies. If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies, then all the hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) occur in {\ident$_1$} are moved too. +(possibly indirectly) occur in the type of {\ident$_1$} are moved +too, and all of them are thus moved before {\ident$_2$} in the order +of dependencies. \begin{Variants} \item {\tt move {\ident$_1$} before {\ident$_2$}} -This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}. +This moves {\ident$_1$} towards and just before the hypothesis named +{\ident$_2$}. As for {\tt move {\ident$_1$} after {\ident$_2$}}, +dependencies over {\ident$_1$} (when {\ident$_1$} comes before +{\ident$_2$} in the order of dependencies) or in the type of +{\ident$_1$} (when {\ident$_1$} comes after {\ident$_2$} in the order +of dependencies) are moved too. \item {\tt move {\ident} at top} @@ -1084,13 +1094,30 @@ This moves {\ident} at the bottom of the local context (at the end of the contex \item \errindex{No such hypothesis} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: - it occurs in {\ident$_2$}} + it occurs in the type of {\ident$_2$}} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: it depends on {\ident$_2$}} \end{ErrMsgs} +\Example + +\begin{coq_example} +Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. +intros x H z y H0. +move x after H0. +Undo. +move x before H0. +Undo. +move H0 after H. +Undo. +move H0 before H. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + \subsection{\tt rename {\ident$_1$} into {\ident$_2$}} \tacindex{rename} @@ -2113,13 +2140,15 @@ The tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} -(see Section~\ref{FunScheme}). +(see Section~\ref{FunScheme}). Note that this tactic is only available +after a {\tt Require Import FunInd}. \begin{coq_eval} Reset Initial. Import Nat. \end{coq_eval} \begin{coq_example} +Require Import FunInd. Functional Scheme minus_ind := Induction for minus Sort Prop. Check minus_ind. Lemma le_minus (n m:nat) : n - m <= n. @@ -4797,6 +4826,7 @@ that performs inversion on hypothesis {\ident} of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been defined using \texttt{Function} (see Section~\ref{Function}). +Note that this tactic is only available after a {\tt Require Import FunInd}. \begin{ErrMsgs} \item \errindex{Hypothesis {\ident} must contain at least one Function} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 36518e6fa..2bb1301c7 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -131,6 +131,52 @@ producing global universe constraints, one can use the polymorphically, not at a single instance. \end{itemize} +\asection{{\tt Cumulative, NonCumulative}} +\comindex{Cumulative} +\comindex{NonCumulative} +\optindex{Inductive Cumulativity} + +Inductive types, coinductive types, variants and records can be +declared cumulative using the \texttt{Cumulative}. Alternatively, +there is an option \texttt{Set Inductive Cumulativity} which when set, +makes all subsequent inductive definitions cumulative. 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 part of the output of the form +\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff } +indicates the universe constraints in order to have the subtyping +$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ +(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$. +In the case of \texttt{list} there is no constraint! +This also means that 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. +Also notice the subtyping constraints for the \emph{non-cumulative} version of list: +\begin{coq_example*} +Polymorphic NonCumulative Inductive list' {A : Type} := +| nil' : list' +| cons' : A -> list' -> list'. +\end{coq_example*} +\begin{coq_example} +Print list'. +\end{coq_example} +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} +Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}. + + \asection{Global and local universes} Each universe is declared in a global or local environment before it can |