Binary Rational Numbers

Development of rational numbers in Coq as finite binary lists and defining field operations on them in two different ways: strict and lazy.

Meta

• Author(s):
  • Milad Niqui (initial)
  • Yves Bertot (initial)
• Coq-community maintainer(s):
  • Hugo Herbelin (@herbelin)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: 8.18 or later
• Additional dependencies: none
• Coq namespace: QArithSternBrocot
• Related publication(s):
  • QArith: Coq Formalisation of Lazy Rational Arithmetic doi:10.1007/978-3-540-24849-1_20

Building and installation instructions

The easiest way to install the latest released version of Binary Rational Numbers is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-qarith-stern-brocot

To instead build and install manually, do:

git clone https://github.com/coq-community/qarith-stern-brocot.git
cd qarith-stern-brocot
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

This project contains a rational arithmetic library for Coq. This includes:

• A binary representation for positive rational numbers Qpositive and its extension to Q by adding a sign bit (also known as Stern-Brocot tree encoding).
• Arithmetic operations on Qpositive and Q defined in an strict way.
• More efficient arithmetic operations on Q defined lazily using homographic and quadratic algorithms for this binary representation (exact rational arithmetic).
• Proof of the correctness of the homographic and quadratic algorithms using the strict operations.
• The files enable the user to use Coq field tactic on Q with two different field structures (using strict or lazy operations).
• The Haskell extraction of the lazy algorithms (quadratic.hs).
• A syntax for using the rational numbers as pair of integers, and writing simple arithmetic operations on them.
• A proof of irrationality of the square root of 2.
• A proof that Q is Archimedean.
• A proof that Q is countable.