[Agda] BFLib for standard

[Sergei Meshveliani]

Dear standard library developers,

I have a certain  BFLib  library for Agda: 
a regular-performance, complete, and certified
* binary arithmetic for integer numbers,
* and the arithmetic of fractions in the general case of
  fractions over arbitrary GCDRing.

It has been tested under  Agda 2.6.0-candidate, MAlonzo, ghc-8.6.3.
I want to propose it as a replacement for the  Bin part and Rational
part in Standard library lib-0.18.

First, I am going to put  BFLib-0.01  to public as an application
library, after it appears an official Agda 2.6.0.

But then, I am going to propose its parts to standard, with modifying
them, when necessary.

BFLib suggests the three improvements.
(I) Essentially faster implementation for `compare', show, gcd for Nat,
    for arithmetic of rational numbers.
(II)  Totally new Bin part (similar to  binary-4  visible on GitHub).
(III) Generic Fraction domain constructor to replace the Rational part.
      In particular, its instance works also for rational number 
      arithmetic in binary representation. 


Can you, please, advise about possible way to propose?
(probably, by pull resquests).

Matthew wrote about pulling-request somewhat "a single item at a time".


I try the following plan, and have questions related to most its parts.


`compare' and `show' for Nat
============================

Pull-request
  Nat.<-cmp  as  compareFast (via _≟_, _∸_),

  toDecimalChars : ℕ → List Char   (via _%_, _div_),

  show : ℕ → String
  show = String.fromList ∘ toDecimalChars   -- fast `show` for ℕ, for ℤ.

These three look easy to make the implementation replacement, it is
backwards compatible.


The division relation
=====================

This is a large thing.
In standard, it is only for ℕ and ℤ (the latter is by 
"on absoluteValue"):

  record _∣_ (m n : ℕ) : Set where
    constructor divides
    field quotient : ℕ
          equality : n ≡ quotient * m
  open _∣_ using (quotient) public


I think, standard library needs generic Fraction over a GCDRing,
this needs a generic GCD notions. And this needs, in its turn, a generic
divisibility notion. I particular, it will serve also for ℤ, for pairs,
for polynomials, and so on.

If the library administrators do not want to consider such a proposal,
then I would skip its pull request, in order to save effort.
In this case there will remain only the Bin part to try (with special
divisibility and gcd for Bin), and Fraction will be removed.

BFLib  defines the divisibility for  Magma.
First, the notion of a quotient is related to any _≈_; _∙_ :

  module _ {α α=} (A : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier A))
    where
    open Setoid A using (_≈_) renaming (Carrier to C)

    RightQuotient : C → C → Set (α ⊔ α=)
    RightQuotient a b =  ∃ (\q → (b ∙ q) ≈ a)

And the notion of divisibility is via RightQuotient: 

-------------------------------------------------------
module Magma-pack {α α=} (M : Magma α α=) 
  where
  open Magma M using (_≈_; _∙_; ∙-cong; ∙-congˡ; setoid)
                                        renaming (Carrier to C)
  module FP≈ = FuncProp _≈_
  
  open Setoid-pack setoid public

  _∣_  _∤_ :  Rel C (α ⊔ α=)
  x ∣ y =  RightQuotient setoid _∙_ y x   -- `x divides y' 

  _∤_ x =  ¬_ ∘ _∣_ x

  open EqR setoid

  ∣cong : _∣_ Respects2 _≈_
  ∣cond = ...

  ...
--------------------------------------------------------

Various properties of _∣_ are derived for Magma, Semigroup,
(Commutative)Monoid, Semiring, Ring, DecCommutativeRing
(there is also introduced _∣?_ for some structures).

The properties of _∣_ for ℕ are expressed as the instances of the above
generic properties for  *-monoid, *-+-semiring  in Nat.Properties.
Similarly this is done for the instances for ℤ.

Now, the property proofs in  Nat.Divisibilty  can be replaced with the
instances of the generic proofs. For example,  
x ∣ y → x ∣ z →  x ∣ (y + z)   is proved in Semiring-pack.

But what to do with the divisibility definition in  Nat.Divisibility ?

I can try to generalize the standard
  record _∣_ (m n : ℕ) : Set where
    constructor divides
    field quotient : ℕ
          equality : n ≡ quotient * m

for Magma, and then to try to agree the things so that old applications
like

  open Data.Nat.Divisibilty 
  open _∣_
  ...

will remain workable but will be done as an instance of the generic _∣_
(if this is ever possible).

On the other hand, as the approach to divisibility is so greatly
generalized, may be, we can ignore the backwards compatibility at this
point?

Another question: does the definition

  RightQuotient a b =  ∃ (\q → (b ∙ q) ≈ a)

  x ∣ y =  RightQuotient setoid _∙_ y x 

look simpler and nicer? Really do we need a record here?


"Packages"
==========

The above implementation introduces several modules of this kind:

  module Magma-pack {α α=} (M : Magma α α=),
  module Semigroup-pack {α α=} (H : Semigroup α α=),
  ...
  module Ring-pack {α α=} (R : Ring α α=)

In each `pack' there are gathered most useful functions and lemmata
(`items', theory) relating to a particular generic _standard_ structure:
Magma, Semigroup, Group, Ring and so on.
For example, divisibility in CommutativeRing has more proved properties 
than in Semigroup, many useful things can be proved for DecIntegralRing
that are not possible for Semiring. And we cannot include these items to
the records of the classical structures, because these records are
intended to be classical definitions, and not a related theory
containers.

The minimality is provided: there are included only those items that are
used in this proposal for standard.

Can we, say, put  Packages.agda  to the  Algebra/  folder and to put
there the above 'pack' parametrized modules?
Can a pull request introduce a new .agda file?

There are much more questions to ask. But I try to follow the rule
"a small item at a time".

Regards,

------
Sergei