Merge pull request #130 from coq-community/preRelease09

Revision book to page 82. deprecate a few symbols

.github/workflows/docker-action.yml

@@ -15,7 +15,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'coqorg/coq:dev-ocaml-4.13.1-flambda'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'

doc/epsilon0-chapter.tex

@@ -353,9 +353,7 @@ \subsubsection{A Predicate for Characterizing Normal Forms}
 \input{movies/snippets/T1/badTerm}
 
 
-This term would have been written \(\omega^1\times 2 + \omega^\omega \times 3\) in the usual mathematical notation. We note that the exponents of $\omega$ are not in the right (strictly decreasing) order.
-Nevertheless, with the help of the order \texttt{lt} on \texttt{T1}, we are now able to characterize
-the set of all well-formed ordinal terms:
+This term would have been written \(\omega^1\times 2 + \omega^\omega \times 3\) in the usual mathematical notation. We note that the exponents of $\omega$ are not in the right (strictly decreasing) order. The following boolean function determines whether a given ordinal term is well formed.
 
 
 \vspace{4pt}
@@ -472,7 +470,7 @@ \subsubsection{\texttt{E0}: a sigma-type for \texorpdfstring{$\epsilon_0$}{epsil
 
 \paragraph*{\gaiasign}
 \index{gaiabridge}{Type of well formed ordinal terms below $\epsilon_0$}
- The library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} defines a \gaia-compatible type \texttt{E0}.
+ Our library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} also defines a type \texttt{E0} (which doesn't exist in \gaia-\texttt{ssete9}). 
 
 
 
@@ -483,7 +481,7 @@ \subsection{Syntactic definition of limit and successor ordinals}
 
 \vspace{4pt}
 \noindent
-\emph{From Module~\href{../theories/html/hydras.Epsilon0.T1.html\#succb}{Epsilon0.T1}}
+\emph{From Module~\href{../theories/html/hydras.Epsilon0.T1.html\#T1is_succ}{Epsilon0.T1}}
 
 
 
@@ -499,7 +497,7 @@ \subsection{Syntactic definition of limit and successor ordinals}
 
 \paragraph*{\gaiasign}
 \index{gaiabridge}{Limit and successor ordinals}
-In \gaia, the boolean functions associated with limit and successor ordinals are called \texttt{T1limit} and \texttt{T1is\_succ}.
+In \gaia, the boolean functions associated with limit and successor ordinals are also called \texttt{T1limit} and \texttt{T1is\_succ}.
 
  From~\href{../theories/html/gaia_hydras.HydraGaia_Examples.html}{gaia\_hydras.HydraGaia\_Examples}.
 
@@ -521,20 +519,21 @@ \subsubsection{Successor}
 \label{Functions:succ-T1}
 
 \vspace{4pt}
+\noindent
 \emph{From Module~\href{../theories/html/hydras.Epsilon0.T1.html\#succ}{Epsilon0.T1}}
 
 
 \input{movies/snippets/T1/succDef}
 
 The following lemma establishes the connection between the  function
-\texttt{succ} and the Boolean predicate \texttt{succb}.
+\texttt{succ} and the Boolean predicate \texttt{T1is\_succ}.
 
 \vspace{4pt}
 
 \input{movies/snippets/T1/succbIff}
 
-\begin{exercise}[\gaiasign]
-  Look for the \gaia-theorem which corresponds to \texttt{succb\_iff}.
+\begin{exercise}
+  \gaiasign Look for the \gaia-theorem which corresponds to \texttt{T1is\_succ\_iff}.
 \end{exercise}
 
 \subsubsection{Successor function on \texttt{E0}}
@@ -738,25 +737,35 @@ \subsubsection{Using a stronger inductive predicate.}
 \inputsnippets{E0/E0LtWf}
 
 
-\begin{remark}
+\begin{remark}[Related work]
 \label{remark:a3pat}
-The alternate proof of well-foundedness using \'Evelyne Contejean's work on
-    recursive path ordering~\cite{DershowitzRPO, a3pat} is available in the
+A proof of well-foundedness using \'Evelyne Contejean's work on
+    recursive path ordering~\cite{DershowitzRPO, a3pat} is also available in the
     library \href{../theories/html/hydras.Epsilon0.Epsilon0rpo.html}{Epsilon0.Epsilon0rpo}.
+
+    In~\cite{Manolios2005}, Manolios and Vroom prove the well-foundedness of ordinal terms below $\epsilon_0$ by reduction to the natural order on the set of natural numbers.
  \end{remark}
 
 
 
 \subsection{An ordinal notation for  \texorpdfstring{$\epsilon_0$}{epsilon0}}
 
-We build an instance of \texttt{ON}, and prove its correctness w.r.t. Schutte's model (see Chapter~\ref{chap:schutte}).
 
+We are now able to build an instance of \texttt{ON}.
+
+\vspace{4pt}
+\noindent
 \emph{From Module~\href{../theories/html/hydras.Epsilon0.E0.html}{Epsilon0.E0}}
 
 \input{movies/snippets/E0/InstanceEpsilon0}
 
 \label{instance-epsilon0}
 
+
+We prove also that this notation is correct w.r.t. Schutte's model (see Chapter~\ref{chap:schutte}).
+
+\vspace{4pt}
+\noindent
 \emph{From Module~\href{../theories/html/hydras.Schutte.Correctness_E0.html}{Schutte.Correctness\_E0}}
 
 
@@ -801,7 +810,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
 
 
-    \section{A refinement of \texttt{E0} : an ordinal notation for \texorpdfstring{$\omega^\omega$}{omega\^omega}}
+    \section{An ordinal notation for \texorpdfstring{$\omega^\omega$}{omega\^omega}}
 
     In Module   \href{https://github.com/coq-community/hydra-battles/blob/master/theories/
       ordinals/OrdinalNotations/OmegaOmega.v}{theories/ordinals/OrdinalNotations/OmegaOmega.v},
@@ -852,7 +861,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
 
 
-\begin{exercise}[not trivial]
+\begin{exercise}
   It may be interesting to write a \emph{direct} proof  of well-foundedness of the order in $\omega^\omega$ (\emph{i.e.}
   without using properties of $\epsilon_0$). This exercise may
   help to understand better the proof structure of Sect.~\vref{sec:strongly-accessible}.
@@ -1045,7 +1054,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
     We prove  the commutativity of $\oplus$ in two steps. 
     First, we prove by transfinite induction on $\alpha$ that the restriction of $\oplus$ to the
-    interval $[0..\alpha)$ is commutative.
+    interval $[0,\alpha)$ is commutative.
 
     \index{maths}{Transfinite induction}
 
@@ -1130,18 +1139,18 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
     \inputsnippets{GHydra/mDef, GHydra/mVariant, GHydra/Termination}
 
-    \section*{Conclusion}
+    % \section*{Conclusion}
 
-    Let us recall three results we have proved so far.
-    \begin{itemize}
-    \item There exists a strictly decreasing variant which maps \texttt{Hydra} into 
-    the segment $[0,\epsilon_0)$ for proving the termination of any hydra battle
-    \item There exists \emph{no} such variant from \texttt{Hydra} into 
-    $[0,\omega^2)$, \emph{a fortiori} into $[0,\omega)$.
-    \end{itemize}
+    % Let us recall three results we have proved so far.
+    % \begin{itemize}
+    % \item There exists a strictly decreasing variant which maps \texttt{Hydra} into 
+    % the segment $[0,\epsilon_0)$ for proving the termination of any hydra battle
+    % \item There exists \emph{no} such variant from \texttt{Hydra} into 
+    % $[0,\omega^2)$, \emph{a fortiori} into $[0,\omega)$.
+    % \end{itemize}
 
-    So, a  natural question is `` Does there exist any strictly decreasing variant mapping
-    type \texttt{Hydra} into some interval $[0,\alpha)$ (where $\alpha <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\alpha$, even if we consider a restriction to the set of ``standard'' battles.
+    % So, a  natural question is `` Does there exist any strictly decreasing variant mapping
+    % type \texttt{Hydra} into some interval $[0,\mu)$ (where $\mu <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\mu$, even if we consider a restriction to the set of ``standard'' battles.
 
 
 

doc/ks-chapter.tex

@@ -31,7 +31,7 @@ \section{Introduction}
 \end{quote}
 
 Our proofs are  constructive and require no axioms: they are  closed terms of the CIC, and are mainly composed on function definitions and proofs of properties of these functions. 
-They  share much theoretical material with Kirby and Paris', although they do not use any knowledge about Peano arithmetic nor model  theory.  The combinatorial arguments we use and implement
+They  borrow much theoretical material from Kirby and Paris, although they do not use any knowledge about Peano arithmetic nor about model  theory.  The combinatorial arguments we use and implement
 come from 
  an article by J.~Ketonen and R.~Solovay~\cite{KS81}, already  cited in the work
  by L.~Kirby and J.~Paris. % on the termination of Goodstein sequences and hydra battles~\cite{KP82}.
@@ -49,31 +49,33 @@ \section{Canonical Sequences}
 
 \index{maths}{Transfinite induction}
 \begin{itemize}
-\item If $\alpha\not=0$, then $\canonseq{\alpha}{i}<\alpha$. Thus canonical sequences can be used for proofs by transfinite induction or function definition by transfinite recursion
+\item If $\alpha\not=0$, then $\canonseq{\alpha}{i}<\alpha$. Thus canonical sequences can be used in proofs by transfinite induction or function definition by transfinite recursion
 \item If $\lambda$ is a limit ordinal, then $\lambda$ is the least upper bound of the set 
 $\{\canonseq{\lambda}{i}\;|\,i\in\mathbb{N}_1\}$
 
 
 \item If $\beta<\alpha<\epsilon_0$, then there is a ``path'' from $\alpha$ to $\beta$, \emph{i.e.} a
 sequence $\alpha_0=\alpha, \alpha_1, \dots, \alpha_n=\beta$, where for every $k<n$, there exists some $i_k$ such that $\alpha_{k+1}=\canonseq{\alpha_k}{i_k}$
-\item Canonical sequences correspond tightly to rounds of hydra battles: if $\alpha\not=0$,
-then $\iota(\alpha)$ is transformed into $\iota(\canonseq{\alpha}{i+1})$ in one round with
-the replication factor $i$ (Lemma \href{../theories/html/hydras.Hydra.O2H.html\#canonS_iota_i}{Hydra.O2H.canonS\_iota\_i}).
-\item From the two previous properties, we infer that whenever $\beta<\alpha<\epsilon_0$, there exists a (free) battle from $\iota(\alpha)$ to $\iota(\beta)$.
 \end{itemize}
 
 \begin{remark}
-  In~\cite{KS81}, canonical sequences are defined for any ordinal $\alpha <\epsilon_0$,
+  Canonical sequences are defined for any ordinal $\alpha <\epsilon_0$,
 by stating that if $\alpha$ is a successor ordinal $\beta+1$,  the sequence associated with 
 $\alpha$ is simply the constant sequence whose terms are equal to $\beta$.
 Likewise, the canonical sequence of $0$ maps any natural number to $0$.
 
-This convention allows us to make total the function that maps any ordinal $\alpha$ and natural number $i$ to the ordinal $\canonseq{\alpha}{i}$.
-
+Thus, the function that maps any ordinal $\alpha$ and natural number $i$ to the ordinal $\canonseq{\alpha}{i}$ is total.
 \end{remark}
 
+\subsection{Canonical sequences and hydra battles}
 
-First, let us recall how canonical sequences are defined in~\cite{KS81}. For efficiency's sake, we decided not to implement directly K.\&S's definitions, but to define in \gallina{} simply typed structurally recursive functions which share the abstract properties which are used in the mathematical proofs\footnote{With a small difference: the $0$-th term of the canonical sequence is not the same in our development as in~\cite{KS81}.}.
+Canonical sequences correspond tightly to rounds of hydra battles: if $\alpha\not=0$,
+then $\iota(\alpha)$ is transformed into $\iota(\canonseq{\alpha}{i+1})$ in one round with
+the replication factor $i$ (Lemma \href{../theories/html/hydras.Hydra.O2H.html\#canonS_iota_i}{Hydra.O2H.canonS\_iota\_i}).
+Thus, whenever $\beta<\alpha<\epsilon_0$, there exists a (free) battle from $\iota(\alpha)$ to $\iota(\beta)$.
+
+\subsection{Definitions}
+First, let us recall how canonical sequences are defined in~\cite{KS81}. For efficiency's sake, we decided not to implement directly K.\&S's definitions, but to define in \gallina{} simply typed structurally recursive functions which share the abstract properties which are used in the mathematical proofs.
 
 
 
@@ -125,8 +127,10 @@ \subsubsection{Canonical sequences in \coq}
 
 \input{movies/snippets/Canon/canonDef}
 
-\paragraph*{\gaiasign} Our library~\href{../theories/html/gaia_hydras.GCanon.html}{gaia\_hydras.GCanon} transposes the  function \texttt{canon} into \gaia's type \texttt{T1}
-(please see Sect.\~ref{sect:gcanon}).
+\paragraph*{\gaiasign}
+The translation of \texttt{canon} compatible with \gaia's data-types is
+defined in ~\href{../theories/html/gaia_hydras.GCanon.html\#canon}{gaia\_hydras.GCanon} (please see Sect.~\ref{sect:gcanon}).
+
 \index{gaiabridge}{Canonical sequences}
 \paragraph*{Remark}
 In the present state of this library, the following specializations of \texttt{canon} are still used in some proofs or lemma statements. They are planned to be deprecated.
@@ -195,8 +199,7 @@ \subsubsection{Limit ordinals are truly limits}
 \label{lemma:canonS-limit}
 
 
-Note the use of \coq's \texttt{sig} type in the theorem's statement, which
-relates the boolean function \texttt{limitb} defined on the \texttt{T1} data-type with a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
+Note the use of \coq's \texttt{sig} type in the theorem's statement, which expresses a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
 We can also state directly that $\lambda$ is a (strict) least upper bound of the elements of its canonical sequence.
 
 \input{movies/snippets/Canon/canonSLimitLub}
@@ -232,7 +235,8 @@ \section{Accessibility inside \texorpdfstring{$\epsilon_0$}{epsilon0}\,: paths}
 \label{sect:pathes-intro}
 
 Let us consider a kind of accessibility problem inside $\epsilon_0$: given two ordinals $\alpha$ and $\beta$, where $\beta<\alpha<\epsilon_0$, find a \emph{path} consisting of a finite sequence $\gamma_0=\alpha,\dots,\gamma_l=\beta$,
-where, for every $i<l$, $\gamma_i \not= 0$ \footnote{This condition allows us to ignore paths which end by a lot of useless $0$s.} and there exists some strictly positive integer $s_i$
+where, for every $i<l$, $\gamma_i \not= 0$
+and there exists some strictly positive integer $s_i$
 such that $\gamma_{i+1}=\canonseq{\gamma}{s_i}$.
 
 Let $s$ be the sequence $\langle s_0,s_1,\dots, s_{l-1} \rangle$. We describe the
@@ -247,15 +251,15 @@ \section{Accessibility inside \texorpdfstring{$\epsilon_0$}{epsilon0}\,: paths}
 
 
 Note that, given $\alpha$ and $\beta$, where $\beta < \alpha$, the sequence $s$ which leads from $\alpha$ to $\beta$ is not unique.
-Indeed, if $\alpha$ is a limit ordinal, the first element of $s$ can be any integer $i$ such that $\beta<\canonseq{\alpha}{i}$, and if $\alpha$ is a successor ordinal,
-then the sequence $s$ can start with any positive integer.
 
 
-For instance, we have also 
-$\omega*2 \xrightarrow[3,4,5,6]{}\omega$. 
+
+For instance, we have 
+$\omega\times 2 \xrightarrow[2]{}\omega$ and
+$\omega\times 2 \xrightarrow[3,4,5,6]{}\omega$. 
 Likewise,
-$\omega*2 \xrightarrow[1,2,1,4]{} 0$ and
-$\omega*2 \xrightarrow[3,3,3,3,3,3,3,3]{} 0$.
+$\omega\times 2 \xrightarrow[1,2,1,4]{} 0$ and
+$\omega\times 2 \xrightarrow[3,3,3,3,3,3,3,3]{} 0$.
 \end{remark}
 
 \subsection{Formal definition}
@@ -285,7 +289,7 @@ \subsection{Formal definition}
 \paragraph*{\gaiasign}
 
 The library~\href{../theories/html/gaia_hydras.GPaths.html}{gaia\_hydras.GPaths} transposes the  notion of path into \gaia's type \texttt{T1}
-(please see Sect.\~ref{sect:gpath}).
+(please see Sect.~\ref{sect:gpath}).
 
 
 \index{hydras}{Exercises}
@@ -312,7 +316,7 @@ \subsection{Existence of a path}
 
 
 \noindent 
-From the lemma \texttt{canon\_LT}~\vref{lemma:canon_LT}, we can convert any path into an inequality on ordinals (by induction on paths).
+By the lemma \texttt{canon\_LT}~(Sct.\vref{lemma:canon_LT}), we can convert any path into an inequality on ordinals (by induction on paths).
 
 \input{movies/snippets/Paths/pathToLT}
 
@@ -532,12 +536,13 @@ \section{The case of standard battles}
 
 
 
-Our goal is now  to transform any inequality $\beta<\alpha<\epsilon_0$ into a standard path $\alpha \xrightarrow[i,j]{} \beta$ for some $i$ and $j$, then into a standard battle
-from $\iota(\alpha+i)$ to $\iota(\beta)$. 
+Our goal is now  to transform any inequality $\beta<\alpha<\epsilon_0$ into a standard path $\alpha \xrightarrow[i,j]{} \beta$ for some $i$ and $j$, which corresponds to a standard battle
+from $\iota(\alpha)$ (at time $i$)  to $\iota(\beta)$
+(at time $j$) .
 Following~\cite{KS81}, we proceed in two stages:
 \begin{enumerate}
 \item we simulate plain (free) paths from $\alpha$ to $\beta$ with
-paths made of steps $(\gamma,\canonseq{\gamma}{n})$, \emph{with the same $n$ all along the path}
+paths made of steps $(\gamma,\canonseq{\gamma}{n})$, \emph{with the same $n$ all along the path}.
 \item we simulate any such path by a standard path.
 \end{enumerate}
 

doc/large-sets-chapter.tex

@@ -1,7 +1,7 @@
 \chapter{Large sets and rapidly growing functions}\label{chap:alpha-large}
 
 \begin{remark}
-Some notations (mainly names of fast-growing functions) of our development may differ slightly from the literature. Although this fact does not affect our proofs, we are preparing a future version where the names $F\_alpha$, $f\_alpha$, $H\_alpha$, etc., are fully consistent with the cited articles.
+Some notations (mainly names of fast-growing functions) of our development may differ slightly from the literature. Although this fact does not affect our proofs, we are preparing a future version where the names $F_\alpha$, $f_\alpha$, $H_\alpha$, etc., are fully consistent with the cited articles.
 
 \end{remark}
 %\section{Introduction}
@@ -109,7 +109,7 @@ \subsection{Examples}
 \section{Length of minimal large sequences}
 \label{sect:lalpha-section}
 
-Now, consider any natural number $k>0$ any ordinal $0<\alpha<\epsilon_0$.  We would like to compute
+Now, let us consider some natural number $k>0$ and an ordinal $0<\alpha<\epsilon_0$.  We would like to compute
 a number $l$ such that the interval $[k,l]$ is $\alpha$-mlarge. So, 
 the standard battle starting with $\iota(\alpha)$ and the replication factor $k$ will end after $(l-k+1)$ steps.
 
@@ -136,7 +136,7 @@ \section{Length of minimal large sequences}
 use \coq{} to reason  about the \emph{specification} of \texttt{L},
 prove properties of any function which satisfies this specification.
 In Sect.~\ref{sect:L-equations}, we use the \texttt{coq-equations} plug-in
-to define a function \texttt{L\_}, and prove its correctness w.r.t. its specification.
+to define  \texttt{L\_}, then prove its correctness w.r.t. its specification.
 
 
 \subsection{Formal specification}

doc/ordinal-chapter.tex

@@ -952,14 +952,11 @@ \section{Comparing two ordinal notations}
    \label{fig:subsegment}
  \end{figure}
 
-If \texttt{OB} is presumed to be correct, then we may consider that \texttt{OA} ``inherits'' its correctness from the bigger notation system \texttt{OB}.
-
-
 \label{types:SubON}
 \index{hydras}{Library OrdinalNotations!Type classes!SubON}
 
-following definition
-(in ~\href{../theories/html/hydras.OrdinalNotations.ON_Generic.html}{ON\_Generic}).
+\noindent
+From~\href{../theories/html/hydras.OrdinalNotations.ON_Generic.html}{ON\_Generic}.
 
 \input{movies/snippets/ON_Generic/SubONDef}
 

meta.yml

@@ -107,8 +107,7 @@ supported_coq_versions:
   opam: '{(>= "8.13" & < "8.16~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
+- version: 'dev-ocaml-4.13.1-flambda'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'

theories/additions/Dichotomy.v

@@ -128,7 +128,7 @@ Proof.
     discriminate.
 Qed.
 
-Global Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI 
+#[global] Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI 
              dicho_aux_le_xIXO dicho_aux_le_xIXI : chains.
 
 Lemma dicho_aux_lt : forall p, 3 < p ->