[Agda] GCD in future standard library

[mechvel at scico.botik.ru]

On 2019-08-06 16:42, mechvel at scico.botik.ru wrote:
> [..]
> 
> 
> II. A generic approach, which I suggest.
> 
> 1) To add to  Algebra.agda  the declaration of a cancellative semiring:
> 
> record CancellativeSemiring α ℓ :  Set _
>   where
>   field  CommutativeSemiring : CommutativeSemiring α ℓ
>   ...
>   field  _≟_       : Decidable _≈_
>          lnzCancel : LeftNZCancellative
> 
> LeftNZCancellative means the Cancellative property already defined in
> the _master_ library, only it adds the
> condition x ≉ 0# for the element being cancelled.
> 
> 2) The GCD notion is defined in the module parameterized by  R :
> CancellativeSemiring _ _:
> 
>   record GCD (a b : Carrier) :  Set _   -- a result of gcd
>     where
>     constructor gcd′
>     field  proper   : Carrier           -- proper gcd value
>            divides₁ : proper ∣ a
>            divides₂ : proper ∣ b
>            greatest : ∀ {d} → (d ∣ a) → (d ∣ b) → (d ∣ proper)


I need to explain how does it appear the condition of 
CancellativeSemiring.
In textbooks, the GCD notion is defined in the environment of 
IntegralDomain
(S.Lang. Algebra (1965) chapter II, paragraph 4).
IntegralDomain is a CommutativeRing without zero divisors (x*y ≈ 0 ==> x 
≈ 0 or y ≈ 0).
This is needed, for example, to provide a certain uniqueness of GCD.
For example, in Integer,  2 and (-2) both fit as  GCD 2 4,  but they 
differ in an invertible factor (-1).
In this sense GCD needs to be unique: unique modulo multiplication by 
invertible factors.
This uniqueness is derived from the condition of IntegralDomain.
It also derived from the condition of CancellativeSemiring.

CancellativeSemiring is used in my proposal instead of IntegralDomain 
because ℕ is not of a Ring, hence not of
IntegralDomain. But it needs a GCD instance similar as ℤ, and it is of a 
CancellativeSemiring.

Mathematicians use a general GCD notion for IntegralDomain, and also use 
a separate notion of GCD for ℕ, even without noticing that formally the 
latter GCD is not a special case for the former GCD. People do not pay 
attention to this,
and this does not lead to bad effects because ℕ is a sub-semiring in ℤ, 
and ℤ is of IntegralDomain.

But in Agda, we need to respect formalities: either to explicitly define 
two corresponding different GCD notions
or generalize further the generic definition. So, I generalize it to 
CancellativeSemiring.

Sorry for the two lengthy messages.

------
Sergei