meta.yml

---
fullname: Binary Rational Numbers
shortname: qarith-stern-brocot
organization: coq-community
community: true
action: true
nix: true

synopsis: Binary rational numbers in Coq

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

doi: 10.1007/978-3-540-24849-1_20

publications:
  pub_doi: 10.1007/978-3-540-24849-1_20
  pub_url: https://hal.inria.fr/inria-00077041
  pub_title: 'QArith: Coq Formalisation of Lazy Rational Arithmetic'

authors:
- name: Milad Niqui
  initial: true
- name: Yves Bertot
  initial: true

maintainers:
- name: Hugo Herbelin
  nickname: herbelin

license:
  fullname: GNU Lesser General Public License v2.1 or later
  identifier: LGPL-2.1-or-later

supported_coq_versions:
  text: 8.18 or later
  opam: '{>= "8.18"}'

tested_coq_opam_versions:
- version: dev
- version: '8.19'
- version: '8.18'

tested_coq_nix_versions:
- coq_version: 'master'

namespace: QArithSternBrocot

keywords:
- name: rational numbers
- name: arithmetic
- name: field tactic
- name: binary lists
- name: Stern-Brocot

categories:
- name: Mathematics/Arithmetic and Number Theory/Rational numbers
- name: Miscellaneous/Extracted Programs/Arithmetic

documentation: |
  ## 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.
---