Author: Lionel Elie Mamane
Title: Surreal Numbers in Coq
Abstract: 
Surreal (or Conway) Numbers form a totally ordered commutative Field,
containing a copy of the reals and of the ordinals. The natural
presentation of surreal numbers uses an induction-recursion scheme,
which is not available in Coq. However, the original presentation by
Conway explicitly works around needing induction-recursion, too. I
encoded the Ring structure of surreal numbers in Coq. This encoding
relies on Peter Aczel's encoding of set theory in type theory. The
definition of the order, originally a direct inductive definition,
needed to be separated into a mutually inductive definition of "at
most" and "not at least" to satisfy Coq's positivity criterion. The
recursion / induction schemes used in definitions / proofs turned out
to be too subtle for Coq to accept straight away. This development
making use of two different defined equalities, the new "Setoid
Rewriting" code in Coq CVS is of great help.