[Agda] Data.Nat.Primality.Prime and irreducibility

[Sergei Meshveliani]

On Fri, 2015-03-06 at 12:49 +0530, N. Raghavendra wrote:
> Hi,
> 
> I am looking at the type
> 
> Irreducible : ℕ → Set
> Irreducible n = n ≢ 1 × ((x y : ℕ) → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1)
> 
> I am able to prove
> 
> primen⇒irreduciblen : (n : ℕ) →
>   Data.Nat.Primality.Prime n → Irreducible n
> 
> I've some questions:
> 
> 1. Is there a short proof of this implication?  The one I wrote is a bit
> long.
> 
> 2. How does one prove the converse of the above implication?
> 
> 3. Is there some special reason for defining Prime as in
> Data.Nat.Primality, instead of something like
> 
> Prime : ℕ → Set
> Prime n = n ≢ 1 × ((x y : ℕ) → n | x * y → n | x ⊎ n | y)
> 
> as is common in informal mathematics?
> 
> Thanks and cheers,
> Raghu.
> 


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.

Regards,

------
Sergei