Merge pull request #108 from math-comp/small-glitches

Small glitches

Author: gares

tex/chProgramming.tex

@@ -12,7 +12,7 @@
 .
 \end{coqdef}
 
-\chapter{Functions and Computation}\label{ch:prog}
+\chapter{Functions and computation}\label{ch:prog}
 
 In the formalism underlying the \Coq{} system, functions play a
 central role akin to the one of sets in set theory. However,

tex/chProofLanguage.tex

@@ -1,4 +1,4 @@
-\chapter{A Proof Language for Formal Proofs}{}
+\chapter{A proof language for formal proofs}{}
 \label{ch:script}
 
 
@@ -87,7 +87,7 @@ \chapter{A Proof Language for Formal Proofs}{}
 %\section{Managing the proof context}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Bookkeeping: Goals as stacks}\label{ssec:stack}
+\section{Bookkeeping: goals as stacks}\label{ssec:stack}
 \index[concept]{goal stack model}
 
 The presentation we gave so far of proof commands like \C{case: n => [|m]}
@@ -247,8 +247,12 @@ \subsection{Pulling from the stack}
 new variable (the predecessor of what used to be called \C{y}).
 Since \C{y} is destructed we could have reused that name for
 its predecessor, as it is often done in the \mcbMC{} library.
-Recall the definition of \C{odd} \marginpar{odd is never given}:
-when applied to \C{z.+1} it simplifies to \C{\~\~ odd z}.
+In fact, the boolean predicate \C{odd} is defined by case analysis,
+and induction, on its argument of type \C{nat}:
+\begin{coq}{}{}
+Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false.
+\end{coq}
+Therefore, when applied to \C{z.+1}, it simplifies to \C{\~\~ odd z}.
 
 Now, the fact that \C{z} is even is not needed to conclude, so we can
 discard it by giving it the \C{\_} dummy name.~\footnote{

tex/chProofs.tex

@@ -31,7 +31,7 @@
 \end{coqdef}
 
 
-\chapter{First Steps in Formal Proofs}{}
+\chapter{First steps in formal proofs}{}
 \label{ch:proofs}
 % In this chapter we explain how to state a lemma,
 % how to prove it, and how to search existing, loaded library.
@@ -1554,8 +1554,7 @@ \subsection{Using lemmas in proofs}
 \end{coq}
 \coqrun{name=testexp}{ssr,exp,abort}
 
-where \D{p \%| m`!} stands for ``\C{p} divides the factorial of \C{m}''.\marginpar{there is a problem with the factorial notation at the beginning
-of this line}
+where \D{p \%| m`!} stands for ``\C{p} divides the factorial of \C{m}''.
 
 The first step of our formal proof will be to give a name to the
 hypothesis \C{(prime p)}, which means that we add it to the

tex/chSigmaBool.tex

@@ -19,7 +19,7 @@
 Require Import tuple.
 \end{coqdef}
 
-\chapter{Sub-Types}{}\label{ch:sigmabool}
+\chapter{Sub-types}{}\label{ch:sigmabool}
 
 Inductive data types have been used to both code data, like lists, and
 logical connectives, like the existential quantifier.
@@ -264,8 +264,9 @@ \section{$n$-tuples, lists with an invariant on the length}
 
 The global table of canonical solutions is extended as follows.
 
+\vspace{1ex}
 \noindent
-\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=Canonical Structures Index]
+\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=Canonical Structures Index]
 projection & value & solution & combines solutions for \\ \hline
 \lstinline/tval N A/ & \lstinline/rev A S/ & \lstinline/rev_tuple N A T/
 	& \lstinline/T/ $\leftarrow$ (\lstinline/tval N A/, \lstinline/S/) \\

tex/chSpecification.tex

@@ -1,4 +1,4 @@
-\chapter{Inductive Specifications}{}
+\chapter{Inductive specifications}{}
 \label{ch:boolrefl}
 
 % in addition to the photos:

tex/chTT.tex

@@ -1,4 +1,4 @@
-\chapter{Dependent Type Theory}{}
+\chapter{Dependent type theory}{}
 \label{ch:ttch}
 
 %% Summary of the 22/02 discussion:
@@ -171,7 +171,6 @@ \section{Propositions as types, proofs as programs}\label{sec:patpap}
 term of the corresponding type. Objects of the formalism are programs,
 and proofs are themselves objects of the formalism.
 
-% \marginpar{meta is condusing here: take more time to talk about this}
 In this setting the analogue of ``a proposition has a proof''
 is that ``a term has a given type''. Such a statement, called a
 \emph{typing judgment}, is a ternary relation written as follows:
@@ -732,8 +731,6 @@ \section{Conversion}\label{sec:conv}
 homonymous algebraic structure~\cite{gregoire:hal-00819484}.
 
 
-%\marginpar{Say here that computation can be used for automation? and
-%  simpl? and that controlling it is a delicate issue?}
 
 
 % One can also benefit from convertibility whenever one applies a lemma;

tex/chTypeInference.tex

@@ -12,7 +12,7 @@
 Abort.
 \end{coqdef}
 
-\chapter{Implicit Parameters}{}
+\chapter{Implicit parameters}{}
 
 The rules of the \mcbCIC{}, as the ones sketched in~\ref{ch:ttch},
 are expressed on the syntax of terms and
@@ -91,7 +91,7 @@ \chapter{Implicit Parameters}{}
 %\mcbLEARN{HO unif is hard}
 %\mcbREQUIRE{}
 %\mcbPROVIDE{terminology}
-\section{Type inference and Higher-Order unification}\label{sec:hounif}
+\section{Type inference and higher-order unification}\label{sec:hounif}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 The type inference algorithm is quite similar to the type checking
@@ -612,7 +612,8 @@ \section{Records as relations}\label{sec:eqtype}
 Whenever a record instance is declared as canonical \Coq{}
 adds to such table an entry for each field of the record type.
 
-\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index]
+\vspace{1ex}
+\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index]
 projection & value & solution \\ \hline
 \lstinline/sort/ & \lstinline/nat/ & \lstinline/nat_eqType/  \\
 \lstinline/sort/ & \lstinline/bool/ & \lstinline/bool_eqType/   \\
@@ -727,8 +728,9 @@ \section{Records as relations}\label{sec:eqtype}
 
 The global table of canonical solutions is extended as follows.
 
+\vspace{1ex}
 \noindent
-\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=canonical structures Index]
+\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=canonical structures Index]
 projection & value & solution & combines solutions for \\ \hline
 \lstinline/sort/ & \lstinline/nat/ & \lstinline/nat_eqType/ & \\
 \lstinline/sort/ & \lstinline/bool/ & \lstinline/bool_eqType/ &  \\
@@ -1531,8 +1533,9 @@ \subsection{Assumptions of a bigop lemma}\label{sec:bigoplemmas}
 This command adds the following rule to the canonical structures
 index:
 
+\vspace{1ex}
 \noindent
-\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index]
+\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index]
 projection & value & solution \\ \hline
 \lstinline/Monoid.operator/ & \lstinline/addn/ & \lstinline/addn_monoid/  \\
 \hline

tex/main.tex

@@ -58,8 +58,8 @@
 \makeindex[name=coq,title=Definitions and Notations,intoc]
 \makeindex[name=vernac,title=Coq Commands,intoc]
 
-\newcommand{\partonename}{Languages for writing Formal Mathematics}
-\newcommand{\parttwoname}{Crafting a Formal Library}
+\newcommand{\partonename}{Languages for writing formal mathematics}
+\newcommand{\parttwoname}{Crafting a formal library}
 
 
 
@@ -127,6 +127,7 @@
 
 \pagestyle{empty} % No headers
 
+\setcounter{tocdepth}{1}
 \tableofcontents % Print the table of contents itself
 
 \cleardoublepage{} % Forces the first chapter to start on an odd page so it's on the right