module Test.Field where
import Protolude
import Data.Field.Galois hiding (recip)
import Test.Tasty
import Test.Tasty.QuickCheck
annihilation :: Eq a => (a -> a -> a) -> a -> a -> Bool
annihilation op e x = op x e == e && op e x == e
associativity :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
associativity op x y z = op x (op y z) == op (op x y) z
commutativity :: Eq a => (a -> a -> a) -> a -> a -> Bool
commutativity op x y = op x y == op y x
distributivity :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
distributivity op op' x y z = op (op' x y) z == op' (op x z) (op y z)
&& op x (op' y z) == op' (op x y) (op x z)
identities :: Eq a => (a -> a -> a) -> a -> a -> Bool
identities op e x = op x e == x && op e x == x
inverses :: Eq a => (a -> a -> a) -> (a -> a) -> a -> a -> Bool
inverses op inv e x = op x (inv x) == e && op (inv x) x == e
groupAxioms :: forall g . (Arbitrary g, Eq g, Show g)
=> (g -> g -> g) -> (g -> g) -> g -> (g -> Bool) -> [TestTree]
groupAxioms add inv id cond =
[ testProperty "associativity" $
associativity add
, testProperty "commutativity" $
commutativity add
, testProperty "identity" $
identities add id
, testProperty "inverses" $
\x -> cond x ==> inverses add inv id x
]
fieldAxioms :: forall k . GaloisField k => k -> TestTree
fieldAxioms _ = testGroup "Field axioms"
[ testGroup "additive group axioms" $
groupAxioms (+) negate (0 :: k) (const True)
, testGroup "multiplicative group axioms" $
groupAxioms (*) recip (1 :: k) (/= 0)
, testProperty "distributivity of multiplication over addition" $
distributivity ((*) :: k -> k -> k) (+)
, testProperty "multiplicative annihilation" $
annihilation ((*) :: k -> k -> k) 0
]
frobeniusEndomorphisms :: forall k . GaloisField k => k -> TestTree
frobeniusEndomorphisms _ = testGroup "Frobenius endomorphisms"
[ testProperty "frobenius endomorphisms are characteristic powers" $
\(x :: k) -> frob x == pow x (char (witness :: k))
, testProperty "frobenius endomorphisms are ring homomorphisms" $
\(x :: k) (y :: k) (z :: k) -> frob (x * y + z) == frob x * frob y + frob z
]
squareRoots :: forall k . GaloisField k => k -> TestTree
squareRoots _ = localOption (QuickCheckMaxRatio 100) $ testGroup "Square roots"
[ testProperty "squares of square roots" $
\(x :: k) -> qr x
==> ((join (*) <$> sr x) == Just x)
, testProperty "solutions of quadratic equations" $
\(a :: k) (b :: k) (c :: k) -> a /= 0 && isJust (quad a b c)
==> (((\x -> (a * x + b) * x + c) <$> quad a b c) == Just 0)
]
testField :: forall k . GaloisField k => TestName -> k -> TestTree
testField s x = testGroup s [fieldAxioms x, frobeniusEndomorphisms x, squareRoots x]