Merge branch 'master' of https://github.com/coq-community/hydra-battles

doc/hydra-chapter.tex

@@ -112,7 +112,7 @@ \subsection{The rules of the game}
 Thus, the replication process will be represented as a binary relation on a data type \texttt{Hydra},
 linking the state of the hydra \emph{before} and \emph{after} the transformation.
 A battle will thus be represented as a sequence of terms of type \texttt{Hydra}, respecting the rules of the game.
-
+ In other terms, we consider hydra battles as \emph{transition systems}.
 
 
 
@@ -154,7 +154,7 @@ \subsection{Example}
 \end{figure}
 
 
-\begin{figure}[hp]
+\begin{figure}[h]
 \centering
 \begin{tikzpicture}[very thick, scale=0.5]
 
@@ -179,7 +179,7 @@ \subsection{Example}
 \label{fig:Hy2}
 \end{figure}
 
-\begin{figure}[hp]
+\begin{figure}[h]
 \centering
 \begin{tikzpicture}[very thick, scale=0.6]
 
@@ -221,7 +221,7 @@ \subsection{Example}
 
 Figs.~\ref{fig:Hy4} and~\vref{fig:Hy5} represent a possible third round of the battle, with a replication factor equal to $2$. Let us call \texttt{Hy'''} the state of the hydra after that third round.
 
-\begin{figure}[hp]
+\begin{figure}[h]
 \centering
 \begin{tikzpicture}[very thick, scale=0.6]
 
@@ -262,7 +262,7 @@ \subsection{Example}
 \caption{A third beheading (wounded part in red) \label{fig:Hy4}}
 \end{figure}
 
-\begin{figure}[hp]
+\begin{figure}[h]
 \centering
 \begin{tikzpicture}[very thick, scale=0.4]
 
@@ -415,9 +415,7 @@ \section{Hydras and their representation in \emph{Coq}}
 \input{movies/snippets/Hydra_Definitions/HydraAlt}
 
 Using this representation, one can re-define all the constructions of this chapter, which is left as an exercise.
-You will probably have to use patterns described for instance in~\cite{BC04} or the archives of the \coq communication channels (please consult~\url{https://coq.inria.fr/community.html}).
-
-
+You will probably have to use patterns described for instance in~\cite{BC04, BC04ch14} or the archives of the \coq communication channels (please consult~\url{https://coq.inria.fr/community.html}).
 \end{remark}
 
 
@@ -552,8 +550,8 @@ \subsubsection{A failed attempt}
 
 \input{movies/snippets/Hydra_Examples/BadInductiond}
 
-We notice that this sub-goal does not contain any hypothesis
-on the height and size of the hydra \texttt{h}. So, it looks hard to prove the conclusion. Let's stop.
+We notice immediately that the context of this sub-goal does not allow to infer its conclusion.
+ Let's stop.
 
 \input{movies/snippets/Hydra_Examples/BadInductione}
 
@@ -611,7 +609,7 @@ \section{Relational description of hydra battles}
 
 
 In this section, we represent the rules of hydra battles as a binary relation associated with
-a \emph{round}, i.e., an interaction composed of the two following actions:
+a \emph{round}\footnote{usually called a \emph{small step semantics}}, i.e., an interaction composed of the two following actions:
 \begin{enumerate}
 \item Hercules chops off one head of the hydra.
 \item Then, the  hydra replicates the wounded part (if the head is at distance $\geq 2$ from the foot).
@@ -635,7 +633,7 @@ \section{Relational description of hydra battles}
 
 \subsection{Chopping off a head at distance 1 from the foot (relation  R1)}
 
-If Hercules chops off a head close to the root, there is no replication at all. We use an auxiliary 
+If Hercules chops off a head next to the root, there is no replication at all. We use an auxiliary 
 predicate \texttt{S0}, associated with the removing of one head from a sequence of hydras.
 
 
@@ -648,7 +646,7 @@ \subsubsection{Example}
 \label{sec:orgheadline45}
 
 Let us represent in \coq{}   the transformation of the hydra of Fig.~\vref{fig:Hy} into
-the configuration represented in Fig.~\ref{fig:Hy-prime}.
+the configuration represented in Fig.~\vref{fig:Hy-prime}.
 
 \vspace{4pt}
 \emph{From Module~\href{../theories/html/hydras.Hydra.Hydra_Examples.html}{Hydra.Hydra\_Examples}}
@@ -697,7 +695,7 @@ \subsubsection{Example}
 
 \subsection{Binary relation associated with a round}
 
-Let us merge \texttt{R1} and \texttt{R1}  into a single relation.
+Let us merge \texttt{R1} and \texttt{R2}  into a single relation.
 First,  we define the  relation \texttt{(round\_n n h h')} where \texttt{n} is the expected number of  replications (irrelevant in the case of an \texttt{R1}-transformation).
 Then, we define a \emph{round} (small step) of a battle
 by abstraction over \texttt{n}, 
@@ -731,13 +729,6 @@ \subsection{Rounds and battles}
 
 \input{movies/snippets/Hydra_Definitions/roundPlus}
 
-\index{hydras}{Exercises}
-
-\begin{exercise}
-  Prove that if \texttt{$h$ -+-> $h'$}, then
-  the height of $h'$ is less or equal than the height of $h$.
-
-\end{exercise}
 
 \begin{remark}
 \label{remark:transitive-closure}
@@ -763,6 +754,12 @@ \subsection{Rounds and battles}
 The same remark also holds for reflexive and transitive closures. 
 \end{remark}
 
+\index{hydras}{Exercises}
+\begin{exercise}
+  Prove that if \texttt{$h$ -+-> $h'$}, then
+  the height of $h'$ is less or equal than the height of $h$.
+
+\end{exercise}
 \index{hydras}{Exercises}
 
 \begin{exercise}
@@ -1007,9 +1004,9 @@ \subsection{Looking for regularities}
 
 \subsection{Testing  \dots}
 \label{sect:testing}
-In order to study \emph{experimentally} the different  configurations of the  battle, we will use a simple data type for representing the states as tuples composed of
-the round number, and the respective number of daughters  \texttt{h2}, \texttt{h1}, and heads
-of the current hydra.
+In order to make the study of this battle easier,  we will use a simple data type for representing a configuration 
+$(\textit{round}, \texttt{hyd}\;n_2\;n_1\; n_h)$ as the $4$-tuple
+
 
 
 \input{movies/snippets/BigBattle/stateDef}
@@ -1039,7 +1036,7 @@ \subsection{Testing  \dots}
 \input{movies/snippets/BigBattle/testDefTests}
 
 The battle we are studying looks to be awfully long. Let us concentrate our
-tests on some particular events : the states where $\texttt{nh}=0$.
+tests on some particular events : the states where $n_h=0$.
 From the value of \texttt{test 5},  it is obvious that at the 10-th round, the counter \texttt{nh} is equal to zero.
 
 
@@ -1068,7 +1065,8 @@ \subsection{Proving \dots}
 We are now able to reason about the sequence of transitions defined by our hydra battle. 
 
 Let us define a binary relation associated with every round of the battle.
-In the following definition \texttt{i} is associated with the round number (or date, if we consider a discrete time), and \texttt{a}, \texttt{b}, \texttt{c} respectively associated with the number of occurrences of \texttt{h2}, \texttt{h1} and heads connected to the hydra's foot. For convenience, we do not use the type \texttt{state} of the preceding section, but consider the round numbers and the number of hydras \texttt{h2}, \texttt{h1} and heads as separate arguments of the relation (which is no more ---formally--- ``binary'').
+In the following definition \texttt{i} is associated with the round number (or date, if we consider a discrete time), and \texttt{a}, \texttt{b}, \texttt{c} respectively associated with the number of occurrences of \texttt{h2}, \texttt{h1} and heads connected to the hydra's foot. For convenience\footnote{In a few words, the type \texttt{state} was designed for performing \emph{computations}, and \texttt{steps} for writing \emph{interactive proofs}, inspired by the aforementionned computations.},
+we do not use the type \texttt{state} of the preceding section, but consider the round numbers and the number of hydras \texttt{h2}, \texttt{h1} and heads as separate arguments of the relation (which is no more ---formally--- ``binary'').
 
 \input{movies/snippets/BigBattle/oneStep}
 
@@ -1088,7 +1086,7 @@ \subsection{Proving \dots}
 
 
 
-The following lemma establishes a relation between \texttt{steps} and the predicate \texttt{battle}.
+The following lemma establishes a relation between \texttt{steps} and the predicate \texttt{rounds}.
 
 \input{movies/snippets/BigBattle/stepsBattle}
 
@@ -1248,7 +1246,7 @@ \subsection{A minoration lemma}
 \vspace{4pt}
 
 
-The number $N$ is greater than or  equal to $2^{2^{95}\times 95}.$ If we wrote $N$ in base $10$, $N$ would require at least $10^{30}$ digits!
+The number $N$ is greater than or  equal to $2^{2^{95}\times 95}.$ If we write $N$ in base $10$, $N$ would require at least $10^{30}$ digits!
 
 
 \section{Generic properties}
@@ -1331,7 +1329,7 @@ \subsection{A  small proof of impossibility}
 one has to consider first a well-founded set $(A,<)$, then a strictly decreasing measure on this set.  The following  lemma shows that,  if  the order structure $(A,<)$ is too simple, it is useless to look for a convenient measure, which simply no exists. Such kind of result is useful, because it saves you time and effort.
 
 
-The best known well-founded order is the natural order on the set $\mathbb{N}$ of natural numbers (the type \texttt{nat} of Standard library). It would be interesting to look for some measure $m:\texttt{nat}\arrow\texttt{nat}$ and prove it is a variant.
+The best known well-founded order is the natural order on the set $\mathbb{N}$ of natural numbers (the type \texttt{nat} of Standard Library). It would be interesting to look for some measure $m:\texttt{nat}\arrow\texttt{nat}$ and prove it is a variant.
 
 Unfortunately, we can prove that 
 \emph{no} instance of class (\texttt{WfVariant round Peano.lt $m$}) can be built, where

doc/hydras.tex

@@ -207,6 +207,13 @@ \section{Generalities}
 necessary. Since the development of a theory is represented as a bunch of computer files,
 everyone is able to read the proofs with an arbitrary level of detail, or to play with the theory by writing alternate proofs or definitions.
 
+If a formal development is large (at least 10 KLOCs), we believe that a human-readable document containing explanations, diagrams, code snippets, examples, exercises, etc.) would be useful
+for a better understanding of both the mathematical contents
+and the formalization techniques used in the
+development~\cite{Chiplunkar23}.
+
+This document has been generated with \alectr (see Sect.~\vref{sect:alectryon-intro}), which ensures the \texttt{pdf} is consistent with the last compiled version of the \coq project.
+
 
 Among all the theorems proved with the help of proof assistants like \coq{}~\cite{Coq,BC04}, \hol{}~\cite{HOL}, \isabelle{}~\cite{isabelle},  etc.,
 several statements and proofs  share some interesting features:
@@ -331,6 +338,7 @@ \section{Generalities}
 
 
 \subsection{Documenting theories with \alectr}
+\label{sect:alectryon-intro}
 
 Quotations of \coq source and answers are progressively replaced from copy-pasted \emph{verbatim} to automatically generated \emph{LaTeX} blocks, using Clément Pit-Claudel's \alectr  tool~\cite{alectryonpaper, alectryongithub}.
 Many thanks to Jérémy Damour, Clément Pit-Claudel  and Théo Zimmermann who designed tools for maintaining consistency between the always evolving \coq{} modules and documentation written in \emph{LaTeX}.
@@ -341,8 +349,8 @@ \subsection{Trust in our proofs}
 \label{sect:trust-in-proofs}
 
 Unlike mathematical literature, where definitions and proofs are spread out over many articles and books,
-the whole proof is now inside your computer. It is composed from the \texttt{.v} files you downloaded and
-parts of \coq's standard library. Thus, there is no ambiguity in our definitions and the premises of the theorems. Furthermore, you will be able to navigate through the development, using your favorite text editor or IDE, and some commands like \texttt{Search}, \texttt{Locate},  etc.
+the whole proof is now inside your computer. It is composed from the \texttt{.v} files you downloaded,
+parts of \coq's standard library, and required \coq packages (see Fig.~\vref{fig:genealogy}).  Thus, there is no ambiguity in our definitions and the premises of the theorems. Furthermore, you will be able to navigate through the development, using your favorite text editor or IDE, and some commands like \texttt{Search}, \texttt{Locate},  etc.
 
 
 
@@ -356,7 +364,8 @@ \subsection{Assumed redundancy}
 several aborted proofs.
 Of course, do not hesitate to contribute nice proofs or alternative definitions!
 
-It may also happen that some proof looks to be useless, because the proven theorem is a trivial consequence of another (also proven) result.
+It may also happen that some direct proof looks to be useless,
+because the proven theorem is a trivial consequence of another (also proven) result.
 For instance, let us consider the three following statements:
 \begin{enumerate}
 \item There is no measure into $\mathbb{N}$ for proving the termination of all hydra battles (Sect~\vref{omega-case}).
@@ -398,7 +407,6 @@ \subsection{Typographical Conventions}
 
 \subsubsection{Using \alectr}
 Whenever possible, we use \alectr to display \coq code (definition, proof scripts) and answers.
-
 Here are two  examples from Chapters~\ref{chapter:primrec}
 and~\ref{chapter-powers}.
 
@@ -410,18 +418,25 @@ \subsubsection{Using \alectr}
 \inputsnippets{Fib2/fibEuclDemo}
 
 \subsubsection{Verbatim quotations}
+In some situations, we replace \alectr snippets with
+verbatim blocks.
 
-Quotations of \coq{} source  from others libraries (\coq's standard library, borrowed plug-ins)  are displayed as follows.
-
-\begin{Coqsrc}
+\begin{itemize}
+\item When the quoted source belongs to some library on which we do not have the write permission, we cannot include
+  directives for generating snippets.
+ For instance, the following code belongs to \coq's standard library.
+  \begin{Coqsrc}
   Inductive CompareSpec (Peq Plt Pgt : Prop) :
   comparison -> Prop :=
     CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
   | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
   | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
 \end{Coqsrc}
 
-We use also verbatim code inclusions when the examples lead to very long computations.
+
+\item 
+We use also verbatim code inclusions when the examples would lead to too long computations during the compilation and the
+documentation generation.
 
 \begin{Coqbad}
 Example C87_ok_slow : chain_correct 87 C87.
@@ -436,7 +451,7 @@ \subsubsection{Verbatim quotations}
 \begin{Coqbad}
 Qed.
 \end{Coqbad}
-
+\end{itemize}
  \subsection{Remark}
 
 In general, we do not include full proof scripts in this document. The only exceptions are very short proofs (\emph{e.g.}, proofs by computation, or by application of automatic tactics). Likewise, we may display only the important steps on a long interactive proof, for instance, in the following lemma (\vref{lemma:L-2_6-1}):
@@ -479,7 +494,7 @@ \subsection{Alternative or bad definitions}
 
 \section{How to install the libraries}
 \label{sec:orgheadline4}
- The present distribution has been checked with version 8.14.1 of the Coq proof assistant, with a few plug-ins. \emph{Please refer to \href{https://github.com/coq-community/hydra-battle\#readme}{the README file of the project}.}
+ The present distribution has been checked with versions up to 8.18 of the Coq proof assistant, with a few plug-ins. \emph{Please refer to \href{https://github.com/coq-community/hydra-battle\#readme}{the README file of the project}.}
 
 
 \section{Comments on exercises and projects}

doc/thebib.bib

@@ -69,10 +69,12 @@ @book{BC04
 
 
 
+
+
 @InBook{BC04ch14,
   author = 	 {Bertot, Yves and Cast\'eran, Pierre},
   title = 	 {Interactive Theorem Proving and Program Development: {Coq'Art}: The Calculus of Inductive Constructions},
-  chapter = 	 {14},
+  chapter = 	 {Foundations of Inductive Types},
   publisher = 	 {Springer},
   year = 	 {2004},
    note = 	 {\url{https://www-sop.inria.fr/members/Yves.Bertot/coqart-chapter14.pdf}},
@@ -1331,3 +1333,13 @@ @Misc{Dowek2023
 note =    {\url{https://arxiv.org/pdf/2303.18099.pdf}},
 }
 
+@InProceedings{Chiplunkar23,
+  author =       {Shardul Chiplunkar and Clément Pit-Claudel },
+  title =        {Diagrammatic notations for interactive theorem proving},
+  OPTcrossref =  {},
+  booktitle =    {4th International Workshop on Human Aspects of Types and Reasoning Assistants},
+  year =      {2023},
+  address =   {Cascais, Portugal},
+  note =      {\url{https://infoscience.epfl.ch/record/305144}}
+}
+

theories/ordinals/Hydra/BigBattle.v

@@ -73,8 +73,7 @@ Qed.
 (* end snippet L23L03 *)
 
 (** From now on, we abstract the configurations of the battle
-  as tuples (round number, n2, n1, nh) where n2 (resp. n1, nh) is the number of 
-  sub-hydras h2 [resp. h1, heads] *)
+  as tuples (round number, n2, n1, nh) where n2 (resp. n1, nh) is the number of daughters of type h2 [resp. h1, heads] *)
 
 (* begin snippet stateDef *)