small corrections

Author: Casteran

doc/chapter-primrec.tex

@@ -624,6 +624,7 @@ \section{Proofs by induction over all primitive recursive functions}
 
 \subsection{Ackermann function}
 
+
 Ackermann function is traditionally defined as a function from 
 $\mathbb{N}\times \mathbb{N}$ into $\mathbb{N}$, through
 three equations:
@@ -738,7 +739,9 @@ \subsubsection{First properties of the Ackermann function}
 
 \input{movies/snippets/AckNotPR/AckNIsPR}
 
+\section{Ackermann function is not primitive recursive}
 
+\label{sect:ack-not-PR}
 
 In order to prove that \texttt{Ack} (considered as a function of two arguments) is not primitive recursive, the usual method consists in two steps:
 
@@ -879,7 +882,7 @@ \subsection{Looking for a contradiction}
 Thus, our impossibility proof is just a sequence of easy small steps.
 
 \begin{remark}
-In the following snippet,  some versions \emph{Alectryon}'s \texttt{Latex} generator  print the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}.
+In the following snippet,  some versions of \emph{Alectryon}'s \texttt{Latex} generator  print the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}.
 Thus the proof script is correct, but the three last sub-goals are not correctly displayed, since 
 they do not show how the inequalities $2\leq x$ and $m \leq x$ could be inferred by \texttt{lia}.
 

doc/schutte-chapter.tex

@@ -689,7 +689,6 @@ \section{Cantor normal form}
 \end{Coqsrc}
 
 Is it true ?
-
 \emph{You may start this exercise with the file
     \href{https://github.com/coq-community/hydra-battles/tree/master/exercises/ordinals/schutte_cnf_counter_example.v}{exercises/ordinals/schutte\_cnf\_counter\_example.v}.}
 \end{exercise}
@@ -706,7 +705,7 @@ \section{Cantor normal form}
 
 \begin{remark}
 The sub-directory
-    \href{https://github.com/coq-community/hydra-battles/tree/master/theories/ordinals/Gamma0}{theories/oridinals/Gamma0} contains an (incomplete, still undocumented) implementation of the set of ordinals below $\Gamma_0$, represented in Veblen normal form. 
+    \href{https://github.com/coq-community/hydra-battles/tree/master/theories/ordinals/Gamma0}{theories/ordinals/Gamma0} contains an (incomplete, still undocumented) implementation of the set of ordinals below $\Gamma_0$, represented in Veblen normal form. 
 \end{remark}
 
 \section{An embedding of \texttt{T1} into \texttt{Ord}}

theories/ordinals/Schutte/CNF.v

@@ -9,6 +9,7 @@ From Coq Require Import Arith List Sorting.Sorted
 From hydras Require Export Schutte_basics  Ordering_Functions
      PartialFun  Countable Schutte.Addition AP.
 From Coq Require Export  Classical.
+Import ListNotations.
 
 Set Implicit Arguments.
 
@@ -312,8 +313,7 @@ Qed.
 
 Lemma cnf_unicity l alpha:
   is_cnf_of alpha l ->
-  forall l', is_cnf_of alpha l' ->
-             l = l'. (* .no-out *)
+  forall l', is_cnf_of alpha l' -> l = l'. (* .no-out *)
 (*| .. coq:: none |*)
 Proof.
   revert alpha; induction l.
@@ -407,12 +407,10 @@ Qed.
 
 (*| .. coq:: no-out |*)
 
-Lemma cnf_of_epsilon0 : is_cnf_of epsilon0 (epsilon0 :: nil).
-Proof.
-  split.
-  - constructor.
-  - simpl; now rewrite alpha_plus_zero, epsilon0_fxp.
+Lemma cnf_of_epsilon0 : is_cnf_of epsilon0 [epsilon0].
+Proof. (*||*)
+  split; [constructor | cbn]. 
+  now rewrite alpha_plus_zero, epsilon0_fxp.
 Qed.
-(*||*)
 
 (* end snippet cnfOfEpsilon0 *)