[Agda] primality definition

[Sergei Meshveliani]

N. Raghavendra <raghu at hri.res.in> write recently


> At 2015-03-06T13:46:21+04:00, Sergei Meshveliani wrote:

        >> Personally, I use a generic primality definition for any GCDRing 
        >> (an integral ring with GCD):
        
        >>  IsPrime : C → Set (α ⊔ α=)
        >>  IsPrime a =  a ≉ 0#  ×  ¬ Invertible a  ×
        >>               (∀ {x y} → (x * y ≈ a) → Invertible x ⊎ Invertible y),
        
        >> which, I think, is the classical definition.
        >> Then, I prove several lemmata about possible Factorization structure for
        >> the elements of such a ring, and find that this my definition works all
        >> right.

> Thanks!  However, my question was specially about how to prove that the
> Data.Nat.Primality definition of an element n of N being Prime is
> equivalent to n being irreducible in the multiplicative monoid of
> non-zero natural numbers.

> Have you put your proofs on the Web?


Do you mean proofs about generic  IsPrime, Factorization etc. ?

The thing is not ready yet. I hope to release it in 2015.

The subject is a bit more complex than one could think. Because factorization 
is not into the prime elements of  C = Carrier.  The factor components are the 
ASD classes -- classes of associated elements. And Factorization is a Multiset 
over ASD classes. A (unique) FactorizationRing uses this definition, 
this way Factorization becomes unique there. And factorization of the product 
of two elements is the sum of the corresponding multisets. And 
Multiset C Nat  is a commutative monoid under _+ms_.

First, I need to finish generic Multiset.
This will form a separate library called  AList.
Then I have to return to Factorization, FactorizationRing,
then to prove various properties of the residue ring  R/(b)  as depending
on the factorization of  b,  and so on. 
The thing is almost ready, but unfortunately this "almost" always lasts 
longer than I hope. 

Regards,

------
Sergei