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}
@@ -817,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/MoreAck/PrimRecExamples.v

@@ -38,7 +38,7 @@ Check (fun n p q : nat =>  n * p + q): naryFunc 3.
 (* begin snippet extEqual2a *)
 Compute extEqual 2.
 
-Example extEqual_ex1: extEqual 2 Nat.mul (fun x y =>  y * x + x - x). (* .no-out *)
+Example extEqual_ex1: (Nat.mul: naryFunc 2) =x= fun x y =>  y * x + x - x. (* .no-out *)
 Proof. 
   intros x y; cbn.
 (* end snippet extEqual2a *)
@@ -119,10 +119,10 @@ End compose2Examples.
 (* begin snippet FirstExamples *)
 Module MoreExamples. 
 
-(** The constant function which returns 0 *)
+(** The unary constant function which returns 0 *)
 Definition cst0 : PrimRec 1 := (PRcomp zeroFunc (PRnil _))%pr.
 
-(** The constant function which returns i *)
+(** The unary constant function which returns i *)
 Fixpoint cst (i: nat) : PrimRec 1 :=
   match i with
     0 => cst0
@@ -170,23 +170,21 @@ Compute PReval fact 5.
 (* end snippet tests *)
 
 (* begin snippet correctness:: no-out *)
-Lemma cst0_correct (i:nat) :
-  forall p:nat, PReval cst0 p = 0.
-Proof. intro p; reflexivity. Qed.
+Lemma cst0_correct : (PReval cst0) =x= (fun _ => 0).
+Proof. intros ?; reflexivity. Qed.
 
-Lemma cst_correct (i:nat) :
-  forall p:nat, PReval (cst i) p = i.
+Lemma cst_correct (k:nat) : PReval (cst k) =x= (fun _ => k).
 Proof.
-  induction i as [| i IHi]; simpl; intros p .
+  induction k as [| k IHk]; simpl; intros p.
   - reflexivity. 
-  - now rewrite IHi. 
+  - now rewrite IHk. 
 Qed. 
 
 Lemma plus_correct: 
-  forall n p, PReval plus n p = n + p. 
+  PReval plus =x= Nat.add.
 Proof. 
-  induction n as [ | n IHn]. 
-  - reflexivity. 
+  intros n; induction n as [ | n IHn]. 
+  - intro; reflexivity. 
   - intro p; cbn in IHn |- *; now rewrite IHn. 
 Qed. 
 
@@ -195,19 +193,19 @@ Remark mult_eqn1 n p:
       PReval plus (PReval mult n p) p.
 Proof. reflexivity. Qed.
 
-Lemma mult_correct n p: PReval mult n p = n * p.
+Lemma mult_correct: PReval mult =x= Nat.mul.
 Proof. 
- revert p; induction n as [ | n IHn].
+ intro n; induction n as [ | n IHn].
  - intro p; reflexivity. 
- - intro p; rewrite mult_eqn1, IHn, plus_correct; ring.
+ - intro p; rewrite mult_eqn1, (IHn p) , plus_correct. cbn. ring.
 Qed.      
 
 
-Lemma fact_correct n : PReval fact n  = Coq.Arith.Factorial.fact n.
+Lemma fact_correct : PReval fact =x= Coq.Arith.Factorial.fact.
 (* ... *)
 (* end snippet correctness *)
 Proof. 
-  assert (fact_eqn1: forall n, PReval fact (S n)  = 
+  intro n;  assert (fact_eqn1: forall n, PReval fact (S n)  = 
                                  PReval mult
                                    (PReval fact n) (S n))
     by  reflexivity. 
@@ -228,9 +226,8 @@ Definition PRcompose1 (g f : PrimRec 1) : PrimRec 1 :=
   PRcomp g [f]%pr.  
 
 Goal forall f g x, evalPrimRec 1 (PRcompose1 g f) x =
-                 evalPrimRec 1 g (evalPrimRec 1 f x).
-reflexivity. 
-Qed.
+                     evalPrimRec 1 g (evalPrimRec 1 f x).
+Proof. reflexivity. Qed.
 
 Remark compose2_0 (a:nat) (g: nat -> nat)  : compose2 0 a g = g a.
 Proof.   reflexivity. Qed.