{-# LANGUAGE RebindableSyntax #-}
module Algebra.PrincipalIdealDomain (
    {- * Class -}
    C,
    extendedGCD,
    gcd,
    lcm,
    coprime,

    {- * Standard implementations for instances -}
    euclid,
    extendedEuclid,

    {- * Algorithms -}
    extendedGCDMulti,
    diophantine,
    diophantineMin,
    diophantineMulti,
    chineseRemainder,
    chineseRemainderMulti,

    {- * Properties -}
    propMaximalDivisor,
    propGCDDiophantine,
    propExtendedGCDMulti,
    propDiophantine,
    propDiophantineMin,
    propDiophantineMulti,
    propDiophantineMultiMin,
    propChineseRemainder,
    propDivisibleGCD,
    propDivisibleLCM,
    propGCDIdentity,
    propGCDCommutative,
    propGCDAssociative,
    propGCDHomogeneous,
    propGCD_LCM,
  ) where

import qualified Algebra.Units          as Units
import qualified Algebra.IntegralDomain as Integral
import qualified Algebra.ZeroTestable   as ZeroTestable

import qualified Algebra.Laws as Laws

import Algebra.Units          (stdAssociate, stdUnitInv)
import Algebra.IntegralDomain (mod, divChecked, divMod, divides, divModZero)
import Algebra.Ring           (one, (*), scalarProduct)
import Algebra.Additive       (zero, (+), (-))
import Algebra.ZeroTestable   (isZero)

import Data.Maybe.HT (toMaybe, )

import Control.Monad (foldM, liftM)
import Data.List (mapAccumL, mapAccumR, unfoldr)

import Data.Int  (Int,  Int8,  Int16,  Int32,  Int64,  )

import NumericPrelude.Base
import Prelude (Integer, )
import Test.QuickCheck ((==>), Property)


{- $setup
>>> import qualified Algebra.PrincipalIdealDomain as PID
>>> import Test.NumericPrelude.Utility ((/\))
>>> import qualified Test.QuickCheck as QC
>>>
>>> genResidueClass :: QC.Gen (Integer,Integer)
>>> genResidueClass = do
>>>    m <- fmap QC.getNonZero $ QC.arbitrary
>>>    a <- QC.choose (min 0 $ 1+m, max 0 $ m-1)
>>>    return (m,a)
-}


{- |
A principal ideal domain is a ring in which every ideal
(the set of multiples of some generating set of elements)
is principal:
That is,
every element can be written as the multiple of some generating element.
@gcd a b@ gives a generator for the ideal generated by @a@ and @b@.
The algorithm above works whenever @mod x y@ is smaller
(in a suitable sense) than both @x@ and @y@;
otherwise the algorithm may run forever.

Laws:

>   divides x (lcm x y)
>   x `gcd` (y `gcd` z) == (x `gcd` y) `gcd` z
>   gcd x y * z == gcd (x*z) (y*z)
>   gcd x y * lcm x y == x * y

(etc: canonical)

Minimal definition:
 * nothing, if the standard Euclidean algorithm work
 * if 'extendedGCD' is implemented customly, 'gcd' and 'lcm' make use of it
-}
class (Units.C a, ZeroTestable.C a) => C a where
    {- |
    Compute the greatest common divisor and
    solve a respective Diophantine equation.

    >   (g,(a,b)) = extendedGCD x y ==>
    >        g==a*x+b*y   &&  g == gcd x y

    TODO: This method is not appropriate for the PID class,
          because there are rings like the one of the multivariate polynomials,
          where for all x and y greatest common divisors of x and y exist,
          but they cannot be represented as a linear combination of x and y.
    TODO: The definition of extendedGCD does not return the canonical associate.
    -}
    extendedGCD :: a -> a -> (a,(a,a))
    extendedGCD = (a -> a -> (a, a)) -> a -> a -> (a, (a, a))
forall a. (C a, C a) => (a -> a -> (a, a)) -> a -> a -> (a, (a, a))
extendedEuclid a -> a -> (a, a)
forall a. C a => a -> a -> (a, a)
divMod

    {- |
    The Greatest Common Divisor is defined by:

    >   gcd x y == gcd y x
    >   divides z x && divides z y ==> divides z (gcd x y)   (specification)
    >   divides (gcd x y) x
    -}
    gcd         :: a -> a -> a
    gcd a
x a
y     = (a, (a, a)) -> a
forall a b. (a, b) -> a
fst ((a, (a, a)) -> a) -> (a, (a, a)) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> (a, (a, a))
forall a. C a => a -> a -> (a, (a, a))
extendedGCD a
x a
y

    {- |
    Least common multiple
    -}
    lcm         :: a -> a -> a
    lcm a
x a
y     =
       if a -> Bool
forall a. C a => a -> Bool
isZero a
x
         then a
x -- avoid computing undefined (gcd 0 0)
         else a -> a -> a
forall a. (C a, C a) => a -> a -> a
divChecked a
x (a -> a -> a
forall a. C a => a -> a -> a
gcd a
x a
y) a -> a -> a
forall a. C a => a -> a -> a
* a
y  -- avoid big temporary results
    -- lcm x y     = divChecked (x * y) (gcd x y)


{-
These do only work if zero and one are really identity elements.

gcdMulti :: (C a) => [a] -> a
gcdMulti = foldl gcd zero

lcmMulti :: (C a) => [a] -> a
lcmMulti = foldl lcm one
-}

coprime :: (C a) => a -> a -> Bool
coprime :: a -> a -> Bool
coprime a
x a
y =
   a -> Bool
forall a. C a => a -> Bool
Units.isUnit (a -> a -> a
forall a. C a => a -> a -> a
gcd a
x a
y)



{-
We could implement a helper function,
which exposes the temporary results.
This could be re-used for extendedEuclid.
-}
euclid :: (Units.C a, ZeroTestable.C a) =>
   (a -> a -> a) -> a -> a -> a
euclid :: (a -> a -> a) -> a -> a -> a
euclid a -> a -> a
genMod =
   let aux :: a -> a -> a
aux a
x a
y =
          if a -> Bool
forall a. C a => a -> Bool
isZero a
y
            then a -> a
forall a. C a => a -> a
stdAssociate a
x
            else a -> a -> a
aux a
y (a
x a -> a -> a
`genMod` a
y)
   in  a -> a -> a
aux

-- could be implemented in a tail-recursive manner
{-
Unfortunately, with the normalization to the stdAssociate,
@gcd 0@ is no longer the identity function,
since @gcd 0 (-2) = 2@.
-}
extendedEuclid :: (Units.C a, ZeroTestable.C a) =>
   (a -> a -> (a,a)) -> a -> a -> (a,(a,a))
extendedEuclid :: (a -> a -> (a, a)) -> a -> a -> (a, (a, a))
extendedEuclid a -> a -> (a, a)
genDivMod =
   let aux :: a -> a -> (a, (a, a))
aux a
x a
y =
          if a -> Bool
forall a. C a => a -> Bool
isZero a
y
            then (a -> a
forall a. C a => a -> a
stdAssociate a
x, (a -> a
forall a. C a => a -> a
stdUnitInv a
x, a
forall a. C a => a
zero))
            else
              let (a
d,a
m) = a
x a -> a -> (a, a)
`genDivMod` a
y   -- x == d*y + m
                  (a
g,(a
a,a
b)) = a -> a -> (a, (a, a))
aux a
y a
m       -- g == a*y + b*m
              in  (a
g,(a
b,a
aa -> a -> a
forall a. C a => a -> a -> a
-a
ba -> a -> a
forall a. C a => a -> a -> a
*a
d))             -- g == a*y + b*(x-d*y)
   in a -> a -> (a, (a, a))
aux


{- |
Compute the greatest common divisor for multiple numbers
by repeated application of the two-operand-gcd.
-}
extendedGCDMulti :: C a => [a] -> (a,[a])
extendedGCDMulti :: [a] -> (a, [a])
extendedGCDMulti [a]
xs =
   let (a
g,[(a, a)]
cs) = (a -> a -> (a, (a, a))) -> a -> [a] -> (a, [(a, a)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL a -> a -> (a, (a, a))
forall a. C a => a -> a -> (a, (a, a))
extendedGCD a
forall a. C a => a
zero [a]
xs
   in  (a
g, (a, [a]) -> [a]
forall a b. (a, b) -> b
snd ((a, [a]) -> [a]) -> (a, [a]) -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> (a, a) -> (a, a)) -> a -> [(a, a)] -> (a, [a])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumR (\a
acc (a
c0,a
c1) -> (a
acca -> a -> a
forall a. C a => a -> a -> a
*a
c0,a
acca -> a -> a
forall a. C a => a -> a -> a
*a
c1)) a
forall a. C a => a
one [(a, a)]
cs)

{- |
A variant with small coefficients.
-}


{- |
@Just (a,b) = diophantine z x y@
means
@a*x+b*y = z@.
It is required that @gcd(y,z) `divides` x@.
-}
diophantine :: C a => a -> a -> a -> Maybe (a,a)
diophantine :: a -> a -> a -> Maybe (a, a)
diophantine a
z a
x a
y =
   ((a, (a, a)) -> (a, a)) -> Maybe (a, (a, a)) -> Maybe (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, (a, a)) -> (a, a)
forall a b. (a, b) -> b
snd (Maybe (a, (a, a)) -> Maybe (a, a))
-> Maybe (a, (a, a)) -> Maybe (a, a)
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> Maybe (a, (a, a))
forall a. C a => a -> a -> a -> Maybe (a, (a, a))
diophantineAux a
z a
x a
y

{- |
Like 'diophantine', but @a@ is minimal
with respect to the measure function of the Euclidean algorithm.
-}
diophantineMin :: C a => a -> a -> a -> Maybe (a,a)
diophantineMin :: a -> a -> a -> Maybe (a, a)
diophantineMin a
z a
x a
y =
   ((a, (a, a)) -> (a, a)) -> Maybe (a, (a, a)) -> Maybe (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> (a, a) -> (a, a)) -> (a, (a, a)) -> (a, a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((a, a) -> a -> (a, a) -> (a, a)
forall a. C a => (a, a) -> a -> (a, a) -> (a, a)
minimizeFirstOperand (a
x,a
y))) (Maybe (a, (a, a)) -> Maybe (a, a))
-> Maybe (a, (a, a)) -> Maybe (a, a)
forall a b. (a -> b) -> a -> b
$
   a -> a -> a -> Maybe (a, (a, a))
forall a. C a => a -> a -> a -> Maybe (a, (a, a))
diophantineAux a
z a
x a
y

minimizeFirstOperand :: C a => (a,a) -> a -> (a,a) -> (a,a)
minimizeFirstOperand :: (a, a) -> a -> (a, a) -> (a, a)
minimizeFirstOperand (a
x,a
y) a
g (a
a,a
b) =
   if a -> Bool
forall a. C a => a -> Bool
isZero a
g
     then (a
forall a. C a => a
zero,a
forall a. C a => a
zero)
     else
       let xl :: a
xl = a -> a -> a
forall a. (C a, C a) => a -> a -> a
divChecked a
x a
g
           yl :: a
yl = a -> a -> a
forall a. (C a, C a) => a -> a -> a
divChecked a
y a
g
           (a
d,a
aRed) = a -> a -> (a, a)
forall a. (C a, C a) => a -> a -> (a, a)
divModZero a
a a
yl
       in  (a
aRed, a
b a -> a -> a
forall a. C a => a -> a -> a
+ a
da -> a -> a
forall a. C a => a -> a -> a
*a
xl)

diophantineAux :: C a => a -> a -> a -> Maybe (a, (a,a))
diophantineAux :: a -> a -> a -> Maybe (a, (a, a))
diophantineAux a
z a
x a
y =
   let (a
g,(a
a,a
b)) = a -> a -> (a, (a, a))
forall a. C a => a -> a -> (a, (a, a))
extendedGCD a
x a
y
       (a
q,a
r) = a -> a -> (a, a)
forall a. (C a, C a) => a -> a -> (a, a)
divModZero a
z a
g
   in  Bool -> (a, (a, a)) -> Maybe (a, (a, a))
forall a. Bool -> a -> Maybe a
toMaybe (a -> Bool
forall a. C a => a -> Bool
isZero a
r) (a
g, (a
qa -> a -> a
forall a. C a => a -> a -> a
*a
a, a
qa -> a -> a
forall a. C a => a -> a -> a
*a
b))


{- |
-}
diophantineMulti :: C a => a -> [a] -> Maybe [a]
diophantineMulti :: a -> [a] -> Maybe [a]
diophantineMulti a
z [a]
xs =
   let (a
g,[a]
as) = [a] -> (a, [a])
forall a. C a => [a] -> (a, [a])
extendedGCDMulti [a]
xs
       (a
q,a
r)  = a -> a -> (a, a)
forall a. (C a, C a) => a -> a -> (a, a)
divModZero a
z a
g
   in  Bool -> [a] -> Maybe [a]
forall a. Bool -> a -> Maybe a
toMaybe (a -> Bool
forall a. C a => a -> Bool
isZero a
r) ((a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a
qa -> a -> a
forall a. C a => a -> a -> a
*) [a]
as)

{- |
Not efficient because it requires duplicate computations of GCDs.
However GCDs of adjacent list elements were not computed before.
It is also quite arbitrary,
because only adjacent elements are used for balancing.
There are certainly more sophisticated solutions.
-}
diophantineMultiMin :: C a => a -> [a] -> Maybe [a]
diophantineMultiMin :: a -> [a] -> Maybe [a]
diophantineMultiMin a
z [a]
xs =
   do [a]
as <- a -> [a] -> Maybe [a]
forall a. C a => a -> [a] -> Maybe [a]
diophantineMulti a
z [a]
xs
      [a] -> Maybe [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ ([(a, a)] -> Maybe (a, [(a, a)])) -> [(a, a)] -> [a]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr
         (\[(a, a)]
as' -> case [(a, a)]
as' of
           ((a
x0,a
a0):(a
x1,a
a1):[(a, a)]
aRest) ->
              let (a
b0,a
b1) = (a, a) -> a -> (a, a) -> (a, a)
forall a. C a => (a, a) -> a -> (a, a) -> (a, a)
minimizeFirstOperand (a
x0,a
x1) (a -> a -> a
forall a. C a => a -> a -> a
gcd a
x0 a
x1) (a
a0,a
a1)
              in  (a, [(a, a)]) -> Maybe (a, [(a, a)])
forall a. a -> Maybe a
Just (a
b0, (a
x1,a
b1)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:[(a, a)]
aRest)
           (a
_,a
a):[] -> (a, [(a, a)]) -> Maybe (a, [(a, a)])
forall a. a -> Maybe a
Just (a
a,[])
           [] -> Maybe (a, [(a, a)])
forall a. Maybe a
Nothing) ([(a, a)] -> [a]) -> [(a, a)] -> [a]
forall a b. (a -> b) -> a -> b
$
         [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs [a]
as

{-
diophantineMultiMin :: C a => a -> [a] -> Maybe [a]
diophantineMultiMin z xs =
   do as <- diophantineMulti z xs
      return $
         case as of
           (c:cs'@(_:_)) ->
              let (cs,cLast) = splitLast cs'
                  (d,as') = mapAccumL (\a b -> swap $ minimizeFirstOperand (gcd a b) (a,b)) c cs
                  (d',cLast') = minimizeFirstOperand (gcd d cLast) d cLast
              in  as' ++ [d',cLast']
           _ -> as
-}

{- |
Not efficient enough, because GCD\/LCM is computed twice.
-}
chineseRemainder :: C a => (a,a) -> (a,a) -> Maybe (a,a)
chineseRemainder :: (a, a) -> (a, a) -> Maybe (a, a)
chineseRemainder (a
m0,a
a0) (a
m1,a
a1) =
   ((a, a) -> (a, a)) -> Maybe (a, a) -> Maybe (a, a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\(a
k,a
_) -> let m :: a
m = a -> a -> a
forall a. C a => a -> a -> a
lcm a
m0 a
m1 in (a
m, a -> a -> a
forall a. C a => a -> a -> a
mod (a
a0a -> a -> a
forall a. C a => a -> a -> a
-a
ka -> a -> a
forall a. C a => a -> a -> a
*a
m0) a
m)) (Maybe (a, a) -> Maybe (a, a)) -> Maybe (a, a) -> Maybe (a, a)
forall a b. (a -> b) -> a -> b
$
   a -> a -> a -> Maybe (a, a)
forall a. C a => a -> a -> a -> Maybe (a, a)
diophantineMin (a
a0a -> a -> a
forall a. C a => a -> a -> a
-a
a1) a
m0 a
m1
{-
a0-k*m0 == a1+l*m1
a0-a1 == k*m0+l*m1
-}

{- |
For @Just (n,b) = chineseRemainderMulti [(m0,a0), (m1,a1), ..., (mk,ak)]@
and all @x@ with @x = b mod n@, the congruences
@x=a0 mod m0, x=a1 mod m1, ..., x=ak mod mk@
are fulfilled.
Also, @n@ is the least common multiplier of all @mi@.

>>> PID.chineseRemainderMulti [(100,21), (10000,2021::Integer)]
Just (10000,2021)
>>> PID.chineseRemainderMulti [(97,90),(99,10),(100,0::Integer)]
Just (960300,100000)
>>> PID.chineseRemainderMulti [(95,30),(97,27),(98,8),(99,1::Integer)]
Just (89403930,1000000)

prop> QC.listOf genResidueClass /\ \xs -> case PID.chineseRemainderMulti xs of Nothing -> True; Just (n,b) -> abs n == abs (foldl lcm 1 (map fst xs)) && map snd xs == map (mod b . fst) xs
prop> \(QC.NonEmpty ms) b -> let xs = map (\(QC.NonZero m) -> (m, mod b m)) ms in case PID.chineseRemainderMulti xs of Nothing -> False; Just (n,c) -> abs n == abs (foldl lcm 1 (map QC.getNonZero ms)) && mod b n == (c::Integer)
-}
chineseRemainderMulti :: C a => [(a,a)] -> Maybe (a,a)
chineseRemainderMulti :: [(a, a)] -> Maybe (a, a)
chineseRemainderMulti [(a, a)]
congs =
   case [(a, a)]
congs of
      [] -> Maybe (a, a)
forall a. Maybe a
Nothing
      ((a, a)
c:[(a, a)]
cs) -> ((a, a) -> (a, a) -> Maybe (a, a))
-> (a, a) -> [(a, a)] -> Maybe (a, a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (a, a) -> (a, a) -> Maybe (a, a)
forall a. C a => (a, a) -> (a, a) -> Maybe (a, a)
chineseRemainder (a, a)
c [(a, a)]
cs



{- * Instances for atomic types -}


{-
There is the binary GCD algorithm,
that is specialised for integers in binary representation.
It does not need a division.
However, since we have an optimized division,
the standard implementation is probably faster.

TODO: Can Integer make use of the GMP GCD routine?
-}

instance C Integer where
    -- possibly more efficient than the default method
    gcd :: Integer -> Integer -> Integer
gcd = (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a. (C a, C a) => (a -> a -> a) -> a -> a -> a
euclid Integer -> Integer -> Integer
forall a. C a => a -> a -> a
mod

instance C Int where
    gcd :: Int -> Int -> Int
gcd = (Int -> Int -> Int) -> Int -> Int -> Int
forall a. (C a, C a) => (a -> a -> a) -> a -> a -> a
euclid Int -> Int -> Int
forall a. C a => a -> a -> a
mod

instance C Int8 where
    gcd :: Int8 -> Int8 -> Int8
gcd = (Int8 -> Int8 -> Int8) -> Int8 -> Int8 -> Int8
forall a. (C a, C a) => (a -> a -> a) -> a -> a -> a
euclid Int8 -> Int8 -> Int8
forall a. C a => a -> a -> a
mod

instance C Int16 where
    gcd :: Int16 -> Int16 -> Int16
gcd = (Int16 -> Int16 -> Int16) -> Int16 -> Int16 -> Int16
forall a. (C a, C a) => (a -> a -> a) -> a -> a -> a
euclid Int16 -> Int16 -> Int16
forall a. C a => a -> a -> a
mod

instance C Int32 where
    gcd :: Int32 -> Int32 -> Int32
gcd = (Int32 -> Int32 -> Int32) -> Int32 -> Int32 -> Int32
forall a. (C a, C a) => (a -> a -> a) -> a -> a -> a
euclid Int32 -> Int32 -> Int32
forall a. C a => a -> a -> a
mod

instance C Int64 where
    gcd :: Int64 -> Int64 -> Int64
gcd = (Int64 -> Int64 -> Int64) -> Int64 -> Int64 -> Int64
forall a. (C a, C a) => (a -> a -> a) -> a -> a -> a
euclid Int64 -> Int64 -> Int64
forall a. C a => a -> a -> a
mod


propGCDIdentity     :: (Eq a, C a) => a -> Bool
propGCDAssociative :: (Eq a, C a) => a -> a -> a -> Bool
propGCDCommutative :: (Eq a, C a) => a -> a -> Bool
propGCDDiophantine :: (Eq a, C a) => a -> a -> Bool
propExtendedGCDMulti :: (Eq a, C a) => [a] -> Bool
propDiophantineGen :: (Eq a, C a) =>
   (a -> a -> a -> Maybe (a,a)) -> a -> a -> a -> a -> Bool
propDiophantine    :: (Eq a, C a) => a -> a -> a -> a -> Bool
propDiophantineMin :: (Eq a, C a) => a -> a -> a -> a -> Bool
propDiophantineMultiGen :: (Eq a, C a) =>
   (a -> [a] -> Maybe [a]) -> [(a,a)] -> Bool
propDiophantineMulti    :: (Eq a, C a) => [(a,a)] -> Bool
propDiophantineMultiMin :: (Eq a, C a) => [(a,a)] -> Bool
propDivisibleGCD   :: C a => a -> a -> Bool
propDivisibleLCM   :: C a => a -> a -> Bool
propGCD_LCM        :: (Eq a, C a) => a -> a -> Bool
propGCDHomogeneous :: (Eq a, C a) => a -> a -> a -> Bool
propMaximalDivisor :: C a => a -> a -> a -> Property
propChineseRemainder :: (Eq a, C a) => a -> a -> [a] -> Property

propMaximalDivisor :: a -> a -> a -> Property
propMaximalDivisor a
x a
y a
z =
   a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
z a
x Bool -> Bool -> Bool
&& a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
z a
y Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
z (a -> a -> a
forall a. C a => a -> a -> a
gcd a
x a
y)
propGCDDiophantine :: a -> a -> Bool
propGCDDiophantine a
x a
y =
   let (a
g,(a
a,a
b)) = a -> a -> (a, (a, a))
forall a. C a => a -> a -> (a, (a, a))
extendedGCD a
x a
y
   in  a
g a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall a. C a => a -> a -> a
gcd a
x a
y  Bool -> Bool -> Bool
&&  a
g a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
aa -> a -> a
forall a. C a => a -> a -> a
*a
xa -> a -> a
forall a. C a => a -> a -> a
+a
ba -> a -> a
forall a. C a => a -> a -> a
*a
y
propExtendedGCDMulti :: [a] -> Bool
propExtendedGCDMulti [a]
xs =
   let (a
g,[a]
as) = [a] -> (a, [a])
forall a. C a => [a] -> (a, [a])
extendedGCDMulti [a]
xs
   in  a
g a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> [a] -> a
forall a. C a => [a] -> [a] -> a
scalarProduct [a]
as [a]
xs  Bool -> Bool -> Bool
&&
       (a -> Bool
forall a. C a => a -> Bool
isZero a
g Bool -> Bool -> Bool
|| (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
g) [a]
xs)
propDiophantineGen :: (a -> a -> a -> Maybe (a, a)) -> a -> a -> a -> a -> Bool
propDiophantineGen a -> a -> a -> Maybe (a, a)
dio a
a a
b a
x a
y =
   let z :: a
z = a
aa -> a -> a
forall a. C a => a -> a -> a
*a
xa -> a -> a
forall a. C a => a -> a -> a
+a
ba -> a -> a
forall a. C a => a -> a -> a
*a
y
   in  Bool -> ((a, a) -> Bool) -> Maybe (a, a) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (\(a
a',a
b') -> a
z a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a'a -> a -> a
forall a. C a => a -> a -> a
*a
xa -> a -> a
forall a. C a => a -> a -> a
+a
b'a -> a -> a
forall a. C a => a -> a -> a
*a
y) (a -> a -> a -> Maybe (a, a)
dio a
z a
x a
y)
propDiophantine :: a -> a -> a -> a -> Bool
propDiophantine    = (a -> a -> a -> Maybe (a, a)) -> a -> a -> a -> a -> Bool
forall a.
(Eq a, C a) =>
(a -> a -> a -> Maybe (a, a)) -> a -> a -> a -> a -> Bool
propDiophantineGen a -> a -> a -> Maybe (a, a)
forall a. C a => a -> a -> a -> Maybe (a, a)
diophantine
propDiophantineMin :: a -> a -> a -> a -> Bool
propDiophantineMin = (a -> a -> a -> Maybe (a, a)) -> a -> a -> a -> a -> Bool
forall a.
(Eq a, C a) =>
(a -> a -> a -> Maybe (a, a)) -> a -> a -> a -> a -> Bool
propDiophantineGen a -> a -> a -> Maybe (a, a)
forall a. C a => a -> a -> a -> Maybe (a, a)
diophantineMin
propDiophantineMultiGen :: (a -> [a] -> Maybe [a]) -> [(a, a)] -> Bool
propDiophantineMultiGen a -> [a] -> Maybe [a]
dio [(a, a)]
axs =
   let ([a]
as,[a]
xs) = [(a, a)] -> ([a], [a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, a)]
axs
       z :: a
z = [a] -> [a] -> a
forall a. C a => [a] -> [a] -> a
scalarProduct [a]
as [a]
xs
   in  Bool -> ([a] -> Bool) -> Maybe [a] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (\[a]
as' -> a
z a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> [a] -> a
forall a. C a => [a] -> [a] -> a
scalarProduct [a]
as' [a]
xs) (a -> [a] -> Maybe [a]
dio a
z [a]
xs)
propDiophantineMulti :: [(a, a)] -> Bool
propDiophantineMulti    = (a -> [a] -> Maybe [a]) -> [(a, a)] -> Bool
forall a.
(Eq a, C a) =>
(a -> [a] -> Maybe [a]) -> [(a, a)] -> Bool
propDiophantineMultiGen a -> [a] -> Maybe [a]
forall a. C a => a -> [a] -> Maybe [a]
diophantineMulti
propDiophantineMultiMin :: [(a, a)] -> Bool
propDiophantineMultiMin = (a -> [a] -> Maybe [a]) -> [(a, a)] -> Bool
forall a.
(Eq a, C a) =>
(a -> [a] -> Maybe [a]) -> [(a, a)] -> Bool
propDiophantineMultiGen a -> [a] -> Maybe [a]
forall a. C a => a -> [a] -> Maybe [a]
diophantineMultiMin
propDivisibleGCD :: a -> a -> Bool
propDivisibleGCD a
x a
y  =  a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides (a -> a -> a
forall a. C a => a -> a -> a
gcd a
x a
y) a
x
propDivisibleLCM :: a -> a -> Bool
propDivisibleLCM a
x a
y  =  a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
x (a -> a -> a
forall a. C a => a -> a -> a
lcm a
x a
y)

propGCDIdentity :: a -> Bool
propGCDIdentity     =  (a -> a -> a) -> a -> a -> Bool
forall a. Eq a => (a -> a -> a) -> a -> a -> Bool
Laws.identity a -> a -> a
forall a. C a => a -> a -> a
gcd a
forall a. C a => a
zero (a -> Bool) -> (a -> a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. C a => a -> a
stdAssociate
propGCDCommutative :: a -> a -> Bool
propGCDCommutative  =  (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (b -> b -> a) -> b -> b -> Bool
Laws.commutative a -> a -> a
forall a. C a => a -> a -> a
gcd
propGCDAssociative :: a -> a -> a -> Bool
propGCDAssociative  =  (a -> a -> a) -> a -> a -> a -> Bool
forall a. Eq a => (a -> a -> a) -> a -> a -> a -> Bool
Laws.associative a -> a -> a
forall a. C a => a -> a -> a
gcd
propGCDHomogeneous :: a -> a -> a -> Bool
propGCDHomogeneous  =  (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
forall a b.
Eq a =>
(a -> b -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
Laws.leftDistributive a -> a -> a
forall a. C a => a -> a -> a
(*) a -> a -> a
forall a. C a => a -> a -> a
gcd (a -> a -> a -> Bool) -> (a -> a) -> a -> a -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. C a => a -> a
stdAssociate
propGCD_LCM :: a -> a -> Bool
propGCD_LCM a
x a
y     =  a -> a -> a
forall a. C a => a -> a -> a
gcd a
x a
y a -> a -> a
forall a. C a => a -> a -> a
* a -> a -> a
forall a. C a => a -> a -> a
lcm a
x a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> a -> a
forall a. C a => a -> a -> a
* a
y
propChineseRemainder :: a -> a -> [a] -> Property
propChineseRemainder a
k a
x [a]
ms =
   Bool -> Bool
not ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ms) Bool -> Bool -> Bool
&& (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
forall a. C a => a -> Bool
isZero) [a]
ms Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
   -- cf. Useful.functionToGraph
   let congs :: [(a, a)]
congs = [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
ms ((a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a -> a
forall a. C a => a -> a -> a
mod a
x) [a]
ms)
   in  Bool -> ((a, a) -> Bool) -> Maybe (a, a) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
          (\(a
mGlob,a
y) ->
             let yk :: a
yk = a
ya -> a -> a
forall a. C a => a -> a -> a
+a
mGloba -> a -> a
forall a. C a => a -> a -> a
*a
k
             in  ((a, a) -> Bool) -> [(a, a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(a
m,a
a) -> a -> a -> a -> Bool
forall a. (C a, C a) => a -> a -> a -> Bool
Integral.sameResidueClass a
m a
a a
yk) [(a, a)]
congs)
          ([(a, a)] -> Maybe (a, a)
forall a. C a => [(a, a)] -> Maybe (a, a)
chineseRemainderMulti [(a, a)]
congs)