GCDDomain.hs

-- | Greatest common divisor (GCD) domains. 
--
-- GCD domains are integral domains in which every pair of nonzero elements 
-- have a greatest common divisor. They can also be characterized as 
-- non-Noetherian analogues of unique factorization domains.
--
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module Algebra.Structures.GCDDomain 
  ( GCDDomain(gcd')
  , propGCD, propGCDDomain
  ) where

import Test.QuickCheck

import Algebra.Structures.IntegralDomain
import Algebra.Structures.BezoutDomain
import Algebra.Ideal


-------------------------------------------------------------------------------
-- | GCD domains

class IntegralDomain a => GCDDomain a where
  -- | Compute gcd(a,b) = (g,x,y) such that g = gcd(a,b) and
  --   a = gx
  --   b = gy
  -- and a, b /= 0
  gcd' :: a -> a -> (a,a,a)


propGCD :: (GCDDomain a, Eq a) => a -> a -> Bool
propGCD a b = a == zero || b == zero || a == g <*> x && b == g <*> y
  where
  (g,x,y) = gcd' a b


-- | Specification of GCD domains. They are integral domains in which every 
-- pair of nonzero elements have a greatest common divisor.
propGCDDomain :: (Eq a, GCDDomain a, Arbitrary a, Show a) => a -> a -> a -> Property
propGCDDomain a b c = if propGCD a b 
                         then propIntegralDomain a b c
                         else whenFail (print "propGCD") False

-- This can be used to compute gcd of a list of non-zero elements
-- genGCD :: ?
-- genGCD = ?

instance BezoutDomain a => GCDDomain a where
  gcd' a b = (g,x,y)
    where (Id [g],_,[x,y]) = toPrincipal (Id [a,b])