Update doc (#178)

* minor change

* small changes in doc

* simplify the proposition 'alpha < phi0 beta'

* simplify the proposition 'alpha < phi0 beta'

* improve Alectryon output

* minor changes in pdf doc

* minor changes in pdf doc

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,6 +1,6 @@
 %------------------------------------------------------------------------
 
-\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}
@@ -659,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}
 
@@ -701,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}
@@ -726,6 +730,7 @@ \subsubsection{Using a stronger inductive predicate.}
 
 \input{movies/snippets/T1/T1Wf}
 
+\subsection{Transfinite induction}
 \index{maths}{Transfinite induction}
 
 
@@ -812,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/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}
 

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).
 
 

theories/ordinals/Epsilon0/Canon.v

@@ -402,15 +402,15 @@ Proof.
               - destruct (Hrec  (cons alpha2_1 n1 alpha2_2)) ; trivial.
                now apply head_lt.
                 discriminate.
-              - apply nf_helper_phi0R.
+              - apply lt_a_phi0_b_phi0R.
                 apply T1.lt_trans with (cons alpha2_1 n1 alpha2_2).
                 + destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial.
                   apply head_lt; auto. 
                   *  discriminate.
                   * tauto.
              +  
-                apply nf_helper_phi0.
-                apply nf_helper_intro with n;auto.
+                apply lt_a_phi0_b_phi0.
+                apply lt_a_phi0_b_intro with n;auto.
             }
             split.
 
@@ -524,15 +524,15 @@ Proof.
               - destruct (Hrec  (cons alpha2_1 n1 alpha2_2)) ; trivial.
                now apply head_lt.
                 discriminate.
-              - apply nf_helper_phi0R.
+              - apply lt_a_phi0_b_phi0R.
                 apply T1.lt_trans with (cons alpha2_1 n1 alpha2_2).
                 + destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial.
                   apply head_lt; auto. 
                   *  discriminate.
                   * tauto.
              +  
-                apply nf_helper_phi0.
-                apply nf_helper_intro with n;auto.
+                apply lt_a_phi0_b_phi0.
+                apply lt_a_phi0_b_intro with n;auto.
             }
             split.
 
@@ -694,7 +694,7 @@ Proof.
            ++ apply LT2; trivial.
               apply nf_intro; trivial.
               now apply nf_canon.
-              apply nf_helper_phi0R.
+              apply lt_a_phi0_b_phi0R.
               apply canon_lt.
               eapply nf_coeff_irrelevance;eauto. 
               discriminate. 
@@ -709,7 +709,7 @@ Proof.
              {
                apply nf_intro; trivial.
                apply nf_canon; trivial.
-               apply nf_helper_phi0R.
+               apply lt_a_phi0_b_phi0R.
                apply canon_lt.
                eapply nf_coeff_irrelevance;eauto.     
                discriminate.  
@@ -728,8 +728,8 @@ Proof.
                --  split.
                    ++ eapply nf_inv2, Hbeta.
                    ++ split. 
-                      ** apply nf_helper_phi0.     
-                      apply nf_helper_intro with n0;auto with T1.
+                      ** apply lt_a_phi0_b_phi0.     
+                      apply lt_a_phi0_b_intro with n0;auto with T1.
                       ** eapply nf_coeff_irrelevance;eauto.     
              }
              subst;
@@ -746,16 +746,16 @@ Proof.
                - split.
                  + eapply nf_inv2, Hbeta. 
                  + split. 
-                 * apply nf_helper_phi0.    
-                  apply nf_helper_intro with n;auto with T1.
+                 * apply lt_a_phi0_b_phi0.    
+                  apply lt_a_phi0_b_intro with n;auto with T1.
                  * eapply nf_coeff_irrelevance;eauto.   
              }
              destruct H4;  exists x; rewrite canon_SSn_zero. 
              apply LT4;auto.
              { 
                apply nf_intro; auto with T1.
                eauto with T1.
-               apply nf_helper_phi0R.   
+               apply lt_a_phi0_b_phi0R.   
                apply canon_lt.
                now apply nf_phi0. 
                intro; subst; discriminate.
@@ -775,11 +775,11 @@ Proof.
              { apply nf_intro;  trivial.
                eauto with T1.
             apply nf_canon; trivial; eauto with T1.
-            apply nf_helper_phi0R.   
+            apply lt_a_phi0_b_phi0R.   
             apply T1.lt_trans with lambda2.
             apply canon_lt; eauto with T1.
-            apply nf_helper_phi0.
-            apply nf_helper_intro with n; eauto with T1.
+            apply lt_a_phi0_b_phi0.
+            apply lt_a_phi0_b_intro with n; eauto with T1.
           }
           auto.
           auto.
@@ -788,11 +788,11 @@ Proof.
              { apply nf_intro. 
                - eauto with T1.
                - apply nf_canon; eauto with T1.
-               - apply nf_helper_phi0R.   
+               - apply lt_a_phi0_b_phi0R.   
                  apply T1.lt_trans with lambda2.
                  apply canon_lt; eauto with T1.
-                 apply nf_helper_phi0.
-                 apply nf_helper_intro with n; eauto with T1.
+                 apply lt_a_phi0_b_phi0.
+                 apply lt_a_phi0_b_intro with n; eauto with T1.
              }
              all: auto. 
       --  subst; assert ({i: nat |  beta2 t1< (canon lambda2 (S i))})%t1.
@@ -807,11 +807,11 @@ Proof.
         apply nf_intro. 
         eauto with T1.
         apply nf_canon; eauto with T1.
-        apply nf_helper_phi0R.   
+        apply lt_a_phi0_b_phi0R.   
         apply T1.lt_trans with lambda2.
         apply canon_lt; eauto with T1.
-        apply nf_helper_phi0.
-        apply nf_helper_intro with n; eauto with T1.
+        apply lt_a_phi0_b_phi0.
+        apply lt_a_phi0_b_intro with n; eauto with T1.
       }
       all: auto. 
   -   destruct s as [t [Ht Ht']]; subst lambda.

theories/ordinals/Epsilon0/E0.v

@@ -651,7 +651,7 @@ Proof.
   destruct H1.
   rewrite cnf_phi0 in H1.
   apply nf_intro; auto.
-  now apply nf_helper_phi0R. 
+  now apply lt_a_phi0_b_phi0R. 
   red.  
   apply succ_lt_limit.
   rewrite cnf_phi0.

theories/ordinals/Epsilon0/Epsilon0rpo.v

@@ -299,8 +299,8 @@ Proof.
                    auto with arith rpo.
                    auto with rpo.
                    apply lt_le_trans with (cons o'1 0 zero).
-                   apply nf_helper_phi0.
-                   eapply nf_helper_intro. 
+                   apply lt_a_phi0_b_phi0.
+                   eapply lt_a_phi0_b_intro. 
                    eauto. 
                    auto with T1 rpo.
                    auto with T1 rpo.