Added Z mod n as Fin

[guilhermehas]

In Data.Integer.DivMod, there are already some properties of Z mod n, but in this pull request, it is represented as Fin n.

[jamesmckinna]

I'm hoping that #1923 will soon be merged, after which it might be easier to consider the 'carry' case of successor/addition in terms of the top/inject₁ view of Fin n. Moreover, that PR already commits a proof of inject₁≢fromℕ... as well as a sizeable chunk of machinery for streamlining the use of lower₁.

[jamesmckinna]

Thanks @Taneb for the reinforcement... I'd previously held off asking about proofs that Fin n, organised with a particular structure of modular arithmetic, satisfied the IsGroup... IsRing etc. axioms, but clearly that is what is eventually required. Towards a first label:addition PR, I agree that we should have more (all?) towards such a collection of Properties...

[guilhermehas]

I think I will wait for https://github.com/agda/agda-stdlib/pull/1923 to be merged to redefine all my solutions.

[jamesmckinna]

If you are going to wait for another PR to merge: suggest that you

• continue to push commits to your branch (as indicated, there's a lot more that might usefully be added to a PR like this one)
• but change your PR status to DRAFT, so that we don't expend reviewing credits ahead of time... ;-)

Good luck, and thanks in advance! Something along these lines has been missing for a long time now.

[laMudri]

Would it be possible to prove one big theorem that any results that hold about ℤ under the mod n equivalence relation also hold of this Fin n (up to propositional equality) representation? When I've tried to implement some modular arithmetic before, I've been left with the impression that the integers really are the right place to start, and that with Fin n, you get buried in cases for boundary checks, though I imagine that Fin n is useful in certain cases.

[Taneb]

@laMudri for that we'd need a definition of the mod n equivalence relation. I've been behind-the-scenes working on one but keep convincing myself I have the wrong definition for it. Currently working on one in terms of ring ideals - this would let us get, for example, the ring of polynomials over the integers modulo x^2 + x + 1 with the same code. But I don't think this PR needs to wait for that!

[jamesmckinna]

PR #1923 now successfully merged.

[guilhermehas]

@jamesmckinna , I have already made the modifications to the code using https://github.com/agda/agda-stdlib/pull/1923 .

[guilhermehas]

I added all of your suggestions if I am not missing anything.

[jamesmckinna]

Having now worked extensively on #2257 (and using it to sketch an implementation of ℤ mod n #2292) I realise that I can't be an objective reviewer of this PR. There may be room for aspects of each PR to be merged, but I no longer think that Fin n is the best way to represent the underlying Carrier of (any version of) ℤ mod n. Very happy to let others arbitrate between the various approaches, or come up with new ones (cf. the discussion on #581 )