Fix typos, some minor wording adjustments

tex/ch0.tex

@@ -10,23 +10,22 @@ \chapter*{Introduction}
 Four Color Theorem~\cite{Gonthier08} and of the
 Odd Order Theorem~\cite{gonthier:hal-00816699}.
 
-The reason of existence of this book is to break down the barriers to entry.
+The reason for this book's existence is to break down the barriers to entry.
 While there are several books around covering the usage of the
 \Coq{} system~\cite{BC04,SF,CPDT}
 and the theory it is based
 on~\cite{Coq:manual}\cite{paulinmohring:hal-01094195,hottbook},
 the \mcbMC{} library is built
 in an unconventional way.  As a consequence, this book provides a
-non-standard presentation of \Coq{}, putting upfront the formalization
+non-standard presentation of \Coq{}, putting up front the formalization
 choices and the proof style that are the pillars of the library.
 
-This book targets two classes of public.  On the one hand, newcomers,
+This book targets two kinds of audience.  On the one hand, newcomers,
 even the more mathematically inclined ones, %may
 find a soft
 introduction to the programming
 language of \Coq{}, Gallina, and the SSReflect proof language.
-On the other hand accustomed \Coq{} users %will hopefully
-find a
+On the other hand, accustomed \Coq{} users will, we hope, find a
 substantial account of the formalization style that made the \mcbMC{}
 library possible.
 
@@ -39,7 +38,7 @@ \chapter*{Introduction}
 given as soon as possible sufficient tools to prove non-trivial
 mathematical results by reusing parts of the library. By the end of
 the first part, the reader has learned how to prove formally the
-infinitude of prime numbers, or the correctness of the Euclidean's
+infinitude of prime numbers, or the correctness of the Euclidean
 division algorithm, in a few lines of proof text.
 
 \paragraph{Acknowledgments.}
@@ -83,21 +82,21 @@ \subsection*{Part 1: \partonename{}}
 % proofs gradually, and takes benefit from frequent interactions with
 % the system.
 \emph{SSReflect} is a language designed to
-ease the activity of writing and maintaining formal proofs.
+ease the task of writing and maintaining formal proofs.
 In particular the maintenance of large
 formal libraries requires a solid writing discipline
 and a language that supports it.
 % . to be tractable,
 % as it is the case for any large corpus of code.
-\emph{SSReflect} provides linguistic constructs well adapted to
+\emph{SSReflect} provides linguistic constructs that are well-adapted to
 writing scripts that can be easily fixed in response to % ancillary
 changes to the contents of the formal libraries.
 % or changing the formal
 % definitions.
 
-Actually, \mcbSSR{} is firstly the name of a
+Actually, \mcbSSR{} is first and foremost the name of a
 formalization methodology, sometimes also called \emph{Boolean Reflection}.
-Initially conceived for  the formal proof
+Initially conceived for the formal proof
 of the Four Colors Theorem, it became a pillar of the \mcbMC{}
 library and of the formal proof of the Odd Order
 Theorem. The SSReflect proof language was named after this methodology
@@ -159,7 +158,7 @@ \subsection*{Conventions}
 
 \Coq{} code is in \C{typewriter} font and \C{(surrounded by parentheses)}
 when it occurs in the middle of the text.  Longer snippets are in boxes with line
-numbers like the following one:
+numbers, like the following one:
 
 \begin{coq}{}{title=A sample snippet}
 Example Gauss n : \sum_(0 <= i < n.+1) i = (n * n.+1) %/ 2.

tex/chFingroup.tex

@@ -4,17 +4,17 @@ \chapter{Finite group theory}
 the \C{fingroup} and \C{solvable} directories.  It covers a substantial
 part of~\cite{gorenstein2007finite} and~\cite{9781139175319} ranging from
 basic notions like morphisms, quotients, actions, cyclic and p-groups to more
-substantial topics as Sylow and Hall groups, the Abelian
-structure theorem and the Jordan Holder theorem.
+substantial topics as Sylow and Hall groups, the abelian
+structure theorem and the Jordan-H\"older theorem.
 The paper~\cite{DBLP:conf/mkm/Mahboubi13}
 describes the constructions and formalization techniques
-needed in order to prove the Jordan Holder theorem.
+needed in order to prove the Jordan-H\"older theorem.
 
 \paragraph{contents}
 
 \lib{..}
 
-\paragraph{Basic formalization choices} To ease the study of sub-groups,
+\paragraph{Basic formalization choices} To ease the study of subgroups,
 the type of groups is indexed over a container group called
 \C{finGroupType}, fixing the group law and imposing finiteness by
 inheriting from \C{finType}.
@@ -25,24 +25,24 @@ \chapter{Finite group theory}
 Concepts already existing on sets are kept there and not redefined.
 Type inference is programmed to infer the group structure whenever possible.
 For example the type of \C{(G :&: H)} is \C{\{set gT\}} but such expression
-is automatically promoted to a group when needed, similarly to what 
+is automatically promoted to a group when needed, similarly to what
 was done in section~\ref{sec:tupleinvariant} for tuples.
 
-group concepts usually here defined on sets, but then
-possibly using the generated group operation to fulfill
-stricter requirements.  This generalized the math concept and
-ease the integration with set stuff.  This is possible because
-the container is a group and we can always generate from a set.
+Group concepts are usually defined on sets, but then
+possibly use the generated group operation to fulfill
+stricter requirements.  This generalizes the math concept and
+eases the integration with set theory.  This is possible because
+the container is a group and we can always generate one from a set.
 
-morphisms carry domain set in type.
+Morphisms carry their domain set in their type.
 
 \paragraph{Notations} The same infix \C{*} notation can be used to
 multiply both sets (or groups) and their points.  For example
 \C{(g * h \\in G * H)} is a valid writing, meaning that
 $g\cdot h \in \{ x\cdot y | x \in G, y \in H\}$.  Given the \C{finGroupType}
 container many open notations are also supported, for example the normalizer
 of \C{A}, written \C{'N(A)} for \C{A} being a \C{\{set gT\}}, is a sensible
-writing. Another bonus from the container.
+writing, another bonus from the container.
 
 \begin{coq}{}{}
 Definition normaliser A := [set x | A :^ x \subset A].
@@ -63,7 +63,7 @@ \chapter{Finite group theory}
 
 notations for actions acts-on, transitive, Fix, 'N(A|P) and co.
 
-\paragraph{Formalization trick: totality of operations} In standard math one
+\paragraph{Formalization trick: totality of operations} In standard mathematics, one
 can write \C{A/H} only if the normality condition \C{(H <| A)} holds.
 Such construction is made total by defining \C{A/H} as
 \C{(('N(H) :&: A) * H) / H)}, i.e. \C{A} is intersected with 
@@ -76,7 +76,7 @@ \chapter{Finite group theory}
 Lemma quotientMl A B : A \subset 'N(H) -> A * B / H = (A / H) * (B / H).
 \end{coq}
 Remark that the equational form lets you require only one precondition:
-if \C{B} exceeds the \C{'N(H)} then the equation still holds, since 
+if \C{B} exceeds \C{'N(H)}, then the equation still holds, since
 the intersection with the normalizer of \C{H} occurs on both sides.
 
 A similar choice is used for the (semi) direct and central product.
@@ -98,15 +98,15 @@ \chapter{Finite group theory}
 the trivial group.
 
 \paragraph{Formalization trick: presentations} One cannot decide if a group
-presented via generators and relations is finite, hence the integration of such
+presented via generators and relations is finite, hence the integration of such a
 concept in a library of finite groups is tricky.  The notation
 \C{(G \\homg Grp (x : (x ^+ n)))} states that the finite group \C{G}
 is generated by a single point \C{x} of order \C{n} (as in the standard
 mathematical notation, \C{(x ^+ n)} really means \C{(x ^+ n = 1)}).
 The shrewdness is that the notation hides an existential quantification
 postulating the existence of a finite tuple of generators satisfying
 the equations and building \C{G}: the potentially infinite object is never
-built as well the \C{\\homg} relation, standing for homomorphic image, 
+built, and the \C{\\homg} relation (standing for homomorphic image)
 suggests the fact that \C{G} is the image of the presented group, not the
 group itself.  Notation
 \C{(G \\homg Grp (x_1 : .. x_n : (s_1 = t_1, .., s_m = t_m))}
@@ -118,7 +118,7 @@ \chapter{Finite group theory}
     == (G,                          (t_1, .. (t_m-1, t_m) ..))] 
 \end{coq}
 Such formula is generated reflexively, i.e. by a \Coq{} program that
-takes in input the syntax of the presentation and produces that statement.
+takes as input the syntax of the presentation and produces that statement.
 Remark the $m+1$ components compared by \C{(_ == _)}.  It first compares
 the group generated by the generators \C{x_1 .. x_n} with \C{G}; then
 it compares all the expressions being related.
@@ -145,6 +145,6 @@ \chapter{Representation and Character theory}
 
 \cite{isaacs1976character}
 
-As an example of application, in particular of the linear algebra
+As an example of application of the library, in particular of the linear algebra
 theory.
 

tex/chGraph.tex

@@ -13,8 +13,8 @@ \chapter{Finite graph theory}
 \item ordinals: injections, enumeration of/projection from a finite
   set. Example of indexing by a finite type (and not In).
 \item pick
-\item tuples, as indexation domains, that can be enumerated by an
-  ordinal and avoid dflt element (cf \C{tnth} in
+\item tuples, as indexing domains, that can be enumerated by an
+  ordinal and avoid default element (cf \C{tnth} in
   6.4).
 \item may be restriction of finite functions by a predicate?
 \item images (of finite functions)

tex/chHierarchy.tex

@@ -42,12 +42,12 @@ \chapter{Organizing Theories}{}
 dependent types, coercions and canonical instances of structures.  It
 is only a ``simple matter of programming'', albeit one that involves
 some new formalisation idioms. This chapter describes the most
-important: telescopes, packed classes, and phantom parameters.
+important ones: telescopes, packed classes, and phantom parameters.
 % class coercions, and quotation.
 
 While some of these formalisation patterns are quite technical, casual
 users do not need to master them all. Indeed the documented interface
-of structures suffices to use and declare instances of structures. We
+of structures suffices for using and declaring instances of structures. We
 describe these interfaces first, so only those who wish to extend old
 or create new hierarchies need to read on.
 
@@ -157,7 +157,7 @@ \section{Structure interface}\label{str:itf}
 
 Line 1 bundles the additive operations (0, $+$, $-$) and their
 properties in a \emph{mixin}, which is then used in line 2 to create a
-canonical instance. After line 2 all the additive algebra provided in
+canonical instance. After line 2 all the additive algebra provided by
 \lib{ssralg} becomes applicable to \lstinline/'I_p/; for example \C{0}
 denotes the zero element, and \C{i + 1} denotes the successor of \C{i} mod $p$.
 
@@ -213,7 +213,7 @@ \section{Structure interface}\label{str:itf}
 
 Constraining the shape of the modulus $p$ is a simple and robust way
 to enforce $p>1$: it standardizes the proofs of $p>0$ and $p>1$, which
-avoid the unpleasantness of multiple interpretations of \C{0}
+avoids the unpleasantness of multiple interpretations of \C{0}
 stemming from different proofs of $p>0$ --- the latter tends to happen
 with ad hoc inference of such proofs using canonical structures or
 tactics. The shape constraint can however be inconvenient when the
@@ -705,9 +705,9 @@ \section{Packed classes}\label{sec:packed}
 Two structures extend rings independently: \C{comRingType} provides
 multiplication commutativity, and \C{unitRingType} provides computable
 inverses for all units (i.e., invertible elements) along with a test
-of invertibility. These structures are incomparable, and there are reasonable
+of invertibility. These structures are incomparable, as there are reasonable
 instances of each: $2\times 2$ matrices over $\mathbb{Q}$ have
-computable inverses but do not commute, while polynomials over
+computable inverses but do not commute, whereas polynomials over
 $\mathbb{Z}_p$ commute but do not have easily computable inverses.
 The respective definitions of \C{comRingType} and \C{unitRingType} follow exactly
 the pattern we have seen,
@@ -875,7 +875,7 @@ \section{Parameters and constructors}\label{sec:phant}
 
 For example, each packed class contains exactly the same definition of
 the clone constructor\footnote{More precisely, the situation is slightly different
-  in the case of structure with a parameter, like modules.}, following the introduction of
+  in the case of a structure with a parameter, like modules.}, following the introduction of
 section variables \C{T} and~\C{cT}, and the definition of \C{class}:
 
 \begin{coq}{name=phant21}{}
@@ -912,7 +912,7 @@ \section{Parameters and constructors}\label{sec:phant}
 The code for the instance constructor for \C{choiceType} is almost
 identical, because it only extends \C{eqType} with a mixin that does
 not depend on \C{eqType}.
-Note that this definition allows \Coq{} to infer \C{T} from \C{m}.
+Note that this definition lets \Coq{} infer \C{T} from \C{m}.
 
 \begin{coq}{name=phant23}{}
 Definition pack T m :=
@@ -981,7 +981,7 @@ \section{Linking a custom data type to the library}
 \begin{coq}{}{}
 Inductive windrose := N | S | E | W.
 \end{coq}
-The most naive way to show that \C{windrose} is a \C{finType} is
+The most na\"ive way to show that \C{windrose} is a \C{finType} is
 to provide a comparison function, then a choice function, \ldots
 finally an enumeration.  Instead, it is much simpler to show one
 can punt \C{windrose} in bijection with a pre-existing finite type,
@@ -1027,12 +1027,12 @@ \section{Linking a custom data type to the library}
 Definition windrose_finMixin := PcanFinMixin pcan_wo4.
 Canonical windrose_finType := FinType windrose windrose_finMixin.
 \end{coq}
-Only one tiny detail has been left on the side so far.  To use
+Only one tiny detail has been left aside so far.  To use
 \C{windrose} in conjunction with the \C{\\in} infix notation or with
 the notation \C{#|...|} for cardinality, the type declaration has to
 be tagged as an instance of the \C{predArgType} structure, for types
-which model a predicate, as it is the one which supports the latter
-notations. It can be done as follows.  \index[coq]{\C{preArgType}}
+which model a predicate, as it is the structure that supports the latter
+notations. It can be done as follows.  \index[coq]{\C{predArgType}}
 
 \begin{coq}{}{}
 Inductive windrose : predArgType := N | S | E | W.
@@ -1047,7 +1047,7 @@ \section{Linking a custom data type to the library}
 A generic technique is available in order to equip a data type with structures of
 \C{eqType}, \C{choiceType}, and \C{countType}. It consists in
 providing a correspondence with the generic tree data type
-\C{(GenTree.tree T)}: an n-ary tree with nodes labelled with
+\C{(GenTree.tree T)}: an n-ary tree with nodes labeled with
 natural numbers and leaves carrying a value in \C{T}.
 \index[coq]{\C{GenTree.tree}}