From 942f219246c2d35836585012791369d523a4d62f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Nov 2020 12:00:41 +0100 Subject: [PATCH] typos --- tex/ch0.tex | 10 +++++----- tex/chProofs.tex | 8 +++----- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/tex/ch0.tex b/tex/ch0.tex index e99e5e89..dbd11a37 100644 --- a/tex/ch0.tex +++ b/tex/ch0.tex @@ -20,7 +20,7 @@ \chapter*{Introduction} non-standard presentation of \Coq{}, putting upfront the formalization choices and the proof style that are the pillars of the library. -This books targets two classes of public. On the one hand, newcomers, +This book targets two classes of public. On the one hand, newcomers, even the more mathematically inclined ones, %may find a soft introduction to the programming @@ -123,7 +123,7 @@ \subsection*{Part 2: \parttwoname{}} Such solutions typically involve notions and theorems that are part of the \mcbMC{} library. By programming type inference one can hence teach \Coq{} the contents of the library. The system -is then able to reconstruct the non-trivial missing pieces of information, +is then able to reconstruct non-trivial missing pieces of information, as the informed reader typically does when reading a mathematical text. Formalized knowledge is organized by means of interfaces (in the spirit of @@ -178,7 +178,7 @@ \subsection*{Conventions} \sum_(0 <= i < n.+2) i = (n.+1 * n.+2) %/ 2 \end{coqout} -Names of components one can \C{Require} in \Coq{} are written +Names of library components one can \C{Require} in \Coq{} are written like \lib{ssreflect} or \lib{fintype}. \subsection*{Running examples in the \Coq{} system} @@ -200,8 +200,8 @@ \subsection*{Running examples in the \Coq{} system} alternative approaches to integrate \Coq{} in their preferred programming environment. For instance, there exist special extensions of \Coq{} for the popular \texttt{Emacs} programming editor (known as \texttt{Proof General}) -and for the \texttt{Eclipse} programming environment -(known as \texttt{coqoon}). These extensions and similar projects can easily +and for the \texttt{Visual Studio Code} programming environment +(known as \texttt{vscoq}). These extensions and similar projects can easily be found by a search on the Internet. When starting a \Coq{} session, a few commands must be sent to the \Coq{} diff --git a/tex/chProofs.tex b/tex/chProofs.tex index d1d794d8..591bac09 100644 --- a/tex/chProofs.tex +++ b/tex/chProofs.tex @@ -1122,7 +1122,7 @@ \subsubsection{Rewriting many identities in one go} of the arguments of the product being zero. And \C{(n1 - n2 == 0)} means \C{(n1 <= n2)}. -The first step is performed using the following equation: +The first step is performed using the following equation:\label{leqE} \begin{coq}{name=LeqDef}{} Lemma leqE m n : (m <= n) = (m - n == 0). @@ -1853,7 +1853,7 @@ \subsection{Proofs by induction}\label{ssec:ind} Here \C{P} is quantified exactly as \C{n} is, but its type is a bit more complex and deserves an explanation. As we have seen in the first -chapter, the \C{->} denotes the type of functions; hence \C{P} is a\marginpar{There is a problem with the \C{-} macro when the first character is -, which cancels the space that precedes it} +chapter, the ~\C{->} denotes the type of functions; hence \C{P} is a function from \C{nat} to \C{Prop}. Recall that \C{Prop} is the type of \emph{propositions}, i.e., something we may want to prove. In the light of that, \C{P} is a function producing a proposition out of a natural @@ -2178,9 +2178,7 @@ \section{Rewrite, a Swiss army knife}\label{sec:rewrite} Another form of simplification that is often needed is the unfolding of a definition. For example, the lemma \C{leqE} that we used in -\marginpar{When reading the text, I thought that \C{leqE} did exist. I -think we should avoid misleading readers like that.} -the proof of \C{leq_mul2l} back in section~\ref{sec:multirew} +the proof of \C{leq_mul2l} back in page~\pageref{leqE} does not exist in the library, and there is no name associated to this equation. It is simply the definition of \C{leq}, and we actually do not need to state a lemma in order to relate