diff options
| -rwxr-xr-x | doc/Changes.tex | 30 | ||||
| -rwxr-xr-x | doc/RefMan-lib.tex | 93 | ||||
| -rw-r--r-- | doc/RefMan-tac.tex | 22 | ||||
| -rwxr-xr-x | doc/biblio.bib | 8 |
4 files changed, 135 insertions, 18 deletions
diff --git a/doc/Changes.tex b/doc/Changes.tex index 2ec6ed3189..e4af1b996a 100755 --- a/doc/Changes.tex +++ b/doc/Changes.tex @@ -307,13 +307,15 @@ details, see the Reference Manual. \paragraph{{\tt Fourier}} written by LoÏc Pottier solves linear inequations. - \paragraph{Others tactics and developments} has been included in the Reals -library: {\tt DiscrR} prove that a real integer constante c1 is non equal to -another real integer constante c2; {\tt SplitAbsolu} allows us to split -Rabsolu; {\tt SplitRmult} allows us to split Rabsolu a product non equal to -zero and give the corresponding subgoals with each term non equal to zero. -All this tactics has been written with the tactic language $\ltac$.\\ -A development on Cauchy series, power series,... has been added.\\ + \paragraph{Other tactics and developments} has been included in the real +numbers library: {\tt DiscrR} proves that a real integer constant c1 is non +equal to another real integer constant c2; {\tt SplitAbsolu} allows us to +unfold {\tt Rabsolu} contants and split corresponding conjonctions; +{\tt SplitRmult} allows us to split a condition that a product is non equal to +zero into subgoals corresponding to the condition on each subterm of the +product. All these tactics have been written with the tactic language +$\ltac$.\\ +A development on Cauchy series, power series,... has been also added.\\ For more details, see the Reference Manual. \subsection{Changes in pre-existing tactics} @@ -525,9 +527,9 @@ located in the source file. \section{Extraction}\label{Extraction} Extraction code has been completely rewritten since version V6.3. This work is still not finished, but most parts of it are already -usable. It was successfully tested on the \coq{} theories. +usable. It was successfully tested on the {\Coq} theories. -The new mechanism is able to extract programs from any \coq{} term +The new mechanism is able to extract programs from any {\Coq} term (including terms at the Type level). However, the resulting ML term is not guaranteed to be typable in ML @@ -540,7 +542,7 @@ A new mechanism to extract Ocaml modules from Coq files has been added. The \verb!ML import! command is not available anymore, use the command -\verb!Extract Constant! to realize a \coq{} axiom by an ML program. +\verb!Extract Constant! to realize a {\Coq} axiom by an ML program. The syntax of commands is described in the Reference Manual. @@ -574,11 +576,13 @@ documentation tool (see the ``doc'' directory in {\Coq} source). \item Default parsers in {\tt Grammar} and {\tt Syntax} are different (see section \ref{GrammarSyntax}). - \item Definition of {\tt D\_in} (Reals/Rderiv.v) is now with Rdiv (Rmult and - Rinv before). + \item Definition of {\tt D\_in} (Rderiv.v) is now with Rdiv and not + with Rmult and Rinv as before. + + \item {\tt Extraction} is currently not available in {\Coq} V7. \item Pattern aliases of dependent type in \verb=Cases= - expressions are currently not supported. + expressions are currently not supported. \end{itemize} diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index d0c16e3c2c..69d1257f6e 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -779,7 +779,6 @@ Inductive identityT [A:Type; a:A] : A->Type := refl_identityT : (identityT A a a). \end{coq_example*} - \section{The standard library} \subsection{Survey} @@ -799,9 +798,10 @@ subdirectories: etc.) \\ {\bf IntMap} & Representation of finite sets by an efficient structure of map (trees indexed by binary integers).\\ - {\bf Reals} & Axiomatization of Real Numbers (classical, basic functions - and results, integer part and fractional part, - requires the \textbf{ZArith} library).\\ + {\bf Reals} & Axiomatization of Real Numbers (classical, basic functions, + integer part, fractional part, limit, derivative, Cauchy + series, power series and results,... Requires the + \textbf{ZArith} library).\\ {\bf Relations} & Relations (definitions and basic results). \\ {\bf Wellfounded} & Well-founded relations (basic results). \\ @@ -880,9 +880,12 @@ naturals using decimal notation. That is he can write \texttt{(3)} for \texttt{(S (S (S O)))}. The number must be between parentheses. This works also in the left hand side of a \texttt{Cases} expression (see for example section \ref{Refine-example}). + +%Remove the redefinition of nat \begin{coq_eval} -Reset Initial. (* Remove the redefinition of nat *) +Reset Initial. \end{coq_eval} + \begin{coq_example*} Require Arith. Fixpoint even [n:nat] : nat := @@ -892,6 +895,86 @@ Cases n of (0) => true end. \end{coq_example*} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\subsection{Real numbers library} + +\subsubsection{Notations for real numbers} +\index{Notations for real numbers} + +This is provided by requiring the module {\tt Reals}. This notation is very +similar to the notation for integer arithmetics (see figure +\ref{zarith-syntax}) where Inverse (/x) and division (x/y) have been added. +This syntax is used parenthesizing by a double back-quote (\verb:``:). + +\begin{coq_example} +Require Reals. +Check ``2+3``. +\end{coq_example} + +A constant, say \verb:``4``:, is equivalent to \verb:``(1+(1+(1+1)))``:. + +\subsubsection{Some tactics} + +In addition to the Ring, Field and Fourier tactics (see chapter \ref{Tactics}) +there are: + +{\tt DiscrR} prove that a real integer constante c1 is non equal to +another real integer constante c2. +\tacindex{DiscrR} + +\begin{coq_example*} +Require DiscrR. +Goal ``5<>0``. +\end{coq_example*} + +\begin{coq_example} +DiscrR. +\end{coq_example} + +\begin{coq_eval} +Abort. +\end{coq_eval} + +{\tt SplitAbsolu} allows us to unfold {\tt Rabsolu} contants and split +corresponding conjonctions. +\tacindex{SplitAbsolu} + +\begin{coq_example*} +Require SplitAbsolu. +Goal (x:R) ``x <= (Rabsolu x)``. +\end{coq_example*} + +\begin{coq_example} +Intro;SplitAbsolu. +\end{coq_example} + +\begin{coq_eval} +Abort. +\end{coq_eval} + +{\tt SplitRmult} allows us to split a condition that a product is non equal to +zero into subgoals corresponding to the condition on each subterm of the +product. +\tacindex{SplitRmult} + +\begin{coq_example*} +Require SplitRmult. +Goal (x,y,z:R)``x*y*z<>0``. +\end{coq_example*} + +\begin{coq_example} +Intros;SplitRmult. +\end{coq_example} + +All this tactics has been written with the new tactic language.\\ + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + \section{Users' contributions} \index{Contributions} \label{Contributions} diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 5e68c26921..6b304816f3 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1702,6 +1702,28 @@ Field}. \SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt Field}. +\subsection{\tt Fourier} +\tacindex{Fourier} + +This tactic written by Loïc Pottier solves linear inequations on real numbers +using Fourier's method (\cite{Fourier}). This tactic must be loaded by +{\tt Require Fourier}. + +\Example +\begin{coq_example*} +Require Reals. +Require Fourier. +Goal (x,y:R)``x < y``->``y+1 >= x-1``. +\end{coq_example*} + +\begin{coq_example} +Intros; Fourier. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + \subsection{\tt AutoRewrite [ \ident$_1$ \dots \ident$_n$ ]} \tacindex{AutoRewrite} diff --git a/doc/biblio.bib b/doc/biblio.bib index 5e3fe8e56b..ad0ff37c0f 100755 --- a/doc/biblio.bib +++ b/doc/biblio.bib @@ -453,6 +453,14 @@ s}, YEAR = {1990} } +@BOOK{Fourier, + AUTHOR = {Jean-Baptiste-Joseph Fourier}, + PUBLISHER = {Gauthier-Villars}, + TITLE = {Fourier's method to solve linear + inequations/equations systems.}, + YEAR = {1890} +} + @INPROCEEDINGS{Gim94, AUTHOR = {E. Gim\'enez}, BOOKTITLE = {Types'94 : Types for Proofs and Programs}, |