diff --git a/doc/Gamma0-chapter.tex b/doc/Gamma0-chapter.tex index 24871163..a9ecdb50 100644 --- a/doc/Gamma0-chapter.tex +++ b/doc/Gamma0-chapter.tex @@ -1,5 +1,5 @@ \chapter{The Ordinal \texorpdfstring{$\Gamma_0$}{Gamma0} (first draft)} - +\label{chap:gamma0} \emph{This chapter and the files it presents are still very incomplete, considering the impressive properties of $\Gamma_0$~\cite{Gallier91}. We hope to add new material soon, and accept contributions!} diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex index a7fd3cdf..6b246ebb 100644 --- a/doc/epsilon0-chapter.tex +++ b/doc/epsilon0-chapter.tex @@ -5,8 +5,8 @@ \label{cnf-math-def} \label{chap:T1} -In this chapter, we adapt to \coq{} the well-known~\cite{KP82} proof that Hercules eventually wins every battle, whichever the strategy of each player. -In other words, we present a formal and self contained proof of termination of all [free] hydra battles. +In this chapter, we adapt to \coq{} the well-known proof~\cite{KP82} that Hercules eventually wins every battle, whichever the strategy of each player. +In other words, we present a formal and self-contained proof of termination of all [free] hydra battles. First, we take from Manolios and Vroon~\cite{Manolios2005} a representation of the ordinal $\epsilon_0$ as terms in Cantor normal form. Then, we define a variant for hydra battles as a measure that maps any hydra to some ordinal strictly less than $\epsilon_0$. @@ -16,7 +16,7 @@ \section{The ordinal \texorpdfstring{\(\epsilon_0\)}{epsilon0}} The ordinal \(\epsilon_0\) is the least ordinal number that satisfies the equation \(\alpha = \omega^\alpha\), where \(\omega\) is -the least infinite ordinal. +the least infinite ordinal\footnote{For a precise ---\,\emph{i.e.} mathematical\,--- definition of $\omega^\alpha$, please see Sect.~\vref{sect:AP-and-phi0}.} . Thus, we can intuitively consider \(\epsilon_0\) as an \emph{infinite} \(\omega\)-tower. @@ -28,10 +28,10 @@ \subsection{Cantor normal form} Any ordinal strictly less that \(\epsilon_0\) can be finitely represented by a unique \emph{Cantor normal form}, -that is, an expression which is either the ordinal \(0\) or +that is, an expression which is a sum \(\omega^{\alpha_1} \times n_1 + \omega^{\alpha_2} \times n_2 + - \dots + \omega^{\alpha_p} \times n_p\) where all the \(\alpha_i\) -are ordinals in Cantor normal form, \(\alpha_1 > \alpha_2 > \alpha_p\), + \dots + \omega^{\alpha_p} \times n_p\) where $p\in\mathbb{N}$, all the \(\alpha_i\) +are ordinals in Cantor normal form, \(\alpha_1 > \alpha_2 > \alpha_p\) and all the \(n_i\) are positive integers. An example of Cantor normal form is displayed in Fig \ref{fig:cnf-example}: @@ -55,8 +55,7 @@ \subsection{Cantor normal form} to this type, and finally prove that our representation fits well with the expected mathematical properties: the order we define is a well order, and the decomposition into Cantor normal form is consistent -with the implementation of the arithmetic operations of exponentiation of base \(\omega\) -and addition. +with usual definition of ordinals, for instance in \gaia~\cite{Gaia}, Schütte's book~\cite{schutte}, or larger ordinal notations~\vref{chap:gamma0}. \paragraph*{Remark} \label{sec:orgheadline65} @@ -131,7 +130,7 @@ \subsubsection{Example} \paragraph{Remark} For simplicity's sake, we chose to forbid expressions of the form $\omega^\alpha\times 0 + \beta$. Thus, the construction (\texttt{cons $\alpha$ $n$ $\beta$}) is intended to represent the ordinal $\omega^\alpha\times(n+1)+\beta$ and not $\omega^\alpha\times n+\beta$. -In a future version, we should replace the type \texttt{nat} with \texttt{positive} in \texttt{T1}'s +In a future version, we would like to replace the type \texttt{nat} with standard library's type \texttt{positive} in \texttt{T1}'s definition. But this replacement would take a lot of time \dots{} @@ -210,11 +209,11 @@ \subsubsection{The ordinal \(\omega\)} \input{movies/snippets/T1/omegaDef} -Note that \texttt{omega} is not an identifier in \HydrasLib, thus any tactic like \texttt{unfold omega} would fail. +Note that \texttt{T1omega} is not an identifier in \HydrasLib, thus any tactic like \texttt{unfold T1omega} would fail. \index{gaiabridge}{The ordinal $\omega$} \paragraph*{\gaiasign} -In \texttt{gaia.ssete9}, the ordinal $\omega$ is bound to the \emph{constant} \texttt{T1omega}. +In \texttt{gaia.ssete9}, the ordinal $\omega$ is bound to the \emph{constant} \texttt{T1omega} (not a notation). @@ -292,7 +291,7 @@ \subsection{Pretty-printing ordinals in Cantor normal form} \index{hydras}{Projects} \begin{project} -Design (in \ocaml?) a set of tools for systematically pretty printing ordinal terms in Cantor normal form. +Design tools for systematically pretty printing ordinal terms in Cantor normal form. \end{project} @@ -315,6 +314,8 @@ \subsection{Comparison between ordinal terms} \input{movies/snippets/T1/compareDef} +\input{movies/snippets/T1/Instances} + \label{Predicates:lt-T1} Please note that this definition of \texttt{lt} makes it easy to write proofs by computation, as shown by the following examples. @@ -325,11 +326,11 @@ \subsection{Comparison between ordinal terms} \input{movies/snippets/T1/ltExamples} -Links between the function \texttt{compare} and the relations -\texttt{lt} and \texttt{eq} are established through the following lemmas (~\vref{sect:comparable-def}). -\vspace{4pt} +% Links between the function \texttt{compare} and the relations +% \texttt{lt} and \texttt{eq} are established through the following lemmas (~\vref{sect:comparable-def}). +% \vspace{4pt} + -\input{movies/snippets/T1/Instances} \paragraph*{\gaiasign} \index{gaiabridge}{Strict order on ordinals below $\epsilon_0$} diff --git a/doc/gaia-chapter.tex b/doc/gaia-chapter.tex index 05574beb..2cd4aa28 100644 --- a/doc/gaia-chapter.tex +++ b/doc/gaia-chapter.tex @@ -121,21 +121,19 @@ \subsubsection{Refinements: Definitions} Functions \texttt{h2g} and \texttt{g2h} allow us to define -a notion of ``data-refinement'' for constants, functions, predicates and relations. The following definitions express that some +a notion of ``data-refinement'' for constants, functions, predicates and relations. The following definitions express that a given constant, function, relation defined in \HydrasLib ``implements'' the same concept of \gaia. - - - - - - +From~\href{../theories/html/gaia_hydras/T1Bridge.html}% +{\texttt{gaia\_hydras.T1Bridge}}. \inputsnippets{T1Bridge/refineDefs} Refinement lemmas can be easily ``reversed''. -\inputsnippets{T1Bridge/refines1R, T1Bridge/refines2R} +\inputsnippets{T1Bridge/refines1R} + +\inputsnippets{T1Bridge/refines2R} \subsection{Examples of refinement} Both of our libraries define constants like $0$, $1$, $\omega$, and arithmetic functions: successor, addition, multiplication, and exponential of base $\omega$ (function $\phi_0$). We prove that these definitions are mutually consistent. Finally, we prove that the boolean predicates `` to be in normal form'' are equivalent. @@ -202,10 +200,10 @@ \subsection{Looking for a lemma} $\alpha \times \beta=\beta$. The following command lists us `gaia's lemmas (thanks to -\gaia's \texttt{cantor\_scope}. +\gaia's \texttt{cantor\_scope}). \inputsnippets{T1Bridge/SearchDemoa} -With \texttt{t1\_scope}: +Within \texttt{t1\_scope}: \inputsnippets{T1Bridge/SearchDemob} \section{Importing Definitions and theorems from \HydrasLib} diff --git a/doc/hydras.tex b/doc/hydras.tex index 4c2ccc8a..375c3980 100644 --- a/doc/hydras.tex +++ b/doc/hydras.tex @@ -556,15 +556,15 @@ \part{Hydras and ordinals} \include{Gamma0-chapter} -\part{Ackermann, G\"{o}del, Peano\,\dots} +%\part{Ackermann, G\"{o}del, Peano\,\dots} -\include{chap-intro-goedel} +%\include{chap-intro-goedel} \include{chapter-primrec} -\include{chapter-fol} -\include{chapter-natural-deduction} -\include{chapter-lnn-lnt} -\include{chapter-encoding} -\include{chapter-expressible} +% \include{chapter-fol} +% \include{chapter-natural-deduction} +% \include{chapter-lnn-lnt} +% \include{chapter-encoding} +% \include{chapter-expressible} \part{A few certified algorithms} diff --git a/doc/schutte-chapter.tex b/doc/schutte-chapter.tex index c083c7ce..a0cddf3b 100644 --- a/doc/schutte-chapter.tex +++ b/doc/schutte-chapter.tex @@ -419,6 +419,7 @@ \subsubsection{Multiplication by a natural number} \input{movies/snippets/Addition/multFin} \section{The exponential of basis \texorpdfstring{$\omega$}{omega}} +\label{sect:AP-and-phi0} In this section, we define the function which maps any $\alpha\in\mathbb{O}$ to the ordinal $\omega^\alpha$, also written @@ -446,6 +447,7 @@ \subsection{Additive principal ordinals} \subsection{The function \texttt{phi0}} + Let us call $\phi_0$ the ordering function of \texttt{AP}. In the mathematical text, we shall use indifferently the notations $\omega^\alpha$ and $\phi_0(\alpha)$. diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v index c9872957..7ac6252c 100644 --- a/theories/ordinals/Epsilon0/T1.v +++ b/theories/ordinals/Epsilon0/T1.v @@ -543,7 +543,7 @@ Fixpoint nf_b (alpha : T1) : bool := (nf_b a && nf_b b && (bool_decide (lt a' a)))%bool end. -Definition nf alpha :Prop := nf_b alpha. +Definition nf alpha :Prop := nf_b alpha. (* end snippet nfDef *) (* begin snippet badTerm *)