Update 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/chapter-primrec.tex

@@ -50,19 +50,25 @@ \subsubsection{Projections}
 For instance, the projection $\pi_{2,3}$ satisfies the equation
 $\pi_{2,3}(x,y,z)=y$ for any natural numbers $x$, $y$ and $z$.
 
-\subsubsection{The constant function of value 0}
+\subsubsection{Constant functions}
 \label{sect:k0}
 
-The \emph{unary} function which always returns $0$ may be defined through the \emph{composition} construction (with $n=1$, $m=0$, and $h=\texttt{zero}$).
+The \emph{nullary} constant function which returns $0$ is
+simply the \texttt{zero} construction.
 
-% If we consider any value of $n$, the same construction
-% builds the constant function of type $\mathbb{N}^n \arrow \mathbb{N}$ which returns $0$.
+If we want to consider the \emph{unary} function which
+maps any natural number $i$ to $0$, we may built it
+through the \emph{composition} construction, instanciated
+with $n=1$, $m=0$, and $h=\texttt{zero}$.
 
 
-\subsubsection{Constant functions}
+\index{hydras}{Exercises}
+
+\begin{exercise}
+Let $m$ and $k$ be two natural numbers; please build the primitive recursive function which maps any
+tuple $t\in \mathbb{N}^m$ to $k$.
+\end{exercise}
 
-Let $k$ be some natural number; the unary constant function which always returns $k$ is built through $k$ nested compositions of the 
-successor function with the  unary constant function which returns $0$.
 
 
 \subsubsection{Addition on natural natural numbers}
@@ -179,10 +185,11 @@ \subsection{Extensional equality}
 \index{ackermann}{Predicates!extEqual}
 \inputsnippets{extEqualNat/extEqualDef}
 
-Module \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec} defines and export  the notation ``\texttt{$f$ =x= $g$}'' for ``\texttt{extEqual $n$ $f$ $g$}'' \footnote{in parsing mode, provided $f$ has explicitely the type (\texttt{naryFunc $n$}).}
-
-
+Module \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec} defines and export  the notation ``\texttt{$f$ =x= $g$}'' for ``\texttt{extEqual $n$ $f$ $g$}'' \footnote{in parsing mode, the provided $f$ should be explicitely typed as  (\texttt{naryFunc $n$}).}
 
+\vspace{6pt}
+\noindent
+\emph{From \href{../theories/html/hydras.MoreAck.PrimRecExamples.html}{MoreAck.PrimRecExamples}}
 
 
 \input{movies/snippets/PrimRecExamples/extEqual2a}
@@ -266,11 +273,11 @@ \subsubsection{Examples}
 \subsection{A little bit of semantics} 
 \label{primrec-semantics}
 
-Inhabitants of type (\texttt{PrimRec $n$}) are not \coq{} functions like \texttt{Nat.mul}, or \texttt{Arith.Factorial.fact}, etc. but terms of an abstract syntax for the language of primitive recursive functions. The bridge between this language and the word of usual functions
+Inhabitants of type (\texttt{PrimRec $n$}) are not \coq{} functions like \texttt{Nat.mul}, \linebreak \texttt{Arith.Factorial.fact}, etc. but terms of an abstract syntax for the language of primitive recursive functions. The bridge between this language and the word of usual functions
 is an interpretation function (\texttt{evalprimRec $n$})  of type
 $\texttt{PrimRec}\,n \rightarrow  \texttt{naryFunc}\,n$.
 This function is defined by mutual recursion,  together with the  function 
-(\texttt{evalprimRecS $n$ $m$}) of type 
+(\texttt{evalprimRecS $n$ $m$}) of type \linebreak
 ($\texttt{PrimRecs}\,n\,m \rightarrow  \texttt{Vector.t}\,(\texttt{naryFunc}\,n)\,m$).
 
 \index{ackermann}{Functions!evalPrimRec}

doc/epsilon0-chapter.tex

@@ -1,12 +1,12 @@
 %------------------------------------------------------------------------
 
-\chapter[A proof of termination, using epsilon0]{A proof of termination, using ordinals below \texorpdfstring{$\epsilon_0$}{Epsilon0}}
+\chapter[The ordinal epsilon0]{The Ordinal  \texorpdfstring{$\epsilon_0$}{Epsilon0}}
 
 \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$}
@@ -658,7 +659,7 @@ \subsubsection{A first attempt}
  $\alpha=\texttt{cons $\beta\;n\;\gamma$}$, and assume that \(\beta\) and \(\gamma\) are \texttt{LT}-accessible.
 In order to prove the accessibility of $\alpha$, we have to consider
 any well formed term \(\delta\) such that \(\delta<\alpha\). 
-But nothing guarantees that \(\delta\)  is strictly  less than \(\beta\) nor \(\gamma\), and we cannot use the induction hypotheses on   \(\beta\) nor \(\gamma\).
+% But nothing guarantees that \(\delta\)  is strictly  less than \(\beta\) nor \(\gamma\), and we cannot use the induction hypotheses on   \(\beta\) nor \(\gamma\).
 
 \input{movies/snippets/T1/wfLTBada}
 
@@ -700,19 +701,23 @@ \subsubsection{Using a stronger inductive predicate.}
 \label{sec:orgheadline79}
 
 First, we prove that, for  any \texttt{LT}-accessible term $\alpha$, $\alpha$ is 
-strongly accessible too (\emph{i.e.} any well formed
-term (\texttt{cons $\alpha$ $n$ $\beta$})  is accessible).
-
-The proof is structured as an induction on $\alpha'$s accessibility. Let us consider
+strongly accessible too.
+The following proof is structured as an induction on $\alpha'$s accessibility. Let us consider
 any  accessible term $\alpha$.
 
 \input{movies/snippets/T1/AccImpAccStrong}
 
 
+First, we prove that, for any $n$ and $\beta$, if (\texttt{cons $\alpha$ $n$ $\beta$}) is in normal form, then
+ $\beta$ is accessible.
+
+\inputsnippets{T1/betaAcc}
+
+The new hypothesis  \texttt{beta\_Acc} allows us to prove by well-founded induction on $\beta$, 
+and natural induction on $n$ that (\texttt{cons $\alpha$ $n$ $\beta$}) is accessible.
+
+\inputsnippets{T1/useBetaAcc}
 
-Let \texttt{n:nat} and \texttt{beta:T1} such that (\texttt{cons alpha n beta}) is in normal form. 
-We prove first that \texttt{beta} is accessible,  which allows us to prove by well-founded induction on \texttt{beta}, 
-and natural induction on \texttt{n}, that (\texttt{cons alpha n beta}) is accessible.
 The proof, quite long, can be consulted in \href{../theories/html/hydras.Epsilon0.T1.html}{Epsilon0.T1}.
 
 \paragraph{Accessibility of any well-formed ordinal term}
@@ -725,6 +730,7 @@ \subsubsection{Using a stronger inductive predicate.}
 
 \input{movies/snippets/T1/T1Wf}
 
+\subsection{Transfinite induction}
 \index{maths}{Transfinite induction}
 
 
@@ -811,7 +817,8 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
 
     \section{An ordinal notation for \texorpdfstring{$\omega^\omega$}{omega\^omega}}
-
+    \label{sect:omegaomega}
+
     In Module   \href{https://github.com/coq-community/hydra-battles/blob/master/theories/
       ordinals/OrdinalNotations/OmegaOmega.v}{theories/ordinals/OrdinalNotations/OmegaOmega.v},
     we represent ordinals below $\omega^\omega$ by lists of pairs of natural numbers (with the same coefficient shift as in \texttt{T1}).

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/ordinal-chapter.tex

@@ -933,14 +933,6 @@ \subsubsection{See also \dots}
 \inputsnippets{ON_gfinite/Examples, ON_gfinite/Examplesb}
 
 
-
-
-
-
-
-
-
-
 %%%
 
 \section{Comparing two ordinal notations}
@@ -1194,5 +1186,9 @@ \section{Other ordinal notations}
  The set of ordinal terms in Cantor normal form (see Chap.~\ref{chap:T1}) and 
 in Veblen normal form (see 
 \href{../theories/html/hydras.Gamma0.Gamma0.html}{Gamma0.Gamma0}) are shown to be ordinal notation systems, but there is a lot of work to be done in order to unify ad-hoc  definitions and proofs which were written before the definition of the \texttt{ON} type class.
+
+
+In Section~\vref{sect:omegaomega}, we present a notation system for the ordinal $\omega^\omega$ as a \emph{refinement}
+of the ordinal notation for $\epsilon_0$.
 \end{remark}
 

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/Ackermann/primRec.v

@@ -31,6 +31,7 @@ with PrimRecs : nat -> nat -> Set :=
 
 (* end snippet PrimRecDef *)
 
+
   Notation "f '=x=' g" := (extEqual _ f g) (at level 70, no associativity).