From b36448114c3853311e31f533657a4d4e78b2820c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 12:38:05 +0200 Subject: Remove commented documentation for Show Tree. --- doc/refman/RefMan-pro.tex | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 0760d716e3..b66659dc8c 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!!. -%% \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. -- cgit v1.2.3 From 4db32ffb3a157077be771f753ba8b5e4a8efc631 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Jun 2017 17:05:27 +0200 Subject: Improving documentation of tactic "move" (report #4561). --- doc/refman/RefMan-tac.tex | 41 ++++++++++++++++++++++++++++++++++------- 1 file changed, 34 insertions(+), 7 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 253eb7f01b..673071c58a 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} -- cgit v1.2.3 From bcaf9af83363f3e1a1c588271e5038984ee1760b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 8 Apr 2017 07:04:56 +0200 Subject: Remove support for Coq 8.4. --- doc/stdlib/index-list.html.template | 1 - 1 file changed, 1 deletion(-) (limited to 'doc') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 1b847414f2..48f82f2d92 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -589,7 +589,6 @@ through the Require Import command.

theories/Compat/AdmitAxiom.v - theories/Compat/Coq84.v theories/Compat/Coq85.v theories/Compat/Coq86.v
-- cgit v1.2.3 From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 23 Jun 2016 15:07:02 +0200 Subject: Prelude : no more autoload of plugins extraction and recdef The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. --- doc/refman/Extraction.tex | 7 +++++++ doc/refman/RefMan-ext.tex | 10 ++++++---- doc/refman/RefMan-sch.tex | 7 +++++-- doc/refman/RefMan-tac.tex | 5 ++++- 4 files changed, 22 insertions(+), 7 deletions(-) (limited to 'doc') diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 01dbcfb1cb..fa3d61b1cd 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-ext.tex b/doc/refman/RefMan-ext.tex index 6dd0ddf81d..939fc87a6e 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-sch.tex b/doc/refman/RefMan-sch.tex index 53aa6b86ab..d3719bed46 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 253eb7f01b..2bab04e90a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2113,13 +2113,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 +4799,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} -- cgit v1.2.3 From e28d3a488c81c6dc59aa8f53d98a95ee93a84d37 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 23 May 2017 23:28:39 +0200 Subject: Document cumulativity for inductive types --- doc/refman/RefMan-cic.tex | 24 +++++++++++++++++++++++- doc/refman/Universes.tex | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 69 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index fdd2725810..96fb1eb752 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/Universes.tex b/doc/refman/Universes.tex index 36518e6fae..2bb1301c79 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 -- cgit v1.2.3