Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 425 insertions, 0 deletions

diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex
new file mode 100644
index 00000000..69dfab87
--- /dev/null
+++ b/doc/refman/Natural.tex
@@ -0,0 +1,425 @@
+\achapter{\texttt{Natural} : proofs in natural language}
+\aauthor{Yann Coscoy}
+
+\asection{Introduction}
+
+\Natural~ is a package allowing the writing of proofs in natural
+language. For instance, the proof in \Coq~of the induction principle on pairs
+of natural numbers looks like this:
+
+\begin{coq_example*}
+Require Natural.
+\end{coq_example*}
+\begin{coq_example}
+Print nat_double_ind.
+\end{coq_example}
+
+Piping it through the \Natural~pretty-printer gives:
+
+\comindex{Print Natural}
+\begin{coq_example}
+Print Natural nat_double_ind.
+\end{coq_example}
+
+\asection{Activating \Natural}
+
+To enable the printing of proofs in natural language, you should
+type under \texttt{coqtop} or \texttt{coqtop -full} the command
+
+\begin{coq_example*}
+Require Natural.
+\end{coq_example*}
+
+By default, proofs are transcripted in english. If you wish to print them 
+in French, set the French option by
+
+\comindex{Set Natural}
+\begin{coq_example*}
+Set Natural French.
+\end{coq_example*}
+
+If you want to go back to English, type in
+
+\begin{coq_example*}
+Set Natural English.
+\end{coq_example*}
+
+Currently, only \verb=French= and \verb=English= are available.
+
+You may see for example the natural transcription of the proof of
+the induction principle on pairs of natural numbers:
+
+\begin{coq_example*}
+Print Natural nat_double_ind.
+\end{coq_example*}
+
+You may  also show in natural language the current proof in progress:
+
+\comindex{Show Natural}
+\begin{coq_example}
+Goal (n:nat)(le O n).
+Induction n.
+Show Natural Proof.
+\end{coq_example}
+
+\subsection*{Restrictions}
+
+For \Natural, a proof is an object of type a proposition (i.e. an
+object of type something of type {\tt Prop}). Only proofs are written
+in natural language when typing {\tt Print Natural \ident}.  All other
+objects (the objects of type something which is of type {\tt Set} or
+{\tt Type}) are written as usual $\lambda$-terms.
+
+\asection{Customizing \Natural}
+
+The transcription of proofs in natural language is mainly a paraphrase of
+the formal proofs, but some specific hints in the transcription
+can be given.
+Three kinds of customization are available.
+
+\asubsection{Implicit proof steps}
+
+\subsubsection*{Implicit lemmas}
+
+Applying a given lemma or theorem \verb=lem1= of statement, say $A
+\Rightarrow B$, to an hypothesis, say $H$ (assuming $A$) produces the
+following kind of output translation:
+
+\begin{verbatim}
+...
+Using lem1 with H we get B.
+...
+\end{verbatim}
+
+But sometimes, you may prefer not to see the explicit invocation to
+the lemma. You may prefer to see:
+
+\begin{verbatim}
+...
+With H we have A.
+...
+\end{verbatim}
+
+This is possible by declaring the lemma as implicit. You should type:
+
+\comindex{Add Natural}
+\begin{coq_example*}
+Add Natural Implicit lem1.
+\end{coq_example*}
+
+By default, the lemmas \verb=proj1=, \verb=proj2=, \verb=sym_equal=
+and \verb=sym_eqT= are declared implicit. To remove a lemma or a theorem
+previously declared as implicit, say \verb=lem1=, use the command
+
+\comindex{Remove Natural}
+\begin{coq_example*}
+Remove Natural Implicit lem1.
+\end{coq_example*}
+
+To test if the lemma or theorem \verb=lem1= is, or is not,
+declared as implicit, type
+
+\comindex{Test Natural}
+\begin{coq_example*}
+Test Natural Implicit lem1.
+\end{coq_example*}
+
+\subsubsection*{Implicit proof constructors}
+
+Let \verb=constr1= be a proof constructor of a given inductive
+proposition (or predicate)
+\verb=Q= (of type \verb=Prop=). Assume \verb=constr1= proves 
+\verb=(x:A)(P x)->(Q x)=. Then, applying \verb=constr1= to an hypothesis,
+say \verb=H= (assuming \verb=(P a)=) produces the following kind of output:
+
+\begin{verbatim}
+...
+By the definition of Q, with H we have (Q a).
+...
+\end{verbatim}
+
+But sometimes, you may prefer not to see the explicit invocation to
+this constructor. You may prefer to see:
+
+\begin{verbatim}
+...
+With H we have (Q a).
+...
+\end{verbatim}
+
+This is possible by declaring the constructor as implicit. You should
+type, as before:
+
+\comindex{Add Natural Implicit}
+\begin{coq_example*}
+Add Natural Implicit constr1.
+\end{coq_example*}
+
+By default, the proposition (or predicate) constructors
+
+\verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=,
+\verb=exT_intro=, \verb=refl_equal=, \verb=refl_eqT= and \verb=exist=
+
+\noindent are declared implicit. Note that declaring implicit the
+constructor of a datatype (i.e. an inductive type of type \verb=Set=)
+has no effect.
+
+As above, you can remove or test a constant declared implicit.
+
+\subsubsection*{Implicit inductive constants}
+
+Let \verb=Ind= be an inductive type (either a proposition (or a
+predicate) -- on \verb=Prop= --, or a datatype -- on \verb=Set=).
+Suppose the proof proceeds by induction on an hypothesis \verb=h=
+proving \verb=Ind= (or more generally \verb=(Ind A1 ... An)=). The
+following kind of output is produced:
+
+\begin{verbatim}
+...
+With H, we will prove A by induction on the definition of Ind.
+Case 1. ...
+Case 2. ...
+...
+\end{verbatim}
+
+But sometimes, you may prefer not to see the explicit invocation to
+\verb=Ind=. You may prefer to see:
+
+\begin{verbatim}
+...
+We will prove A by induction on H.
+Case 1. ...
+Case 2. ...
+...
+\end{verbatim}
+
+This is possible by declaring the inductive type as implicit. You should
+type, as before:
+
+\comindex{Add Natural Implicit}
+\begin{coq_example*}
+Add Natural Implicit Ind.
+\end{coq_example*}
+
+This kind of parameterization works for any inductively defined
+proposition (or predicate) or datatype. Especially, it works whatever
+the definition is recursive or purely by cases.
+
+By default, the data type \verb=nat= and the inductive connectives
+\verb=and=, \verb=or=, \verb=sig=, \verb=False=, \verb=eq=,
+\verb=eqT=, \verb=ex= and \verb=exT= are declared implicit.
+
+As above, you can remove or test a constant declared implicit.  Use
+{\tt Remove Natural Contractible $id$} or {\tt Test Natural
+Contractible $id$}.
+
+\asubsection{Contractible proof steps}
+
+\subsubsection*{Contractible lemmas or constructors}
+
+Some lemmas, theorems or proof constructors of inductive predicates are
+often applied in a row and you obtain an output of this kind:
+
+\begin{verbatim}
+...
+Using T with H1 and H2 we get P.
+      * By H3 we have Q.
+      Using T with theses results we get R.
+...
+\end{verbatim}
+
+where \verb=T=, \verb=H1=, \verb=H2= and \verb=H3= prove statements
+of the form \verb=(X,Y:Prop)X->Y->(L X Y)=, \verb=A=, \verb=B= and \verb=C=
+respectively (and thus \verb=R= is \verb=(L (L A B) C)=).
+
+You may obtain a condensed output of the form
+
+\begin{verbatim}
+...
+Using T with H1, H2, and H3 we get R.
+...
+\end{verbatim}
+
+by declaring \verb=T= as contractible:
+
+\comindex{Add Natural Contractible}
+\begin{coq_example*}
+Add Natural Contractible T.
+\end{coq_example*}
+
+By default, the lemmas \verb=proj1=, \verb=proj2= and the proof
+constructors \verb=conj=, \verb=or_introl=, \verb=or_intror= are
+declared contractible. As for implicit notions, you can remove or
+test a lemma or constructor declared contractible.
+
+\subsubsection*{Contractible induction steps}
+
+Let \verb=Ind= be an inductive type. When the proof proceeds by
+induction in a row, you may obtain an output of this kind:
+
+\begin{verbatim}
+...
+We have (Ind A (Ind B C)).
+We use definition of Ind in a study in two cases.
+Case 1: We have A.
+Case 2: We have (Ind B C).
+  We use definition of Ind in a study of two cases.
+  Case 2.1: We have B.
+  Case 2.2: We have C.
+...
+\end{verbatim}
+
+You may prefer to see
+
+\begin{verbatim}
+...
+We have (Ind A (Ind B C)).
+We use definition of Ind in a study in three cases.
+Case 1: We have A.
+Case 2: We have B.
+Case 3: We have C.
+...
+\end{verbatim}
+
+This is possible by declaring \verb=Ind= as contractible:
+
+\begin{coq_example*}
+Add Natural Contractible T.
+\end{coq_example*}
+
+By default, only \verb=or= is declared as a contractible inductive
+constant.
+As for implicit notions, you can remove or test an inductive notion declared
+contractible.
+
+\asubsection{Transparent definitions}
+
+``Normal'' definitions are all constructions except proofs and proof constructors.
+
+\subsubsection*{Transparent non inductive normal definitions}
+
+When using the definition of a non inductive constant, say \verb=D=, the
+following kind of output is produced:
+
+\begin{verbatim}
+...
+We have proved C which is equivalent to D.
+...
+\end{verbatim}
+
+But you may prefer to hide that D comes from the definition of C as
+follows:
+
+\begin{verbatim}
+...
+We have prove D.
+...
+\end{verbatim}
+
+This is possible by declaring \verb=C= as transparent:
+
+\comindex{Add Natural Transparent}
+\begin{coq_example*}
+Add Natural Transparent D.
+\end{coq_example*}
+
+By default, only \verb=not= (normally written \verb=~=) is declared as
+a non inductive transparent definition.
+As for implicit and contractible definitions, you can remove or test a
+non inductive definition declared transparent.
+Use \texttt{Remove Natural Transparent} \ident or 
+\texttt{Test Natural Transparent} \ident.
+
+\subsubsection*{Transparent inductive definitions}
+
+Let \verb=Ind= be an inductive proposition (more generally: a
+predicate \verb=(Ind x1 ... xn)=). Suppose the definition of
+\verb=Ind= is non recursive and built with just
+one constructor proving something like \verb=A -> B -> Ind=.
+When coming back to the definition of \verb=Ind= the
+following kind of output is produced:
+
+\begin{verbatim}
+...
+Assume Ind (H).
+      We use H with definition of Ind.
+      We have A and B.
+      ...
+\end{verbatim}
+
+When \verb=H= is not used a second time in the proof, you may prefer
+to hide that \verb=A= and \verb=B= comes from the definition of
+\verb=Ind=. You may prefer to get directly:
+
+\begin{verbatim}
+...
+Assume A and B.
+...
+\end{verbatim}
+
+This is possible by declaring \verb=Ind= as transparent:
+
+\begin{coq_example*}
+Add Natural Transparent Ind.
+\end{coq_example*}
+
+By default, \verb=and=, \verb=or=, \verb=ex=, \verb=exT=, \verb=sig=
+are declared as inductive transparent constants.  As for implicit and
+contractible constants, you can remove or test an inductive
+constant declared transparent.
+
+As for implicit and contractible constants, you can remove or test an
+inductive constant declared transparent.
+
+\asubsection{Extending the maximal depth of nested text}
+
+The depth of nested text is limited. To know the current depth, do:
+
+\comindex{Set Natural Depth}
+\begin{coq_example}
+Set Natural Depth.
+\end{coq_example}
+
+To change the maximal depth of nested text (for instance to 125) do:
+
+\begin{coq_example}
+Set Natural Depth 125.
+\end{coq_example}
+
+\asubsection{Restoring the default parameterization}
+
+The command \verb=Set Natural Default= sets back the parameterization tables of
+\Natural~ to their default values, as listed in the above sections.
+Moreover, the language is set back to English and the max depth of
+nested text is set back to its initial value.
+
+\asubsection{Printing the current parameterization}
+
+The commands {\tt Print Natural Implicit}, {\tt Print Natural
+Contractible} and {\tt Print \\ Natural Transparent} print the list of
+constructions declared {\tt Implicit}, {\tt Contractible},
+{\tt Transparent} respectively.
+
+\asubsection{Interferences with \texttt{Reset}}
+
+The customization of \texttt{Natural} is dependent of the \texttt{Reset}
+command. If you reset the environment back to a point preceding an
+\verb=Add Natural ...= command, the effect of the command will be
+erased. Similarly, a reset back to a point before a 
+\verb=Remove Natural ... = command invalidates the removal.
+
+\asection{Error messages}
+
+An error occurs when trying to \verb=Print=, to \verb=Add=, to
+\verb=Test=, or to \verb=remove= an undefined ident. Similarly, an
+error occurs when trying to set a language unknown from \Natural.
+Errors may also occur when trying to parameterize the printing of
+proofs: some parameterization are effectively forbidden.
+Note that to \verb=Remove= an ident absent from a table or to
+\verb=Add= to a table an already present ident does not lead to an
+error.
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: