Small corrections in Chapter 3

doc/hydra-chapter.tex

@@ -846,7 +846,7 @@ \subsection{Big steps}
 
 \input{movies/snippets/Hydra_Definitions/battleRelDef}
 
-The following property allows us to build battle rounds by composition of smaller ones.
+The following property allows us to build battles by composition of smaller ones.
 
 %% TODO display subgoals when fixed
 

doc/ordinal-chapter.tex

@@ -46,8 +46,7 @@ \chapter{Introduction to ordinal numbers and ordinal notations}
 \item Dots : ``$\ldots$'' stand for  infinite sequences of ordinals, not shown for lack of space. For instance, the ordinal $42$ is not shown in the first line, but it exists, somewhere between $17$ and $\omega$.
 \item Each ordinal printed in black is the immediate successor of another ordinal. We call it a \emph{successor} ordinal. For instance, $12$ is the successor of $11$, and $\omega^4+1$ the successor of $\omega^4$.
 \item Ordinals (displayed in red)  that  follow immediately dots are called \emph{limit ordinals}. With respect to the order induced by this sequence, any limit ordinal $\alpha$ is the least upper bound of  the set $\mathbb{O}_\alpha$ of all ordinals strictly less than $\alpha$.
-\item
-For instance $\omega$ is the least upper bound of the set of all finite ordinals (in the first line). It is also the first limit ordinal, and the first infinite ordinal, in the sense that 
+For instance,$\omega$ is the least upper bound of the set of all finite ordinals (in the first line). It is also the first limit ordinal, and the first \emph{infinite ordinal number}, in the sense that 
 the set $\mathbb{O}_\omega$ is infinite.
 \item The ordinal $\epsilon_0$ is the first number which is equal to its own exponential of base $\omega$. It plays an important role in proof theory, and is particularly studied in chapters~\ref{chap:T1} to \ref{chap:alpha-large}.
 \item Any ordinal is  either the ordinal \textcolor{blue}{$0$},
@@ -59,6 +58,15 @@ \chapter{Introduction to ordinal numbers and ordinal notations}
 
 \section{The mathematical point of view}
 
+
+
+We cannot cite all the literature published on ordinals since Cantor's book
+\cite{cantorbook}, and 
+leave it to the reader to explore the bibliography.
+The introduction of Jos\'e Grimm's report~\cite{grimm:hal-00911710} contains also a nice presentation of the main properties of ordinals.
+
+For simplicity's sake, we will only give the definitions which are useful for understanding our \coq development.
+
 \subsection{Well-ordered sets}
 Let us start with some definitions.
 A  \emph{well-ordered set} is a set provided with a binary relation $<$ which has the following properties.
@@ -88,21 +96,15 @@ \subsection{Ordinal numbers}
 there exists a strictly monotonous bijection $b$ from $A$ to $B$, \emph{i.e.} which verifies the proposition
 $\forall x\,y\in A,\, x <_A y \Rightarrow b(x) <_B  b(y)$.
 
-Having the same order type is an equivalence relation between well-ordered sets. Ordinal numbers (in short: \emph{ordinals})  are descriptions (\emph{names}) of the equivalence classes.
+Having the same order type is an equivalence relation between well-ordered sets. Ordinal numbers (in short: \emph{ordinals})  are descriptions (\emph{names}) of the associated equivalence classes.
 For instance, the order type of $(\mathbb{N},<)$ is associated with the ordinal called  $\omega$, and the order we considered on 
-the disjoint union of $\mathbb{N}$ and itself is named $\omega+\omega$.
+the disjoint union of two copies of $\mathbb{N}$ is associated with  $\omega \times 2$ (a.k.a. $\omega+\omega$).
 
 In a set-theoretic framework, one can consider any ordinal $\alpha$ as a well-ordered set, whose  elements are just the ordinals strictly less than $\alpha$, \emph{i.e.} the \emph{segment} $\mathbb{O}_\alpha=[0, \alpha)$. So, one can speak about \emph{finite}, \emph{infinite}, \emph{countable}, etc., ordinals. Nevertheless, since we work within type theory, 
 we do not identify ordinals as sets of ordinals, but consider the correspondence between ordinals and sets of ordinals as the function that maps $\alpha$ to $\mathbb{O}_\alpha$.
 For instance $\mathbb{O}_\omega=\mathbb{N}$, and $\mathbb{O}_7=\{0,1,2,3,4,5,6\}$.
 
 
-We cannot cite all the literature published on ordinals since Cantor's book
-\cite{cantorbook}, and 
-leave it to the reader to explore the bibliography.
-
-The introduction of Jos\'e Grimm's report~\cite{grimm:hal-00911710} contains a nice presentation of the main properties of ordinals.
-
 
 \section{Ordinal numbers in Coq}
 
@@ -139,7 +141,7 @@ \section{Ordinal Notations}
 Fortunately, the ordinals we need for  studying hydra battles are much simpler than Schütte's, and can be represented as quite simple data types in \gallina. 
 
 Let $\alpha$ be some (countable) ordinal; 
-in \coq{} terms, we call \emph{ordinal notation for $\alpha$} a structure composed 
+we call \emph{ordinal notation for $\alpha$} any structure composed 
 of:
 \begin{itemize}
 \item A data type $A$ for representing all ordinals strictly below $\alpha$,
@@ -163,7 +165,7 @@ \subsubsection{The \texttt{Comparable} class}
 
 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}.
+\texttt{Datatypes.CompareSpec} and predicate \texttt{Datatypes.CompSpec}.
 
 \begin{Coqsrc}
   Inductive CompareSpec (Peq Plt Pgt : Prop) :
@@ -291,13 +293,16 @@ \section{Sum of  two ordinal notations}
 Standard library's lemma \texttt{Wellfounded.Disjoint\_Union.wf\_disjoint\_sum} 
 is applied  to prove that our order \texttt{lt} is well-founded, allowing us to build an instance of \texttt{ON}:
 
-\inputsnippets{ON_plus/ltWf, ON_plus/OnPlus}
+\inputsnippets{ON_plus/ltWf}
 
-\subsection{The ordinal \texorpdfstring{$\omega+\omega$}{omega + omega}}
+\inputsnippets{ON_plus/OnPlus}
+
+\subsection{Example: The ordinal \texorpdfstring{$\omega+\omega$}{omega + omega}}
 
 The ordinal $\omega+\omega$ (also known as $\omega\times 2$) may be represented as the concatenation 
 of two copies of $\omega$ (Figure~\ref{fig:omega-plus-omega}).
 It is also represented by the two first lines of Figure~\ref{fig:ordinal-sequence}.
+We define this notation in \coq{} as an instance of \texttt{ON\_plus}.
 
 \begin{figure}[h]
    \centering
@@ -324,7 +329,7 @@ \subsection{The ordinal \texorpdfstring{$\omega+\omega$}{omega + omega}}
    \label{fig:omega-plus-omega}
  \end{figure}
 
-We can define this notation in \coq{} as an instance of \texttt{ON\_plus}.
+
 
 
 \vspace{4pt}
@@ -523,7 +528,9 @@ \subsubsection{Addition}
 
 We can define on \texttt{Omega2} an addition which extends the addition on \texttt{nat}. Please note that this operation is not commutative:
 
-\inputsnippets{ON_Omega2/plusDef, ON_Omega2/plusExamples}
+\inputsnippets{ON_Omega2/plusDef}
+
+\inputsnippets{ON_Omega2/plusExamples}
 
 
 \subsubsection{Finite multiplication}

theories/ordinals/Hydra/Hydra_Definitions.v

@@ -497,7 +497,7 @@ Class Hvariant {A:Type}{Lt:relation A}
       (Wf: well_founded Lt)(B : Battle)
       (m: Hydra -> A): Prop :=
   {variant_decr: forall i h h',
-      h <> head -> battle_rel B i  h h' -> Lt (m h') (m h)}.
+      h <> head -> battle_rel B i h h' -> Lt (m h') (m h)}.
 
 (* end snippet HvariantDef *)
 

theories/ordinals/Hydra/Hydra_Lemmas.v

@@ -206,10 +206,10 @@ Qed.
 (** ** Properties of [battle] *)
 
 (* begin snippet battleTrans *)
-Lemma rounds_trans {b:Battle} :
-  forall i h j h', rounds b i h j h' ->
-                   forall k h0,  rounds b k h0 i h ->
-                                 rounds b k h0 j h'. (* .no-out *)
+Lemma rounds_trans {B:Battle} :
+  forall i h j h', rounds B i h j h' ->
+                   forall k h0,  rounds B k h0 i h ->
+                                 rounds B k h0 j h'. (* .no-out *)
 (*| .. coq:: no-out |*)
 Proof. 
   intros i h j h' H k h0. induction 1 /dr. 

theories/ordinals/Hydra/Omega2_Small.v

@@ -21,7 +21,7 @@ Section Impossibility_Proof.
 
   Variable m : Hydra -> ON_Omega2.t.
   Context
-    (Hvar: @Hvariant _ _ (ON_Generic.ON_wf (ON:=Omega2)) free m).
+    (Hvar: Hvariant (ON_Generic.ON_wf (ON:=Omega2)) free m).
 
   (* end snippet Impossibilitya *)
 

theories/ordinals/OrdinalNotations/ON_Finite.v

@@ -43,7 +43,7 @@ Abort.
 
 (* begin snippet compareDef:: no-out *)
 
-#[global] Instance compare_t {n:nat} : Compare (t n) :=
+#[global] Instance compare_fin {n:nat} : Compare (t n) :=
   fun (alpha beta : t n) => Nat.compare (proj1_sig alpha) (proj1_sig beta).
 
 Lemma compare_correct {n} (alpha beta : t n) :

theories/ordinals/OrdinalNotations/ON_Generic.v

@@ -26,6 +26,7 @@ Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   ON_comp :> Comparable lt cmp;
   ON_wf : well_founded lt;
   }.
+#[global] Existing Instance ON_comp.
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)
@@ -333,3 +334,5 @@ End SubON_properties.
 
 
 
+
+

theories/ordinals/OrdinalNotations/ON_O.v

@@ -31,15 +31,15 @@ Definition le {a:A} : relation (t a) :=
   clos_refl (t a) lt.
 
 #[global]
-Instance compare_t {a:A} : Compare (t a) :=
+Instance compare_O {a:A} : Compare (t a) :=
 fun (alpha beta : t a) =>
   compare (proj1_sig alpha) (proj1_sig beta).
 
 Lemma compare_correct {a} (alpha beta : t a) :
   CompSpec eq lt alpha beta (compare alpha beta).
 Proof.
  unfold CompSpec, compare.
-  - destruct alpha, beta; unfold compare,compare_t; cbn.
+  - destruct alpha, beta; unfold compare,compare_O; cbn.
     case_eq (compare x x0); unfold lt; cbn.
     + constructor 1.
       destruct (comparable_comp_spec x x0); try discriminate.

theories/ordinals/OrdinalNotations/ON_Omega2.v

@@ -13,10 +13,10 @@ Open Scope ON_scope.
 
 (* begin snippet Omega2Def:: no-out *)
 
-#[ global ] Instance compare_nat_nat : Compare t :=
- compare_t compare_nat compare_nat.
+#[ global ] Instance compare_omega2 : Compare ON_mult.t :=
+ compare_mult compare_nat compare_nat.
 
-#[ global ] Instance Omega2: ON _ compare_nat_nat := ON_mult Omega Omega.
+#[ global ] Instance Omega2: ON _ compare_omega2 := ON_mult Omega Omega.
 
 Definition t := ON_t.
 (* end snippet Omega2Def *)
@@ -89,6 +89,7 @@ Qed.
 
 Lemma lt_succ_le alpha beta :
   alpha o< beta <-> succ alpha o<= beta. (* .no-out *)
+(* ... *)
 (*|
 .. coq:: none
 |*)
@@ -241,6 +242,7 @@ Qed.
 
 Lemma succ_ok alpha beta :
   Successor beta alpha <-> beta = succ alpha. (* .no-out *)
+(* ... *)
 (*|
 .. coq:: none 
 |*)
@@ -380,9 +382,8 @@ Infix "+" := plus : ON_scope.
 
 Lemma plus_compat (n p: nat) :
   fin  (n + p )%nat =  fin n + fin p. (* .no-out *)
-Proof. (* .no-out *)
-  destruct n; now cbn. 
-Qed.
+Proof. (* .no-out *) destruct n; reflexivity. Qed.
+
 (* end snippet plusDef *)
 
 
@@ -391,12 +392,10 @@ Qed.
 Compute 3 + omega.
 
 Compute omega + 3.
-(* end snippet plusExamples *)
-
-
-Example non_commutativity_of_plus :  omega + 3 <> 3 + omega. 
-Proof.  discriminate. Qed.
 
+Example non_commutativity_of_plus: omega + 3 <> 3 + omega. (* .no-out *)
+Proof.  (* .no-out *) discriminate. Qed.
+(* end snippet plusExamples *)
 
 (* begin snippet multFinDef *)
 
@@ -436,16 +435,14 @@ Proof. reflexivity. Qed.
 
 #[global] Instance plus_assoc: Assoc eq  plus. 
 Proof.
-  intros alpha beta gamma; destruct alpha, beta, gamma.
+  intros (n,n0) (n1, n2) (n3,n4); cbn. 
   destruct n,  n0, n1, n2, n3, n4; cbn; auto; f_equal; abstract lia.
 Qed.
 
-
 Lemma succ_is_plus_1  alpha : alpha + 1 = succ alpha.
 Proof.
- unfold succ ;
-simpl; 
- destruct alpha; cbn; destruct n, n0; try f_equal; abstract lia.
+ unfold succ ; cbn; destruct alpha; cbn; destruct n, n0; 
+   try f_equal; abstract lia.
 Qed.
 
 Lemma lt_omega alpha : alpha o< omega <-> exists n:nat,  alpha = fin n.

theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v

@@ -15,15 +15,17 @@ Open Scope opo_scope.
 (* begin snippet OmegaPlusOmegaDef:: no-out *)
 
 #[global] Instance compare_nat_nat : Compare t :=
- compare_t compare_nat compare_nat.
+ compare_plus compare_nat compare_nat.
 
 #[global] Instance Omega_plus_Omega: ON _ compare_nat_nat :=
  ON_plus Omega Omega.
 
 Definition t := ON_t.
 
-Example ex1 : inl 7 o< inr 0. 
-Proof. now apply compare_lt_iff. Qed.
+Compute inl 42 o?= inr 0.
+
+Example ex1 : inl 7 o< inr 8. 
+Proof. apply compare_lt_iff. trivial. Qed.
 
 (* end snippet OmegaPlusOmegaDef *)
 

theories/ordinals/OrdinalNotations/ON_mult.v

@@ -35,7 +35,7 @@ Section Defs.
   Definition lt : relation t := lexico ltB ltA.
   Definition le := clos_refl _ lt. 
 
-  #[global] Instance compare_t : Compare t :=
+  #[global] Instance compare_mult : Compare t :=
     fun (alpha beta: t) =>
     match compare (fst alpha) (fst beta) with
     | Eq => compare (snd alpha) (snd beta)
@@ -66,7 +66,7 @@ Section Defs.
     | Gt => lt beta  alpha
     end.
   Proof.
-    destruct alpha, beta; cbn. unfold compare, compare_t; cbn.
+    destruct alpha, beta; cbn. unfold compare, compare_mult; cbn.
     destruct (comparable_comp_spec b b0).
     - subst; destruct (comparable_comp_spec a a0).
       + now subst.
@@ -86,25 +86,23 @@ Section Defs.
 
   (* begin snippet multComp:: no-out *)
 
-  #[global] Instance mult_comp:  Comparable lt compare_t.
-  (* end snippet multComp *)
-
-  Proof.
+  #[global] Instance mult_comp:  Comparable lt compare_mult.
+   Proof.
     split.
     - apply lt_strorder.
     - apply compare_correct.
   Qed. 
+  (* end snippet multComp *)
 
-  (* begin snippet ONMult:: no-out *)
-  #[global] Instance ON_mult: ON lt compare_t.
-  (* end snippet ONMult *)
 
-  Proof.
-    split.
+  (* begin snippet ONMult:: no-out *)
+  #[global] Instance ON_mult: ON lt compare_mult. 
+  Proof. 
+    split. 
     - apply mult_comp.
     - apply lt_wf.
   Qed.
-
+  (* end snippet ONMult *)
 
   Lemma lt_eq_lt_dec alpha beta :
     {lt alpha  beta} + {alpha = beta} + {lt beta alpha}.