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?

[JacquesCarette]

My leaning would be to have DecidableField use definition 2, and Field use definition 1. Yes, that implicitly argues for having 2 definitions of field in the library. Right now, we have too little experience with non-algebraic structures (i.e. with guarded axioms) to really know what's going to work best.

That way the decidable domains can be maximally usable. The other domains should be hard to deal with (constructively)!

[mechvel]

Of course, a definition for NonZero must not rely on a decidable equality.

Also it is regularly is needed NonZero? : Decidable NonZero
-- and it is for the domains that have _≟_ : Decidable₂ _≈_.

For example lib-1.7 has _≤_ for PartialOrder and _≤?_ for, say, DecTotalOrder.
NonZero is under, say, Semiring.
So, NonZero? has to be under DecSemiring.

But as standard library has not DecSemigroup, DecSemiring etc,
the library could use a module parameterized by Semiring and _≟_. Like this:

module OfSemiring {α α≈} (R : Semiring α α≈)
  where
  open Semiring R
  
  record NonZero (x : Carrier) : Set α≈ where
     constructor mkNonZero
     field
        nonZero : x ≉ 0#
 
module OfDecSemiring {α α≈} (R : Semiring α α≈)  (let open Semiring R)
                                                  (_≟_ : Decidable₂ _≈_) 
  where
  open OfSemiring R
  open NonZero

  Nonzero? : Decidable NonZero
  Nonzero? x  with x ≟ 0#
  ... | no x≉0  =  yes (mkNonZero x≉0)
  ... | yes x≈0 =  no ...

?

Also I wonder what is IsField of which Matthew writes?
Is this of the algebraic structure of Field (a Commutative ring in which each nonzero has an inverse) ?
I do not see such in master.

[JacquesCarette]

Yes, something like that seems to make sense.

[mechvel]

Jacques writes.

That way the decidable domains can be maximally usable. The other domains should be hard to deal with (constructively)!

There is some mystery secret about this.

1. Indeed, we can compute almost nothing without a decidable equality _=?_.
2. On the other hand mathematicians often do "compute" with transcendent numbers. This is done by mixing applying algorithms with inventing a proof in some necessary points.
3. Some people in the Agda list referred to their works on constructive computation with real numbers.
4. So, I asked the Agda list of how could it look, briefly, a program that divides two polynomials over real numbers:
   divMod (x^5 + a*x^3 + b*x + c) (a'*x4 + b'*x^2 + c'*),
   where a,b,c,a',b',c' are real numbers. Something like this.
   In classical algebra, it is done by the "algorithm", like this:
   "find 1/a'; if a - b'*c = 0, then do this, otherwise do that ...".
   And how could it look the Agda program, and how could it look its result?
   But nobody responded to my question.

[Akshobhya1234]

I found this work around definition
LeftInverseNonZero : (zero e : A) → Op₁ A → Op₂ A → Set _
LeftInverseNonZero zero e _⁻¹ _·_ = ∀₁ λ x → x ≉ zero → (x ⁻¹) · x ≈ e

And they also define field structure here
https://github.com/crypto-agda/agda-nplib/blob/45fa0a16de862c4c1a546f1a510def23cd4590a5/lib/Algebra/Field.agda#L17

[mechvel]

And they also define field structure here
[..]

It is desirable for Standard to intoduce the Field abstract domain:
(Def)
A CommutativeRing is a Field, when it has an inversion operation inv which inverses with respect to *each nonzero element.
And it is natural to define Field in the same style as the previous classical algebra categories are introduced.
For example, it has IsMonoid, Monoid, IsGroup, Group (_⁻¹ added).
Similarly, it needs to have IsCommutativeRing CommutativeRing, IsField, Field (inv added),
where the last two express the above definition (Def).

[JacquesCarette]

Parts of algebra are indeed quite a bit harder without decidable equality. A lot of algorithms need it. Classical mathematics builds it in (that's a consequence of excluded middle). This shows up most clearly when you try to compute with "fields of functions": you can't decide if an arbitrary function is constantly 0 or not.

Even classically, Field is weird: it's not given equationally. Fields do not form a variety.

[mechvel]

Jacques writes

Even classically, Field is weird: it's not given equationally. Fields do not form a variety.

I recall, after my talk in 2013 Jacques asked me: why do I define various domain constructors (or polymorphic functions) specially for Semigroup, Group, etc, instead of doing this in a general way.
I misunderstood the question, because it was evident to me from the experience in algebra that this is not possible to
generalize this.
But later I recalled of universal algebras, and understood that the question was about possible approach with universal algebras. And exactly this approach is not possible, due to the conditions like x \= 0, not (invertible x),
"denominator is not zero in a fraction", "if the ideal is not maximal", and such,
that appear as addition to the laws expressed as equations only.
Algebra is not only a matter of equations.

But I think that even with this kind of conditions algebra is programmed more or less all right in Agda.
For example, "denominator is not zero in a fraction" does not bring any problem to programming various properties of
fraction arithmetic in Agda.
If you keep in mind proofs by equational reasoning in Term rewriting, then inequality can be expressed as equality on
the domain Bool. For example, x /= 0 expressed as (x == 0) = false, where _==_ is an explicit operator for term rewriting.

?

[JacquesCarette]

Equality being boolean-valued is equivalent to asking for decidable equality. In the presence of decidable equality, many algorithms in Algebra do go through.

It's quite fine to have a parallel hierarchy of Algebra that assumes that the underlying equality is decidable. The current library has made a different design decision: constructive and Setoid-based. So the main Algebra has to stay that way.

[mechvel]

May be it is all right for Standard to have a Setoid-based Algebra only.
But it is natural for applied libraries to have dec-versions.
For example, on practice one very often has to deal with DecCommutativeRing (CommutativeRing with a decidable _≈_ ),
DecMonoid, etc.
Also in many cases it is needed a decidable divisibility _∣?_.
For example, Dec2CommutativeRing may denote DecCommutativeRing with a decidable divisibility _∣?_.
Another way for applications is to provide _≟_ or _∣?_ as the module or function parameters.

I wonder of whether Standard needs these "Dec, Dec2" classes (from Magma to CommutativeRing).