Comments (10)
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.
Related Issues (20)
- Add bundles for lattice-like and module-like morphisms
- Document `variable` block indentation style HOT 5
- [DRY] what's the best way to `public`ly re-export properties/structure? HOT 5
- Use the Monoid structure of Endomorphisms to define powering HOT 1
- [DRY] More redundant `zero` fields in `Algebra.Structures`
- Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole HOT 5
- What's the 'right' notion of equality between functions? HOT 7
- [DRY] Refactor `Algebra.Solver.*Monoid` (or deprecate entirely?)
- Rename `WeaklyDecidable`? HOT 4
- Add `Algebra.Properties.IdempotentCommutativeMonoid`
- Naming of new functions `tail∘inits` and `tail∘tails` HOT 5
- comments on lib-2.1 candidate 1 HOT 9
- Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer HOT 7
- Style for lower/upper case for initial letter in denotations HOT 7
- Restore missing proofs from `Algebra.Operations.CommutativeMonoid`
- Proofs in `Data.Vec.Properties` take general properties as inputs HOT 23
- Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365 HOT 3
- [DRY] Refactor the various definitions of 'pointwise' equality on functions/`Function`s/pointwise `Algebra`s HOT 2
- Data.Nat.Properties.≤-total should be implemented with _<ᵇ_ HOT 14
- Data.List.upTo/applyUpTo can be made faster HOT 5
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda-stdlib.