History

The C-CoRN repository grew out of the FTA project, where a constructive proof of the Fundamental Theorem of Algebra was formalized in Coq. This theorem states that every non-constant polynomial f over the complex numbers has a root, i.e. there is a complex number z such that f(z) = 0. The FTA project was performed by Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack, Milad Niqui, and Henk Barendregt. The motivations for starting this project were the following

The proof did not proceed by constructing the reals in Coq, but by axiomatic reasoning. So the axioms of the real numbers were defined in Coq. As a matter of fact, we have proceeded even more generally by first defining an algebraic hierarchy (semi-groups, monoids, groups, rings, fields, ordered fields); see {GeuversPollackWiedijkZwanenburg-JSC-2002}. The advantages of this approach are: reuse of proven results and reuse of notation. (The reals and complex numbers are fields and the polynomials form a ring.) Then IR was defined to be an (arbitrary) Cauchy-complete Archimedean ordered field. Given such an IR, the complex numbers can be defined by CC := IR x IR. To make sure that the axioms for IR make sense, a concrete instantiation for IR has been constructed by Niqui.
Completely formalized in the theorem prover Coq, the proof and theory development amounts to the following. This is the size of the input files (definitions, lemmas, tactic scripts) To modularize the proof and in order to create a real ``library'', we have first defined an algebraic hierarchy in the FTA project. In proving FTA, we have to deal with real numbers, complex numbers and polynomials and many of the properties we use are generic and algebraic. To be able to reuse results (also for future developments) we have defined a hierarchy of algebraic structures. The basic level consists of constructive setoids, (A, #, =), with A: Set, # an apartness and = an equivalence relation. (Classically, apartness is just the negation of equality, but constructively, apartness is more `primitive' than equality and equality is usually defined as the negation of apartness. To understand this, think of two reals x and y as (infinite) Cauchy sequences: we may determine in a finite amount of time whether x # y, but we can in general never know in a finite amount of time that x=y.) On the next level we have semi-groups, (S, +), with S a setoid and + an associative binary operation on S.

Inside the algebraic hierarchy we have `inheritance via coercions'. We have the following coercions.
OrdField >-> Field >-> Ring >-> Group Group >-> Monoid >-> Semi_grp >-> Setoid
This means that all properties of groups are inherited by rings, fields, etc. Also notation is inherited: x[+]y denotes the addition of x and y for x,y:G from any semi-group (or monoid, group, ring,...) G. The coercions must form a tree, so there is no real multiple inheritance, e.g. it is not possible to define rings in such a way that it inherits both from its additive group and its multiplicative monoid.

In the proof of FTA we needed proofs of equalities between rational expressions. These were automatized using so called `partial reflection'.

The axioms for real numbers are (apart from the fact that the reals form a constructive ordered field)

The axiom of Archimedes proves that `epsilon-Cauchy sequences' and `1/k-Cauchy sequences' coincide (and similar for limits). Viz: g:nat->F is a 1/k-Cauchy sequence if
forall k: nat. \exists N:nat.forall m\geq N(|g_m - g_N| <1/k

To be sure that our axioms can be satisfied, we have also constructed a Real Number Structure via the standard technique of taking the Cauchy sequences of rational numbers and defining an appropriate apartness on them. It turns out (as was to be expected) that real number structures are categorical: Any two real number structures are isomorphic. This fact has been proved within Coq.

In conclusion we have found:

See the publications page for more information.

[Home] [History] [People] [On-line Documentation] [Publications] [Library] [Download] [Contact Information]