Modular arithmetic based on Data.Nat.Bounded #2257

[jamesmckinna]

Adds:

• Data.Integer.Modulo.{Base|Literals|Properties} ;
• extra material to, and refactors, both Data.Nat.Bounded.Base and Data.Nat.Bounded.Properties; no CHANGELOG for these revisions, given the recency of the (hypothetical/proposed) additions of those modules;
• proves there is IsRing structure/Ring bundle based on integers modulo

Outstanding issues (could be tackled mostly/all by downstream PRs):

• upstream: depends (sort of) on merge of Add Data.Nat.Bounded #2257 ; merge conflict in CHANGELOG (now fixed);
• addition: Commutative properties of addition and multiplication;
• addition: DecSetoid structure;
• addition: proving that the quotient map fromℤ gives rise to a RingHomomorphism (or that there's a SemiringHomomorphism based on the quotient map fromℕ...);
• addition: README.Data.Integer.Modulo etc.;
• refactoring: equational reasoning mod n isn't developed in terms of Relation.Binary.Reasoning.Syntax;
• refactoring: streamlining of the infrastructure... esp. concerning equational reasoning and further algebraic/congruence properties;
• 'inefficient' representation by reference to ℕ, so no attempt to consider efficient 'wide' Word64-(or better)-sized modulus cf. Modular arithmetic #581

But all of this should be consider provisional until we've achieved consensus on the what, where, and how, of tackling #581 (see @Taneb 's comment below).

[Taneb]

I, personally, don't like implementing modular arithmetic this way, for two actual reasons and one emotional reason:

• This is doing a division after every operation, which can slow things down a lot if you're doing a lot of additions, say. In my view it's better to only reduce occasionally or before an operation where the size of the operands really matters
• It doesn't readily generalize to other rings. One of my formalization goals is the AKS primality test, which relies on polynomials considered modulo a polynomial
• (the emotional reason) I think my approach is better (for the preceding two reasons) and I'm annoyed you're grabbing the module name before I've gotten a chance

[jamesmckinna]

@Taneb thanks for the frank feedback, and I do get both the rational and emotional sides of it.

Re: definition via quotient rings, so that you can get polynomial ideals, absolutely, absolutely, absolutely. But until that development comes home, the lack of modular arithmetic has been a years-long embarrassing gap in the library. But I'd be entirely happy to be patient rather than agitate to have this merged, and indeed to convert to Draft (it's in any case blocking on Data.Nat.Bounded, which I am tempted to push harder on, in that case, with the additions from this PR pushed to that one), although I do still welcome other/more feedback on the PR. Especially those parts of it (eg the definition of _~_ which does generalise to rings, unless I am mistaken? especially even in the underlying notion from Data.Nat.Bounded, with the 'middle' term {k} : ℕ< n replaced by an element of the ideal, and the /~≡ view generalising to arithmetic in the ring) which can be (intelligently/critically) reused... ; NB. bearing in mind that my approach deliberately avoids what I thought were potential culs-de-sac/pitfalls in amongst the discussion on #581 .

Re: efficiency. @JacquesCarette has already made the point that it would be good to have one model for 'easy' verification, with others for 'efficient' implementation... but again, absent the latter...
... but I do agree that 'normalising' eagerly on every operation is clearly ordinarily, never mind asymptotically, absurd; but that's also true for binary addition and multiplication generally, when it's much better to consider n-ary operations, with staging/partial evaluation to improve their performance, never mind frex-like approaches to organising all the data for such, coupled with Reflection machinery, cf. the polynomial representations in the RingSolver implementations etc. But I haven't seen evidence, other than in the backend(s), for taking the computational efficiency (except wrt typechecking in the Algebra.*.*.*.TCOptimised modules) of algebraic operations seriously. But this latter point may reflect my ignorance of the wider Agda ecosystem engineering/design principles.

Re: emotion. Contrary perhaps to appearances, I've no (over-)commitment to where things live, so if you feel I'm squatting on an important part of the namespace/concrete hierarchy under Data.Integer, then happy for us to have that discussion! It seems to me that there ought to be a place for the (instantiation of) Ring theory (developed under Algebra.Properties.Ring?) for any concrete instance of Ring to be able to peacefully coexist with other concrete implementations (esp. wrt the proof/efficiency trade-offs already alluded to). So a good discussion, with or without any extra emotional baggage, would be one concerning where should things live as the library starts to grow in (algebraic) maturity. And I'm sure the other maintainers will have good insights/proposals to offer on that topic...

[jamesmckinna]

Re: inefficiency (@Taneb 's comment above)

• for addition, since we can get overflow by at most n, the normalisation step can be made a 'simple(r)' subtraction, rather than invoke the quotient map directly
• for multiplication, we'd need to iterate over the previous step (so a bit of crunchiness/over-concreteness about how multiplication is implemented, rather than working 'abstractly' via the quotient)