E0 coercion

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!}
 

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,13 +55,12 @@ \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 other usual definitions of ordinals, for instance in \gaia~\cite{Gaia}, Schütte's book~\cite{schutte}, or larger ordinal notations cf. Chapter~\vref{chap:gamma0}.
 
 \paragraph*{Remark}
 \label{sec:orgheadline65}
 Unless explicitly mentioned, the term ``ordinal" will be used instead of
-``ordinal strictly less than \(\epsilon_0\)" (except in Chapter~\ref{chap:schutte} where it stands for ``countable ordinal'').
+``ordinal strictly less than \(\epsilon_0\)" (except in Chapter~\ref{chap:schutte} where it stands for ``countable ordinal'', and Chapter~\ref{chap:gamma0}.).
 
 
 
@@ -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$}

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}

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}

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)$. 
 

theories/ordinals/Epsilon0/E0.v

@@ -35,6 +35,8 @@ Class E0 : Type := mkord {cnf : T1; cnf_ok : nf cnf}.
 
 Arguments cnf : clear implicits.
 
+Coercion cnf : E0 >-> T1.
+
 #[export] Hint Resolve cnf_ok : E0.
 
 (* end snippet E0Def *)
@@ -66,9 +68,9 @@ Infix "o<=" := E0le : E0_scope.
  Notation _Omega := E0_omega (only parsing).
 
 (* begin snippet SuccOnE0:: no-out *)
-#[global, program] Instance E0_succ (alpha : E0) : E0 :=
+#[export, refine] Instance E0_succ (alpha : E0) : E0 :=
 @mkord (T1.succ (@cnf alpha)) _. 
-Next Obligation.  apply succ_nf, cnf_ok. Defined.
+Proof. apply succ_nf, cnf_ok. Defined.
 (* end snippet SuccOnE0 *)
 
 #[deprecated(note="use E0_succ")]
@@ -85,18 +87,18 @@ Definition E0is_succ (alpha : E0) : bool :=
 #[deprecated(note="use E0is_succ")]
  Notation E0succb := E0is_succ (only parsing).
 
-#[global, program] Instance E0one : E0:= @mkord (T1.succ zero) _.
-Next Obligation. now compute. Defined.
+#[export, refine] Instance E0one : E0:= @mkord (T1.succ zero) _.
+Proof. now compute. Defined.
 
 (* begin snippet plusE0 *)
 
 (*|
 .. coq:: no-out
 |*)
 
-#[global, program] Instance E0add (alpha beta : E0) : E0 :=
+#[export, refine] Instance E0add (alpha beta : E0) : E0 :=
   @mkord (T1add (@cnf alpha) (@cnf beta))_ . 
-Next Obligation.  apply plus_nf; apply cnf_ok. Defined.
+Proof.  apply plus_nf; apply cnf_ok. Defined.
 
 Infix "+" := E0add : E0_scope.
 
@@ -114,25 +116,25 @@ Check E0_omega + E0_omega.
 (* end snippet CheckPlus *)
 
 
-#[global, program] Instance E0_phi0 (alpha: E0) : E0 :=
+#[export, refine] Instance E0_phi0 (alpha: E0) : E0 :=
  @mkord (T1.phi0 (cnf alpha)) _. 
-Next Obligation. apply nf_phi0; apply cnf_ok. Defined.
+Proof. apply nf_phi0; apply cnf_ok. Defined.
 
 Notation "'E0_omega^'" := E0_phi0 (only parsing) : E0_scope.
 
-#[global, program] Instance Omega_term (alpha: E0) (n: nat) : E0 :=
+#[export, refine] Instance Omega_term (alpha: E0) (n: nat) : E0 :=
    @mkord (cons (cnf alpha) n zero) _.
-Next Obligation.  apply nf_phi0; apply cnf_ok. Defined.
+Proof.  apply nf_phi0; apply cnf_ok. Defined.
 
-#[global] Instance Cons (alpha : E0) (n: nat) (beta: E0) : E0
+#[export] Instance Cons (alpha : E0) (n: nat) (beta: E0) : E0
   := (Omega_term alpha n + beta)%e0.                                                          
 
-#[global, program] Instance E0finS (i:nat) : E0:= @mkord (FS i)%t1 _.
-Next Obligation. apply T1.nf_FS. Defined.
+#[export, refine] Instance E0finS (i:nat) : E0:= @mkord (FS i)%t1 _.
+Proof. apply T1.nf_FS. Defined.
 
 
 
-#[global, program] Instance E0fin (i:nat) : E0:=
+#[export] Instance E0fin (i:nat) : E0:=
   match i with
     0 => E0zero
   | S i => E0finS i
@@ -144,18 +146,18 @@ Next Obligation. apply T1.nf_FS. Defined.
 
 Coercion E0fin : nat >-> E0.
 
-#[global, program] Instance E0mul (alpha beta : E0) : E0 :=
+#[export, refine] Instance E0mul (alpha beta : E0) : E0 :=
   @mkord (cnf alpha * cnf beta)%t1 _.
-Next Obligation. apply mult_nf; apply cnf_ok. Defined.
+Proof. apply mult_nf; apply cnf_ok. Defined.
 
 #[deprecated(note="use E0mul")]
  Notation Mult := E0mul (only parsing).
 
 Infix "*" := E0mul : E0_scope.
 
-#[global, program] Instance Mult_i  (alpha: E0) (n: nat) : E0 :=
+#[export, refine] Instance Mult_i  (alpha: E0) (n: nat) : E0 :=
   @mkord (cnf alpha * n)%t1  _.
-Next Obligation.  apply mult_nf_fin, cnf_ok. Defined.
+Proof. apply mult_nf_fin, cnf_ok. Defined.
 
 (** ** Lemmas *)
 
@@ -310,12 +312,12 @@ Definition E0_pred (alpha: E0) : E0 :=
 
 Tactic Notation "mko" constr(alpha) := refine (@mkord alpha eq_refl).
 
-#[global] Instance Two : E0 :=  ltac:(mko (\F 2)).
+#[export] Instance Two : E0 :=  ltac:(mko (\F 2)).
 
-#[global] Instance Omega_2 : E0 :=ltac:(mko (T1omega * T1omega)%t1).
+#[export] Instance Omega_2 : E0 :=ltac:(mko (T1omega * T1omega)%t1).
 
 
-#[global] Instance E0_sto : StrictOrder E0lt.
+#[export] Instance E0_sto : StrictOrder E0lt.
 Proof.
   split.
   - intro x ; destruct x; unfold E0lt; red.
@@ -324,7 +326,7 @@ Proof.
     apply LT_trans.
  Qed.
 
-#[ global ] Instance compare_E0 : Compare E0 :=
+#[ export ] Instance compare_E0 : Compare E0 :=
  fun (alpha beta:E0) => compare (cnf alpha) (cnf beta).
 
 Lemma compare_correct (alpha beta : E0) :
@@ -495,10 +497,10 @@ Qed.
 .. coq:: no-out
  *)
 
-#[global] Instance E0_comp: Comparable E0lt compare.
+#[export] Instance E0_comp: Comparable E0lt compare.
 Proof. split; [apply E0_sto | apply compare_correct]. Qed.
 
-#[global] Instance Epsilon0 : ON E0lt compare.
+#[export] Instance Epsilon0 : ON E0lt compare.
 Proof. split; [apply E0_comp | apply E0lt_wf]. Qed.
 
 (*||*)
@@ -668,13 +670,13 @@ Proof.
 Qed.
 
 
-#[global, program] Instance Oplus (alpha beta : E0) : E0 :=
+#[export, refine] Instance Oplus (alpha beta : E0) : E0 :=
 @mkord (oplus (cnf alpha) (cnf beta)) _.
-Next Obligation. apply oplus_nf; apply cnf_ok. Defined.
+Proof. apply oplus_nf; apply cnf_ok. Defined.
 
 Infix "O+" := Oplus (at level 50, left associativity): E0_scope.
 
-#[global] Instance Oplus_assoc : Assoc eq Oplus.
+#[export] Instance Oplus_assoc : Assoc eq Oplus.
 Proof. 
  red;  destruct x,y, z. unfold Oplus.  cbn.
   apply E0_eq_intro; cbn; now rewrite oplus_assoc.
@@ -812,7 +814,7 @@ Proof.
 Qed.
 
 
-#[global] Instance plus_assoc : Assoc eq E0add . 
+#[export] Instance plus_assoc : Assoc eq E0add . 
 Proof.
   intros alpha beta gamma; destruct alpha, beta, gamma; apply E0_eq_intro; cbn;
   apply  T1.T1addA.

theories/ordinals/Epsilon0/T1.v

@@ -543,7 +543,8 @@ 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.
+(** For compatibility with the Ensembles library *)
+Definition nf alpha : Prop := nf_b alpha. 
 (* end snippet nfDef *)
 
 (* begin snippet badTerm *)