[ add ] Algebra.Definitions.Integral and its consequences

[jamesmckinna]

Fixes #2554 . With thanks to @mechvel for discussion and his contributions on #2559 , from which this obviously diverges slightly.

TODO:

• Algebra.Definitions.Integral etc. and one Algebra.Consequences.Base
• (Is)Semiring etc. up to (Is)IntegralCommutativeRing
• (Is)IntegralDomain as the orthodox special case of (Is)IntegralCommutativeRing satisfying 1#≉0# : 1# ≉ 0#, and hence NoZeroDivisors 0# _•_ outright

WON'T DO (from #2559 ):

• NonZero properties of a general product defined on IntegralSemiring.monoid: this should be a downstream PR after the dust has settled on [ refactor ] Add Data.Nat.ListAction #2558 and [ refactor ] Add Data.Bool.ListAction #2561 , and once we can agree a strategy for replacing/augmenting Algebra.Definitions.RawMonoid.sum, with which such things overlap...
• instances of the constructions for Nat etc. (but could be done, once we agree the overall shape of this PR)

Issues: possible refactoring/deprecation opportunities

• deprecate (Is)CancellativeCommutativeSemiring in favour of Integral versions?
• fold definition of Trivial better into Algebra.Definitions so that Algebra.Definitions.Integral can make use of it
• breaking rephrase Algebra.Properties.Semiring.Primality in terms of Trivial?
• revisit in the light of any work done on Standardise implicit arguments of cancellation properties. #1436 , Refactor Algebra.Consequences.*? #2502 etc.

Also:

• naming
• dependencies in how all this has worked out... room for improvement
• usual issues about exports from Algebra.Structures and Algebra.Bundles: have we got everything?

[mechvel]

James,
thank you for correcting the proposal.
Is it possible to get the archive of the source of the pull request 3f6bdbb you have done?
If it is possible, I would copy it, install it as the library version, with calling it for myself say lib-2.3-rc1
(earlier I had difficulties with pull requests, it is easier for me to deal with a release candidate).
Then I could continue it by proposing the items that you announce as TODO.
?

[Taneb]

@mechvel you can download an archive at that commit here: https://github.com/agda/agda-stdlib/archive/3f6bdbb86b3c45f8eb1af8e9d042dac26893123f.zip

I found this link by clicking the commit, pressing the "Browse files" button, and then looking in the green "Code" button drop down

[jamesmckinna]

@mechvel Sergei, I chose to begin pushing to this PR before it was finished (so, properly, I should have marked it as DRAFT!), but as you perhaps can see, I am still actively making commits. Suggest that you hold off from downloading just at the moment?

[mechvel]

James, please inform me when it appears a reasonable moment for me to download the library version (I hope I will be able to download the archive of the source).
There remain a couple of items in my proposal onIntegralSemiring.zip which are not currently in CHANGELOG.md.

[mechvel]

Taneb wrote

@mechvel, you can download an archive at that commit here: https://github.com/agda/agda-stdlib/archive
/3f6bdbb86b3c45f8eb1af8e9d042dac26893123f.zip

I found this link by clicking the commit, pressing the "Browse files" button, and then looking in the green "Code" button > drop down

Thank you. I shall try this, after James signals that the commit is ready.

[mechvel]

@jamesmckinna asks

deprecate (Is)CancellativeCommutativeSemiring in favour of Integral versions?

For Ring, I believe, these two are equivalent. So that CancellativeRing is not needed.

But how do you derive Integral ==> LeftCancellative for Semiring?
For Ring' , I derive this this way: Let x*y == x*z and x \= 0 . Then x*y - x*z == 0 == x*(y-z). Then it follows from Integralthat y-z == 0, and y == z. But inSemiring, the above subtraction operation does not exist. And I do not know how to prove this implication. So that for Semiring I provide bothIntegralandCancellative`.
What people think of this?

I suspect now that it is possible to prove. But this is currently under question for me.
S : IntegralSemiring can, probably be embed into a certain R : Ring by adding the element (- x) for each x in S
( I never thought of this, if S is integral, will R be an integral ring? ). As the above implication holds for R,
probably, it will hold for S.
I do not know, this may occur wrong, I need to look into this.

[JacquesCarette]

don't have time to fully try, but could this be

either x≉0 y≉0 (noZeroDivisors xy≈0)

[jamesmckinna]

Ah!? Will investigate tomorrow...
... which function/property is either in this context?

[JacquesCarette]

other than the one item, this is looking nice to me.

[mechvel]

James wrote

• fold definition of Trivial better into Algebra.Definitions so that Algebra.Definitions.Integral can make use of it?
• breaking rephrase Algebra.Properties.Semiring.Primality in terms of Trivial?

Is Trivial ever defined in lib-2.2 Algebra?

[jamesmckinna]

@JacquesCarette : thanks for the early review
@mechvel : this is ready to look at now, but please be aware that the general 'NonZero' properties will not get covered here; there's too much going on with #2558 #2561 and then rationalising the designs for v3.0 to consider such additions now, I think.

Also: your comments about Cancellative are sensible: it is more that I believed we now have a redundant' entry in the namespace, but I need to think more about your comments about the Semiring structures/bundles.

[jamesmckinna]

@mechvel writes:

James wrote

* fold definition of Trivial better into Algebra.Definitions so that Algebra.Definitions.Integral can make use of it?

* breaking rephrase Algebra.Properties.Semiring.Primality in terms of Trivial?

Is Trivial ever defined in lib-2.2 Algebra?

No, this is new to this v2.3-badged PR.

[mechvel]

I wrote about trying to derive Integral ==> LeftCancellative for Semiring.
Each S : Ring has the commutative additive Monoid M. M can be extended to A : AbeleanGroup (probably called enveloping group for M). So there is a hope that IntegralSemiring can be extended to IntegralRing, and by this,
the equivalence IntegralSemigring <--> LeftCancellativeSemiring can be proved.
It is not so difficult to verify. But setting this whole proof to Standard library will need to add many items.
So that (Commutative)CancellativeSemiring cannot be replaced, so far, with IntegralSemiring
(may be there is possible a simpler proof , I do not know).

[mechvel]

The definition of AlmostLeft(Right)Cancellative
∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
is given (by myself) several years ago again with ignoring the case of undecidable equality.
If the team cares for this feature, we have to change this to disjunction.
?

[Taneb]

I'm not convinced these should directly be in Algbera.{Structures,Bundles}. As I've said elsewhere, there's two different classically equivalent constructively distinct definitions we want here (especially in the future when we've got real numbers). I'd like to suggest Algebra.Discrete.{Structures,Bundles} as a counterpart to the existing Algebra.Apartness

[Taneb]

Assuming that 0# and 1# have their normal properties wrt multiplication, 1# ≈ 0# implies all other equalities:
x = 1*x = 0*x = 0 = 0*y = 1*y = y

In particular, this means that it satisfies NoZeroDivisors 0# anyway. So we don't need to special-case 1# ≈ 0#

[mechvel]

I think Taneb is right.

lemma1 :  (1# ≈ 0# ⊎ NoZeroDivisors 0# _∙_) → NoZeroDivisors 0# _∙_
lemma1 (inj₁ 1≈0)    = noZeroDivisors  -- because everything equals zero due to `1≈0`.
lemma1 (inj₂ noZDiv) = noZDiv

lemma2 :  NoZeroDivisors 0# _∙_ → (1# ≈ 0# ⊎ NoZeroDivisors 0# _∙_)
lemma2 =  inj₂	

Therefore 1# ≈ 0# ⊎ NoZeroDivisors 0# _∙_
is equivalent to NoZeroDivisors 0# _∙_.
Right?
Further, the initial (my suggested and classical one too) definition was

(D)
record IsIntegralSemiring ...
  where
  field
    1≉0 : 1 ≉ 0#                                                  -- (I)
    noZeroDivisors : NoZeroDivisors 0# _∙_   -- (II)

We cannot remove (I), because the classical definition requires IntegralSemiring to be non-zero.

Neither we need to remove (I) with changing (II) to
1# ≈ 0# ⊎ (NoZeroDivisors 0# _∙_).
Because of the equivalence given by lemma1 and lemma2.
I am sorry for that I missed this when agreed with changing the definition (D)
and for agreeing with the definition Integral.

It comes out that we have to
a) return to (D),
b) remove the definition Integral,
c) remove from the library these wise comments about "positive" definitions with relation to the case of undecidable equality -- for the case of `Integral'
(for other cases it is all right, but for this particular case of the property 1# ≈ 0# and zero ring, it is not needed).

Do I mistake?
If I do not mistake, then I am sorry for spending our effort,
and the whole proposal needs to be returned to the first version .

[mechvel]

But I have lost the first archive that I uploaded to here. Can people find it on GitHub?

[jamesmckinna]

Ai! What can I have been thinking/doing!?
Apologies to all, I'd better have a long rethink.

[mechvel]

James writes

Ai! What can I have been thinking/doing!?
Apologies to all, I'd better have a long rethink.

Today I fixed my Version 2 of proposal to the Version 3, which returns to the initial definition

(D)
record IsIntegralSemiring ...
  where
  field
    1≉0 : 1 ≉ 0#                                                  -- (I)
    noZeroDivisors : NoZeroDivisors 0# _∙_   -- (II)

of which I wrote above.
Together with my message here I uploaded here the archive onIntegralSemiring-3.zip of sources.
But this message has disappeared, in a strange way.
Please, do you find this onIntegralSemiring-3.zip ?
Do I need to repeat uploading it here?