{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Math.NumberTheory.Moduli.Singleton
(
SFactors
, sfactors
, someSFactors
, unSFactors
, proofFromSFactors
, CyclicGroup
, cyclicGroup
, cyclicGroupFromFactors
, cyclicGroupFromModulo
, proofFromCyclicGroup
, pattern CG2
, pattern CG4
, pattern CGOddPrimePower
, pattern CGDoubleOddPrimePower
, cyclicGroupToSFactors
, sfactorsToCyclicGroup
, Some(..)
) where
import Control.DeepSeq
import Data.Constraint
import Data.Kind
import Data.List (sort)
import qualified Data.Map as M
import Data.Proxy
import GHC.Generics
import GHC.TypeNats (KnownNat, Nat, natVal)
import Numeric.Natural
import Unsafe.Coerce
import Math.NumberTheory.Roots (highestPower)
import Math.NumberTheory.Primes
import Math.NumberTheory.Primes.Types
import Math.NumberTheory.Utils.FromIntegral
data Some (a :: Nat -> Type) where
Some :: a m -> Some a
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
newtype SFactors a (m :: Nat) = SFactors
{ forall a (m :: Nat). SFactors a m -> [(Prime a, Word)]
unSFactors :: [(Prime a, Word)]
} deriving (Int -> SFactors a m -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (m :: Nat). Show a => Int -> SFactors a m -> ShowS
forall a (m :: Nat). Show a => [SFactors a m] -> ShowS
forall a (m :: Nat). Show a => SFactors a m -> String
showList :: [SFactors a m] -> ShowS
$cshowList :: forall a (m :: Nat). Show a => [SFactors a m] -> ShowS
show :: SFactors a m -> String
$cshow :: forall a (m :: Nat). Show a => SFactors a m -> String
showsPrec :: Int -> SFactors a m -> ShowS
$cshowsPrec :: forall a (m :: Nat). Show a => Int -> SFactors a m -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (m :: Nat) x. Rep (SFactors a m) x -> SFactors a m
forall a (m :: Nat) x. SFactors a m -> Rep (SFactors a m) x
$cto :: forall a (m :: Nat) x. Rep (SFactors a m) x -> SFactors a m
$cfrom :: forall a (m :: Nat) x. SFactors a m -> Rep (SFactors a m) x
Generic)
instance Eq (SFactors a m) where
SFactors a m
_ == :: SFactors a m -> SFactors a m -> Bool
== SFactors a m
_ = Bool
True
instance Ord (SFactors a m) where
SFactors a m
_ compare :: SFactors a m -> SFactors a m -> Ordering
`compare` SFactors a m
_ = Ordering
EQ
instance NFData a => NFData (SFactors a m)
instance Ord a => Eq (Some (SFactors a)) where
Some (SFactors [(Prime a, Word)]
xs) == :: Some (SFactors a) -> Some (SFactors a) -> Bool
== Some (SFactors [(Prime a, Word)]
ys) =
[(Prime a, Word)]
xs forall a. Eq a => a -> a -> Bool
== [(Prime a, Word)]
ys
instance Ord a => Ord (Some (SFactors a)) where
Some (SFactors [(Prime a, Word)]
xs) compare :: Some (SFactors a) -> Some (SFactors a) -> Ordering
`compare` Some (SFactors [(Prime a, Word)]
ys) =
[(Prime a, Word)]
xs forall a. Ord a => a -> a -> Ordering
`compare` [(Prime a, Word)]
ys
instance Show a => Show (Some (SFactors a)) where
showsPrec :: Int -> Some (SFactors a) -> ShowS
showsPrec Int
p (Some SFactors a m
x) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
p SFactors a m
x
instance NFData a => NFData (Some (SFactors a)) where
rnf :: Some (SFactors a) -> ()
rnf (Some SFactors a m
x) = forall a. NFData a => a -> ()
rnf SFactors a m
x
sfactors :: forall a m. (Ord a, UniqueFactorisation a, KnownNat m) => SFactors a m
sfactors :: forall a (m :: Nat).
(Ord a, UniqueFactorisation a, KnownNat m) =>
SFactors a m
sfactors = if a
m forall a. Eq a => a -> a -> Bool
== a
0
then forall a. HasCallStack => String -> a
error String
"sfactors: modulo must be positive"
else forall a (m :: Nat). [(Prime a, Word)] -> SFactors a m
SFactors (forall a. Ord a => [a] -> [a]
sort (forall a. UniqueFactorisation a => a -> [(Prime a, Word)]
factorise a
m))
where
m :: a
m = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m))
someSFactors :: (Ord a, Num a) => [(Prime a, Word)] -> Some (SFactors a)
someSFactors :: forall a. (Ord a, Num a) => [(Prime a, Word)] -> Some (SFactors a)
someSFactors
= forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: Nat). [(Prime a, Word)] -> SFactors a m
SFactors
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.assocs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. Num a => a -> a -> a
(+)
proofFromSFactors :: Integral a => SFactors a m -> (() :- KnownNat m)
proofFromSFactors :: forall a (m :: Nat).
Integral a =>
SFactors a m -> (() :: Constraint) :- KnownNat m
proofFromSFactors (SFactors [(Prime a, Word)]
fs) = forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce (forall (n :: Nat). (KnownNat n => Dict (KnownNat n)) -> Magic n
Magic forall (a :: Constraint). a => Dict a
Dict) (forall a b. (Integral a, Num b) => a -> b
fromIntegral' (forall a. Num a => [(Prime a, Word)] -> a
factorBack [(Prime a, Word)]
fs) :: Natural)
data CyclicGroup a (m :: Nat)
= CG2'
| CG4'
| CGOddPrimePower' (Prime a) Word
| CGDoubleOddPrimePower' (Prime a) Word
deriving (Int -> CyclicGroup a m -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (m :: Nat). Show a => Int -> CyclicGroup a m -> ShowS
forall a (m :: Nat). Show a => [CyclicGroup a m] -> ShowS
forall a (m :: Nat). Show a => CyclicGroup a m -> String
showList :: [CyclicGroup a m] -> ShowS
$cshowList :: forall a (m :: Nat). Show a => [CyclicGroup a m] -> ShowS
show :: CyclicGroup a m -> String
$cshow :: forall a (m :: Nat). Show a => CyclicGroup a m -> String
showsPrec :: Int -> CyclicGroup a m -> ShowS
$cshowsPrec :: forall a (m :: Nat). Show a => Int -> CyclicGroup a m -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (m :: Nat) x. Rep (CyclicGroup a m) x -> CyclicGroup a m
forall a (m :: Nat) x. CyclicGroup a m -> Rep (CyclicGroup a m) x
$cto :: forall a (m :: Nat) x. Rep (CyclicGroup a m) x -> CyclicGroup a m
$cfrom :: forall a (m :: Nat) x. CyclicGroup a m -> Rep (CyclicGroup a m) x
Generic)
instance Eq (CyclicGroup a m) where
CyclicGroup a m
_ == :: CyclicGroup a m -> CyclicGroup a m -> Bool
== CyclicGroup a m
_ = Bool
True
instance Ord (CyclicGroup a m) where
CyclicGroup a m
_ compare :: CyclicGroup a m -> CyclicGroup a m -> Ordering
`compare` CyclicGroup a m
_ = Ordering
EQ
instance NFData a => NFData (CyclicGroup a m)
instance Eq a => Eq (Some (CyclicGroup a)) where
Some CyclicGroup a m
CG2' == :: Some (CyclicGroup a) -> Some (CyclicGroup a) -> Bool
== Some CyclicGroup a m
CG2' = Bool
True
Some CyclicGroup a m
CG4' == Some CyclicGroup a m
CG4' = Bool
True
Some (CGOddPrimePower' Prime a
p1 Word
k1) == Some (CGOddPrimePower' Prime a
p2 Word
k2) =
Prime a
p1 forall a. Eq a => a -> a -> Bool
== Prime a
p2 Bool -> Bool -> Bool
&& Word
k1 forall a. Eq a => a -> a -> Bool
== Word
k2
Some (CGDoubleOddPrimePower' Prime a
p1 Word
k1) == Some (CGDoubleOddPrimePower' Prime a
p2 Word
k2) =
Prime a
p1 forall a. Eq a => a -> a -> Bool
== Prime a
p2 Bool -> Bool -> Bool
&& Word
k1 forall a. Eq a => a -> a -> Bool
== Word
k2
Some (CyclicGroup a)
_ == Some (CyclicGroup a)
_ = Bool
False
instance Ord a => Ord (Some (CyclicGroup a)) where
compare :: Some (CyclicGroup a) -> Some (CyclicGroup a) -> Ordering
compare (Some CyclicGroup a m
x) (Some CyclicGroup a m
y) = case CyclicGroup a m
x of
CyclicGroup a m
CG2' -> case CyclicGroup a m
y of
CyclicGroup a m
CG2' -> Ordering
EQ
CyclicGroup a m
_ -> Ordering
LT
CyclicGroup a m
CG4' -> case CyclicGroup a m
y of
CyclicGroup a m
CG2' -> Ordering
GT
CyclicGroup a m
CG4' -> Ordering
EQ
CyclicGroup a m
_ -> Ordering
LT
CGOddPrimePower' Prime a
p1 Word
k1 -> case CyclicGroup a m
y of
CGDoubleOddPrimePower'{} -> Ordering
LT
CGOddPrimePower' Prime a
p2 Word
k2 ->
Prime a
p1 forall a. Ord a => a -> a -> Ordering
`compare` Prime a
p2 forall a. Semigroup a => a -> a -> a
<> Word
k1 forall a. Ord a => a -> a -> Ordering
`compare` Word
k2
CyclicGroup a m
_ -> Ordering
GT
CGDoubleOddPrimePower' Prime a
p1 Word
k1 -> case CyclicGroup a m
y of
CGDoubleOddPrimePower' Prime a
p2 Word
k2 ->
Prime a
p1 forall a. Ord a => a -> a -> Ordering
`compare` Prime a
p2 forall a. Semigroup a => a -> a -> a
<> Word
k1 forall a. Ord a => a -> a -> Ordering
`compare` Word
k2
CyclicGroup a m
_ -> Ordering
GT
instance Show a => Show (Some (CyclicGroup a)) where
showsPrec :: Int -> Some (CyclicGroup a) -> ShowS
showsPrec Int
p (Some CyclicGroup a m
x) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
p CyclicGroup a m
x
instance NFData a => NFData (Some (CyclicGroup a)) where
rnf :: Some (CyclicGroup a) -> ()
rnf (Some CyclicGroup a m
x) = forall a. NFData a => a -> ()
rnf CyclicGroup a m
x
cyclicGroup
:: forall a m.
(Integral a, UniqueFactorisation a, KnownNat m)
=> Maybe (CyclicGroup a m)
cyclicGroup :: forall a (m :: Nat).
(Integral a, UniqueFactorisation a, KnownNat m) =>
Maybe (CyclicGroup a m)
cyclicGroup = forall a (m :: Nat).
(Integral a, UniqueFactorisation a) =>
a -> Maybe (CyclicGroup a m)
fromModuloInternal a
m
where
m :: a
m = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m))
cyclicGroupFromFactors
:: (Eq a, Num a)
=> [(Prime a, Word)]
-> Maybe (Some (CyclicGroup a))
cyclicGroupFromFactors :: forall a.
(Eq a, Num a) =>
[(Prime a, Word)] -> Maybe (Some (CyclicGroup a))
cyclicGroupFromFactors = \case
[(forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some forall a (m :: Nat). CyclicGroup a m
CG2'
[(forall a. Prime a -> a
unPrime -> a
2, Word
2)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some forall a (m :: Nat). CyclicGroup a m
CG4'
[(forall a. Prime a -> a
unPrime -> a
2, Word
_)] -> forall a. Maybe a
Nothing
[(Prime a
p, Word
k)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some forall a b. (a -> b) -> a -> b
$ forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGOddPrimePower' Prime a
p Word
k
[(forall a. Prime a -> a
unPrime -> a
2, Word
1), (Prime a
p, Word
k)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some forall a b. (a -> b) -> a -> b
$ forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
[(Prime a
p, Word
k), (forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some forall a b. (a -> b) -> a -> b
$ forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
[(Prime a, Word)]
_ -> forall a. Maybe a
Nothing
cyclicGroupFromModulo
:: (Integral a, UniqueFactorisation a)
=> a
-> Maybe (Some (CyclicGroup a))
cyclicGroupFromModulo :: forall a.
(Integral a, UniqueFactorisation a) =>
a -> Maybe (Some (CyclicGroup a))
cyclicGroupFromModulo = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: Nat).
(Integral a, UniqueFactorisation a) =>
a -> Maybe (CyclicGroup a m)
fromModuloInternal
fromModuloInternal
:: (Integral a, UniqueFactorisation a)
=> a
-> Maybe (CyclicGroup a m)
fromModuloInternal :: forall a (m :: Nat).
(Integral a, UniqueFactorisation a) =>
a -> Maybe (CyclicGroup a m)
fromModuloInternal = \case
a
2 -> forall a. a -> Maybe a
Just forall a (m :: Nat). CyclicGroup a m
CG2'
a
4 -> forall a. a -> Maybe a
Just forall a (m :: Nat). CyclicGroup a m
CG4'
a
n
| forall a. Integral a => a -> Bool
even a
n -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(Integral a, UniqueFactorisation a) =>
a -> Maybe (Prime a, Word)
isOddPrimePower (a
n forall a. Integral a => a -> a -> a
`div` a
2)
| Bool
otherwise -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGOddPrimePower' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(Integral a, UniqueFactorisation a) =>
a -> Maybe (Prime a, Word)
isOddPrimePower a
n
isOddPrimePower
:: (Integral a, UniqueFactorisation a)
=> a
-> Maybe (Prime a, Word)
isOddPrimePower :: forall a.
(Integral a, UniqueFactorisation a) =>
a -> Maybe (Prime a, Word)
isOddPrimePower a
n
| forall a. Integral a => a -> Bool
even a
n = forall a. Maybe a
Nothing
| Bool
otherwise = (, Word
k) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. UniqueFactorisation a => a -> Maybe (Prime a)
isPrime a
p
where
(a
p, Word
k) = forall a. Integral a => a -> (a, Word)
highestPower a
n
proofFromCyclicGroup :: Integral a => CyclicGroup a m -> (() :- KnownNat m)
proofFromCyclicGroup :: forall a (m :: Nat).
Integral a =>
CyclicGroup a m -> (() :: Constraint) :- KnownNat m
proofFromCyclicGroup = forall a (m :: Nat).
Integral a =>
SFactors a m -> (() :: Constraint) :- KnownNat m
proofFromSFactors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: Nat). Num a => CyclicGroup a m -> SFactors a m
cyclicGroupToSFactors
sfactorsToCyclicGroup :: (Eq a, Num a) => SFactors a m -> Maybe (CyclicGroup a m)
sfactorsToCyclicGroup :: forall a (m :: Nat).
(Eq a, Num a) =>
SFactors a m -> Maybe (CyclicGroup a m)
sfactorsToCyclicGroup (SFactors [(Prime a, Word)]
fs) = case [(Prime a, Word)]
fs of
[(forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> forall a. a -> Maybe a
Just forall a (m :: Nat). CyclicGroup a m
CG2'
[(forall a. Prime a -> a
unPrime -> a
2, Word
2)] -> forall a. a -> Maybe a
Just forall a (m :: Nat). CyclicGroup a m
CG4'
[(forall a. Prime a -> a
unPrime -> a
2, Word
_)] -> forall a. Maybe a
Nothing
[(Prime a
p, Word
k)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGOddPrimePower' Prime a
p Word
k
[(Prime a
p, Word
k), (forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
[(forall a. Prime a -> a
unPrime -> a
2, Word
1), (Prime a
p, Word
k)] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
[(Prime a, Word)]
_ -> forall a. Maybe a
Nothing
cyclicGroupToSFactors :: Num a => CyclicGroup a m -> SFactors a m
cyclicGroupToSFactors :: forall a (m :: Nat). Num a => CyclicGroup a m -> SFactors a m
cyclicGroupToSFactors = forall a (m :: Nat). [(Prime a, Word)] -> SFactors a m
SFactors forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
CyclicGroup a m
CG2' -> [(forall a. a -> Prime a
Prime a
2, Word
1)]
CyclicGroup a m
CG4' -> [(forall a. a -> Prime a
Prime a
2, Word
2)]
CGOddPrimePower' Prime a
p Word
k -> [(Prime a
p, Word
k)]
CGDoubleOddPrimePower' Prime a
p Word
k -> [(forall a. a -> Prime a
Prime a
2, Word
1), (Prime a
p, Word
k)]
pattern CG2 :: CyclicGroup a m
pattern $mCG2 :: forall {r} {a} {m :: Nat}.
CyclicGroup a m -> ((# #) -> r) -> ((# #) -> r) -> r
CG2 <- CG2'
pattern CG4 :: CyclicGroup a m
pattern $mCG4 :: forall {r} {a} {m :: Nat}.
CyclicGroup a m -> ((# #) -> r) -> ((# #) -> r) -> r
CG4 <- CG4'
pattern CGOddPrimePower :: Prime a -> Word -> CyclicGroup a m
pattern $mCGOddPrimePower :: forall {r} {a} {m :: Nat}.
CyclicGroup a m -> (Prime a -> Word -> r) -> ((# #) -> r) -> r
CGOddPrimePower p k <- CGOddPrimePower' p k
pattern CGDoubleOddPrimePower :: Prime a -> Word -> CyclicGroup a m
pattern $mCGDoubleOddPrimePower :: forall {r} {a} {m :: Nat}.
CyclicGroup a m -> (Prime a -> Word -> r) -> ((# #) -> r) -> r
CGDoubleOddPrimePower p k <- CGDoubleOddPrimePower' p k
{-# COMPLETE CG2, CG4, CGOddPrimePower, CGDoubleOddPrimePower #-}