agda-stdlib
agda-stdlib copied to clipboard
agda
Additional DivMod proofs.
Hello there.
I would like to explore a contribution to the standard library. I have a few DivMod proofs that I use all the time and that I think others might find useful.
I'm not sure, though, whether my Agda skills and mathematical reasoning are sufficiently mature. So, feel free to just close the pull request, if the proofs don't meet the library's standards.
If the proofs are OK, then I'd like some guidance on two dependency issues, please. Lines 103 and 342 currently contain commented-out code:
- Line 103 is in the % section of the file, but requires a proof from further down in the / section of the file.
- Line 342 requires a proof from
Data.Nat.Divisibility, which leads to a circular dependency.
Are there any standard ways to deal with dependency issues like this?
The proofs type-check with Agda 2.6.2.2 as well as with current master.
Oh, wait! What was I thinking! The proof from Data.Nat.Divisibility is trivial. I fixed line 342 simply by inlining the proof. Which gets rid of the circular dependency. I pushed the change.
Which leaves the ordering issue in line 103, which refers to a proof further down in the file.
Hmmm. I'm now having second thoughts about the ordering of the other proofs as well. Maybe it would be wiser to create a new file for these more complex proofs that depend on the simpler proofs from Data.Nat.DivMod? Something like Data.Nat.DivMod.Properties?
As I'm already asking for guidance, please allow for another question: Where does the standard library draw the line between what's to be included and what isn't?
As an example, I just added aonther potential proof that served me quite well: [m*n+o]%[p*n]≡[m*n]%[p*n]+o. (Yes, it could probably use a more concise name.) This particular proof has been useful for me when dealing with base-n numbers represented as fixed-length vectors. It basically says that you can pull out the least significant digit from under the % prescribed by the vector length. So, it's a little more niche than the other proofs. Would something like this still be interesting enough to be included in the standard library? Err on the side of including something? Or rather err the other way around?
Sorry for all the questions. I'm just trying to better understand how the standard library structures things and what goes into it and what doesn't.
FWIW, I went and checked the Coq standard library, and it does have variants of the last proof I added. I guess it's not just me who found it useful.
See mul_mod_distr_l in https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.NatInt.NZDiv.html .
Thank you for your encouragement and guidance!
I just pushed the changes. Let's see how much progress we made towards a final version.
Oh, wait. One more thing, in line 97: m*n≤o⇒[o∸m*n]%n≡o%n {m = o / pm * p} lem, where Agda cannot infer the implicit argument m.
Is the universe telling me here to make m an explicit parameter instead?
Oh! I seem to have caused a name clash with m/n/o≡m/[n*o] in Data.Nat.Divisibility.
I guess I should pick a different name for my proof, right? I assume that this is preferable over changing the proof's name in Data.Nat.Divisibility, as this would break existing proofs that depend on it.
Regarding the implicit m argument: I looked around and the Pattern Matching section of Inference in Agda seems to suggest that m, in fact, cannot be inferred: m only occurs in m * n, and * pattern-matches on its LHS, i.e., on m.
I'll make m explicit. Which leaves the naming conflict.
And again it shows that the hardest problem in computer science is... naming things!
Yes, the m/n/o≡m/[n*o] from Data.Nat.Divisibility is a bit of an imposter and should probably be called m/n/o≡m/[n*o]-terms-and-conditions-may-apply because of its divisibility precondition, but I guess that backward compatibility trumps that.
So I renamed mine to m/n/o≡m/[n*o]-nsa (no strings attached) for now, just to make CI go through. But then again, having "NSA" in a code base will likely start rumors of conspiracies.
Can anybody else think of a reasonable name?
I guess I should pick a different name for my proof, right? I assume that this is preferable over changing the proof's name in Data.Nat.Divisibility, as this would break existing proofs that depend on it.
So we're actually in luck! Unless I'm getting confused, it looks like your version is strictly more general than the one in Data.Nat.Divisibility right? In which case we can take advantage of the fact that we're preparing for v2.0 and break compatibility, by removing the one in Data.Nat.Divisibility. As long as we note it in the CHANGELOG, under the minor breaking changes section, it should be fine!
Otherwise, apart from that and the small comment above, it all looks good. All that's left is to add some entries in the CHANGELOG, describing the new functions.
Oh, great! Yes, I also think that the new version is strictly more general than the one in Data.Nat.Divisibility.
I'll remove the old version and I'll update the CHANGELOG.
Thanks again for your help!
Alright. I made the changes. I hope that I did the CHANGELOG modifications correctly.