# Contribution: QArith

A Library for Rational Numbers (QArith)

## Authors

• Pierre Letouzey

## Description

This contribution is a proposition of a library formalizing rational number in Coq.

## Keywords

q, arithmetic, rational numbers, setoid, ring

```          A Library for Rational Numbers (QArith)

P. Letouzey

This contribution is a proposition for what could become a QArith
Standard Library. The need for such a QArith Standard Library seems
clear from the number of users contribution dealing with Rationals.
There are at least:

Rocq/RATIONAL
Nijmegen/QArith
Nijmegen/C-CoRN/model/field/Fraction_Rat.v

and probably more. The present contribution is based on C-CoRN
(former FTA) file,  enhanced via the use of Coq's tools for Setoids.
In particular, it inherits its definition of Q datatype:

Record Q : Set :=  Qmake { Qnum: Z; Qden: positive }.

The immediate problem with this representation is the lack of
canonicity. In particular, from the Coq point of view, 1/2 <> 2/4.
In Rocq/RATIONAL, this issue is addressed via a quotient type.
In Nijmegen/QArith, another representation is chosen, that fulfill
the canonicity. The third way we propose is to stick to the simple
original definition, and to define a setoid equality predicate over Q.

Two reasons for this third way:

- Coq has now tools to deal with Setoid equalities, Setoid Rewrite and
Setoid Replace. There is even a Setoid Ring adapation of the Ring
tactic (see file Qring.v)

- This simple representation allows a relatively small library, and at
the same time gives relatively efficient extracted functions. On the
contrary, the Nijmegen/QArith clever data-representation seems to have
as drawback slow operations (Qplus is done via decoding to nat numbers,
adding in nat, and then recoding, is that correct ?)

THE FILES:

QArith.v: basic definitions and lemmas, Q seen as a Setoid.

Qring.v: Q seen as a Setoid Ring, some example of Ring tactic being used.

Qreals.v: Unlike Ring, the Field tactic does currently not work over
Setoids. In the meanwhile, we can emulate a Field over Q by injecting the
equality inside Coq Reals, and then using Field. This file provides a
tactic QField which do that.

Qreduction.v: Transforming a fraction into its reduced form.

SQRT2:

In this subdirectory can be found a small experiment about constructive
reals made with the help of H. Schwichtenberg. Even if this experiment
is not in a finished state, I've included it along with QArith as a
example of use for these rationals and as a test-suite.

```