minor corrections

Author: Casteran

doc/chapter-primrec.tex

@@ -712,6 +712,7 @@ \subsubsection{First properties of the Ackermann function}
 \input{movies/snippets/Ack/nestedAckBound}
 
 
+\label{sect:AcknPR}
 
 Please note also that for any given $n$, the unary function
 (\texttt{Ack\,$n$}) is primitive recursive.
@@ -864,6 +865,10 @@ \subsection{Looking for a contradiction}
 $\texttt{Ack}\,x\,y\leq \texttt{Ack}\,n\,(\texttt{max}\,x\,y)$ holds.
 Thus, our impossibility proof is just a sequence of easy small steps.
 
+\begin{todo}
+Fix the display the local definition of \texttt{x} in the following proof.
+\end{todo}
+
 \input{movies/snippets/AckNotPR/AckNotPR}
 
 \begin{remark}
@@ -884,11 +889,12 @@ \subsection{Looking for a contradiction}
 \end{remark}
 
 \begin{remark}
-Note that the Ackermann function is a counter-example to the (false) statement:
-\begin{quote}
-{\color{red}
-  ``Let $f$ be a function of type \texttt{naryFunc\,2}. If, for any $n$, the function $f(n)$ is primitive recursive, then f is primitive recursive.''}
-\end{quote}
+  It may be interesting to compare the following statements:
+
+  \begin{itemize}
+  \item Ackermann function is not primitive recursive.
+  \item For any $n$, the function \texttt{Ack $n$ \_} is primitive recursive (see~\vref{sect:AcknPR}).
+  \end{itemize}
 \end{remark}
 
 \subsection{Related work}

theories/ordinals/Epsilon0/T1.v

@@ -108,8 +108,8 @@ Fixpoint T1limit alpha :=
   match alpha with
     | zero => false
     | cons zero _ _ => false
-    | cons alpha n zero => true
-    | cons alpha n beta => T1limit beta
+    | cons alpha _ zero => true
+    | cons _ _ beta => T1limit beta
   end.
 
 Compute T1limit T1omega.

theories/ordinals/MoreAck/AckNotPR.v

@@ -396,8 +396,8 @@ Section Impossibility_Proof.
 
   Lemma Ack_not_PR : False. (* .no-out *)
   Proof. (* .no-out *)
-    destruct (majorPR2_strict Ack HAck) as [m Hm]; 
-    set (x := max 2 m).  
+    destruct (majorPR2_strict Ack HAck) as [m Hm].
+    set (x := Nat.max 2 m).  
     specialize (Hm x x); rewrite Nat.max_idempotent in Hm.
     assert (H0: Ack m x <= Ack x x) by (apply Ack_mono_l; lia). 
     lia.

theories/ordinals/OrdinalNotations/ON_Generic.v

@@ -20,7 +20,7 @@ Delimit Scope ON_scope with on.
   Ordinal notation system on type [A] :
 *)
 
-(* begin snippet ONDef *)
+(* begin snippet ONDef:: no-out *)
 Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   {
   ON_comp :> Comparable lt cmp;

theories/ordinals/Prelude/Comparable.v

@@ -1,7 +1,7 @@
 From Coq Require Import Relations RelationClasses Setoid.
 Require Export MoreOrders STDPP_compat.
 
-(* begin snippet ComparableDef *)
+(* begin snippet ComparableDef:: no-out *)
 Class Compare (A:Type) := compare : A -> A -> comparison.
 
 Class Comparable {A:Type} (lt: relation A) (cmp : Compare A) :=