`IntegralSemiring` proposal

[mechvel]

Matthew Daggitt wrote on lib-2.2-rc1
on January 4, 2025

product≢0 : All NonZero ns → NonZero (product ns)
while I agree that it would be good to develop the theory in terms of an
appropriate algebraic structure, unfortunately the library is not
currently set up to do so. We would need someone to be motivated to make
those contributions, but regardless those changes would also not make it
into v2.2.

The --attached archive-- contains the .agda files that set up lib-2.2 to do so,
which makes it lib-2.2-next.
It is set in the standard library style.
It consists of the following files.

Algebra-Definitions.agda
to be merged to Algebra/Definitions.agda of lib-2.2.
It defines the property NoZeroDivisor
zero _∙_ = {x y : A} → (x ∙ y) ≈ zero → x ≈ zero ⊎ y ≈ zero

Algebra-Properties-Monoid.agda
to be set as Algebra/Properties/Monoid.agda.
It defines

Π₁ : C → List C → C    -- product of a nonempty list of elements,
Π : List C → C         -- product of a list of elements.
It proves
Π[x] : ∀ x → Π (x ∷ []) ≈ x

Algebra-Structures.agda
to be merged to Algebra/Structures.agda.
It defines

record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiring    : IsSemiring + * 0# 1#
    0≉1           : ¬ 0# ≈ 1#
    noZeroDivisor : NoZeroDivisor 0# *

  open IsSemiring isSemiring public

Algebra-Bundles.agda
to merge to Algebra/Bundles.agda.
It defines

record IntegralSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  ...
  isIntegralSemiring : IsIntegralSemiring _≈_ _+_ _*_ 0# 1#

Algebra-Properties-Semiring-Integral.agda
to set as Algebra/Properties/Semiring/Integral.agda.
It proves

nonzero*nonzero :  ∀ {x y} → x ≉ 0# → y ≉ 0# → (x * y) ≉ 0#
nonzero*nonzero {x} {y} x≉0 y≉0 xy≈0 with noZeroDivisor xy≈0
... | inj₁ x≈0 = x≉0 x≈0
... | inj₂ y≈0 = y≉0 y≈0

Π≉0 : {xs : List Carrier} → All (_≉ 0#) xs → Π xs ≉ 0#
Π≉0 {_}      []           = 1≉0
Π≉0 {x ∷ xs} (x≉0 ∷ xs≉0) = nonzero*nonzero x≉0 (Π≉0 xs≉0)

Data-Nat-Properties.agda
to be merged to Data/Nat/Properties.agda.
It proves

+-*-isIntegralSemiring : IsIntegralSemiring _+_ _*_ 0 1
+-*-isIntegralSemiring = record
  { isSemiring    = +-*-isSemiring
  ; 0≉1           = λ()
  ; noZeroDivisor = λ m {n} → m*n≡0⇒m≡0∨n≡0 m {n}
  }

But this latter instance is not type-checked, I do not know why, so far.
After it is fixed, it will be added there

integralSemiring : IntegralSemiring _ _

for ℕ.

If all this is accepted and merged, it will be easy to add

1. IntegralRing, IntegralDomain to Algebra.Bundles,
2. the instance of IntegralDomain to Integer.Properties,
3. several more proofs for the fnction Π.

onIntegralSemiring.zip

[jamesmckinna]

Looks promising!

[mechvel]

I wrote a certain erroneous message and have deleted it.
Please, read this new one.

I think now that the notice by James@jamesmckinna is important.
I have missed the following point.

Consider the example with Field: "CommutativeRing in which each nonzero element is invertible".

The classical definition has the second axiom ∀ {x} → x ≉ 0# → x ∣ 1#.
And the Agda library would probably need to change this to
∀ x → x ≈ 0# ⊎ x ∣ 1#.

And IsField can be expressed as

record IsField 0# 1# + * ... where                                              
  field                                                                         
    isCommutativeRing :  IsCommutativeRing ...                                  
    inversion         :  ∀ x → x ≈ 0# ⊎ x ∣ 1#    --                            
                                                                                
    -- x equals zero or x divides unity                                         

Probably @jamesmckinna and @JacquesCarette meant this approach and call it "positive".
Right?

For the two definitions, we have F = (¬ A → B) vs G = A ⊎ B.
Then, G → F is derived in Agda:

G→F (y→Ay⊎By) x ¬Ax  with (y→Ay⊎By) x                                           
... | inj₂ Bx = Bx                                                              
... | inj₁ Ax = contradiction Ax ¬Ax                                            

And F → G cannot be derived in Agda. So, classical is weaker.
Do I mistake?

If A is decidable, then F → G is derived too.

So, the traditional classical definition is not equivalent to the one desirable for Agda.
Right?

If so, how to name it in the Agda library?
I suggest to use the same name.

On practice, this notion difference will not show great.
Because in computational symbolic algebra almost all sensible methods are based on a decidable equality and even on decidable divisibility.

Now consider the definition of IsIntegralSemiring.
The classical definition in mathematics will be this:

-- recall:                                                                      
NoZeroDivisor =  {x y : A} → (x * y) ≈ 0# → x ≈ 0# ⊎ y ≈ 0#                            
(I)                                                                             
record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set _ where               
  field                                                                         
    isSemiring    :  IsSemiring + * 0# 1#                                       
    0≉1           :  0# ≉ 1#                                                    
    noZeroDivisor :  NoZeroDivisor 0# *                                         

Here 0≉1 is equivalent to "not all elements equal zero".

The definition for Agda is proposed as

(II)                                                                            
record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set _ where               
  field                                                                         
    isSemiring        :  IsSemiring + * 0# 1#                                   
    0≈1∨NoZeroDivisor :  0# ≈ 1# ⊎ NoZeroDivisor 0# *                           

I expect this is what was meant by James@jamesmckinna.
Is this?

Then (I) ⇒ (II) is derived constructively:
Suppose that R : IntegralSemiring-I.
Then, it holds NoZeroDivisor 0# *, and 0≈1∨NoZeroDivisor holds as the second member of disjunction,
and R : IntegralSemiring-II.

Try to derive (II) ⇒ (I) when all the involved relations are decidable.
Suppose that R : IntegralSemiring-II.

case (0 ≟ 1 , NoZeroDivisor?)                                                   
of                                                                              
(no 0≉1,  yes noZeroDiv) →  0≉1 , noZeroDiv   -- (I) proved                     
(no 0≉1,  no ¬noZeroDiv) →  Impossible case, because the second disjunction  member holds.                                       
(yes 0≈1, no ¬noZeroDiv) →  Impossible case, because zero semiring contradicts to existence of zero divisor.                       
(yes 0≈1, yes noZeroDiv) →  This case is possible, (II) cannot be proved in this case.                                          

So (I) and (II) are equivalent for all nonzero semirings.
Right?

If so, then I suggest the version (II) of the definition and expect that it is actually what James@jamesmckinna suggested
(is it?).

But may be I have missed something.
So, please, comment.

[jamesmckinna]

Sergei, thanks very much for the careful consideration of my earlier comments, and for taking the trouble to check that, at least in the presence of decidability, that there is only a difference of presentation between the two approaches, but that the 'positive' formulation is more general. (Incidentally, while I no longer really remember the source(s), I guess that the terminology of 'positive' comes from substructural logics/proof theory, or first-order model theory?, to refer to theories whose axiomatisation involves no negated atoms/formulae... just as 'geometric' refers to that fragment involving ∃ and ∨ occurring positively, and thus are preserved by geometric morphisms between toposes... and the role of category theorists/categorical logic in championing non-classical/substructural logics as the internal logics of various categories is a significant influence on 'constructivism' generally, as well as individuals such as myself...)

The emphasis on 'positive' formulations, as a design style, I take originally from Mines, Richman and Ruitenberg, "A Course in Constructive Algebra", and perhaps more so from other writings of Fred Richman (whose website, like that of Gabriel Stolzenberg, another early influence on my thinking, seems inaccessible at the moment, alas).

I think that, following Richman (and of course, Bishop and others before that), working in a constructive meta-language such as the type theory of Agda is to be taken as an opportunity to work a bit harder in exploring mathematical concepts, while keeping a firm eye on their classical/orthodox definitions. Richman's pons asinorum example of a positive/constructive resolution of the problem of finding "two irrationals a, b such that a ̂ b is rational" is another, rather simpler, instance of the phenomenon.

[mechvel]

James, thank you for your comments.
I an surprised with that I have forgotten light-headedly of the difference between ¬ A → B and A ⊎ B.
Now I revisit the definitions of Field and IntegralSemiring and try to accommodate them to constructive algebra in a better way.
My last letter in this issue have several places with the questions like "Right?", "is it?".
The comments are welcome from people.

[mechvel]

I think that the above "positive" approach to definitions of Field and IntegralSemiring accommodates them better to the needs of constructive algebra, because sometimes the equality is not decidable.
On the other hand we need to keep in mind that the case of a non-decidable equality is esoteric in computational algebra.
Most essential methods there require decidable equality and many of them also require decidable divisibility relation.

[mechvel]

Please, find attached the improved version archive of the proposal.
First see there Readme.lagda.

onIntegralSemiring.zip

[jamesmckinna]

#2563 resolves most of this proposal into the 'right' places in stdlib, but leaves unfinished the general product construction, and its NonZero properties to subsequent PRs, for reasons of complexity, together with a wider need to refactor things fo v3.0 before proceeding.

[mechvel]

The fresh version (version 3) of the proposal had been lost somewhere in pull requests.
For any occasion I upload it here:

onIntegralSemiring-3.zip