Carsten Hornung: Bachelor Thesis
Constructing Number Systems in Coq
Author: Carsten Hornung
Advisor: Chad E. Brown
Supervisor: Gert Smolka
Talks

27.08.2010, 14:15: First talk (Building E1 3, Room 528)
You can find the slides here.

29.10.2010, 14:15: Proposal talk (Building E1 3, Room 528)
You can find the slides here.

29.04.2011, 15:15: Final talk (Building E1 3, Room 528)
You can find the slides here.
Abstract
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 higherlevel language called Gallina. Gallina is based on an expressive formal language called the Calculus of Inductive Con structions that itself combines both a higherorder logic and a richlytyped 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.
Downloads
Thesis
You can find the finished thesis here.
Proof script
The proof script is split into different parts. You can find them below.
Important References

E. Landau : Grundlagen der Analysis (1930), Online Version

G. Smolka, C.E. Brown : Introduction to Computational Logic, Lecture Notes SS 2010

Y. Bertot, P. Castéran : Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions (2004)

J. Harrison : Theorem Proving with the Real Numbers (1998)

G. Peano : The principles of arithmetic, presented by a new method pp. 8397, (1889)

A. Ciaffaglione and P. Di Gianantonio : A Coinductive Approach to Real Numbers (2000)

H. Geuvers and M. Niqui : Constructive Reals in Coq: Axioms and Categoricity (2002)
Legal notice, Privacy policy