<div dir="ltr">Hi Sergei,<div> As your message is primarily discussing changes to the standard library and is aimed at the standard library maintainers, you should talk about this on the standard library Github repository. You've already opened an issue <a href="https://github.com/agda/agda-stdlib/issues/757">here</a> which could be used to discuss it.</div><div>Best,</div><div>Matthew </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Aug 7, 2019 at 2:57 AM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2019-08-06 16:42, <a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a> wrote:<br>
> [..]<br>
> <br>
> <br>
> II. A generic approach, which I suggest.<br>
> <br>
> 1) To add to  Algebra.agda  the declaration of a cancellative semiring:<br>
> <br>
> record CancellativeSemiring α ℓ :  Set _<br>
>   where<br>
>   field  CommutativeSemiring : CommutativeSemiring α ℓ<br>
>   ...<br>
>   field  _≟_       : Decidable _≈_<br>
>          lnzCancel : LeftNZCancellative<br>
> <br>
> LeftNZCancellative means the Cancellative property already defined in<br>
> the _master_ library, only it adds the<br>
> condition x ≉ 0# for the element being cancelled.<br>
> <br>
> 2) The GCD notion is defined in the module parameterized by  R :<br>
> CancellativeSemiring _ _:<br>
> <br>
>   record GCD (a b : Carrier) :  Set _   -- a result of gcd<br>
>     where<br>
>     constructor gcd′<br>
>     field  proper   : Carrier           -- proper gcd value<br>
>            divides₁ : proper ∣ a<br>
>            divides₂ : proper ∣ b<br>
>            greatest : ∀ {d} → (d ∣ a) → (d ∣ b) → (d ∣ proper)<br>
<br>
<br>
I need to explain how does it appear the condition of <br>
CancellativeSemiring.<br>
In textbooks, the GCD notion is defined in the environment of <br>
IntegralDomain<br>
(S.Lang. Algebra (1965) chapter II, paragraph 4).<br>
IntegralDomain is a CommutativeRing without zero divisors (x*y ≈ 0 ==> x <br>
≈ 0 or y ≈ 0).<br>
This is needed, for example, to provide a certain uniqueness of GCD.<br>
For example, in Integer,  2 and (-2) both fit as  GCD 2 4,  but they <br>
differ in an invertible factor (-1).<br>
In this sense GCD needs to be unique: unique modulo multiplication by <br>
invertible factors.<br>
This uniqueness is derived from the condition of IntegralDomain.<br>
It also derived from the condition of CancellativeSemiring.<br>
<br>
CancellativeSemiring is used in my proposal instead of IntegralDomain <br>
because ℕ is not of a Ring, hence not of<br>
IntegralDomain. But it needs a GCD instance similar as ℤ, and it is of a <br>
CancellativeSemiring.<br>
<br>
Mathematicians use a general GCD notion for IntegralDomain, and also use <br>
a separate notion of GCD for ℕ, even without noticing that formally the <br>
latter GCD is not a special case for the former GCD. People do not pay <br>
attention to this,<br>
and this does not lead to bad effects because ℕ is a sub-semiring in ℤ, <br>
and ℤ is of IntegralDomain.<br>
<br>
But in Agda, we need to respect formalities: either to explicitly define <br>
two corresponding different GCD notions<br>
or generalize further the generic definition. So, I generalize it to <br>
CancellativeSemiring.<br>
<br>
Sorry for the two lengthy messages.<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>