`Data.Nat.Base._≤″_` and `Algebra.Definitions.RawMagma._∣_`

[jamesmckinna]

So... ... part of issue #1726 was a concern about the proliferation of (allegedly) useful variants on the usual ordering relation on Nats. Yet another one of these, _≤″_, is nothing more or less than the (abstract, algebraic) divisibility ordering induced by the (raw) _+_, _≡_-monoid (magma) structure, while (usual) divisibility is... the same for the (raw) _*_, _≡_-m... structure...

... three distinct representations of the 'same' algebraic concept, differing even up to the direction of the underlying equality, records vs. ∃ for packaging up the data, different field names, ... etc.

Now that Data.X.Base modules #1810 (for better or worse) expose their underlying Raw structure/bundle(s), ... Is it time to reconsider whether the above (non-)duplication is A Good Thing?

UPDATED: Aaargh! I've just discovered that this would be a reversion (and then some) of #192 / #196 ... groan. But I think the original reasons for that issue/PR no longer hold, not because the semantics of pattern-matching (and let in particular wrt records) has got so much more sophisticated since 2017... and the change proposed here, and embarked upon in #2013 is 'only' to replace a custom record with a Σ-type, so I don't think it should cause a problem?

... still: :facepalm: those who forget the (lessons/mistakes of the) past are condemned to repeat them...

[deleted: attached to the wrong issue]

[jamesmckinna]

Oh... and the underlying adjunction structure across the ordering to define monus, quotient, etc.

[JacquesCarette]

So I'm quite pro having alternate representation of things, but I'm not fond of stuffing them all in .Base. I would prefer seeing a Data.Nat.Extra (I'm not wed to that name) where this is defined. I strongly dislike having .Base modules filled with seldom-used things.

So, for me:

• alternate representations are good and belong in the library
• they don't belong in the core

[jamesmckinna]

Jacques, [UPDATED with code spans] I certainly agree as regards alternative representations, where the alternatives are actually mathematically distinct, so indeed it's ok by me for there to be 5 distinct representations if _<_on Nat (I think IIRC , Matthew found five to be two too many), wherever they end up being put (but yes, some quarantining away from *.Base seems a Good Idea)

But the issue here is that, for this definition of _<″_ (in terms of a partial inverse to addition), and that of divides _∣_ on Nat, and that of abstract divisibility on magmas, these are all the same definition, but represented in inessentially distinct ways: records vs. products, different field names in the record representations, which direction is given to the representing equation underlyling the relation, etc.

Now these considerations are not inessential inasmuch as Agda doesn't allow field names to be renamed (or does it?) although one can rename field names (that's a good start), inasmuch as the direction of an equation affects how it is used, the left/right order in the application order of the magma operation similarly, and whether fields/argument positions are marked implicit/explicit etc. but those are surface considerations to my mind, to do with a pragmatic layer on top of the underlying semantics...

... so the 'issue' at hand for me is about clarifying, simplifying, and improving the abstract interface given by their common semantics (instantiated at different magma structures, to be sure, but that's the only point of variation), and only specialising the pragmatic aspects in each deployment context.

TL:DR Better reuse through better abstraction!

[JacquesCarette]

I did not understand that the main point of this issue are those inessential differences. Your comment above laid them out somewhat more clearly, but could you do so even more explicitly? Github markdown allows you to link to source code spans, which go a very long way towards being precise about describing such issues in detail.

[JacquesCarette]

Thanks for the edits: I now understand the issue much better.

I've basically already written up my (shared) opinion in the paper Realms: A Structure for Consolidating Knowledge about Mathematical Theories. TL;DR: I think that this kind of duplication is good. We know that there are many settings where there are equivalent presentations of concepts, but the presentations have inequivalent usability profiles, i.e. in different contexts, one may wish to switch which presentation is smoother to work with.

The road to getting a system where one can smoothly choose between equivalent presentation requires a lot of engineering still (don't listen to the HoTT folks who say that the Structure Identity Principle (SIP) says the problem's solved -- SIP merely says that in a nice enough meta-theory, a solution is theoretically well-founded and may be feasible and then stops dead. Realms encompass a broader view of 'equivalence' as well.)

One of the interesting things about Lean is that there's 100:1 library developers to system developers. Another interesting thing is that the system developers pay really close attention to what is stopping the library developers from being even more productive and change the system to improve things. And it is done correctly: the system developers don't give the library developers what they say they need, but rather what they seem to actually need, distilled through the 'good taste' of highly experienced language developers.

Coming back from that side-comment to the issue at hand: I do think kind of duplication is a good thing. And that we don't quite know how to make it all 'work'. And that it will require experimentation. Picking a single "blessed" representation is, as far as I'm concerned, a false choice. Picking a "principal" representation to go into *.Base is a necessary evil that we don't have the tools to avoid. Polluting *.Base with equivalent definitions also seems bad.

In the far future, should we have all sorts of meta-programming-like features that let us navigate these waters smoothly? Absolutely! Are we close? Nope. We don't even really know what the spec is, we just have a whole lot of examples.

[jamesmckinna]

Hmmm. I think we might still be at cross-purposes, inasmuch as I don't mind the lack of a 'single "blessed" representation' of ... well anything really.

But as I say in my opening remarks on the 'issue' (perhaps it isn't one any more, from your point of view), I find it strange to encounter 'abstract divisibility orderings' in various guises in concrete instances (wherever they may happen to have been put), without being able to recognise them as such, along with their (cf. Lambek calculus) properties (which do live under Algebra.Properties.*.Divisibility):

• IsSemigroup implies transitivity of the ordering;
• IsMonoid implies reflexivity;
• IsCommutativeMonoid implies 'left-divisible iff right-divisible'
• (right) adjoint operations across the ordering: eg m + p ≤ n ⇔ m ≤ n ∸ p etc.

Perhaps this comes from a too-early exposure to Mathematics Made Difficult ... before I could see the joke.

[JacquesCarette]

Ah yes, now I see where you're coming from, I think. Let me rephrase:

Should we prove many things using as simple as possible proofs, without leaving any traces that the deeper reason it is true?

It's a very tempting, very slippery slope, to obtain many (many!) results by instantiating various levels of abstract nonsense. It helps hugely with the size of the code base, and the overall maintenance effort (there's just fewer things to prove). It also hinders two things a lot:

1. recruiting future maintainers (who might feel they need 3 Ph.D.s to understand any part of the library. Right now, barely over 1 is needed...
2. having anyone use the library for pedagogical reasons.

You can't learn anything from reading Coq proofs, not unless you've invested a huge amount of time in it. There are extremely few printed-on-paper Coq proofs because of this. They are 'only' understandable when interactively replayed. (Oversimplification, I know.) Agda proofs, on the other hand, are frequently quite readable, at least if the author made some effort to make them so.

Instantiating from the 'true' result in higher mathematics has a strong pull for me. I have resisted doing so. It would be a very interesting experiment indeed. My current feeling: it would be a neat agda-alternate-lib project. That I'd love to work on...

[jamesmckinna]

Yes, perhaps, but even more so than you describe: it's not, for me, even about proofs, but about definitions...

[JacquesCarette]

Ah, indeed - I'm on board for that as well.

[jamesmckinna]

A separate issue: the equality in the definitions in Data.Nat.Divisibility is the 'wrong' way round wrt the direction in Algebra.Definitions.RawMagma, so the pattern synonym tricks I used in #1948 won't work for reconciling these two developments. Suggestion welcome as to how to proceed!?

[JacquesCarette]

Can you link in to the exact clashing lines? I'm not immediately seeing the clash.

[jamesmckinna]

Added line refs above. TL;DR: in Data.Nat.Divisibility.Core, the equality defining the quotient structure goes from the number being divided on the LHS to its expression as a composite on the RHS.

In Algebra.Definitions.RawMagma, it's the other way round (plus using Sigma rather than an explicit record type). So that's fine as far as proofs are concerned, but not fine for defining pattern synonyms to apply sym to the equations .

My tentative proposal would be to reverse the direction in Data.Nat.Divisibility.Core, despite this having the greater knock-on viscosity. My reasoning being that:

• many of the arguments appeal, implicitly or explicitly, to sym anyway;
• the main heavy lifting done in proofs based on pattern-matching ondivides actually take a reflexive proof of equality, so are agnostic wrt symmetry
• (so, in any case, there's an opportunity (see PR #2013) for conceptual optimisation by introducing a pattern synonym for this common case)

Contra:

• the Algebra definitions go against the 'unfold from LHS to RHS' design heuristic to express the arbitrary divisible quantity as a concrete product.
• the knock-on viscosity would be much lower; currently the definitions are imported only by Algebra.Definitions.RawMonoid and Algebra.Properties.{Magma|Semigroup|Monoid}.Divisibility (excluding third-party clients), AFAICT...

[JacquesCarette]

Certainly having to use sym more often than not is a sign that the equality is the "wrong way around". That certainly argues strongly in favour of flipping that one.

Oddly, I would be tempted to flip the one in Algebra too, even though that would keep the clash still there, just flipped! There ought to be good reasons to go against the "design heuristic". But maybe the argument exists, and it is right above: in actual use, we want to "expand things out" when dealing with divisibility. [This might indicate that similar flipping might occur for minus too.]

[jamesmckinna]

(More) Food for thought; if one were to keep the record definition, then an option (too horrible!?) would be to cache a symmetric equality proof in the record, and deploy whichever was required? But I don't immediately see how one might simulate that with the Sigma typed version under Algebra...?

[JacquesCarette]

I like the idea - but I think this is really an Agda-level design discussion. Having easy access to "conservative extensions" is nice, especially if the system knows that it is definitional. I'd hate to open the door for people to store incoherent proofs because we intended these to be 'caches'.

[jamesmckinna]

I should really have split out the _*_/Divisibility version of this issue (embarked upon in #2013) from the _+_/_≤_ one (achieved in #1948). Apologies for the muddle!