Add Data.Nat.Bounded
#2257
Add Data.Nat.Bounded
#2257
Conversation
src/Data/Nat/Bounded.agda
Outdated
| constructor ⟦_⟧< | ||
| field | ||
| value : ℕ | ||
| .{{bounded}} : value < n |
There was a problem hiding this comment.
I don't think we very often have instances floating around of type a < b. Does this get inferred often?
There was a problem hiding this comment.
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)?
There was a problem hiding this comment.
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.)
There was a problem hiding this comment.
OK, so that's two of you... so either:
- I remove the
instancebracketing (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_<_onNat, plus consequences #2000 )
I guess it's the first choice, then, with the second as a possible downstream refactoring? DONE.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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...?
src/Data/Nat/Bounded.agda
Outdated
| constructor ⟦_⟧< | ||
| field | ||
| value : ℕ | ||
| .{{bounded}} : value < n |
There was a problem hiding this comment.
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.)
|
|
||
| {-# OPTIONS --cubical-compatible --safe #-} | ||
|
|
||
| module Data.Nat.Bounded where |
There was a problem hiding this comment.
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...
There was a problem hiding this comment.
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);
Digitbases 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 ofFinto ensure thatmodis 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_≤″_beyondData.Nat.*#2262 - Modular arithmetic! (See link to draft branch at top)
|
Previously...
This cashes out as the following 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 nand ( _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 nSuggestions on how to proceed, if, like me, you find these compelling. |
|
I think I proved |
|
Am now in a (better) position to prove the two lemmas relating |
src/Data/Nat/Bounded/Properties.agda
Outdated
| module _ .{{_ : NonZero n}} (m o : ℕ) where | ||
|
|
||
| open ≡-Reasoning | ||
|
|
||
| +-distribˡ-% : ((m % n) + o) ≡ (m + o) modℕ n | ||
| +-distribˡ-% = %≡%⇒≡-mod $ begin | ||
| (m % n + o) % n ≡⟨ ℕ.%-distribˡ-+ (m % n) o n ⟩ | ||
| (m % n % n + o % n) % n ≡⟨ cong ((_% n) ∘ (_+ o % n)) (ℕ.m%n%n≡m%n m n) ⟩ | ||
| (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ | ||
| (m + o) % n ∎ | ||
|
|
||
| +-distribʳ-% : (m + (o % n)) ≡ (m + o) modℕ n | ||
| +-distribʳ-% = %≡%⇒≡-mod $ begin | ||
| (m + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m (o % n) n ⟩ | ||
| (m % n + o % n % n) % n ≡⟨ cong ((_% n) ∘ (m % n +_)) (ℕ.m%n%n≡m%n o n) ⟩ | ||
| (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ | ||
| (m + o) % n ∎ | ||
|
|
||
| +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n | ||
| +-distrib-% = %≡%⇒≡-mod $ begin | ||
| (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ | ||
| (m + o) % n ∎ | ||
|
|
||
| *-distribˡ-% : ((m % n) * o) ≡ (m * o) modℕ n | ||
| *-distribˡ-% = %≡%⇒≡-mod $ begin | ||
| (m % n * o) % n ≡⟨ ℕ.%-distribˡ-* (m % n) o n ⟩ | ||
| (m % n % n * (o % n)) % n ≡⟨ cong ((_% n) ∘ (_* (o % n))) (ℕ.m%n%n≡m%n m n) ⟩ | ||
| (m % n * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ | ||
| (m * o) % n ∎ | ||
|
|
||
| *-distribʳ-% : (m * (o % n)) ≡ (m * o) modℕ n | ||
| *-distribʳ-% = %≡%⇒≡-mod $ begin | ||
| (m * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m (o % n) n ⟩ | ||
| (m % n * (o % n % n)) % n ≡⟨ cong ((_% n) ∘ (m % n *_)) (ℕ.m%n%n≡m%n o n) ⟩ | ||
| (m % n * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ | ||
| (m * o) % n ∎ |
There was a problem hiding this comment.
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.
|
In the event that #2292 is not merged, then the |
|
Aaargh... |
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.Finas such...... and I decided to post it as a PR directly, rather than go via a separate issue first.
Outstanding issues:
(eg. why can't I call thevaluefield⟦_⟧directly?)READMEcontribution?README.Data.Refinementexample ofData.Refinement?isBoundedas a manifest field, but Agda complains that it needs the unsafe--irrelevant-projectionsflag to do this, whereas the pattern-matching version is fine? issue raised as [bug?] Mismatch between pattern-matching and manifestrecordfield requiringunsafeirrelevant projection? agda#7063the version offromℕ<here as a possible improvement onData.Fin.Base.fromℕ<;toFin/fromFin;toℕ/fromℕ;Numberliterals; cf. Literals for any ring? #1363 , ahead of anyStructures/{Raw}Bundlesinstances...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 onData.Nat.Bounded#2257 #2292 ;If approved, then I would refactor to reflect the customary
Data.X.Base|Properties|Literals|Show|...hierarchical decomposition... DONEComments welcome!