Redefining `Data.Nat.DivMod.DivMod` about agda-stdlib HOT 10 CLOSED

So for starters, in the last 8 years I've never had any feedback that someone has actually used that specification. Furthermore, to be honest, I think we really haven't put enough effort into thinking about how to design the library around specifications of operations. If and when we do so, we will probably end up deprecating this definition anyway.

So in my opinion I think adding properties about it is pretty low priority... Having said that divMod⇒nonZero seems reasonable if you do really want to go ahead and add it.

from agda-stdlib.

So for starters, in the last 8 years I've never had any feedback that someone has actually used that specification.

Maybe @mechvel has?

but @andreasabel how much do you want this now? If not that much, suggest we close, as I had originally...

Not much. Sure.

from agda-stdlib.

Maybe because this would be redundant? NonZero divisor is a trivial consequence of DivMod:

------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of DivMod
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Nat.DivMod.Properties where

open import Data.Nat using (ℕ; suc; NonZero)
open import Data.Nat.DivMod using (DivMod)

divMod-non-zero-divisor : {dividend divisor : ℕ}
   → DivMod dividend divisor
   → NonZero divisor
divMod-non-zero-divisor {divisor = suc _} _ = _

Shall I PR this, @MatthewDaggitt ?

from agda-stdlib.

Ha! Of course, using the Fin-typed field ... I'm not thinking clearly. Thanks, I'll close...

from agda-stdlib.

On second thoughts (and stifling the instinct to hide my stupidity 🤦 ), please feel free to file a PR... not sure what @MatthewDaggitt will say!

from agda-stdlib.

Maybe @MatthewDaggitt or @gallais has some advice where to place this lemma and how to name it...

from agda-stdlib.

Given I only tagged the issue as v2.0 for the sake of it being a breaking change, which it turns out not to be, I suspect this will in any case get pushed to v2.1 at the earliest.
Regarding naming: I'd be tempted by divMod⇒nonZero (plain nonZero seems a hostage to fortune)
Regarding placement: given the addition, it probably makes most sense to leave in-place in Data.nat.DivMod?

Alternatively, I suppose it could simply be added as a manifest field of the record DivMod:

record DivMod (dividend divisor : ℕ) : Set where
  ...

  nonZero : NonZero divisor
  nonZero with remainder
  ... | zero  = _
  ... | suc _ = _

UPDATED: better still, a new lemma in Data.Fin.Properties

nonZero : Fin n → ℕ.NonZero n
nonZero {n = suc _} _ = _

and then the above manifest field reduces to DivMod.nonZero = Fin.nonZero remainder...

from agda-stdlib.

Well, once it was pointed out to me that it's an admissible property, I was certainly less committed to it ;-) but @andreasabel how much do you want this now? If not that much, suggest we close, as I had originally...

As for the discussion of the specification vs. implementation, its only use as I understand it is in Data.Nat.DivMod.WithK, where the remainder field is (re-)implemented with an erasing version fromℕ<″ but I think that even that might better be reconsidered down the road at some point...?

from agda-stdlib.

As I understand it, @mechvel uses the binary representations of natural numbers and general algebraic structures in their project...

from agda-stdlib.

As I understand it, @mechvel uses the binary representations of natural numbers and general algebraic structures in their
project...

So far, I used Nat/Binary only once, for programming the binary method for powering in Monoid.
And I do widely use general algebraic structures of Standard, and also implement further classical structures:
DecCommutativeRing, IntegralDomain, EuclideanDomian, Field, FactiorizationDomain, and such.

As to Data.Nat.DivMod, my project relates to it as follows. I define the format

DivRem :  Set _                                                                 
DivRem =  C → (y : C) → y ≉ 0# → C × C                                          

under the environment of any DecIntegralDomain. My impression is that this direct usage of y ≉ 0# is better that various tricks with a particular usage of Nonzero, with taking suc in account (which does not exist in many popular domains), with searching instances by {{....}}, and with defining these instances.

Then, the abstract EuclideanDomain includes divRem : DivRem.
The EuclideanDomain instance for ℤ includes the instance of divRem, and this instance implementation still uses the items from Data.Nat.DivMod this way:

quotₙ :  ℕ → (n : ℕ) → n ≢ 0 → ℕ                                                   
quotₙ m n n≢0 =  _/_ m n {fromWitnessFalse n≢0}  

remₙ :  ℕ → (n : ℕ) → n ≢ 0 → ℕ                  
remₙ m n n≢0 =  _%_ m n {fromWitnessFalse n≢0} 

(using lib-1.7.3). I just use the instances of divRem, and sometimes I am forced to prove irrelevance of certain results on the proofs for y ≉ 0#
(In the definition of IsEuclideanDomain, this irrelevance for the quotient is also required as axiom).
I do not really know of whether the Standard library approach to Nat.DivMod is the best on not, whether it is in 1.7.3 or in 2.0.
I am going to change respectively the implementation of quotₙ : ℕ → (n : ℕ) → n ≢ 0 → ℕ
depending on the way the items in Nat.DivMod are defined in Standard.

from agda-stdlib.