The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Tue, Sep 07, 2004 at 10:36:43AM +0200, 
casteran AT labri.fr
 wrote:

>   I am looking for any development in Coq allowing to work with
> ordinal numbers.

I looked for it two years ago and didn't find much. The only concrete
thing I found was section 1.6.1 of
http://pauillac.inria.fr/cdrom/projs/logical/dea/cours1.v.html, which
does not give you all what you want. It is also mentioned again in
section 3.3.1 of
http://pauillac.inria.fr/cdrom/projs/logical/dea/cours3.v.html.


Now, my Master's thesis was about making a Coq development of
something that includes the ordinals, namely Conway Numbers (or
Surreal Numbers) and more generally Conway Games. And I *do* have a
Coq type that (I claim) represents Conway Games, so it is (I claim)
theoretically possible to have ordinals in Coq.

(Surreal Numbers: a collection that includes ordinals and reals, in a
 totally ordered commutative Field structure.)

I don't think that seeing ordinals as a sub-collection of Conway Games
will be anywhere near practical for the things I imagine you want to
do with ordinals; I presume you want to do things around well-founded
induction principles.


Depending on how concrete you want to really get, it might pay off to
"slaughter down" my Conway Games type down to something that would
make acceptable ordinals. I'm thinking of something along the lines
of:

Inductive Ord : Type :=
 Ord_cons : (I:Type) (I -> Ord) -> Ord.

and interpreting Ord_cons as ($\suc$ is successor):

\begin{displaymath}
  \text{Ord_cons} I f := \lim_{i\in I} (\suc (f i))
\end{displaymath}


(You probably don't want to "slaughter down" the operations defined
 over Conway games/numbers to this type, they won't give you what you
 expect: Conway Games addition restricted to ordinals is not the
 ordinal addition.)


For rather theoretical developments, this may be "practical" enough,
but if you want to actually build concrete ordinals, note that you
will need "big enough" index types: To construct an ordinal o, you
need a type whose ordinality is at least o. So, in some sense, to
construct an ordinal (in the type Ord), you already need that ordinal
(in another form) or a bigger one (still in another form).


If in spite of all what I said, you want to take a look at my Master's
thesis, take a look at http://www.mamane.lu/concoq/ . The code is Coq
7.4 and a bit messy. I intend to "upgrade" it to Coq 8.0 and clean it
up in October / November and then submit it to Coq contribs.


Best Regards,

-- 
Lionel