Corrections in doc

doc/Gamma0-chapter.tex

@@ -1,5 +1,5 @@
 \chapter{The Ordinal \texorpdfstring{$\Gamma_0$}{Gamma0} (first draft)}
-
+\label{chap:gamma0}
 
 \emph{This chapter and the files it presents are still very incomplete, considering the impressive properties of $\Gamma_0$~\cite{Gallier91}.  We hope to add new material soon, and accept contributions!}
 

doc/epsilon0-chapter.tex

@@ -5,8 +5,8 @@
 \label{cnf-math-def}
 \label{chap:T1}
 
-In this chapter, we adapt to \coq{} the well-known~\cite{KP82}  proof that Hercules eventually wins every battle, whichever the strategy  of each player.
-In other words, we present  a formal and self contained proof of termination  of all [free] hydra battles.
+In this chapter, we adapt to \coq{} the well-known proof~\cite{KP82} that Hercules eventually wins every battle, whichever the strategy  of each player.
+In other words, we present  a formal and self-contained proof of termination  of all [free] hydra battles.
 First, we take from Manolios and Vroon~\cite{Manolios2005} a representation of the ordinal $\epsilon_0$ as terms in Cantor normal form. Then, we define a variant for hydra battles as a measure that maps any hydra to some ordinal strictly less than $\epsilon_0$.
 
 
@@ -16,7 +16,7 @@ \section{The ordinal \texorpdfstring{\(\epsilon_0\)}{epsilon0}}
 
 The ordinal \(\epsilon_0\) is the least ordinal number that satisfies 
 the equation \(\alpha = \omega^\alpha\), where \(\omega\) is 
-the least infinite ordinal.
+the least infinite ordinal\footnote{For a precise ---\,\emph{i.e.} mathematical\,--- definition of $\omega^\alpha$, please see Sect.~\vref{sect:AP-and-phi0}.} .
 Thus, we can intuitively consider \(\epsilon_0\) as an
 \emph{infinite} \(\omega\)-tower.
 
@@ -28,10 +28,10 @@ \subsection{Cantor normal form}
 
 Any ordinal strictly less that \(\epsilon_0\) 
 can be finitely represented by a unique  \emph{Cantor normal form}, 
-that is, an expression  which is either  the ordinal \(0\) or 
+that is, an expression  which is 
 a sum  \(\omega^{\alpha_1} \times n_1 + \omega^{\alpha_2} \times n_2 + 
-  \dots + \omega^{\alpha_p} \times n_p\) where all the \(\alpha_i\) 
-are ordinals in Cantor  normal form, \(\alpha_1 > \alpha_2 > \alpha_p\), 
+  \dots + \omega^{\alpha_p} \times n_p\) where $p\in\mathbb{N}$, all the \(\alpha_i\) 
+are ordinals in Cantor  normal form, \(\alpha_1 > \alpha_2 > \alpha_p\)
 and all the \(n_i\) are positive integers.
 
 An example of Cantor normal form is displayed in Fig \ref{fig:cnf-example}:
@@ -55,8 +55,7 @@ \subsection{Cantor normal form}
 to this type, and finally prove that our representation fits well with 
 the expected mathematical properties: the order we define is a well order, 
 and the decomposition into Cantor normal form  is consistent 
-with the implementation of the arithmetic operations of exponentiation of base \(\omega\) 
-and addition.
+with usual definition of ordinals, for instance in \gaia~\cite{Gaia}, Schütte's book~\cite{schutte}, or larger ordinal notations~\vref{chap:gamma0}.
 
 \paragraph*{Remark}
 \label{sec:orgheadline65}
@@ -131,7 +130,7 @@ \subsubsection{Example}
 \paragraph{Remark}
 For simplicity's sake, we chose to forbid  expressions of the form $\omega^\alpha\times 0 + \beta$. Thus, the construction (\texttt{cons $\alpha$ $n$ $\beta$}) is intended to represent the
 ordinal $\omega^\alpha\times(n+1)+\beta$ and not $\omega^\alpha\times n+\beta$.
-In a future version, we should replace  the type \texttt{nat} with \texttt{positive} in \texttt{T1}'s 
+In a future version, we would like to replace  the type \texttt{nat} with standard library's type \texttt{positive} in \texttt{T1}'s 
 definition. But this replacement would take a lot of time \dots{}
 
 
@@ -210,11 +209,11 @@ \subsubsection{The ordinal \(\omega\)}
 
 \input{movies/snippets/T1/omegaDef}
 
-Note that \texttt{omega} is not an identifier in \HydrasLib, thus any tactic like \texttt{unfold omega} would fail.
+Note that \texttt{T1omega} is not an identifier in \HydrasLib, thus any tactic like \texttt{unfold T1omega} would fail.
 
 \index{gaiabridge}{The ordinal $\omega$}
 \paragraph*{\gaiasign}
-In \texttt{gaia.ssete9}, the ordinal $\omega$ is bound to the \emph{constant}  \texttt{T1omega}.
+In \texttt{gaia.ssete9}, the ordinal $\omega$ is bound to the \emph{constant}  \texttt{T1omega} (not a notation).
 
 
 
@@ -292,7 +291,7 @@ \subsection{Pretty-printing ordinals in Cantor normal form}
 
 \index{hydras}{Projects}
 \begin{project}
-Design  (in \ocaml?) a set of tools for systematically pretty printing ordinal terms in Cantor normal form.
+Design tools for systematically pretty printing ordinal terms in Cantor normal form.
 \end{project}
 
 
@@ -315,6 +314,8 @@ \subsection{Comparison between ordinal terms}
 
 \input{movies/snippets/T1/compareDef}
 
+\input{movies/snippets/T1/Instances}
+
 
 \label{Predicates:lt-T1}
 Please note that this definition of \texttt{lt} makes it easy to write proofs by computation, as shown by the following examples.
@@ -325,11 +326,11 @@ \subsection{Comparison between ordinal terms}
 \input{movies/snippets/T1/ltExamples}
 
 
-Links between the function \texttt{compare} and the relations
-\texttt{lt} and \texttt{eq} are established through the following lemmas (~\vref{sect:comparable-def}).
-\vspace{4pt}
+% Links between the function \texttt{compare} and the relations
+% \texttt{lt} and \texttt{eq} are established through the following lemmas (~\vref{sect:comparable-def}).
+% \vspace{4pt}
+
 
-\input{movies/snippets/T1/Instances}
 
 \paragraph*{\gaiasign}
 \index{gaiabridge}{Strict order on ordinals below $\epsilon_0$}

doc/gaia-chapter.tex

@@ -121,21 +121,19 @@ \subsubsection{Refinements: Definitions}
 
 
 Functions \texttt{h2g} and \texttt{g2h} allow us to define
-a notion of ``data-refinement''  for constants, functions, predicates and relations. The following definitions express that some
+a notion of ``data-refinement''  for constants, functions, predicates and relations. The following definitions express that a given
 constant, function, relation defined in \HydrasLib ``implements'' the same concept of \gaia.
 
-
-
-
-
-
-
+From~\href{../theories/html/gaia_hydras/T1Bridge.html}%
+{\texttt{gaia\_hydras.T1Bridge}}.
 
 \inputsnippets{T1Bridge/refineDefs}
 
 Refinement lemmas can be easily ``reversed''.
 
-\inputsnippets{T1Bridge/refines1R, T1Bridge/refines2R}
+\inputsnippets{T1Bridge/refines1R}
+
+\inputsnippets{T1Bridge/refines2R}
 
 \subsection{Examples of refinement}
 Both of our libraries define constants like $0$, $1$, $\omega$, and arithmetic functions: successor, addition, multiplication, and exponential of base $\omega$ (function $\phi_0$). We prove that these definitions are mutually consistent. Finally, we prove that the boolean predicates `` to be in normal form'' are equivalent.
@@ -202,10 +200,10 @@ \subsection{Looking for a lemma}
 $\alpha \times \beta=\beta$.
 
 The following command lists us `gaia's lemmas (thanks to
-\gaia's  \texttt{cantor\_scope}.
+\gaia's  \texttt{cantor\_scope}).
 \inputsnippets{T1Bridge/SearchDemoa}
 
-With \texttt{t1\_scope}:
+Within \texttt{t1\_scope}:
 \inputsnippets{T1Bridge/SearchDemob}
 
 \section{Importing Definitions and theorems from \HydrasLib}

doc/hydras.tex

@@ -556,15 +556,15 @@ \part{Hydras and ordinals}
 \include{Gamma0-chapter}
 
 
-\part{Ackermann, G\"{o}del, Peano\,\dots}
+%\part{Ackermann, G\"{o}del, Peano\,\dots}
 
-\include{chap-intro-goedel}
+%\include{chap-intro-goedel}
 \include{chapter-primrec} 
-\include{chapter-fol}
-\include{chapter-natural-deduction}
-\include{chapter-lnn-lnt}
-\include{chapter-encoding}
-\include{chapter-expressible}
+% \include{chapter-fol}
+% \include{chapter-natural-deduction}
+% \include{chapter-lnn-lnt}
+% \include{chapter-encoding}
+% \include{chapter-expressible}
 
 
 \part{A few  certified algorithms}

doc/schutte-chapter.tex

@@ -419,6 +419,7 @@ \subsubsection{Multiplication by a natural number}
 \input{movies/snippets/Addition/multFin}
 
 \section{The exponential of basis \texorpdfstring{$\omega$}{omega}}
+\label{sect:AP-and-phi0}
 
 In this section, we define the function which maps any $\alpha\in\mathbb{O}$ to
 the ordinal  $\omega^\alpha$, also written 
@@ -446,6 +447,7 @@ \subsection{Additive principal ordinals}
 
 \subsection{The function \texttt{phi0}}
 
+
 Let us call  $\phi_0$ the ordering function of \texttt{AP}.
 In the mathematical text, we shall use indifferently the notations  $\omega^\alpha$ and $\phi_0(\alpha)$. 
 

theories/ordinals/Epsilon0/T1.v

@@ -543,7 +543,7 @@ Fixpoint nf_b (alpha : T1) : bool :=
       (nf_b a && nf_b b && (bool_decide (lt a' a)))%bool
   end.
 
-Definition nf alpha :Prop := nf_b alpha.
+Definition nf alpha :Prop := nf_b alpha. 
 (* end snippet nfDef *)
 
 (* begin snippet badTerm *)