(re-)Definition of `Prime` (and `Irreducible`) in `Data.Nat.Primality`

[jamesmckinna]

Reflecting on @Taneb 's PR #1969 , and wanting to add the definition of Irreducible to Data.Nat.Primality, with

IrreducibleAt : ℕ → Pred ℕ _
IrreducibleAt n m = m ∣ n → m ≡ 1 ⊎ m ≡ n

Irreducible : ℕ → Set
Irreducible n = ∀[ IrreducibleAt n ]

I found myself wanting to redefine Composite and Prime to eliminate the special cases for 0 and 1 which otherwise pollute the definitions and properties given there.

This leads to the following definitions [REVISED in PR #2181 but not updated here]:
[DELETED: please see #2181 for heavily revised/redacted versions]
with this last pattern synonym essentially permitting proofs formerly involving Prime to access the second functional component without difficulty, and moreover to enforce that the argument to Prime must be of the form suc (suc _), and thus eliminate some now-redundant pattern matching against patterns of that form. with a constructor prime introducing witnesses to Prime p imposing that p must be NonTrivial ie > 1 (and much else besides ;-))

I have a revised version of Data.Nat.Primality based on these re-definitions, towards a breaking PR. So I'm cheekily tagging this as v2.0 in order to try to sneak it into the upcoming release.

[jamesmckinna]

Above revised in the light of comments on #2181 as a potential refactoring of the Rough component of #1969 .

[jamesmckinna]

On the PR #2181 I wrote:

The main issue as I see it ... is the label:breaking change to the definition of Prime, but I think in view of @Taneb 's #1969, plus the fact that Prime has already once been redefined for v2.0, that this is a last chance for a while to sort this out... and obvs. IMHO, better than before. But it is a slightly 'fiddly' definition, so I have taken care to introduced enough pattern synonyms to (hopefully!) smooth that path.

Suggest we continue the discussion aspects of this issue/PR here, with implementation details/review comments on the code on the PR.

[Taneb]

Hmm, I wonder if we could go even more (semi)-ring theoretical.

• instead of using 1 < d, we could write something like NonZero d × NonInvertible d
• We could make a definition of "strict" divisibility, which includes a not-equal. This implies _<_.

With these, the core definitions work for any (commutative?) semiring, and they're equivalent to what you have for ℕ

[Taneb]

Also, with radical definition changes, I think Prime p should be something like the RHS of euclidsLemma, i.e. p ∣ m * n → p ∣ m ⊎ p ∣ n rather than the negative definition you have here

[jamesmckinna]

Hmm, I wonder if we could go even more (semi)-ring theoretical.

* instead of using `1 < d`, we could write something like `NonZero d × NonInvertible d`

* We could make a definition of "strict" divisibility, which includes a not-equal. This implies `_<_`.

With these, the core definitions work for any (commutative?) semiring, and they're equivalent to what you have for ℕ

Fantastic! (I think... but I had got sufficiently engrossed by the direction that you had taken, which I felt I was simply streamlining, to look up and think about such things)

Definitely 👍 to 'strict' divisibility (there's a long, omitted/suppressed digression via well-foundedness of that relation that I embarked upon, before realising that at least for your definitions, no appeal to Data.Nat.Induction, never mind Induction.WellFounded was actually necessary... here, at least, but it almost certainly is needed in the rest of #1969 )

As for proxying 1 < d in favour of something more abstract algebraic, again, my instincts are to agree, but for all the upheaval that even the current changes cause, while still retaining the ℕ-theoretic character of things as bounded quantification over decidable atomic predicates (and thus as PRA-expressible notions, for which we could have external oracle decision procedures as tactics, whose results we then internally check, cf. work on Pocklington's Criterion from the 1990s in Coq... UPDATED: published in 2001 ;-)).

Ditto the Prime ideal definition: such a move then takes us away from the concrete computational aspects of Data.Nat.Primality, in favour of abstract algebra. Elsewhere, I've seen gestures towards defining ID, PID, UFD in the hierarchy, towards showing that ℤ satisfies the definitions, and I think that we should, but not under Data.*, or perhaps only under Data.*.Properties. So (for now!?) I think I would be happier leaving euclidsLemma as a theorem, rather than a definition...

... but agreed, the 'negative' definition of Prime seems, perhaps, unsatisfactory from a constructive point-of-view, except that we are working in the bounded/decidable fragment here, so such definitions are 'harmless'. Your singling out of Rough as a definition, though, is, via its positive counterpart BoundedComposite BoundedNonTrivialDivisor (as I now have it in #2181 ), I think the key step, and Rough/Prime on that account, is a negative definition...

Mind you, Irreducible is about as positive as you can get, and it's equivalent to Prime... on ℕ ;-)

[jamesmckinna]

All that said, if you want to take this forward to a more algebraic approach, I shouldn't stop you!

Indeed, all the refactoring work I've done so far is only towards:

• a better infrastructure for Add prime factorization and its properties #1969 , so please feel free to re-incorporate this work into that PR, if that's a worthwhile thing to do (but perhaps that can now be more cleanly decoupled as a standalone proof of the Fundamental Theorem?)
• getting rid of the, to me, ugly warts of the special base cases of Prime and Composite... (possibly a margin call, but for an obsessive mind like mine)
• provoking this discussion... ;-)

[jamesmckinna]

Re: (semi)ring-theoretic prime ideals. We do/will need at some point that the (semi)rings ℕ, ℤ are Noetherian (generalising the well-foundedness of strict divisibility) towards more abstracts proofs of UFD, but I think that can wait for v2.1. As can/should some of the changes you propose above?

But I can imagine @JacquesCarette (and/among others!) will have views on the matter!