generic Nonzero proposal

[mechvel]

The master lib of April 28, 2020 has NonZero for Integer, ℚ and maybe for other special domains.

I suggest to generalize this to IsNonzero : Pred Carrier _
and Nonzero = Σ Carrier IsNonzero,

declaring this for arbitrary Semiring. This can be put to Algebra.Properties.Semiring.
Motivation.

1. IsNonzero "happens" in various semirings.
2. The Nonzero subset in many semirings (the ones without zero divisors: Nat,Integer, and many
   others) is a monoid by _*_. This sub-monoid is often used, it is an usual construction applied
   to a (semi)ring.

Also I have an impression that they write in literature Nonzero rather than NonZero,
Nonempty rather than NonEmpty.
?

[MatthewDaggitt]

I'm happy for you to add the definition to Agelbra.Properties.Semiring if you'd like.

I suggest to generalize this to IsNonzero : Pred Carrier _
and Nonzero = Σ Carrier IsNonzero,

We should not generalise the existing examples in Nat, Integer and Rational however as using them would then rely on first proving that they're a semiring. They therefore would be unable to live in e.g. Data.Nat.Base.

Also I have an impression that they write in literature Nonzero rather than NonZero,

I think Non-zero appears the most in the literature, but that doesn't follow the naming conventions. If you feel strongly about it and submit a PR before v1.4 releases then I'm not bothered by you changing it to Nonzero.

[mechvel]

The generic IsNonzero : Pred Carrier _ can be defined only as _≉ 0#.
Because in an arbitrary semiring it does not hold ∀ x → 1 + x ≉ 0#.
So, that for Nat, there will be the two versions of IsNonzero and Nonzero.
May be, we rename NonZero of lib-1.3 to IsNonzero' ?
As to the `Is' prefix, probably it is needed to distinguish a predicate and a data of kind
Σ _ IsNonzero'.

Another point is that the approach of lib-1.3 with \top and \bottom and implicit Nonzero for Nat
cannot be applied in general. May be it is better to write _≢ 0 everywhere in Nat.Base ?
And in further modules to use only IsNonzero and Nonzero of general?

[mechvel]

I have committed this PR.
I hope that it does not override the PR of Binary.DivMod.
I have entered https://github.com/agda/agda-stdlib and clicked at Fork.
Then I created the folder foo/NonzeroPR/ on my machine and commanded

cd NonzeroPR
git  clone https://github.com/mechvel/agda-stdlib agda-stdlib-fork
...

And now there are the folders

foo/adga-stlib-fork/           
foo/NonzeroPR/adga-stlib-fork/ 

on my machine. And I hope that they present the two independent branches and two independent PR-s. If so, then this is a great achievement.

[gallais]

You have pushed the change to the divmod PR

[mechvel]

I am sorry.
If the Binary.DivMod PR has not disappeared, then, please, consider this DivMod.
If you also can add there Algebra.Properties.Semigroup, then all right.
If not, then let us remain with DivMod, so far.
?

[mechvel]

I suggest to generalize this to IsNonzero : Pred Carrier _
and Nonzero = Σ Carrier IsNonzero,

We should not generalise the existing examples in Nat, Integer and Rational however as using them would then rely on first
proving that they're a semiring. They therefore would be unable to live in e.g. Data.Nat.Base.

In lib-1.7, Data.Nat.Base defines NonZero, but does not use it. Does it?
Nat.DivMod could use it. But it imports Data.Nat.Properties, so that +-*-semiring for Nat is accessible there, and it can use the instance of the generic NonZero. Probably the same is with Integer.
In Algebra.Properties.Semiring:

IsNonZero : Pred A α≈                                                           
IsNonZero = (_≉ 0#)                                                             
                                                                                  
NonZero :  Set (α ⊔ α≈)                                                         
NonZero =  Σ A IsNonZero                                                        

Further, everywhere where (nz : NonZero) is needed as argument, it has to be used Algebra.Properties.Semiring.NonZero R,
where R is the needed instance for Semiring.
For example, Nat.DivMod imports Data.Nat.Properties and can import +-*-semiring from it.
?

[mechvel]

Currently I use this general definition under Semiring :

NonZero =  Σ Carrier (_≉ 0#)

And now I propose instead (for Standard):

data ButOne (b : Carrier) :  Set (α ⊔ α≈)         -- for (Raw)Setoid
    where
    butOne : {x : Carrier} → x ≉ b → ButOne b

NonZero : Set _                      -- for (Roaw)Semiring
NonZero = ButOne 0#

Example of usage:

f : NonZero → Carrier 
f (butOne {x} x≉0) =  remainder (x * x + 5#) x x≉0

It is also possible to first define ButOne and NonZero may be in Algebra.Definitions, for the Raw structures, etc.

?

[MatthewDaggitt]

As pointed out by @mechvel in #1581 we should also look at generalising Positive/Negative etc.

Positivity/negativity has sense for any Ordered (Abelian) Group.
There < is agreed with + in a certain way.
It is desirable to have the corresponding general definition.

[MatthewDaggitt]

Okay, in light of PR #1582 which adds fields, I've been thinking hard about how to come up with a generic definition for NonZero and it's a bit tricky as there are two possible definitions for non-zeroness over some algebraic structure with a carrier set A, a zero element 0# and an equality relation ≈.

Definition 1: Does not use decidability

record NonZero (x : A) : Set where
  field
    nonZero : x ≉ 0#

Definition 2: Uses decidability relation =ᵇ

record NonZero (n : A) : Set where
  field
    nonZero : T (not (n =ᵇ 0))

(records are needed to make instance search play nice which is a separate issue)

In general Definition 1 is definitely preferable as it applies to non-decidable domains such as the reals.

However in decidable domains (e.g. Data.(Nat/Int/Rational)) we currently get a massive increase in usability by using Definition 2, as it means that the type of the proof can be reduced to ⊥ when the element is zero, and hence Agda will remove a lot of the "obviously" impossible cases. For example we can write:

proof : ∀ n .{{_ : NonZero n}} → P n
proof (suc n) = ...

whereas if we use Definition 1 then we would have to write:

proof : ∀ n .{{_ : NonZero n}} → P n
proof zero {{nonZero}} = contradiction nonZero 0-notNonZero
proof (suc n) {{_}}    = ...

and I'm kind of reluctant to give that up...

So there a two options I guess:

1. Drop the use of definition 2 entirely, and take usability hit our existing numeric modules.
2. Have two different generic definitions NonZero and DecNonZero and require that the IsField definition provides it's own notion of NonZero, along with a proof it has the required properties. This is ugly as it kind of distinguishes otherwise identical fields though, by the type of definition of non-zero.

What are people's thoughts. Can anyone see any others?