diff options
Diffstat (limited to 'doc/refman/Natural.tex')
| -rw-r--r-- | doc/refman/Natural.tex | 425 |
1 files changed, 0 insertions, 425 deletions
diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex deleted file mode 100644 index 69dfab87..00000000 --- a/doc/refman/Natural.tex +++ /dev/null @@ -1,425 +0,0 @@ -\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: |