Literals for any ring?

[gallais]

Should we add an Algebra.Structures.Literals module declaring a Number instance for any SemiringWithoutAnnihilatingZero interpreting n as 1 + ... + 1?

[JacquesCarette]

Is SemiringWithoutAnhilatingZero the smallest theory in the library that has the natural numbers as initial (and free theory on 0 generators)?

[jamesmckinna]

UPDATED Hmmm. Seems as though the free Semiring on no generators should still be ℕ, surely? (0# ≠ 1# in the free theory?) (I'm less ignorant now about Algebra.Structures than when I wrote that...)

Having Number instances for nilpotent (semi-)rings seems ok too... so that eg ℤₙ would be able to work 'automatically' eg 3+5 reduces to 1 mod 7, so that we could render literals in that form, or am I missing something?

[jamesmckinna]

So, I think that this issue is better tackled with Algebra.Definitions.RawMonoid._×_ (suitably renamed, if necessary), with properties and their proofs similarly in Algebra.Properties.Monoid.Mult. There's no need for distributivity from Semiring{WithoutAnnihilatingZero}, AFAICT... but you do need an element 1# (although no relation to 0#, nor any properties, need be pre-supposed... and we don't have a Structure or {Raw}Bundle for

-- Structures with 1 binary operation & 2 elements

ie. MonoidWithGenerator... esp. as Generator would be have to be heavily scare-quoted... in this context; PointedMonoid? uh-oh adding a Pointed hierarchy to Relation.Binary.Structures|Bundles, and thence to Algebra.*... #1957 / #1958 revisited!? cf. #2252 )

Outstanding issues, though, concerning the Number instance:

• do we take the Constraint field to be constant ⊤ as in Data.Nat.Literals?
• for fromNat, should we try to develop a theory of Group/Monoid order, or Ring characteristic, as additional structure (needs DecidableEquality?) to then normalise numerals to the order/characteristic?

UPDATED: introduce SuccessorSet #2273 #2277 , for which the natural numbers are the initial/free object on 0 generators.

[gallais]

I have a bunch of results

  fromℕ′ : ℕ → Carrier
  fromℤ′ : ℤ → Carrier

  fromℕ′-+ : ∀ m n → fromℕ′ (m ℕ.+ n) ≈ fromℕ′ m + fromℕ′ n
  fromℕ′-∸ : ∀ {m n} → n ℕ.≤ m → fromℕ′ (m ℕ.∸ n) ≈ fromℕ′ m - fromℕ′ n
  fromℤ′‿-‿homo : ∀ i → fromℤ′ (ℤ.- i) ≈ - (fromℤ′ i)
  fromℤ′-⊖ : ∀ m n → fromℤ′ (m ℤ.⊖ n) ≈ fromℕ′ m - fromℕ′ n
  fromℤ′-+ : ∀ i j → fromℤ′ (i ℤ.+ j) ≈ fromℤ′ i + fromℤ′ j

Happy to open a PR if folks think that'd be useful.

[JacquesCarette]

Don't those result all follow from initiality and the two from functions being (rig/ring) homomorphisms? The one tricky one would be about fromℕ′-∸ because that's not a "classical" operation that is named.

That's not to say that these are not useful! The library would be better off having them. (I was discussing something very much like this with @TOTBWF yesterday, where rings was definitely an important example.)

[jamesmckinna]

How much overlaps with/is covered by #2272 ?

[jamesmckinna]

As a footnote to the original question: were we to have it, QuasiringWithoutAnnihilatingZero might be the highest diamond to aim for (in terms of which Algebra.Properties.* module to situate the Semiring-homomorphism properties from Nat), because there's no requirement on commutativity of the additive Monoid structure, as multiples of a single element always (additively and multiplicatively!) commute with one another; moreover, #1 being a multiplicative identity means that 0# annihilates 1# without necessarily annihilating every element...

... so the missing step seems to be to establish that given a SuccessorSet with 1# defined to be suc# zero#, that the (natural number) multiples of 1# give rise to a QuasiringWithoutAnnihilatingZero which nevertheless happens also to be a full Semiring...?