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