Carsten Hornung: Bachelor Thesis

Saarland University Computer Science

Constructing Number Systems in Coq

Author: Carsten Hornung
Advisor: Chad E. Brown
Supervisor: Gert Smolka



The primary goal of this thesis is to give elegant constructions of the natural numbers, positive rational numbers and finally the real numbers in the proof assistant Coq. Coq is a widely used proof assistant implementing a program specification and mathematical higher-level language called Gallina. Gallina is based on an expressive formal language called the Calculus of Inductive Con- structions that itself combines both a higher-order logic and a richly-typed func- tional programming language. Thus Coq provides a platform to define functions and predicates, to state mathematical theorems and to interactively develop for- mal proofs of them. To construct the number systems we use Landau's book Grundlagen der Analysis as a guide. It contains constructions of the (positive) rational numbers, the real numbers (based on Dedekind cuts) and the complex numbers starting from the natural numbers and the Peano axioms.



You can find the finished thesis here.

Proof script

The proof script is split into different parts. You can find them below.

Important References

Carsten Hornung, Tue Apr 26 12:58:11 2011