type-natural-0.4.0.0: Data/Type/Natural.hs
{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-}
{-# LANGUAGE TypeOperators, UndecidableInstances, EmptyCase, LambdaCase #-}
-- | Type level peano natural number, some arithmetic functions and their singletons.
module Data.Type.Natural (-- * Re-exported modules.
module Data.Singletons,
-- * Natural Numbers
-- | Peano natural numbers. It will be promoted to the type-level natural number.
Nat(..),
SSym0, SSym1, ZSym0,
-- | Singleton type for 'Nat'.
SNat, Sing (SZ, SS),
-- ** Arithmetic functions and their singletons.
min, Min, sMin, max, Max, sMax,
MinSym0, MinSym1, MinSym2,
MaxSym0, MaxSym1, MaxSym2,
(:+:), (:+),
(:+$), (:+$$), (:+$$$),
(%+), (%:+), (:*), (:*:),
(:*$), (:*$$), (:*$$$),
(%:*), (%*), (:-:), (:-),
(:**:), (:**), (%:**), (%**),
(:-$), (:-$$), (:-$$$),
(%:-), (%-),
-- ** Type-level predicate & judgements
Leq(..), (:<=), (:<<=),
(:<<=$),(:<<=$$),(:<<=$$$),
(%:<<=), LeqInstance,
boolToPropLeq, boolToClassLeq, propToClassLeq,
LeqTrueInstance, propToBoolLeq,
-- * Conversion functions
natToInt, intToNat, sNatToInt,
-- * Quasi quotes for natural numbers
nat, snat,
-- * Properties of natural numbers
succCongEq, plusCongR, plusCongL, succPlusL, succPlusR,
pluSZR, pluSZL, eqPreserveSS, plusAssociative,
multAssociative, multComm, multZL, multZR, multOneL,
multOneR, snEqZAbsurd, succInjective, plusInjectiveL, plusInjectiveR,
plusMultDistr, multPlusDistr, multCongL, multCongR,
sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent,
eqSuccMinus, plusMinusEqL, plusMinusEqR,
zAbsorbsMinR, zAbsorbsMinL, pluSSR, plusNeutralR, plusNeutralL,
leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,
-- * Properties of ordering 'Leq'
leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,
minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR,
leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd,
-- * Useful type synonyms and constructors
zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven,
twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,
Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten,
Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty,
ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0,
SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0,
ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0,
EighteenSym0, NineteenSym0, TwentySym0,
sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven,
sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty,
n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20,
N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20,
N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0,
sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,
sN15, sN16, sN17, sN18, sN19, sN20
) where
import Data.Type.Natural.Compat
import Data.Type.Natural.Core
import Data.Type.Natural.Definitions hiding ((:<=))
import Data.Constraint hiding ((:-))
import Data.Singletons
import Data.Type.Monomorphic
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Prelude (Bool (..), Eq (..), Int,
Integral (..), Ord ((<)), error,
otherwise, ($), (.))
import Prelude (Ord (..))
import qualified Prelude as P
import Proof.Equational
--------------------------------------------------
-- * Conversion functions.
--------------------------------------------------
-- | Convert integral numbers into 'Nat'
intToNat :: (Integral a, Ord a) => a -> Nat
intToNat 0 = Z
intToNat n
| n < 0 = error "negative integer"
| otherwise = S $ intToNat (n P.- 1)
-- | Convert 'Nat' into normal integers.
natToInt :: Integral n => Nat -> n
natToInt Z = 0
natToInt (S n) = natToInt n P.+ 1
-- | Convert 'SNat n' into normal integers.
sNatToInt :: P.Num n => SNat x -> n
sNatToInt SZ = 0
sNatToInt (SS n) = sNatToInt n P.+ 1
instance Monomorphicable (Sing :: Nat -> *) where
type MonomorphicRep (Sing :: Nat -> *) = Int
demote (Monomorphic sn) = sNatToInt sn
promote n
| n < 0 = error "negative integer!"
| n == 0 = Monomorphic SZ
| otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn
--------------------------------------------------
-- * Properties
--------------------------------------------------
pluSZR :: SNat n -> n :+: 'Z :=: n
pluSZR SZ = Refl
pluSZR (SS n) =
start (SS n %+ SZ)
=~= SS (n %+ SZ)
=== SS n `because` cong' SS (pluSZR n)
eqPreserveSS :: n :=: m -> 'S n :=: 'S m
eqPreserveSS Refl = Refl
pluSZL :: SNat n -> 'Z :+: n :=: n
pluSZL _ = Refl
succCongEq :: n :=: m -> 'S n :=: 'S m
succCongEq Refl = Refl
snEqZAbsurd :: 'S n :=: 'Z -> a
snEqZAbsurd _ = bugInGHC
succInjective :: 'S n :=: 'S m -> n :=: m
succInjective Refl = Refl
plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l
plusInjectiveL SZ _ _ Refl = Refl
plusInjectiveL (SS n) m l eq = plusInjectiveL n m l $ succInjective eq
plusInjectiveR :: SNat n -> SNat m -> SNat l -> n :+ l :=: m :+ l -> n :=: m
plusInjectiveR n m l eq = plusInjectiveL l n m $
start (l %:+ n)
=== n %:+ l `because` plusCommutative l n
=== m %:+ l `because` eq
=== l %:+ m `because` plusCommutative m l
sAndPlusOne :: SNat n -> 'S n :=: n :+: One
sAndPlusOne SZ = Refl
sAndPlusOne (SS n) =
start (SS (SS n))
=== SS (n %+ sOne) `because` cong' SS (sAndPlusOne n)
=~= SS n %+ sOne
plusAssociative :: SNat n -> SNat m -> SNat l
-> n :+: (m :+: l) :=: (n :+: m) :+: l
plusAssociative SZ _ _ = Refl
plusAssociative (SS n) m l =
start (SS n %+ (m %+ l))
=~= SS (n %+ (m %+ l))
=== SS ((n %+ m) %+ l) `because` cong' SS (plusAssociative n m l)
=~= SS (n %+ m) %+ l
=~= (SS n %+ m) %+ l
pluSSR :: SNat n -> SNat m -> 'S (n :+: m) :=: n :+: 'S m
pluSSR n m =
start (SS (n %+ m))
=== (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)
=== n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)
=== n %+ SS m `because` plusCongL n (symmetry $ sAndPlusOne m)
plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'
plusCongL _ Refl = Refl
plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n
plusCongR _ Refl = Refl
succPlusL :: SNat n -> SNat m -> 'S n :+ m :=: 'S (n :+ m)
succPlusL _ _ = Refl
succPlusR :: SNat n -> SNat m -> n :+ 'S m :=: 'S (n :+ m)
succPlusR SZ _ = Refl
succPlusR (SS n) m =
start (SS n %+ SS m)
=~= SS (n %+ SS m)
=== SS (SS (n %+ m)) `because` succCongEq (succPlusR n m)
=~= SS (SS n %+ m)
minusCongEq :: n :=: m -> SNat l -> n :-: l :=: m :-: l
minusCongEq Refl _ = Refl
minusNilpotent :: SNat n -> n :-: n :=: Zero
minusNilpotent SZ = Refl
minusNilpotent (SS n) =
start (SS n %:- SS n)
=~= n %:- n
=== SZ `because` minusNilpotent n
plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n
plusCommutative SZ SZ = Refl
plusCommutative SZ (SS m) =
start (SZ %+ SS m)
=~= SS m
=== SS (m %+ SZ) `because` cong' SS (plusCommutative SZ m)
=~= SS m %+ SZ
plusCommutative (SS n) m =
start (SS n %+ m)
=~= SS (n %+ m)
=== SS (m %+ n) `because` cong' SS (plusCommutative n m)
=== (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)
=== m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)
=== m %+ SS n `because` plusCongL m (symmetry $ sAndPlusOne n)
eqSuccMinus :: ((m :<<= n) ~ 'True)
=> SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m))
eqSuccMinus _ SZ = Refl
eqSuccMinus (SS n) (SS m) =
start (SS (SS n) %:- SS m)
=~= SS n %:- m
=== SS (n %:- m) `because` eqSuccMinus n m
=~= SS (SS n %:- SS m)
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
eqSuccMinus _ _ = bugInGHC
#endif
plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
plusMinusEqL SZ m = minusNilpotent m
plusMinusEqL (SS n) m =
case propToBoolLeq (plusLeqR n m) of
Dict -> transitivity (eqSuccMinus (n %+ m) m) (eqPreserveSS $ plusMinusEqL n m)
plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n
plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)
zAbsorbsMinR :: SNat n -> Min n 'Z :=: 'Z
zAbsorbsMinR SZ = Refl
zAbsorbsMinR (SS n) =
case zAbsorbsMinR n of
Refl -> Refl
zAbsorbsMinL :: SNat n -> Min 'Z n :=: 'Z
zAbsorbsMinL SZ = Refl
zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl
minComm :: SNat n -> SNat m -> Min n m :=: Min m n
minComm SZ SZ = Refl
minComm SZ (SS _) = Refl
minComm (SS _) SZ = Refl
minComm (SS n) (SS m) = case minComm n m of Refl -> Refl
maxZL :: SNat n -> Max 'Z n :=: n
maxZL SZ = Refl
maxZL (SS _) = Refl
maxComm :: SNat n -> SNat m -> (Max n m) :=: (Max m n)
maxComm SZ SZ = Refl
maxComm SZ (SS _) = Refl
maxComm (SS _) SZ = Refl
maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl
maxZR :: SNat n -> Max n 'Z :=: n
maxZR n = transitivity (maxComm n SZ) (maxZL n)
multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l)
multPlusDistr SZ _ _ = Refl
multPlusDistr (SS (n :: SNat n')) m l =
start (SS n %* (m %+ l))
=~= (n %* (m %+ l)) %+ (m %+ l)
=== ((n %* m) %+ (n %* l)) %+ (m %+ l)
`because` plusCongR (m %+ l) (multPlusDistr n m l :: n' :* (m :+ l) :=: (n' :* m) :+ (n' :* l))
=== (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)
=== n %* m %+ (n %*l %+ (l %+ m)) `because` symmetry (plusAssociative (n %* m) (n %* l) (l %+ m))
=== n %* l %+ (l %+ m) %+ n %* m `because` plusCommutative (n %* m) (n %*l %+ (l %+ m))
=== (n %* l %+ l) %+ m %+ n %* m `because` plusCongR (n %* m) (plusAssociative (n %* l) l m)
=~= (SS n %* l) %+ m %+ n %* m
=== (SS n %* l) %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (SS n %* l) m (n %* m))
=== (SS n %* l) %+ ((n %* m) %+ m) `because` plusCongL (SS n %* l) (plusCommutative m (n %* m))
=~= (SS n %* l) %+ (SS n %* m)
=== (SS n %* m) %+ (SS n %* l) `because` plusCommutative (SS n %* l) (SS n %* m)
plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l)
plusMultDistr SZ _ _ = Refl
plusMultDistr (SS n) m l =
start ((SS n %+ m) %* l)
=~= SS (n %+ m) %* l
=~= (n %+ m) %* l %+ l
=== n %* l %+ m %* l %+ l `because` plusCongR l (plusMultDistr n m l)
=== m %* l %+ n %* l %+ l `because` plusCongR l (plusCommutative (n %* l) (m %* l))
=== m %* l %+ (n %* l %+ l) `because` symmetry (plusAssociative (m %* l) (n %*l) l)
=~= m %* l %+ (SS n %* l)
=== (SS n %* l) %+ (m %* l) `because` plusCommutative (m %* l) (SS n %* l)
multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l
multAssociative SZ _ _ = Refl
multAssociative (SS n) m l =
start (SS n %* (m %* l))
=~= n %* (m %* l) %+ (m %* l)
=== (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssociative n m l)
=== (n %* m %+ m) %* l `because` symmetry (plusMultDistr (n %* m) m l)
=~= (SS n %* m) %* l
multZL :: SNat m -> Zero :* m :=: Zero
multZL _ = Refl
multZR :: SNat m -> m :* Zero :=: Zero
multZR SZ = Refl
multZR (SS n) =
start (SS n %* SZ)
=~= n %* SZ %+ SZ
=== SZ %+ SZ `because` plusCongR SZ (multZR n)
=~= SZ
multOneL :: SNat n -> One :* n :=: n
multOneL n =
start (sOne %* n)
=~= sZero %* n %+ n
=~= sZero %:+ n
=~= n
multOneR :: SNat n -> n :* One :=: n
multOneR SZ = Refl
multOneR (SS n) =
start (SS n %* sOne)
=~= n %* sOne %+ sOne
=== n %+ sOne `because` plusCongR sOne (multOneR n)
=== SS n `because` symmetry (sAndPlusOne n)
multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l
multCongL _ Refl = Refl
multCongR :: SNat n -> m :=: l -> m :* n :=: l :* n
multCongR _ Refl = Refl
multComm :: SNat n -> SNat m -> n :* m :=: m :* n
multComm SZ m =
start (SZ %* m)
=~= SZ
=== m %* SZ `because` symmetry (multZR m)
multComm (SS n) m =
start (SS n %* m)
=~= n %* m %+ m
=== m %* n %+ m `because` plusCongR m (multComm n m)
=== m %* n %+ m %* sOne `because` plusCongL (m %* n) (symmetry $ multOneR m)
=== m %* (n %+ sOne) `because` symmetry (multPlusDistr m n sOne)
=== m %* SS n `because` multCongL m (symmetry $ sAndPlusOne n)
plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: 'Z
plusNeutralR SZ m eq =
start m
=~= SZ %:+ m
=== SZ `because` eq
plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq
plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: 'Z
plusNeutralL n m eq = plusNeutralR m n $
start (m %:+ n)
=== n %:+ m `because` plusCommutative m n
=== m `because` eq
--------------------------------------------------
-- * Properties of 'Leq'
--------------------------------------------------
leqRefl :: SNat n -> Leq n n
leqRefl SZ = ZeroLeq SZ
leqRefl (SS n) = SuccLeqSucc $ leqRefl n
leqSucc :: SNat n -> Leq n ('S n)
leqSucc SZ = ZeroLeq sOne
leqSucc (SS n) = SuccLeqSucc $ leqSucc n
leqTrans :: Leq n m -> Leq m l -> Leq n l
leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq
leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
leqTrans _ _ = error "impossible!"
#endif
instance Preorder Leq where
reflexivity = leqRefl
transitivity = leqTrans
plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)
plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)
plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =
case pluSSR m (leqRhs leq) of
Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq
plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'
plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
plusLeqL SZ m = ZeroLeq $ coerce (symmetry $ pluSZL m) m
plusLeqL (SS n) m =
start (SS n)
=<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)
=~= SS n %+ m
plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
plusLeqR n m =
case plusCommutative n m of
Refl -> plusLeqL m n
minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq SZ
minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n
minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)
minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
minLeqR n m = case minComm n m of Refl -> minLeqL m n
leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl
leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreserveSS $ leqAnitsymmetric leq1 leq2
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
leqAnitsymmetric _ _ = error "impossible!"
#endif
maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)
maxLeqL SZ m = ZeroLeq (sMax SZ m)
maxLeqL n SZ = case maxZR n of
Refl -> leqRefl n
maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m
maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
maxLeqR n m = case maxComm n m of
Refl -> maxLeqL m n
leqSnZAbsurd :: Leq ('S n) 'Z -> a
leqSnZAbsurd = \case {}
leqnZElim :: Leq n 'Z -> n :=: 'Z
leqnZElim (ZeroLeq SZ) = Refl
leqSnLeq :: Leq ('S n) m -> Leq n m
leqSnLeq (SuccLeqSucc leq) =
let n = leqLhs leq
m = SS $ leqRhs leq
in start n
=<= SS n `because` leqSucc n
=<= m `because` SuccLeqSucc leq
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
leqSnLeq _ = bugInGHC
#endif
leqPred :: Leq ('S n) ('S m) -> Leq n m
leqPred (SuccLeqSucc leq) = leq
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
leqPred _ = bugInGHC
#endif
leqSnnAbsurd :: Leq ('S n) n -> a
leqSnnAbsurd (SuccLeqSucc leq) =
case leqLhs leq of
SS _ -> leqSnnAbsurd leq
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
_ -> bugInGHC "cannot be occured"
leqSnnAbsurd _ = bugInGHC
#endif
--------------------------------------------------
-- * Quasi Quoter
--------------------------------------------------
-- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type.
--
-- for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@
nat :: QuasiQuoter
nat = QuasiQuoter { quoteExp = P.foldr appE (conE 'Z) . P.flip P.replicate (conE 'S) . P.read
, quotePat = P.foldr (\a b -> conP a [b]) (conP 'Z []) . P.flip P.replicate 'S . P.read
, quoteType = P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read
, quoteDec = error "not implemented"
}
-- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.
--
-- For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@
snat :: QuasiQuoter
snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read
, quotePat = P.foldr (\a b -> conP a [b]) (conP 'SZ []) . P.flip P.replicate 'SS . P.read
, quoteType = appT (conT ''SNat) . P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read
, quoteDec = error "not implemented"
}