revision book (<= p. 61)

doc/ordinal-chapter.tex

@@ -148,7 +148,7 @@ \section{Ordinal Notations}
 \end{itemize}
 
 
-Such a structure may be proved correct relatively to a bigger ordinal notation or to Schütte's or \gaia's model.
+Such a structure should be proved correct relatively to a bigger ordinal notation or to Schütte's or \gaia's model.
 
 
 
@@ -159,9 +159,9 @@ \subsection{Classes for ordinal notations}
 From the \coq{} user's point of view, an ordinal notation is
 a structure allowing to compare two ordinals by computation, and proving by well-founded induction.
 
-\subsubsection{The \texttt{Comparison} and \texttt{Comparable} classes}
+\subsubsection{The \texttt{Comparable} class}
 
-We use the operational class \texttt{Comparison} of comparison functions to define the \texttt{Comparable} class, contributed by Jérémy Damour and Théo Zimmermann, which allows us to apply generic lemmas and tactics about decidable strict orders.
+The \texttt{Comparable} class, contributed by Jérémy Damour and Théo Zimmermann, allows us to apply generic lemmas and tactics about decidable strict orders.
 The correctness of the comparison function is expressed through Stdlib's type 
 \texttt{Datatypes.CompareSpec} as specialized by \texttt{Datatypes.CompSpec}.
 
@@ -213,7 +213,7 @@ \subsubsection{The \texttt{ON} class}
 \inputsnippets{ON_Generic/ONDefsb}
 
 \begin{remark}
-The infix notations \texttt{o<} and \texttt{o<=} are defined in order to make apparent the distinction between the various notation scopes that may co-exist in a same statement. So the infix \texttt{<} and \texttt{<=} are reserved to the natural numbers. In the mathematical formulas, however, we still use $<$ and $\leq$ for comparing ordinals.
+The infix notations \texttt{o<} and \texttt{o<=} are defined in order to make apparent the distinction between the various notation scopes that may co-exist in a same statement. So the infix \texttt{<} and \texttt{<=} are reserved to the natural numbers. In mathematical formulas, however, we still use $<$ and $\leq$ for inequalities between ordinals.
 \end{remark}
 
 
@@ -250,7 +250,8 @@ \section{Example: the ordinal \texorpdfstring{$\omega$}{omega}}
 \vspace{4pt}
 \noindent\emph{From Library~\href{../theories/html/hydras.OrdinalNotations.ON_Omega.html}{OrdinalNotations.ON\_Omega}}
 
-\inputsnippets{ON_Omega/OmegaDefa, ON_Omega/OmegaDefb}
+\inputsnippets{ON_Omega/OmegaDefa}
+\inputsnippets{ON_Omega/OmegaDefb}
 
 
 \section{Sum of  two ordinal notations}
@@ -409,7 +410,7 @@ \subsection{Definitions}
 \begin{itemize}
 \item A \emph{least} element is a minorant (in the large sense) of the full set  on $A$,
 \item $y$ is a \emph{successor} of $x$ if $x<y$ and there is no element between $x$ and $y$. We will also say that $x$ is a \emph{predecessor} of $y$.
-\item $x$ is a \emph{limit} if $x$ is not a least element, and for any $y$ such that $yo<x$,
+\item $x$ is a \emph{limit} if $x$ is not a least element, and for any $y$ such that $y<x$,
  there exists some $z$ such that $y<z<x$.
 \end{itemize}
 
@@ -502,7 +503,7 @@ \section{The ordinal \texorpdfstring{$\omega^2$}{omega2}}
 \inputsnippets{ON_Omega2/Omega2Def, ON_Omega2/Defs}
 \inputsnippets{ON_Omega2/Ex1}
 
-\subsection{Arithmetic of \texorpdfstring{$\omega^2$}{omega^2}} 
+\subsection{Arithmetic on \texorpdfstring{$\omega^2$}{omega^2}} 
 
 \subsubsection{Successor}
 
@@ -525,7 +526,7 @@ \subsubsection{Addition}
 \inputsnippets{ON_Omega2/plusDef, ON_Omega2/plusExamples}
 
 
-\subsubsection{Multiplication}
+\subsubsection{Finite multiplication}
 
 The restriction of ordinal multiplication to the segment $[0,\omega^2)$ is not a total function.
 For instance $\omega\times\omega= \omega^2$ is outside the set of represented values.
@@ -696,7 +697,7 @@ \subsubsection{Proof of the inequality \texttt{m big\_h o<= m small\_h} }
 \input{movies/snippets/Omega2_Small/mGe}
 
 
-A case analysis on $i$ and $j$ allows us to
+A case analysis on $i$ and $j$ leads  us to
 consider three cases :
 
 \begin{itemize}
@@ -817,7 +818,7 @@ \subsubsection{Examples}
 
 \subsubsection{Comparison function}
 
-In order to build an instance of \texttt{ON}, we define a comparison function,  and prove its correctiness.
+In order to build an instance of \texttt{ON}, we define a comparison function, then prove its correctness.
 
 \vspace{4pt}
 
@@ -852,7 +853,7 @@ \subsubsection{Comparison function}
 
 Thus unicity of proofs of \texttt{Nat.ltb x0 (S n)}  comes from the decidability of
 equality on type \texttt{bool}.
-This is why we used the boolean function \texttt{Nat.ltb} instead of the inductive predicate \texttt{Nat.lt} in the definition of type \texttt{t $n$} (see page~\pageref{def: Finite-ord-type}).
+This is why we used the boolean function \texttt{Nat.ltb} instead of the inductive predicate \texttt{Nat.lt} in the definition of type \texttt{t $n$} (see page~\pageref{def:Finite-ord-type}).
 For more information about this pattern, please look at the numerous mailing lists and 
 FAQs on \coq{}).
 
@@ -896,7 +897,7 @@ \subsubsection{Building an instance of \texttt{ON}}
 
 \section{See also \dots}
 
-Finite ordinals are also formalized in \ssreflect/\mathcomp~\cite{MCB}. In Module~\href{../theories/html/gaia_hydras.ON_gfinite.html}{gaia\_hydras.ON\_gfinite}, we build an instance of class \texttt{ON}.
+\gaiasign Finite ordinals are also formalized in \ssreflect/\mathcomp~\cite{MCB}. In Module~\href{../theories/html/gaia_hydras.ON_gfinite.html}{gaia\_hydras.ON\_gfinite}, we build an instance of class \texttt{ON}.
 
 \inputsnippets{ON_gfinite/finordLtDef, ON_gfinite/finordON}
 
@@ -918,20 +919,20 @@ \section{Comparing two ordinal notations}
 It is sometimes useful to compare two ordinal notations with respect to expressive power
 (the segment of ordinals  they represent). 
 
-The following class specifies a strict inclusion of segments. The notation \texttt{OA} describes a segment $[0,\alpha)$, and \texttt{OB} is a larger segment (which contains a notation for $\alpha$, whilst $\alpha$ is not represented in \texttt{OA}). We require also  that the comparison functions of the two notation systems are compatible.
+The following class specifies a strict inclusion of segments. The ordinal notation \texttt{OA} describes a segment $[0,\alpha)$, and \texttt{OB}  a larger segment (which contains a notation for $\alpha$, whilst $\alpha$ is not represented in \texttt{OA}) (like in Fig.~\ref{fig:subsegment}). We require also the comparison functions of the two notation systems to be compatible.
 
 \begin{figure}[h]
    \centering
    \begin{tikzpicture}[very thick, scale=0.6]
 \begin{scope}[color=blue]
-\node (A) at (0,0) {$A$};
+\node (A) at (0,0) {$\omega$};
 \node(A0) at (2,0)[label=below:$0$]{$\bullet$};
 \node(A1) at (3,0)[label=below:$1$]{$\bullet$};
 \node(A2) at (4,0)[label=below:$2$]{$\bullet$};
 \node (Adots) at (6,0) {$\ldots$};
 \end{scope}
 \begin{scope}[color=red]
-\node (B) at (0,2) {$B$};
+\node (B)  at (0,2) {$\omega+\omega$};
 \node(B0) at (2,2)[label=above:$0$]{$\bullet$};
 \node(B1) at (3,2)[label=above:$1$]{$\bullet$};
 \node(B2) at (4,2)[label=above:$2$]{$\bullet$};
@@ -947,7 +948,7 @@ \section{Comparing two ordinal notations}
 \draw [->,thin] (Adots) -- node [auto] {$\iota$} (Bdots);
 \end{scope}
 \end{tikzpicture}
-   \caption{\textcolor{blue}{$A$} is a sub-segment  of \textcolor{red}{$B$}}
+   \caption{\textcolor{blue}{$\omega$} is a sub-segment  of \textcolor{red}{$\omega+\omega$}}
    \label{fig:subsegment}
  \end{figure}
 

theories/ordinals/Hydra/Omega2_Small.v

@@ -103,9 +103,7 @@ Section Impossibility_Proof.
 |*)
 
   Corollary m_lt : m small_h o< m big_h.
-  Proof.
-    apply m_strict_mono with (1:=Hvar) (2:=big_to_small) .  
-  Qed.
+  Proof. apply m_strict_mono with (1:=Hvar) (2:=big_to_small). Qed.
   (*||*)
 
   (* end snippet mLt *)

theories/ordinals/OrdinalNotations/ON_Generic.v

@@ -33,27 +33,22 @@ Section Definitions.
 
   Context {A:Type} {lt : relation A} {cmp : Compare A} {on: ON lt cmp}.
 
-  #[using="All"]
-   Definition ON_t := A.
+  #[using="All"] Definition ON_t := A.
 
-  #[using="All"]
-   Definition ON_compare : A -> A -> comparison := compare.
+  #[using="All"] Definition ON_compare : A -> A -> comparison := compare.
 
-  #[using="All"]
-   Definition ON_lt := lt.
+  #[using="All"] Definition ON_lt := lt.
 
-  #[using="All"]
-   Definition ON_le:  relation A := leq lt.
+  #[using="All"] Definition ON_le:  relation A := leq lt.
 
   #[using="All"]
-   Definition measure_lt {B : Type} (m : B -> A) : relation B :=
+    Definition measure_lt {B : Type} (m : B -> A) : relation B :=
     fun x y =>  ON_lt (m x) (m y).
 
   #[using="All"]
-   Lemma wf_measure {B : Type} (m : B -> A) :
+    Lemma wf_measure {B : Type} (m : B -> A) :
     well_founded (measure_lt m).
 (* end snippet ONDefsa *)
-
   Proof.
     intro x; eapply Acc_incl  with (fun x y =>  ON_lt (m x) (m  y)).
     - intros y z H; apply H.
@@ -96,11 +91,9 @@ Class  SubON
        (iota: A -> B):=
   {
   SubON_compare: forall x y : A,
-      compareB (iota x) (iota y) =
-      compareA x y;
+      compareB (iota x) (iota y) = compareA x y;
   SubON_incl : forall x, ltB (iota x) alpha;
-  SubON_onto : forall y,
-      ltB y alpha  -> exists x:A, iota x = y}.
+  SubON_onto : forall y, ltB y alpha  -> exists x:A, iota x = y}.
 
 (* end snippet SubONDef *)
 
@@ -134,7 +127,7 @@ Class ON_correct `(alpha : Ord)
                                 exists b, iota b = beta;
     On_compare_spec : forall a b:A,
         match compareA a b with
-          Datatypes.Lt => lt (iota a) (iota b)
+        | Datatypes.Lt => lt (iota a) (iota b)
         | Datatypes.Eq => iota a = iota b
         | Datatypes.Gt => lt (iota b) (iota a)
         end

theories/ordinals/OrdinalNotations/ON_Omega.v

@@ -12,16 +12,14 @@ Import Relations RelationClasses.
 Instance compare_nat : Compare nat := Nat.compare.
 
 (* begin snippet OmegaDefa:: no-out *)
-#[global]
- Instance Omega_comp : Comparable Peano.lt compare_nat.
+#[global] Instance Omega_comp : Comparable Peano.lt compare_nat.
 Proof.
   split.
   - apply Nat.lt_strorder.
   - apply Nat.compare_spec.
 Qed.
 
-#[global]
- Instance Omega : ON Peano.lt compare_nat.
+#[global] Instance Omega : ON Peano.lt compare_nat.
 Proof.
  split.
  - apply Omega_comp.

theories/ordinals/OrdinalNotations/ON_Omega2.v

@@ -575,7 +575,7 @@ Section Merge.
             {wf (measure_lt m) xys} :
     list A :=
     match xys with
-      (nil, ys) => ys
+    | (nil, ys) => ys
     | (xs, nil) => xs
     | (x :: xs, y :: ys) =>
       if ltb x y then x :: merge  ltb (xs, (y :: ys))

theories/ordinals/Prelude/Comparable.v

@@ -28,15 +28,13 @@ Section Comparable.
    Notation lt_irrefl := StrictOrder_Irreflexive (only parsing).
 
   (* Relation Lt *)
-  Lemma lt_not_gt (a b: A):
-    lt a b -> ~lt b a.
+  Lemma lt_not_gt (a b: A): lt a b -> ~lt b a.
   Proof.
     intros Hlt Hgt.
     apply StrictOrder_Irreflexive with a; now transitivity b.
   Qed.
 
-  Lemma lt_not_ge (a b: A):
-    lt a b -> ~ le b a.
+  Lemma lt_not_ge (a b: A): lt a b -> ~ le b a.
   Proof.
     intros Hlt Hle.
     apply le_lt_eq in Hle as [Hgt | Heq].
@@ -61,15 +59,13 @@ Section Comparable.
     now transitivity b. 
   Qed.
 
-  Lemma compare_lt_irrefl (a: A):
-    ~compare a a = Lt.
+  Lemma compare_lt_irrefl (a: A): ~compare a a = Lt.
   Proof.
     intro H.
     now apply compare_lt_iff, StrictOrder_Irreflexive in H.
   Qed.
 
-  Lemma compare_eq_iff (a b: A):
-    compare a b = Eq <-> a = b.
+  Lemma compare_eq_iff (a b: A): compare a b = Eq <-> a = b.
   Proof.
     pose proof (comparable_comp_spec a b) as [Heq | H | H];
     split; intro; subst; try easy;