Skip to content

Commit

Permalink
- Fixed various Overfull in documentation.
Browse files Browse the repository at this point in the history 
- Removed useless coq-tex preprocessing of RecTutorial.
- Make "Set Printing Width" applies to "Show Script" too.
- Completed documentation (specially of ltac) according to CHANGES file.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information
herbelin committed Jan 27, 2009
1 parent 94b1e67 commit 3394cf3
Show file tree
Hide file tree
Showing 9 changed files with 131 additions and 88 deletions.
42 changes: 21 additions & 21 deletions Makefile.doc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,15 @@ doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt

doc-html:\
doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.v.html
doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html

doc-pdf:\
doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \
doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.v.pdf
doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf

doc-ps:\
doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps
doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps

refman: \
doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf
Expand All @@ -38,8 +38,8 @@ stdlib: \

faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf

rectutorial: doc/RecTutorial/RecTutorial.v.html \
doc/RecTutorial/RecTutorial.v.ps doc/RecTutorial/RecTutorial.v.pdf
rectutorial: doc/RecTutorial/RecTutorial.html \
doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf

######################################################################
### Implicit rules
Expand Down Expand Up @@ -216,32 +216,32 @@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li
(cd doc/stdlib;\
$(LATEX) -interaction=batchmode Library;\
$(LATEX) -interaction=batchmode Library > /dev/null;\
../tools/show_latex_messages Library.log)
../tools/show_latex_messages -no-overfull Library.log)

doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
(cd doc/stdlib;\
$(PDFLATEX) -interaction=batchmode Library;\
../tools/show_latex_messages Library.log)
../tools/show_latex_messages -no-overfull Library.log)

######################################################################
# Tutorial on inductive types
######################################################################

doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex
doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex
(cd doc/RecTutorial;\
$(LATEX) -interaction=batchmode RecTutorial.v;\
$(BIBTEX) -terse RecTutorial.v;\
$(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
$(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
../tools/show_latex_messages RecTutorial.v.log)
$(LATEX) -interaction=batchmode RecTutorial;\
$(BIBTEX) -terse RecTutorial;\
$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
../tools/show_latex_messages RecTutorial.log)

doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi
doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi
(cd doc/RecTutorial;\
$(PDFLATEX) -interaction=batchmode RecTutorial.v.tex;\
../tools/show_latex_messages RecTutorial.v.log)
$(PDFLATEX) -interaction=batchmode RecTutorial.tex;\
../tools/show_latex_messages RecTutorial.log)

doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v)
doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)

######################################################################
# Index file for CoqIDE
Expand All @@ -267,7 +267,7 @@ install-doc-html:
$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq)
$(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman
$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib
$(INSTALLLIB) doc/RecTutorial/RecTutorial.v.html $(FULLDOCDIR)/html/RecTutorial.html
$(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html
$(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq
$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html

Expand All @@ -278,8 +278,8 @@ install-doc-printable:
$(INSTALLLIB) doc/refman/Reference-Manual.ps \
doc/stdlib/Library.ps $(FULLDOCDIR)/ps
$(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf
$(INSTALLLIB) doc/RecTutorial/RecTutorial.v.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
$(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
$(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf
$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
$(INSTALLLIB) doc/RecTutorial/RecTutorial.v.ps $(FULLDOCDIR)/ps/RecTutorial.ps
$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps
49 changes: 25 additions & 24 deletions doc/RecTutorial/RecTutorial.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -724,7 +724,7 @@ \subsection{The existential quantifier.}\label{ex-def}
\noindent The former quantifier inhabits the universe of propositions.
As for the conjunction and disjunction connectives, there is also another
version of existential quantification inhabiting the universes $\Type_i$,
which is noted \texttt{sig $P$}. The syntax
which is written \texttt{sig $P$}. The syntax
``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''.


Expand Down Expand Up @@ -934,7 +934,7 @@ \subsubsection{Example: strong specification of the predecessor function.}
Defined.
\end{alltt}

If we print the term built by {\coq}, we can observe its dependent pattern-matching structure:
If we print the term built by {\coq}, its dependent pattern-matching structure can be observed:

\begin{alltt}
predecessor = fun n : nat {\funarrow}
Expand All @@ -950,8 +950,9 @@ \subsubsection{Example: strong specification of the predecessor function.}
\end{alltt}


Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at the reference manual and/or the book: tactics
\texttt{destruct}, ``~\texttt{intro \emph{pattern}}~'', etc.
Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at for tactics
``~\texttt{destruct}~'', ``~\texttt{intro \emph{pattern}}~'', etc. in
the reference manual and/or the book.

\noindent The command \texttt{Extraction} \refmancite{Section
\ref{ExtractionIdent}} can be used to see the computational
Expand Down Expand Up @@ -1240,7 +1241,7 @@ \subsubsection{The Predicate $n {\leq} m$}
of type $\citecoq{nat}\arrow{}\Prop$.
If $H$ is a proof of ``~\texttt{n {\coqle} p}~'',
$H_0$ a proof of ``~\texttt{$Q$ n}~'' and
$H_S$ a proof of ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'',
$H_S$ a proof of the statement ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'',
then the term
\begin{alltt}
match H in (_ {\coqle} q) return (Q q) with
Expand Down Expand Up @@ -2604,8 +2605,8 @@ \subsection{Proofs by Structural Induction}
\end{alltt}

Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$,
another combinator \texttt{nat\_double\_rect} for constructing
(certified) programs can be defined in exactly the same way.
another combinator for constructing
(certified) programs, \texttt{nat\_double\_rect}, can be defined in exactly the same way.
This definition is left as an exercise.\label{natdoublerect}

\iffalse
Expand Down Expand Up @@ -2751,8 +2752,8 @@ \subsection{Using Elimination Combinators.}


Therefore,
in this case the abstraction must be explicited using the tactic
\texttt{pattern}. Once the right abstraction is provided, the rest of
in this case the abstraction must be explicited using the
\texttt{pattern} tactic. Once the right abstraction is provided, the rest of
the proof is immediate:

\begin{alltt}
Expand Down Expand Up @@ -2804,8 +2805,8 @@ \subsection{Using Elimination Combinators.}

\begin{exercise}
\begin{enumerate}
\item Define a recursive function \emph{nat2itree}
mapping any natural number $n$ into an infinitely branching
\item Define a recursive function of name \emph{nat2itree}
that maps any natural number $n$ into an infinitely branching
tree of height $n$.
\item Provide an elimination combinator for these trees.
\item Prove that the relation \citecoq{itree\_le} is a preorder
Expand All @@ -2831,7 +2832,7 @@ \subsection{Well-founded Recursion}

Structural induction is a strong elimination rule for inductive types.
This method can be used to define any function whose termination is
based on the well-foundedness of certain order relation $R$ decreasing
a consequence of the well-foundedness of a certain order relation $R$ decreasing
at each recursive call. What makes this principle so strong is the
possibility of reasoning by structural induction on the proof that
certain $R$ is well-founded. In order to illustrate this we have
Expand Down Expand Up @@ -2867,8 +2868,8 @@ \subsection{Well-founded Recursion}
\end{verbatim}


The equality test on natural numbers can be represented as the
function \textsl{eq\_nat\_dec} defined page \pageref{iseqpage}. Giving $x$ and
The equality test on natural numbers can be implemented using the
function \textsl{eq\_nat\_dec} that is defined page \pageref{iseqpage}. Giving $x$ and
$y$, this function yields either the value $(\textsl{left}\;p)$ if
there exists a proof $p:x=y$, or the value $(\textsl{right}\;q)$ if
there exists $q:a\not = b$. The subtraction function is already
Expand Down Expand Up @@ -3112,7 +3113,7 @@ \section{A case study in dependent elimination}\label{CaseStudy}
"vector A n"
\end{alltt}

In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill typed,
In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill-typed and this is
because the type ``~\citecoq{vector A n}~'' is not \emph{convertible}
with ``~\citecoq{vector A 0}~''.

Expand Down Expand Up @@ -3264,11 +3265,11 @@ \section{A case study in dependent elimination}\label{CaseStudy}

\begin{alltt}
Definition vector_double_rect :
{\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
P 0 Vnil Vnil {\arrow}
({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
P (S n) (Vcons a v1) (Vcons b v2)) {\arrow}
{\prodsym} n (v1 v2 : vector A n), P n v1 v2.
{\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
P 0 Vnil Vnil {\arrow}
({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
P (S n) (Vcons a v1) (Vcons b v2)) {\arrow}
{\prodsym} n (v1 v2 : vector A n), P n v1 v2.
induction n.
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
auto.
Expand Down Expand Up @@ -3361,7 +3362,7 @@ \section{Co-inductive Types and Non-ending Constructions}


It is also possible to define co-inductive types for the
trees with infinite branches (see Chapter 13 of~\cite{coqart}).
trees with infinitely-many branches (see Chapter 13 of~\cite{coqart}).

Structural induction is the way of expressing that inductive types
only contain well-founded objects. Hence, this elimination principle
Expand Down Expand Up @@ -3555,7 +3556,7 @@ \subsection{Extensional Properties}
\end{alltt}
\begin{exercise}
Define a co-inductive type $Nat$ containing non-standard
Define a co-inductive type of name $Nat$ that contains non-standard
natural numbers --this is, verifying
$$\exists m \in \mbox{\texttt{Nat}}, \forall\, n \in \mbox{\texttt{Nat}}, n<m$$.
Expand Down Expand Up @@ -3591,8 +3592,8 @@ \subsection{About injection, discriminate, and inversion}
Qed.
Lemma injection_demo : {\prodsym} (A:Type)(a b : A)(l l': LList A),
LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
a = b {\coqand} l = l'.
LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
a = b {\coqand} l = l'.
Proof.
intros A a b l l' e; injection e; auto.
Qed.
Expand Down
6 changes: 3 additions & 3 deletions doc/refman/RefMan-ext.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -343,18 +343,18 @@ \subsubsection{Second destructuring {\tt let} syntax\index{let '... in}}
Reset fst.
\end{coq_eval}
\begin{coq_example}
Definition fst (A B:Set) (p:A * B) := let 'pair x _ := p in x.
Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
\end{coq_example}

This is useful to match deeper inside tuples and also to use notations
for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary
patterns to do the deconstruction. For example:

\begin{coq_example}
Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A :=
Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
let '((a,b), (c, d)) := x in (a,b,c,d).
Notation " x 'with' p " := (exist _ x p) (at level 20).
Definition proj1_sig' (A :Set) (P : A -> Prop) (t:{ x : A | P x }) : A :=
Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
let 'x with p := t in x.
\end{coq_example}

Expand Down
6 changes: 3 additions & 3 deletions doc/refman/RefMan-gal.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -226,7 +226,7 @@ \subsection{Syntax of terms}

\begin{figure}[htbp]
\begin{centerframe}
\begin{tabular}{lcl@{\qquad}r}
\begin{tabular}{lcl@{\quad~}r} % warning: page width exceeded with \qquad
{\term} & ::= &
{\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\
& $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
Expand Down Expand Up @@ -266,10 +266,10 @@ \subsection{Syntax of terms}
{\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\
& $|$ & {\binder} \nelist{\binderlet}{} &\\
&&&\\
{\binder} & ::= & {\name} & \ref{Binders} \\
{\binder} & ::= & {\name} & (\ref{Binders}) \\
& $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\
&&&\\
{\binderlet} & ::= & {\binder} & \ref{Binders} \\
{\binderlet} & ::= & {\binder} & (\ref{Binders}) \\
& $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
& & &\\
{\name} & ::= & {\ident} &\\
Expand Down
18 changes: 11 additions & 7 deletions doc/refman/RefMan-lib.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -267,11 +267,11 @@
\begin{coq_example*}
End equality.
Definition eq_ind_r :
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y.
Definition eq_rec_r :
forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y.
Definition eq_rect_r :
forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y.
\end{coq_example*}
\begin{coq_eval}
Abort.
Expand All @@ -290,8 +290,9 @@
For instance {\tt f\_equal3} is defined the following way.
\begin{coq_example*}
Theorem f_equal3 :
forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
(x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
\end{coq_example*}
\begin{coq_eval}
Abort.
Expand Down Expand Up @@ -478,7 +479,9 @@ \subsection{Specification}
\ttindex{A+\{B\}}

\begin{coq_example*}
Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
Inductive sumor (A:Set) (B:Prop) : Set :=
| inleft (_:A)
| inright (_:B).
\end{coq_example*}

We may define variants of the axiom of choice, like in Martin-Löf's
Expand Down Expand Up @@ -675,7 +678,8 @@ \subsection{Basic Arithmetics}

\begin{coq_example*}
Theorem nat_case :
forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
forall (n:nat) (P:nat -> Prop),
P 0 -> (forall m:nat, P (S m)) -> P n.
\end{coq_example*}
\begin{coq_eval}
Abort All.
Expand Down
Loading

0 comments on commit 3394cf3

Please sign in to comment.