proposal to reorganize the divisibility relation ``_|_ ``

[mechvel]

Matthew wrote

The discussion for how this stage of the changes should be laid out should
really be continued in an issue on Github. If you'd like to open an issue there?

All right, I open it.

I think, standard library needs a generic divisibility notion _|_.
Currently there exists _|_ for Nat and ℤ.
I suggest to remove it, and to replace it with a generic divisibility defined for Magma:
First, the notion of a quotient is related to any _≈_, _∙_ :

module _ {α α=} (A : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier A))
    where
    open Setoid A using (_≈_) renaming (Carrier to C)

    RightQuotient : C → C → Set (α ⊔ α=)
    RightQuotient a b =  ∃ (\q → (b ∙ q) ≈ a)

And the notion of divisibility is via RightQuotient:

module _ {α α=} (M : Magma α α=) 
  where
  open Magma M using (_≈_; _∙_; ∙-cong; ∙-congˡ; setoid)  renaming (Carrier to C) 

  _∣_  _∤_ :  Rel C (α ⊔ α=)
  x ∣ y =  RightQuotient setoid _∙_ y x    -- `x divides y' 

  _∤_ x =  ¬_ ∘ _∣_ x

  open EqR setoid

  ∣cong : _∣_ Respects2 _≈_
  ∣cond = ...
  ...

In particular, it will serve also for ℕ, ℤ, for pairs, for polynomials, and so on.
The existing divisibility for ℕ, ℤ to be replaced with _|_ imported from
Algebra.Properties.Magma (Nat.Properties *-magma) and from
Algebra.Properties.Magma (Integer.Properties *-magma).

The modules Algebra.Properties.Magma, Algebra.Properties.Monoid, ...
to be parametrized by Magma, Monoid, and so on. They contain theories related to Magma, Monoid, and so on. In particular, there are proved properties of _|_ related to these structures.

This notion of _|_ will serve the generic definition of GCD, etc.
How precisely is this all organized will be demonstrated in BFLib-0.01, which has to appear after the release of Agda-2.6.0.
But BFLib-0.01 will try to merge into standard so, that it modules to distribute their parts between the modules of standard library.

[MatthewDaggitt]

As I said in the email thread I believe that

RightQuotient : C → C → Set (α ⊔ α=)
RightQuotient a b =  ∃ (\q → (b ∙ q) ≈ a)

belongs in Algebra.FunctionProperties.

We already have Algebra.Properties and Algebra.Operations so perhaps we need Algebra.Relation as well where _|_ would live in Algebra.Relation.Magma. I still feel that this part of the library feels the worst organised as at the moment Algebra.Operations.CommutativeMonoid contains many properties as well, not just simply operations. I'm open to suggestions for how to start cleaning this up?

The existing divisibility for ℕ, ℤ to be replaced with | imported from
Algebra.Properties.Magma (Nat.Properties *-magma) and from
Algebra.Properties.Magma (Integer.Properties *-magma).

I think that the question of whether we replace the implementations in ℕ and ℤ with the general form is best decided after we have the general form nailed down.

[mechvel]

I still feel that this part of the library feels the worst organised as at the moment
Algebra.Operations.CommutativeMonoid contains many properties as well, not just simply
operations. I'm open to suggestions for how to start cleaning this up?

The whole Algebra needs to be like this.
The Algebra/ folder to contain the files Structures0.agda, Structures1.agda, Structures2.agda,
Structures3.agda -- probably four files are enough.

The files in Algebra/ to include the contents of Algebra/Structures.agda of the current standard.

Algebra/Structures0.agda to contain the definition record Magma ... and the module
module Magma-theory ... (H : Magma _ _) where ...
where are given various items for an arbitrary Magma. For example, a definition for the divisibility relation |, declaration for various properties of the magma items and their proofs
(separate parts of ...Properties.agda of the current standard to be merged into these Algebra/* files).

Further, Structures0.agda contains record Semigroup ..., and the module
module Semigroup-theory ... (H : Semigroup _ _) where ....
And so on.
I expect that Structures0.agda will include the theory modules for Magma, Semigroup,
Monoid, CommutativeMonoid, Group, AbelianGroup.

Structures1.agda is a continuation. It will contain the theory modules for Semiring, Ring, CommutativeRing, DecCommutativeRing, DecIntegralRing, GCDRing.

Structures2.agda to contain the theory modules for Field and (may be) for LeftModule, VectorSpace.
Structures3.agda to contain the theory for GCD (defined in Structures1).

No more files are needed there, because standard library must not be large.
The items for Nat, Integer, Bin, BinaryInteger to remain in the Data/ folder. They need to include the implementation of the instances of the abstract structures defined in the folder Algebra/.

It is needed to add Data/Fraction/ containing the modules Fraction.agda, F0.agda F1.agda
that define a general notion of Fraction over any GCDRing and prove the corresponding theory
and implement for the domain (Fraction (R : GCDRing _ _)) various instances for the structures defined in Algebra/
(all the code for Bin, BinaryInteger, Fraction is ready in the library BFLib-0.01).

This can be called "reorganizing the Algebra part".

[mechvel]

Two more notes:
Algebra/Operations/ is a wrong folder. Its contents needs to merge to the -theory modules in the files Algebra/Structures.agda.
The same is with Algebra/Properties/.

[mechvel]

To separate "Properties" and "Operations" and such to other folders is a wrong idea.
A natural approach is to follow the style of the textbooks on algebra:
define a Setoid, desribe items for Setoid and prove some of their properties.
All this in the same paragraph, that is in the same .agda file.
Then describe a more complex structure that inherits setoid, prove some theory about it.
The related Operations, Relations, Functions, Properties and proofs -- in the same file, like in the same paragraph.
And so on.

These are intermingled wit the domain constructors: Nat, Integer, Fraction. In the textbooks, the instances for them are in paragraphs that can be scattered among the paragraphs for abstract theories. Say, Ring is defined in one paragraph, and the instance of Ring for Integer is described in another paragraph, which can be neighbor or can be in another chapter.
In a program library, the concrete instances are natural to keep in a separate folder, say, Data/.

Generally, we need to follow textbooks on science, this is a reliable approach.

[MatthewDaggitt]

I'm afraid I'm not a fan of the Algebra.Structures0, Algebra.Structures1 etc. approach as it fails the meaningful name test. I's impossible to know what is in each module from the it's name.

A natural approach is to follow the style of the textbooks on algebra:
define a Setoid, desribe items for Setoid and prove some of their properties.
All this in the same paragraph, that is in the same .agda file.
Then describe a more complex structure that inherits setoid, prove some theory about it.

Generally, we need to follow textbooks on science, this is a reliable approach.

I'm also not sure I'd agree with this. Textbooks work at a considerably higher level of abstraction than a library of formal proofs and therefore can take liberties with organising their content that a library cannot. This is because introducing assumptions is nearly cost free in text, whereas if assumptions are handled in a program incorrectly it can often add considerable code bloat and usage cost.

Textbooks also don't have to worry about pseudo-dependency cycles. For example if you have two modules X and Y and Y.a depends on X.a and X.b depends on Y.b then Agda will flag this as a dependency cycle even though it's not. Written mathematics has no such problem.

Also, just to note, @mechvel you can click the ... button then Edit at the top right of your post to add an edit on to the end of your post instead of making a whole new post if you want to make a correction.

[mechvel]

I'm afraid I'm not a fan of the Algebra.Structures0, Algebra.Structures1 etc. approach as it fails
the meaningful name test. I's impossible to know what is in each module from the it's name.

But currently you have a single name Algebra for all the hierarchy.
It can be Algebra-I, Algebra-II, Algebra-III, as there Volume I, Volume-II ... in textbooks.
It can be also FromSetoid-to-Monoid.agda, FromGroup-to-Field.agda.

if you have two modules X and Y and Y.a depends on X.a and X.b depends on Y.b then Agda will
flag this as a dependency cycle even though it's not.

As usual, the modules are split into X1, Y1, X2, Y2, so that the ones more close to the head do not import further ones. If this is not possible, then they need join, and may be the `mutual' construct to apply.

I still feel that this part of the library feels the worst organised as at the moment
Algebra.Operations.CommutativeMonoid contains many properties as well, not just simply
operations. I'm open to suggestions for how to start cleaning this up?

This .agda file contains a piece of the generic theory for CommutativeMonoid.
The word Attributes' is more generic than Operations'. The word Theory is even more generic.
And as to me, the very subfolder `Operations' looks unnatural.

[JacquesCarette]

I completely agree with @MatthewDaggitt that textbooks are not a good model for structuring libraries. The requirements are completely different. For one, textbooks are optimized by pedagogy, while libraries should be optimized for scalability and re-use. These are radically different "forces", and thus good solutions are quite different. Plus classical mathematics in textbooks picks and chooses so very few structures to talk about, while the zoo is a couple of orders of magnitude larger.

On Wikipedia, both the Algebraic Structures and List of algebraic Structures are still small, Jipsen's list with > 300 entries gets better.

[MatthewDaggitt]

On Wikipedia, both the Algebraic Structures and List of algebraic Structures are still small, Jipsen's list with > 300 entries gets better.

Well that list is terrifying 😨

[JacquesCarette]

If you're going to do it "by hand" the current way things are done? Yes, yes it is. I'm not going to suggest/ask that it be done that way... Working with others to create a sane way to get there. Hope to be able to report on it in a couple of months.

[MatthewDaggitt]

This isn't going to happen for v2.0 unfortunately...