(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 :+1: 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 #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!

[jamesmckinna]

Aaaargh! What about the fixities? #207

[jamesmckinna]

As I have worked and reworked the definitions, I couldn't help but think there's an API/encapsulation failure in that I have had to revise the single proof Data.Nat.Coprimality.prime⇒coprime each time to reflect the/any new representation of Prime. But one (more robust) answer seems to be to use prime⇒irreducible!

[jamesmckinna]

@Taneb wrote:

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`

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

Yes, I've had a few days to sit on this and think, and I agree. Two things, though:

• I'd prefer NonUnit to NonInvertible (not least because invertibility per se makes less sense on the context of ℕ...), and I think Unit/NonUnit is (nowadays?) more conventional usage in ring theory?
• This would be a larger (if not breaking, only a further addition to Data.Nat.*) change in terms of the PR footprint, because surely such things belong in Data.Nat.{Base|Properties}, and ... I'd been trying for v2.0 to localise breaking changes as much as possible.

And a third: I'm more convinced that the various d < 1 etc. conditions should be parlayed as instance arguments... so another round of rather fiddly refactoring might be in order before #2181 would be ready? Do we have time to do this? UPDATED: it seems that I do! commit 0a6954d12d94747e6ae7816f86fe598393954d93 and its subsequent corrections...

... ending up after another round of revisions with @MatthewDaggitt as:

record NonTrivial (n : ℕ) : Set where
  field
    nonTrivial : T (1 <ᵇ n)