Add Data.Nat.Bounded

[jamesmckinna]

Prompted by a recent discussion on the Agda Zulip, and realising that we don't actually have the details of this spelt out in Data.Fin as such...

... and I decided to post it as a PR directly, rather than go via a separate issue first.

Outstanding issues:

• names? (eg. why can't I call the value field ⟦_⟧ directly?)
• where should this live? It even occurred to me that this might belong purely as a README contribution?
• does this even stand on its own feet, or should it simply be refactored as a README.Data.Refinement example of Data.Refinement?
• I tried writing isBounded as a manifest field, but Agda complains that it needs the unsafe --irrelevant-projections flag to do this, whereas the pattern-matching version is fine? issue raised as [bug?] Mismatch between pattern-matching and manifest record field requiring unsafe irrelevant projection? agda#7063
• the version of fromℕ< here as a possible improvement on Data.Fin.Base.fromℕ<;
• DONE: proof of the isomorphism witnessed by toFin/fromFin;
• DONE: proof of the retraction witnessed by toℕ/fromℕ;
• DONE: added support for Number literals; cf. Literals for any ring? #1363 , ahead of any Structures/{Raw}Bundles instances...
• DONE: arithmetic modulo n Modular arithmetic #581 , based on this design, at: https://github.com/jamesmckinna/agda-stdlib/blob/modular-arithmetic/src/Data/Integer/Modulo.agda (will raise separate PR when/if this gets approval) see Modular arithmetic based on Data.Nat.Bounded #2257 #2292 ;
• other things that may occur to you ;-)

If approved, then I would refactor to reflect the customary Data.X.Base|Properties|Literals|Show|... hierarchical decomposition... DONE

Comments welcome!

[Taneb]

I don't think we very often have instances floating around of type a < b. Does this get inferred often?

[jamesmckinna]

Well, that had been my thinking underlying #1998 and (the reverted parts of) #2000 ... but indeed reimplementing this via Data.Refinement wouldn't introduce that extra twist. I had the ... even 'gut feeling' seems a bit strong ... sense that in suitable deployment contexts (fixed-width arithmetic; positional notation for numerals; ...) it might be the case the ambient instances would be available from the context ... but perhaps you're correct... UPDATED: unless it's replaced by #2000 's T (value <ᵇ n)?

[JacquesCarette]

I like the idea of adding BoundedNat as an equivalent for Fin, but I think the 'experiment' of using an instance for bounded is premature.

Supporting evidence: in code that Conor and I were playing around with, we had exactly BoundedNat in our extensional universe as our definition of Fin, and we did have to supply the proof a non-trivial number of times. (That the proof was irrelevant without needed Agda's irrelevance machinery was what we were really after.)

[jamesmckinna]

OK, so that's two of you... so either:

• I remove the instance bracketing (easy);
• I go all-out for T (value <ᵇ n) as above (more involved, but most of the machinery is already in Refactoring (inversion) properties of _<_ on Nat, plus consequences #2000 )

I guess it's the first choice, then, with the second as a possible downstream refactoring? DONE.

[jamesmckinna]

NB making bounded an 'ordinary' (even if irrelevant) field vitiates somewhat my choice of ⟦_⟧< as a constructor, which could be used 'bare', without bracketing, as a pattern constructor, in favour of ⟦_⟧<_ with the explicit bound argument, and the value argument position now mostly redundant... oh well. The redundancy is harmless, unless someone else has a compelling improvement on my notation?

[jamesmckinna]

The addition of a Number instance with Constraint m = T (m <ᵇ n) biases towards the second alternative...
... but stdlib style suggests using True (m <? n) instead... cf. Data.Fin.Literals

Any comment on the trade-offs between the two, given that the latter is much more indirect than the former...?

[JacquesCarette]

I like the idea of adding BoundedNat as an equivalent for Fin, but I think the 'experiment' of using an instance for bounded is premature.

Supporting evidence: in code that Conor and I were playing around with, we had exactly BoundedNat in our extensional universe as our definition of Fin, and we did have to supply the proof a non-trivial number of times. (That the proof was irrelevant without needed Agda's irrelevance machinery was what we were really after.)

[MatthewDaggitt]

So to touch on your question of whether this belongs in the library or a readme file, I guess my question is what circumstances is this easier to work with than Fin? In general we try to avoid duplicate but equivalent definitions unless there is clear reason that sometimes one representation is easier to work with than the other...

[jamesmckinna]

Thanks, Matthew! I can think of two or three, some already in the initial preamble (which was really about helping someone solve a related problem of representation, where Fin didn't seem to fit well):

• fixed-width arithmetic (or even: its extension to variable-widths, but in a way which retains predictable/computable bounds);
• Digit bases for arithmetic, as a specialised instance/mode of use of the above;
• revising the 'specification' of Data.Nat.DivMod, to avoid the marshalling/unmarshalling required by the use of Fin to ensure that mod is suitably bounded.

Now, none of these could be said to be a deal-breaker, but I increasingly wonder whether Fin is better suited to its use as an indexing type (for Vec, List, de Bruijn representations, Reflection/deeply embedded syntaxes more generally, etc.), with ℕ< as an arithmetic type/Number instance... cf. #2073 which I might now think makes the 'wrong' choice in using Fin...

Perhaps other pros (and cons!) might be lurking off-stage...
... UPDATED: (pro)

• re: 3rd point above. This might (eventually) lead to the deprecation of Data.Nat.DivMod.WithK (no longer any need to consider erasing proofs of _≤″_...?) and hence perhaps to the deprecation of _≤″_ altogether, cf. Remove (almost!) all external use of _≤″_ beyond Data.Nat.* #2262
• Modular arithmetic! (See link to draft branch at top)

[jamesmckinna]

Previously...

... UPDATED:

* re: 3rd point above. This might (eventually) lead to the deprecation of `Data.Nat.DivMod.WithK` (no longer any need to consider erasing proofs of `_≤″_`...?) and hence perhaps to the deprecation of `_≤″_` _altogether_, cf. [Remove all external use of `_≤″_` beyond `Data.Nat.*` #2262](https://github.com/agda/agda-stdlib/pull/2262)

This cashes out as the following breaking (because type-signature-changing... hence not committed to this PR) simplifications to Data.Nat.DivMod and Data.Nat.DivMod.WithK:

record DivMod (dividend divisor : ℕ) : Set where
  constructor result
  field
    quotient  : ℕ
    remainder : ℕ< divisor
    property  : dividend ≡ ⟦ remainder ⟧ + quotient * divisor

  nonZeroDivisor : NonZero divisor
  nonZeroDivisor = nonZeroIndex remainder


infixl 7 _div_ _mod_ _divMod_

_div_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
_div_ = _/_

_mod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ< divisor
m mod n = ⟦ m % n ⟧< (m%n<n m n)

_divMod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} →
           DivMod dividend divisor
m divMod n = result (m / n) (m mod n) $ m≡m%n+[m/n]*n m n

and (WithK)

_divMod_ : (dividend divisor : ℕ) → .{{ NonZero divisor }} →
           DivMod dividend divisor
m divMod n = result (m / n) (m mod n) $ ≡-erase $ m≡m%n+[m/n]*n m n

Suggestions on how to proceed, if, like me, you find these compelling.

[jamesmckinna]

I think I proved Bijective believing that to proxy for Isomorphism (of Propositional setoids), and that to be stronger than Equivalence. But... @JacquesCarette , suitably chided by your "wow", perhaps you should school me in what I should have proved instead... (and see previous discussions about my obliviousness/lack of skill with the Function.* hierarchy...)

[jamesmckinna]

This section might benefit from some (more intelligent) refactoring, but I made these last two commits in order to make this PR disjoint from #2292, against that one not being merged.
Latest commit refactors.

[jamesmckinna]

In the event that #2292 is not merged, then the Semiring structure of ℕ< should be developed as a followup PR to this one, by analogy with the Ring development there, so the additional arithmetic lemmas are stubs towards such eventual downstream development. But I'll definitely stop here now.

[JacquesCarette]

If you're going to keep tweaking a PR, you should mark it as Draft. That doesn't prevent us from reviewing, but it will make our expectations match reality.

[jamesmckinna]

Of course you're right re: tweaking, so apologies for this.
I was spooked by wanting to disconnect this PR from #2292 after @Taneb 's comments on that.

[jamesmckinna]

Aaargh... CHANGELOG hell. (Partly self-inflicted; hopefully this will converge soon)

[gallais]

I think we should use Data.Irrelevant because we don't have irrelevant projects and so manipulating these
records is annoying in my experience.

[jamesmckinna]

Well, in that case, it's probably better simply to define this as an instance of Data.Refinement?
That being so, I'll reconvert to DRAFT and take it off the v2.2 table for the time being...