[ add ] Definition, consequences, properties, structures, and bundles for `Algebra.*`s with the 'no zero divisors' property

[jamesmckinna]

Lifted from #2542 , but has arisen before in various scattered proposals to extend the Algebra hierarchy to include:

• IntegralDomain
• EuclideanDomain
• UniqueFactorisationDomain
• PrincipalIdealDomain
• ...

which is (probably) too big a project to identify as a single issue/PR?

[mechvel]

James writes
"

    IntegralDomain
    EuclideanDomain
    UniqueFactorisationDomain
    PrincipalIdealDomain
    ...

which is (probably) too big a project to identify as a single issue/PR?
"
My application has the first three.
And the first one is much simpler for Standard library and more basic than others.
I think that it has sense to first try with IntegralSemiring , and then, to see.
I am going now to propose several small files for IntegralSemiring .
This will not be a pull request but something close to such.

[Taneb]

I've thought about this kind of thing in the past, and we want to be really careful about our definitions, because not every way of defining them that's classically equivalent is constructively equivalent. We probably want two hierarchies of these:

• Discrete doohickeys, where every element is (decidabely) either zero or not a zero divisor (these are more useful, but e.g. the real numbers fail to be this constructively). This implies that the structure has decidable equality (because we can tell whether x - y is zero or not).
• Heyting doohickeys, where an element that is apart from zero (for some apartness relation) is not a zero divisor. This is a weaker notion, but the real numbers (and things like polynomials over the real numbers) admit these structures.

[jamesmckinna]

Thanks @Taneb I very much agree about the need to take care over these things.

As with #2542 and the subsequent proposal offered by @mechvel in #2559 , IIUC, it is possible to phrase 'no zero divisor' in a positive way. Where I would be tempted to go further, however, would be to relax his insistence on 1# ≉ 0# in favour of the positive (geometric) condition (in the scope an assumption/field of the form Zero 0#):

Integral = 1# ≈ 0# ⊎ ∀ {x y} → x ∙ y ≈ 0#  → x ≈ 0#  ⊎ y ≈ 0# 

This avoids/finesses/is orthogonal to the question of whether any equation z ≈ 0# be decidable, ¬¬-stable, given by apartness, etc. in particular the instance z = 1#... and makes it easier to identify the Initial and Terminal such (Semi)Rings. The cost, potentially, is in one or two of the classical characterisations, eg. that ℤ/nℤ is Integral iff n is Prime, but since we have already committed to a NonTrivial qualifier for primality on Nat, I think that this could (happily?) extend to Integral(Semi)Ring...

I think that such a condition moreover also smoothly extends to the 'usual' lifting constructions such as 'ring of polynomials' etc. so should do no harm, while avoiding constructively troublesome conditions of the form z ≉ 0#...

... but yes, eventually, we may wish to pick out the Decidable sub-hierarchy of such algebras, and even the Heyting ones, but so far, in fact, their use has (largely) been on an ad hoc basis, again IIUC.

@JacquesCarette any thoughts on this?

[JacquesCarette]

I definitely agree with @Taneb that we need proceed carefully. Unfortunately, I don't have enough experience formalizing Algebra are these parts (IntegralSemiring, etc) so I don't have reliable opinions on the way to proceed. My general knowledge around constructivity again agrees with @Taneb that having multiple hierarchies is likely the way to go.

Certainly my experience also agrees with @jamesmckinna 's implicit point that phrasing any definition in a positive way tends to work much better constructive. So that for those parts of the hierarchy where such definitions are available, that would be the way to go.

[mechvel]

jamesmckinna writes

"As with #2542 and the subsequent proposal offered by @mechvel in #2559 , IIUC,
it is possible to phrase 'no zero divisor' in a positive way. Where I would be
tempted to go further, however, would be to relax his insistence on 1# ≉ 0#
in favour of the positive (geometric) condition (in the scope an
assumption/field of the form Zero 0#):

Integral = 1# ≈ 0# ⊎ ∀ {x y} → x ∙ y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
[..]
"

Logically, it is all right.
But the matter is in tradition.
Your definition allows 0# ≈ 1# to happen in integral domain.
And the traditional mathematical terminology is:

"an integral domain is a nonzero commutative ring in which the product of
any two nonzero elements is nonzero.
"
Mathematicians had good reasons to introduce such a notion.
(And generally there is no problem in merging the classical mathematical definitions into Agda stdlib in such a way that they would not be confused with their constructive versions).

Futher, if R : Semiring satisfies 0# ≈ 1#, then R consists only of #0
-- it is a zero semiring. Because it is derived in this case ∀ x (x ≈ 1 * x ≈ 0# * x ≈ 0#.

So, you suggestion disagrees with a known mathematical definition.
In our current case of Semiring in the Agda library, we need to have
"an integral semiring is a nonzero semiring in which the product of any two nonzero elements is nonzero.
"
So, a reasonable way to express this is

NoZeroDivisor : A → Op₂ A → Set _
NoZeroDivisor zero _∙_ = {x y : A} → (x ∙ y) ≈ zero → x ≈ zero ⊎ y ≈ zero
...
record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiring    : IsSemiring + * 0# 1#
    0≉1           : ¬ 0# ≈ 1#           -- now I think it needs to be changed to what James suggested
    noZeroDivisor : NoZeroDivisor 0# *

As to IntegralDomain, it will be respectively CommutativeRing which inherited semiring is integral (this will be defined after IntegralSemiring is accepted).

Below there follow by erroneous remarks.
Now they several erroneous fragments are deleted (see my further message on the subject of IntegralSemiring proposal).
[skip]

James wrote
"I think that such a condition moreover also smoothly extends to the 'usual'
lifting constructions such as 'ring of polynomials' etc. so should do no harm,
while avoiding constructively troublesome conditions of the form z ≉ 0#...
"
Ones you program something for polynomials with coefficients in R : CommutativeRing _ _,
you can do almost nothing if you do not have _≟_ : Decidable _≈_.
For example, subtract (a*x^2 + 1#) - b*x^2.
Has the result degree 2 or 0 ? This depends on whether a ≈ b.
So, once you get to polynomials, the conditions of z ≉ 0# for coefficients must not be a problem, and this is solved,
for example, by setting the parameter (_≟_ : Decidable _≈_) environment module.
And if _≟_ holds for R, than it is proved easily that _≟_ holds for polynomials overR.

Here are general considerations about constructivity in the Agda library.
Generally there is no problem in merging the classical mathematical definitions into Agda stdlib in such a way that they would not be confused with their constructive versions.
In fact, stdlib does not meet with this effect, so far.

The definitions of Setoid, Semigroup, ..., CommutativeRing
[skip]

They are correct and also usable on practice, they do not confused with anything classical, they have not any constructive-specific in them.

Now, suppose that a user needs to program operations with polynomials with coefficients in CommutativeRing.
In most cases, one will be forced to add the condition _≟_ : Decidable _≈_
to one's functions. Because otherwise many useful algorithms would not work.
Therefore it has sense to add DecCommutativeRing -- even to the stdlib algebra hierarchy.
Because otherwise the user will need either to include it in his applied library or to set an additional argument
(_≟_ : Decidable _≈_) to the signature of many functions.
By the way, a reasonable alternative is to set this condition as a parameter of the environment module.

This is similar to the reason for which DecSetoid is added to stdlib.
Of course, I do this in my application library.
And whether it is added in stdlib or not added - this does not break anything.
[..]
CommutativeRing, etc, do not have in them any constructive specifics,
while the above DecCommutativeRing will have specifics of constructive mathematics, the prefix Dec shows this.
(In classical mathematics, CommutativeRing is considered as decidable, there is not a question of decidability).

Again, if the team needs to include constructive-specific methods to stdlib,
it can simply include (foo? : Decidable Foo) to the parameters of an environment module.
If it wants to add a constructive-specific version of a known abstract domain, - say, decidable group, a ring with a decidable division, - then the name needs to be changed to ``DecGroup, DecRing-with-∣?`, and such,
in order to distinguish them from classical traditional notions in mathematics.

For example, in my applied library, I introduce Dec2IntegralDomain:
a commutative integral ring in which the division relation _∣_ is decidable.

See my further message on the subject of IntegralSemiring proposal. This is about "positive" style in the definition of
IsIntegralSemiring, I agree now that "positive" style does make difference.

[jamesmckinna]

Thanks @mechvel for your comments on #2559 where I have replied.

Regarding constructive/computational polynomial arithmetic, I take some inspiration from discussion with James Davenport at Bath (UK) (who is fond of the undecidability results in Shepherdson/Froehlich as an important test of the suitability of various representations): if we regard (classically) a polynomial in one variable x as a n : Nat-sequence of coefficients (at each power x ̂ n), then constructively we'll have problems deciding the order of the polynomial, equivalently its leading coefficient, if equality is undecidable. But if we regard polynomials as elements of a suitably (inductively-defined) Free construction, then (an upper bound on) the order, and 'leading' coefficient, may be computed by recursion... we just can't tell if that leading coefficient is zero or not, and hence whether the upper bound is actually attained. But such a computation is sufficient, again IIRC, for eg. the Hilbert Basissatz to go through, again for a suitably positive statement of the Noetherian property (in the style of Induction.WellFounded) for Ring etc.

[mechvel]

Response to jamesmckinna :

Symbolic computational (call it SC) mathematics is somewhat 1/4 of mathematics in the sense of the ideas and essential scientific content and value.
Constructive mathematics is somewhat 1/10 of SC mathematics.
Constructive mathematics with undecidable base equality (call it CUeq) constitute somewhat 1/20 of constructive mathematics.
To my mind, it still has sense to investigate even in CUeq, if a person is interested. And people do this, and it is all right.

Personally, I would never investigate into polynomial algebra in which the coefficient equality is not decidable. Because there are much more interesting problems, to my taste, in the case when it is decidable.

Also I pay attention to constructive approach only because it is a default in Agda, and also consider this as a strange game.
If a proof of existence of O is together with an algorithm that builds O, this is better than only an abstract proof. But if it is a great problem to provide an algorithm, then use ExcludedThird or a certain parameter function.

I do not think that using ExcludedThird in proofs can lead to something bad. For a predicate P, either there exists x such that (P x) or does not exist. I do not know of how to call the third possibility. May be, people know?

About Bath: I visited Bath somewhat in 2013. At the conference one listener asked me after my message
about provable computer algebra with Agda:
"Really, do you write proofs in Agda ? I - cannot write proof in Agda !".
There was a sincere suffer in his exclamation.
And I also had certain difficulties in Agda proofs.
I said "But what can we do? I am a beginner, we are trying ... Well, may be use Coq ? ... do you use Coq ?".
He said nothing. Strangely, other people have not intrude with explaining anything.
Someone could ask "give a sensible simple example, and we would answer later". No one said, probably all were confused :-)

I am sorry, probably such a correspondence is not for stdlib-issues nor for agda-issues, I wonder even about Zulip ...

[jamesmckinna]

Thanks @mechvel for the personal comments, but I think you're right: this isn''t the place, so my apologies for banging the drum for constructivism in general outside the scope of the details of this issue/PR.

When I have time, I'll look at making your contributions on #2559 into a PR in line with the discussion.

[mechvel]

Thanks @mechvel for the personal comments, but I think you're right: this isn''t the place, so my apologies for

Alternatively you can write to me personally by email. The address can be found in the net by name etc.