announce of Binary-3.0
(too old to reply)
Sergei Meshveliani
2018-01-13 15:25:57 UTC

Binary-3.0 -- a Pure Binary Natural Number Arithmetic library
for Agda

is available on


(see license.txt and the manual README.agda in the archive).

Binary-3.0 is a pure, regular-performance, complete, and certified
binary arithmetic for natural numbers
written in Agda.

It has been tested under Agda 2.5.3, MAlonzo, lib-0.14.

It is also suggested as a replacement for the Bin part in
Standard library lib-0.14
(the modules Data.Bin.agda, Data.Bin.Properties.agda).

means that Binary-3.0 never uses a built-in arithmetic (on Nat) to
essentially change performance.
The performance order is supposed to remain with replacing the Nat
arithmetic with the naive unary arithmetic.

`Regular performance'
means that the arithmetic on Bin of Binary-3.0 has a regular performance
cost order -- the one expected for the corresponding known naive
operations with bit lists.
* The comparison <-cmp x y on Bin costs O(|x| + |y|),
where |z| = bitLength z.

* Division with remainder divMod x y y≢0 on Bin is implemented as a
of {s = shift n dr for certain n; dd := dd -. s} repeated O(|x|)
So that it costs O( |x|^2 ).

means that all the items are implemented that are usually
required for standard arithmetic. There are provided the
following items.

* DecTotalOrder instance for Bin,
for x <= y defined on Bin as x < y or x == y.
* StrictTotalOrder instance for Bin, _<_.
* The bijection property for the map pair toNat, fromNat.
* Subtraction _-._ on Bin, with the needed properties proved.
* The proofs for isomorphism for _+_, _*_, _-._ for toNat, fromNat.
* The monotonicity proofs for toNat, fromNat for _<=_ and Nat._<=_.
A similar monotonicity for _<_ and Nat._<=_ are proved.
* Various kinds of monotonicity for _+_, _*_, _-._ for _<=_
and _<_ are proved.
* The CommutativeSemiring instance for Bin.
* Division with remainder and GCD for Bin.
* The demonstration/test programs for divMod and gcd.

`Certified' means that everything is proved in Agda which is regularly
required of the above operations.

Usage of Standard library lib-0.14

Bin0.agda _copies_ the following items from Data.Bin of Standard

Bin⁺, data Bin, 2^_, toBits, ⌊log₂_⌋, _*2,
_*2+1, ⌊_/2⌋, Carry, addBits, addCarry, _+_,
_*_, fromBits, addBitList,

The last three have a slight change in implementation.

Nothing else about Bin is taken from Standard lib-0.14.

The definition for inequalities on Bin is totally changed in Bin0, Bin1.

More detailed explanations are given in README.agda.

Binary-3.0 has been tested under Agda 2.5.3,
and it relies on Standard library lib-0.14.

It also includes the module LtReasoning.agda -- a support for
inequality reasoning by Ulf Norell.

agda -c $agdaLibOpt GCDTest.agda

Comments and improvements are welcome.

Sergei D. Meshveliani