Carsten Hornung: Bachelor Thesis

Programming Systems

Carsten Hornung

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 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.

Downloads

Thesis

You can find the finished thesis here.

Proof script

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

Logical - contains common logical laws. Code
Algebra - contains definitions for algebraic properties. Code
Natural Numbers - contains the proofs of the properties of the natural numbers. Code
Fractions - contains the proofs of the properties of fractions. Code
Rational Numbers - contains the proofs of the properties of the positive rational numbers. Code
Dedekind Cuts - contains the proofs of the properties of Dedekind Cuts. Code
Real Numbers - contains the proofs of the properties of the real numbers. Code
Completeness - contains different completeness properties of the real numbers. Code
Structures - contains the structures corresponding to the axiom systems. Code
Inhabitants - contains the inhabitants of the different structures. Code

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. 83-97, (1889)
A. Ciaffaglione and P. Di Gianantonio : A Co-inductive Approach to Real Numbers (2000)
H. Geuvers and M. Niqui : Constructive Reals in Coq: Axioms and Categoricity (2002)

Legal notice, Privacy policy