Continuing with generic GCD.

[mechvel]

Please, consider this my commit of January 2, 2021.
It continues with proving properties of generic GCD, and introduces GCDSemiring
(over CancellativeCommutativeSemiring).

new file: src/Algebra/Properties/CancellativeCommutativeSemiring.agda
new file: src/Algebra/Properties/CancellativeCommutativeSemiring/GCD.agda
changed: CHANGELOG.md
changed: src/Algebra/Bundles.agda
changed: src/Algebra/Structures.agda
changed: src/Algebra/Divisibility.agda
changed: src/Algebra/Properties/Monoid/Divisibility.agda
changed: src/Algebra/Properties/Semiring/GCD.agda

• Algebra.Divisibility.IsGCD : added two values.
• Algebra.Properties.Monoid.Divisibility : added ∣∣-reflexive.
• Algebra.Properties.Semiring.GCD : added a couple of GCD properties.
• Algebra.Properties.CancellativeCommutativeSemiring :
  certain important GCD properties proved.
• Algebra.Bundles.GCDSemiring introduced.

[MatthewDaggitt]

First review.

[MatthewDaggitt]

This proof is pretty messy and unreadable. There must be a way of breaking it up into meaningful constituent parts, in the same way we have done so in Data.Nat.GCD!

[mechvel]

This is not so simple!
I do not know of how to simplify it any essentially.
Data.Nat.GCD would not help. Because it uses the properties of division with remainder (_/_ relies on division with remainder), on the properties of _/_ on ℕ.
And generic CancellativeCommutativeSemiring does not possess such an operation with such properties.
Among R : CancellativeCommutativeSemiring there are some domains R for which there is not possible a division operation with the properties similar to ones of Nat.DivMod... In particular there is not possible in general to solve
x ∣? y in R, while for ℕ it is solved via divMod.

gcd-distr is a subtle and a particular lemma. It nicety is in that its proof does not use anything besides the three
axioms of GCD (and the properties of generic _∣_).
The first impression is that gcd-distr cannot be derived only from these laws. But it occurs that the goal is achieved by combining these three laws repeatedly, and in a certain way.

I do not find this lemma in textbooks. This is a folklore. A certain referee has pointed at its formulation.
Then, I searched for the question at a mathematical forum, and found there a proof sketch.
The true author of the lemma is not known. It is almost the same as the generic Euclid's lemma (which is also
a folklore).
Coq does have its proof.
But I prefer to take things from literature rather than to read programs: to read an in-formal proof, to add details, and to convert it to Agda.
I have rewritten this proof in detail, with generalizing it from IntegralDomain to CancellativeCommutativeSemiring,
and programmed it.
Hear is this short and clear in-formal proof:

proof2.lagda.zip

Can you provide a simpler proof?

In Agda, it takes some code. Thus, the line

If c = 0 then  gcd ac bc  ∥  gcd 0 0  ∣∣  0  ∣∣  c ∙ (gcd a b).

of 65 characters is expressed in Agda in 240 characters (not counting trailing blanks).

This is, for example, due to the following reasons.
a) Agda needs all details.
b) For readability, these assignments with '=' need to be one per line.
c) In comparison to Nat, ≡ is replaced in many cases with ∣∣, which is expanded to the expressions
containing two pairs of values, the two equalities to be proved, the two factor values to be introduced.

Please, consider the issue once more.

[MatthewDaggitt]

Here's an example of one of your earlier proofs that I've just rewritten from:

x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] : ∀ {x y d} → (x ≉ 0#) ⊎ (y ≉ 0#) →
                               ((isGCDᶜ (q₁ , _) (q₂ , _) _) : IsGCD x y d) →
                               Coprime q₁ q₂     
x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] {x} {y} {d} nz⊎nz
  isGCD@(isGCDᶜ (quot₁ , quot₁∙gcd≈x) (quot₂ , quot₂∙gcd≈y) greatest)
  {c} (q₁ , q₁c≈quot₁) (q₂ , q₂c≈quot₂) = c∣1
  where
  d≉0     = x≉0∨y≉0⇒gcd≉0 isGCD nz⊎nz
  q₁*dc≈x = begin
    q₁ * (d * c)    ≈⟨ Of*CSemig.x∙yz≈xz∙y q₁ d c ⟩
    (q₁ * c) * d    ≈⟨ *-congʳ q₁c≈quot₁ ⟩
    quot₁ * d       ≈⟨ quot₁∙gcd≈x ⟩
    x               ∎

  q₂*dc≈y = begin
    q₂ * (d * c)    ≈⟨ Of*CSemig.x∙yz≈xz∙y q₂ d c ⟩
    (q₂ * c) * d    ≈⟨ *-congʳ q₂c≈quot₂ ⟩
    quot₂ * d       ≈⟨ quot₂∙gcd≈y ⟩
    y               ∎

  dc∣x = q₁ , q₁*dc≈x
  dc∣y = q₂ , q₂*dc≈y
  c∣1  = let
           (q , q*dc≈d) = greatest dc∣x dc∣y
           d*qc≈d*1     = begin
             d * (q * c)   ≈⟨ Of*CSemig.x∙yz≈y∙xz d q c ⟩
             q * (d * c)   ≈⟨ q*dc≈d ⟩
             d             ≈⟨ sym (*-identityʳ d) ⟩
             d * 1#        ∎

           qc≈1 = *-cancelˡ-nonZero {d} (q * c) 1# d≉0 d*qc≈d*1
        in
        q , qc≈1

to

x∣y∧z∣x/y⇒x*z∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x * z ∣ y 
x∣y∧z∣x/y⇒x*z∣y {x} {y} {z} (x/y , x/y*x≈y) (p , p*z≈x/y) = p , (begin
  p * (x * z)  ≈⟨ Of*CSemig.x∙yz≈xz∙y p x z ⟩
  (p * z) * x  ≈⟨ *-congʳ p*z≈x/y ⟩
  x/y * x      ≈⟨ x/y*x≈y ⟩
  y            ∎)

x*y∣x⇒y∣1 : ∀ {x y} → x ≉ 0# → x * y ∣ x → y ∣ 1#
x*y∣x⇒y∣1 {x} {y} x≉0 (q , q*xy≈x) = q , *-cancelˡ-nonZero (q * y) 1# x≉0 (begin
  x * (q * y) ≈⟨  Of*CSemig.x∙yz≈y∙xz x q y ⟩
  q * (x * y) ≈⟨  q*xy≈x ⟩
  x           ≈˘⟨ *-identityʳ x ⟩
  x * 1#      ∎)

x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd]2 : ∀ {x y d} → x ≉ 0# ⊎ y ≉ 0# →
                                ((isGCDᶜ (q₁ , _) (q₂ , _) _) : IsGCD x y d) →
                                Coprime q₁ q₂
x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd]2 x≉0∨y≉0 gcd@(isGCDᶜ d∣x d∣y greatest) x/d∣z y/d∣z =
  x*y∣x⇒y∣1 (x≉0∨y≉0⇒gcd≉0 gcd x≉0∨y≉0) (greatest
    (x∣y∧z∣x/y⇒x*z∣y d∣x x/d∣z)
    (x∣y∧z∣x/y⇒x*z∣y d∣y y/d∣z))

Can you see the difference? There's significantly less code duplication and I've split out the sub-results into useful lemmas that can be re-used by other proofs. In contrast your proof is brittle as it relies on implementation details of the divisibility relation, hard to understand and therefore difficult to refactor.

Please do the same for this proof.

[mechvel]

This is an improvement for x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] . Thank you.
I must have introduced this x∣y∧z∣x/y⇒x*z∣y.
Also I did not know of the possibility to set patterns like ((foo , _) : x ∣ y) →
to signatures.
x*y∣x⇒y∣1 is also useful.
Now, I
a) rename x∣y∧z∣x/y⇒x*z∣y to x∣y∧z∣x/y⇒xz∣y
(in mathematics, they often write xy for x * y, and I suggest to do this in names
- - when it is clear that this means x * y or x ∙ y),
b) rename x*y∣x⇒y∣1 to xy∣x⇒y∣1,
c) move x∣y∧z∣x/y⇒xz∣y to Algebra.Properties.CommutativeSemigroup.Divisibility,
because it is more generic, it is for CommutativeSemigroup and its _∙_.
d) move xy∣x⇒y∣1 to Algebra.Properties.CancellativeCommutativeSemiring,
because its usage is not only for the GCD items.

I have a minor note. Being a shorter proof does not mean being a more clear or understandable proof. For example the last three lines in your code are quite brain-twisting. This concerns the expressions in the last two lines. Putting
foo1 = x∣y∧z∣x/y⇒x*z∣y d∣x x/d∣z, who divides who according to foo1 ?
Putting foo2 = x∣y∧z∣x/y⇒x*z∣y d∣y y/d∣z, does it return the same value as foo1 ?
How many minutes with take of the reader to find this out?
Personally I can find it out, but have not done this, so far ...
Do we need to frighten readers?
Probably it worth to write where <this>|<that> = x∣y∧z∣x/y⇒x*z∣y d∣x x/d∣z
with setting appropriate names for <this> and <that>.

gcd-distr : Decidable _≈_ → ∀ {a b c d d'} → IsGCD a b d →                        
                  IsGCD (c * a) (c * b) d' → d' ∣∣ (c * d)

Please do the same for this proof.

I add the lemma x∣y⇒zx∣zy to Algebra.Properties.CommutativeSemigroup.Divisibility
and use it here three times.
I change where to let in a part of this proof in order to use patterns like
(x , xc≈d') = IsGCD.greatest ... and to save extracting values from it by the two projections.
Now it is somewhat simper and shorter. I wonder of what else can be done.

[MatthewDaggitt]

Putting foo1 = x∣y∧z∣x/y⇒xz∣y d∣x x/d∣z, who divides who according to foo1 ?
Putting foo2 = x∣y∧z∣x/y⇒xz∣y d∣y y/d∣z, does it return the same value as foo1 ?

I'm afraid I do not understand what you mean.

Now it is somewhat simper and shorter. I wonder of what else can be done.

Nowhere should the proof explicitly rely on the fact that divisibility is implemented as a pair. It should never directly construct or deconstruct a divisibility proof. Anything else breaks the abstraction boundary. Please fix.

[mechvel]

1. The whole subject is evident, and has nothing to do with mathematics.
2. If we define divisibility as a record Divides with constructor divides, the fields quotient and
   equality, then (divides q eq) : Divides a b is an abstract enough thing.
3. Probably Matthew is right in that gcd-distr can be written in a better way.
4. Even the current version of divisibility, IsGCD, and gcd-distr is still much better than the whole design in lib-1.5 for divisibility, GCD, Rational and such - even if the latter's are programmed very "encapsulatedly".
   Generally it is desirable to distinguish intuitively important things from not so important.

[mechvel]

More point:
when a language relies heavily on pattern matching, this drives it from the abstraction of the kind you people are so eager of.
For example, I expect to find in standard library programs similar to

f (_ :: (_ , y) :: ps) = y + ( f  ps)
f  _ = 0

What do you write for the "abstract & encapsulated" style?
Is it

f ps  = case null? ps
           of \
           { (yes _) -> 0 
           ; (no notNull-ps) -> 
                   case null? (tail ps notNull-ps)
                   of \
                    { (yes _) -> 0
                    ; (no notNull-tlPs) -> proj-2  (head (tail ps notNull-ps) notNull-tlPs) + (f ...)
                    } 
              }

?

[JacquesCarette]

That second is not at all "abstract and encapsulated". I would call that imperative-style programming. It is an ugly version of the first code, with pretty much nothing going for it.

Relying heavily on pattern-matching makes things representation-dependent. That is fine for implementing the base routines, and then gets problematic, eventually, for higher-level code.

The code for f clearly is a kind of fold that works on even length lists. The "abstract and encapsulated" way of doing this would be to provide such a fold abstraction, and then instantiate it with 0 and \x acc -> proj-2 x + acc.

[mechvel]

That second is not at all "abstract and encapsulated".

Is it representation dependent? I think, not.
It uses only 1) null? to decide of emptiness,
2) head and tail for a nonempty a list, these actually constitute a definition of what is a list,
3) second projection for a direct product.
Only basic mathematical notions, the representation details are not visible.
"Encapsulated style" or not - anyway, what is wrong in it (except its ugliness) ?

to provide such a fold abstraction, and then instantiate it with 0 and \x acc -> proj-2 x + acc.

There is a concrete example of two lines. Can you write the function source for what you suggest?

[mechvel]

and then gets problematic, eventually, for higher-level code.

Operating with gcd , IsGCD is higher-level.
Does this mean that one needs to avoid writing things like

let (mkIsGCD g g|a g|b greatest) = gcd a b in ...

?

[mechvel]

What is the final solution for the record constructor names : isGCDᶜ or mkIsGCD ?

[mechvel]

Please, consider my commit of January 5, 2021.
It improves the code according to your notes.
See my (coming) replies to the above notes.
The two points about the lemma of .../CancellativeCommutativeSemiring/GCD.gcd-distr are questionable
-- see my coming replies.
I am going to improve the code assuming your answers to these two questions.

[MatthewDaggitt]

Hi @mechvel I've updated this PR after having merged in the changes from PR #1387. You will need to run git pull in your local repository to get the changes. I'll address the rest of your comments in a bit.

[mechvel]

[..]
You will need to run git pull in your local repository to get the changes.

All right, I have applied git pull; make clean; make test.
It shows OK.

[MatthewDaggitt]

Here's an example of one of your earlier proofs that I've just rewritten from:

x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] : ∀ {x y d} → (x ≉ 0#) ⊎ (y ≉ 0#) →
                               ((isGCDᶜ (q₁ , _) (q₂ , _) _) : IsGCD x y d) →
                               Coprime q₁ q₂     
x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] {x} {y} {d} nz⊎nz
  isGCD@(isGCDᶜ (quot₁ , quot₁∙gcd≈x) (quot₂ , quot₂∙gcd≈y) greatest)
  {c} (q₁ , q₁c≈quot₁) (q₂ , q₂c≈quot₂) = c∣1
  where
  d≉0     = x≉0∨y≉0⇒gcd≉0 isGCD nz⊎nz
  q₁*dc≈x = begin
    q₁ * (d * c)    ≈⟨ Of*CSemig.x∙yz≈xz∙y q₁ d c ⟩
    (q₁ * c) * d    ≈⟨ *-congʳ q₁c≈quot₁ ⟩
    quot₁ * d       ≈⟨ quot₁∙gcd≈x ⟩
    x               ∎

  q₂*dc≈y = begin
    q₂ * (d * c)    ≈⟨ Of*CSemig.x∙yz≈xz∙y q₂ d c ⟩
    (q₂ * c) * d    ≈⟨ *-congʳ q₂c≈quot₂ ⟩
    quot₂ * d       ≈⟨ quot₂∙gcd≈y ⟩
    y               ∎

  dc∣x = q₁ , q₁*dc≈x
  dc∣y = q₂ , q₂*dc≈y
  c∣1  = let
           (q , q*dc≈d) = greatest dc∣x dc∣y
           d*qc≈d*1     = begin
             d * (q * c)   ≈⟨ Of*CSemig.x∙yz≈y∙xz d q c ⟩
             q * (d * c)   ≈⟨ q*dc≈d ⟩
             d             ≈⟨ sym (*-identityʳ d) ⟩
             d * 1#        ∎

           qc≈1 = *-cancelˡ-nonZero {d} (q * c) 1# d≉0 d*qc≈d*1
        in
        q , qc≈1

to

x∣y∧z∣x/y⇒x*z∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x * z ∣ y 
x∣y∧z∣x/y⇒x*z∣y {x} {y} {z} (x/y , x/y*x≈y) (p , p*z≈x/y) = p , (begin
  p * (x * z)  ≈⟨ Of*CSemig.x∙yz≈xz∙y p x z ⟩
  (p * z) * x  ≈⟨ *-congʳ p*z≈x/y ⟩
  x/y * x      ≈⟨ x/y*x≈y ⟩
  y            ∎)

x*y∣x⇒y∣1 : ∀ {x y} → x ≉ 0# → x * y ∣ x → y ∣ 1#
x*y∣x⇒y∣1 {x} {y} x≉0 (q , q*xy≈x) = q , *-cancelˡ-nonZero (q * y) 1# x≉0 (begin
  x * (q * y) ≈⟨  Of*CSemig.x∙yz≈y∙xz x q y ⟩
  q * (x * y) ≈⟨  q*xy≈x ⟩
  x           ≈˘⟨ *-identityʳ x ⟩
  x * 1#      ∎)

x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd]2 : ∀ {x y d} → x ≉ 0# ⊎ y ≉ 0# →
                                ((isGCDᶜ (q₁ , _) (q₂ , _) _) : IsGCD x y d) →
                                Coprime q₁ q₂
x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd]2 x≉0∨y≉0 gcd@(isGCDᶜ d∣x d∣y greatest) x/d∣z y/d∣z =
  x*y∣x⇒y∣1 (x≉0∨y≉0⇒gcd≉0 gcd x≉0∨y≉0) (greatest
    (x∣y∧z∣x/y⇒x*z∣y d∣x x/d∣z)
    (x∣y∧z∣x/y⇒x*z∣y d∣y y/d∣z))

Can you see the difference? There's significantly less code duplication and I've split out the sub-results into useful lemmas that can be re-used by other proofs. In contrast your proof is brittle as it relies on implementation details of the divisibility relation, hard to understand and therefore difficult to refactor.

Please do the same for this proof.

[MatthewDaggitt]

Just brought back up to date with master. Just to note that from now on I'm going to be more strict in not providing a detailed review until the code conforms to the conventions of the style guide. I'm also not going to be providing in depth explanations of style-guide violations that we've discussed with you before.

[MatthewDaggitt]

What is the final solution for the record constructor names : isGCDᶜ or mkIsGCD ?

We decided on mkIsGCD

[mechvel]

Please, consider my commit of January 30, 2021.
All your notes are taken in account.
My replies are coming soon.

[mechvel]

1. isGCDᶜ replaced with mkIsGCD everywhere.
2. A couple of your notes occur repeated above, I do not know why.

See my replies above.

[mechvel]

Aren't we using ∨ in names?

Probably, yes, but I am not sure.
Anyway I replace now ⊎ with ∨ (disjunction) everywhere in names.

[mechvel]

Please, consider my commit of February 2, 2021.
All your notes are implemented, except the ones for which I provide questions.
My notes are inserted above.

And the first note is here:
I see now that IsGCD occurs defined in two different modules -- !?
Probably it needs to be only in RawMagma (?)
The next commit will have too fix this and may be other issues.

[MatthewDaggitt]

@mechvel if it's okay with you I'm going to remove the GCD parts of this PR and merge in the stuff that's ready to go. If you come back to the GCD proofs at some later point, you can open a new PR.

[mechvel]

if it's okay with you I'm going to remove the GCD parts of this PR and merge in the stuff that's ready to go.

All right.