Generic GCD proposal

[mechvel]

gcdProposal.lagda.zip
The proposal of a generic GCD notion for standard library

---

0. Introduction
   ===========

Agda is nice, and generally, its library is nice.
But it is evident that the desgn for divisibility and GCD needs improvement.

A generic GCD notion can easily be defined on the base of lib-1.4
for any CancellativeSemiring
-- a CommutativeSemiring with the law of cancellation by a nonzero.
It provides an uniform definition and many property proofs for GCD for Nat, Integer, and many other domains.
The implementation is simple and will not increase the library code, nor the type check cost.

It is as follows.
....

module Algebra.Bundles ... where
...
record CancellativeSemiring α α≈ :  Set _
  where                                                                             
  field commutativeSemiring : CommutativeSemiring α α≈                           
  -----                                                  
  open CommutativeSemiring commutativeSemiring public                             
  open OfMonoid *-monoid using (_∣_)           
  open OfSemiring semiring using (LeftNZCancellative; ...)

  field cancelNZˡ : LeftNZCancellative  
  -----                                                        kind of integral semiring

...
module Algebera.Properties.CancellativeSemiring {α α≈}
                           (R : CancellativeSemiring α α≈) where          

open CancellativeSemiring R public using ...   renaming (Carrier to C)
...
open OfMonoid *-monoid using (_∣_; _∤_; ...)           

IsIrreducible :  Pred C (α ⊔ α≈)        
IsIrreducible p =  p ∤ 1#  ×  (∀ {x y} → (p ≈ x * y) → x ∣ 1# ⊎ y ∣ 1#) 

Coprime : Rel C (α ⊔ α≈)       
Coprime a b =  ∀ {c} → c ∣ a → c ∣ b → c ∣ 1#  

record GCD (a b : C) :  Set (α ⊔ α≈)    -- a result of gcd       
  where                      
  constructor gcdᶜ                                                           
                                                                                     
  field proper   : C                 -- proper gcd        
        divides₁ : proper ∣ a                                        
        divides₂ : proper ∣ b        
        greatest : ∀ {d} → (d ∣ a) → (d ∣ b) → (d ∣ proper)    

...

record GCDSemiring α α≈ :  Set (suc (α ⊔ α≈)) 
  where                                                                                        
  field cancellativeSemiring : CancellativeSemiring α α≈         
  -----                                 
  ...                                             
  field  gcd : (a b : Carrier) → GCD a b         

Several properties of GCD are highly usable, and their proofs can be easily implemented.
(I can provide a simple implementation).
...

8. Avoid special notions of IsIrreducible, Coprime, GCD declared for ℕ, ℕᵇ, ℤ, ℤᵇ
   ==============================================================
   Instead they will import such from
   Algebra.Properties.CancellativeSemiring and Algebra.Bundles.
   Also the property proofs for these items for ℕ, ℕᵇ, ℤ, ℤᵇ to be imported as general.
   A large corresponding part in Data.Nat.GCD, Data.Integer.GCD and such
   will be replaced with import of the generic items.
   ...

Why CancellativeSemiring ?
Textbooks usually define the GCD notion for IntegralDomain. ℤ is of IntegralDomain. But ℕ is not. So the textbooks
define the GCD for ℕ individually. Also the relation between ℤ and ℕ is so evident, that textbooks do not even consider
the difference between these two GCD notions.

In Agda, proofs are fully formal, so these two notions need to be agreed in some nice way. The proposal does this by
introducing CancellativeSemiring and by providing all the necessary proofs. The condition of cancellation by a nonzero
is needed to provide the property of GCD uniqueness (in a certain sense), which actually makes the GCD notion sensible.

The full proposal text (233 lines) is attached.
gcdProposal.lagda.zip

Please, read it.

[MatthewDaggitt]

Agda is nice, and generally, its library is nice.

Glad to hear it.

If you would like to add, then I suggest your first PR is simply to add CancellativeSemiring. Note that currently your definition of it does not follow the "structure"/"bundle" pattern followed by the rest of the library, something we've discussed extensively. Therefore before that PR is made, you will need to adjust it's definition to match the rest of the library.

[mechvel]

Note that currently your definition of it does not follow the "structure"/"bundle" pattern followed by the rest of the library,
something we've discussed extensively.

It adds to CommutativeSemiring only a single property of LeftNZCancellative.

From our old discussion I do not recall clearly, currently do not understand:
what evil is in the following declaration which avoids declaring IsSemigroup ?
I am sorry if I have forgotten the point. Can people, please, explain?

open import Level 
open import Algebra using (Magma)
open import Algebra.Definitions

record Semigroup α α≈ :  Set (suc (α ⊔ α≈)) 
  where
  field magma : Magma α α≈
  open Magma magma using (_≈_; _∙_) 

  field assoc : Associative _≈_ _∙_ 

Its advantage is that messy IsSemigroup is skipped, the definition is more plain and clear.
What drawback has it?

Is there any objection besides "it does not follow the style of existing versions of the library" ?

[mechvel]

If you would like to add, then I suggest your first PR is simply to add CancellativeSemiring.

Done: on the master branch #1308.

[MatthewDaggitt]

From our old discussion I do not recall clearly, currently do not understand:
what evil is in the following declaration which avoids declaring IsSemigroup ?
I am sorry if I have forgotten the point. Can people, please, explain?

The beauty of the internet is that you can go back and look at the conversations you initiated in the past:

• https://lists.chalmers.se/pipermail/agda/2020/012088.html
• Setoid parameter in algebra records #1238

[mechvel]

No. This were the replies to my suggestion to put setoid into parameters.
And this question is different:
what drawback has the following change in the definition of Semigroup?

record Semigroup α α≈ :  Set (suc (α ⊔ α≈)) 
  where
  field magma : Magma α α≈
  open Magma magma using (_≈_; _∙_) 

  field assoc : Associative _≈_ _∙_

This definition avoids IsSemigroup. What is its drawback in comparison to the definition in lib-1.4 that declares IsSemigroup ?
The question is only on Semigroup individually.
A concrete example is desirable. Say, "Let H and H' be two semigroups over the same magma ...".
Sorry, I am so silly that I do not see such.
I asked this question 2-3 years ago, and I do not recall whether there was a clear answer to it. Most probably it was not, because the subject is important for me, and I would remember.

[MatthewDaggitt]

No. This were the replies to my suggestion to put setoid into parameters.
And this question is different:

I think most of the comments by @JacquesCarette and @jespercockx in #1238 apply equally to this variation on the question. In particular, @jespercockx wrote:

... the problem is that there are many possible designs that all look reasonable, and the disadvantages of a certain approach do not appear until one is 9 levels deep in a hierarchy of algebraic structures (this is the point made in the paper). My point is not that these problems are impossible to solve, but rather that there are many choices to be made and their effects are not apparent until much later.

One of the first problems that springs to mind is that your scheme doesn't work for defining bundles with two different sub-bundles that need to have fields shared between them. For example using your pattern NearSemiring would be defined as:

record NearSemiring a ℓ : Set (a ⊔ ℓ) where
  field
    monoid    : Monoid a ℓ
    semigroup : Semigroup a ℓ
    distribʳ  : * DistributesOverʳ +
    zeroˡ     : LeftZero 0# *

However this doesn't capture the constraint that monoid and semigroup must share the same set and the same equality.

@mechvel as has been said before, the current "bundles"/"structures" design used in the standard library is a common pattern used by other proof assistants. It definitely has it's drawbacks but they appear to be the best compromise solution in the current generation of languages. Unless something changes with Agda language, the record hierarchies are extremely unlikely to change.

[MatthewDaggitt]

@mechvel whilst working on a way of avoiding having to reprove all the properties of min/max in #1390 for each type, I've worked out a way of greatly improving the definition of IsGCD so that we can use various different definitions of the actual function that calculates the gcd whilst still only having to prove the properties once.

The release of v1.5 is imminent so I'm going to temporarily strip out our definition of IsGCD and then we can add the better version back in immediately once the release is done.

[mechvel]

All right, let you try. I have to wait.
For any occasion, I describe shortly the mathematical issue of the subject.

The GCD notion is common for a great class (say, CancellativeCommutativeSemiring) of domains.
The gcd algorithms (methods) for different instances of this class differ quite often. Respectively, their proofs often differ.
For example, gcd оn Integer and gcd on Integer[x] (polynomials in x over integer coefficients) are usually
computed by different methods, and I do not see how to unify the corresponding proofs.
Even for the very same domain there may have sense different methods for gcd.
For example, in Integer[x] it has sense to evaluate gcd by pseudo-division and also by projections
modulo prime coefficients. Each of these methods has its advantages. And I do not see, how can one
provide a common proof for these two.
A simple common proof is known for Nat, Integer, and F[x] (polynomials over a Field F for coefficients),
and for certain other domains (not likely to be in Standard). It is based on the EuclideanDomain class.
But this needs introducing EuclideanDomain (which has a generic division with remainder).

I think, Field and EuclideanDomain do need to be introduced to Standard algebra.
But I was silent about this because you would say "this increases the code"
(the items for EuclideanDomain will take some code), while the issue of
CancellativeCommutativeSemiring + IsGCD is evidently useful in any case and does not increase the code.

Still:
a) CancellativeCommutativeSemiring + current IsGCD is sufficient for all this arrangement
(EulideanDomain belongs to CancellativeCommutativeSemiring),
b) there are usable domains (like Integer[x]) for which gcd needs to be evaluated by different methods,
not based on the Euclidean method, because these domains cannot have an Euclidean division with
remainder. The proofs for these methods will be different, I expect.
So that I do not guess, so far, what is your idea of a common proof for the gcd algorithms.