StronglyDiscrete.hs

module Algebra.Structures.StronglyDiscrete 
  ( StronglyDiscrete(member)
  , propStronglyDiscrete
  ) where

import Algebra.Structures.CommutativeRing
import Algebra.Ideal


-------------------------------------------------------------------------------
-- | Strongly discrete rings
--
-- A ring is called strongly discrete if ideal membership is decidable.
-- Nothing correspond to that x is not in the ideal and Just is the witness.
-- Examples include all euclidean domains and the polynomial ring.
--
class Ring a => StronglyDiscrete a where
  member :: a -> Ideal a -> Maybe [a]

-- | Test that the witness is actually a witness that the element is in the 
-- ideal.
propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a)
                     => a -> Ideal a -> Bool                  
propStronglyDiscrete x id@(Id xs) = case member x id of
  Just as -> x == sumRing (zipWith (<*>) xs as) && length xs == length as
  Nothing -> True