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

[N. Raghavendra]

At 2015-03-07T12:21:33+08:00, Dr. ERDI Gergo wrote:

> Would it make sense to add Irreducible to the standard library? Here's
> the generalization I have in mind:

I too feel it'd be good to have the general notion of irreducible
element in stdlib.

> open import Algebra
> open import Relation.Nullary
> open import Data.Sum
> open import Level using (Level; _⊔_)
> import Algebra.FunctionProperties
>
> module _ {c ℓ : Level} (R : Algebra.CommutativeSemiring c ℓ) where

All you need is a monoid structure to define irreducible element.  Most
books I've seen assume that the monoid is cancellative and commutative.
That's needed in the proofs of some statements, but isn't necessary for
the definition to make sense.

> data Irreducible (n : Carrier) : Set (ℓ ⊔ c) where
>   irreducible : (not0 : ¬ is0 n) → (not1 : ¬ is1 n) →
>                 (prf : ∀ x y → ≈ x * y → is1 x ⊎ is1 y) →
>                 Irreducible n

module _ {c ℓ : Level} (R : Algebra.CommutativeMonoid c ℓ) where

...

data Irreducible (n : Carrier) : Set (ℓ ⊔ c) where
  irreducible : (notUnit : ¬ isUnit n) →
                (prf : ∀ x y → n ≈ x * y → isUnit x ⊎ isUnit y) →
                Irreducible n

where isUnit n means that n . m ~ e for some m, where e is the identity
element of the monoid.

A lot of the basic stuff about divisibility, irreducibility, primality,
coprimality, gcd, lcm, etc., can be done for cancellative commutative
monoids, as in, e.g., Jacobson's Basic Algebra, vol. 1, section 2.14
(Factorial monoids and rings).  I think it'd be nice to have that
generality in stdlib.

Incidentally, why do you want to define Irreducible as a type, rather
than a function like Prime in Data.Nat.Primality?  I ask because I've
been wondering when to define a type, and when to define a function, in
my own proofs.

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/