type-natural-0.8.3.1: Data/Type/Natural.hs
{-# LANGUAGE CPP, DataKinds, EmptyCase, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GADTs, KindSignatures, LambdaCase, MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-}
{-# LANGUAGE TypeOperators, UndecidableInstances #-}
-- | 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,
#if MIN_VERSION_singletons(2,6,0)
SNat (SZ, SS),
#else
Sing(SZ,SS),
#endif
-- ** Arithmetic functions and their singletons.
min, Min, sMin, max, Max, sMax,
MinSym0, MinSym1, MinSym2,
MaxSym0, MaxSym1, MaxSym2,
type (+),
type (+@#@$), type (+@#@$$), type (+@#@$$$),
(%+), type (*),
type (*@#@$), type (*@#@$$), type (*@#@$$$),
(%*), type (-),
type (**), (%**),
type (-@#@$), type (-@#@$$), type (-@#@$$$),
(%-),
-- ** Type-level predicate & judgements
Leq(..), type (<=), LeqInstance,
boolToPropLeq, boolToClassLeq, propToClassLeq,
propToBoolLeq,
-- * Conversion functions
natToInt, intToNat, sNatToInt,
-- * Quasi quotes for natural numbers
nat, snat,
-- * Properties of natural numbers
IsPeano(..),
plusCong, plusCongR, plusCongL,
snEqZAbsurd, plusInjectiveL, plusInjectiveR,
multCongL, multCongR, multCong,
plusMinusEqL,
plusNeutralR, plusNeutralL,
-- * Properties of ordering 'Leq'
PeanoOrder(..),
reflToSEqual, sLeqReflexive, nonSLeqToLT,
-- * 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.Singleton.Compat
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Natural.Class hiding (One, Zero, sOne, sZero)
import Data.Type.Natural.Core
import Data.Type.Natural.Definitions hiding (type (<=))
import Data.Void
import Language.Haskell.TH (appE, appT, conE, conP, conT)
import Language.Haskell.TH.Quote
import Proof.Equational
import Proof.Propositional hiding (Not)
--------------------------------------------------
-- * 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 - 1)
-- | Convert 'Nat' into normal integers.
natToInt :: Integral n => Nat -> n
natToInt Z = 0
natToInt (S n) = natToInt n + 1
-- | Convert 'SNat n' into normal integers.
sNatToInt :: Num n => SNat x -> n
sNatToInt SZ = 0
sNatToInt (SS n) = sNatToInt n + 1
--------------------------------------------------
-- * Properties
--------------------------------------------------
-- | Since 0.5.0.0
instance IsPeano Nat where
{-# SPECIALISE instance IsPeano Nat #-}
induction base _step SZ = base
induction base step (SS n) = step n (induction base step n)
plusMinus n SZ =
start (n %+ SZ %- SZ)
=== (n %- SZ) `because` minusCongL (plusZeroR n) SZ
=~= n
plusMinus n (SS m) =
start (n %+ SS m %- SS m)
=== SS (n %+ m) %- SS m `because` minusCongL (plusSuccR n m) (SS m)
=~= (n %+ m) %- m
=== n `because` plusMinus n m
succInj Refl = Refl
succOneCong = Refl
succNonCyclic _ a = case a of {}
plusZeroL _ = Refl
plusSuccL _ _ = Refl
multZeroL _ = Refl
multSuccL _ _ = Refl
predSucc _ = Refl
snEqZAbsurd :: SingI n => 'S n :~: 'Z -> a
snEqZAbsurd = absurd . succNonCyclic sing
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 $ succInj 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` plusComm l n
=== m %+ l `because` eq
=== l %+ m `because` plusComm m l
reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n == m)
reflToSEqual SZ _ Refl = Witness
reflToSEqual (SS n) (SS m) Refl = reflToSEqual n m Refl
reflToSEqual (SS _) SZ refl = case refl of {}
sequalToRefl :: SNat n -> SNat m -> IsTrue (n == m) -> n :~: m
sequalToRefl SZ SZ Witness = Refl
sequalToRefl SZ (SS _) witness = case witness of {}
sequalToRefl (SS n) (SS m) Witness = succCong $ sequalToRefl n m Witness
sequalToRefl (SS _) SZ witness = case witness of {}
snequalToNoRefl :: SNat n -> SNat m -> IsTrue (Not (n == m)) -> n :~: m -> Void
snequalToNoRefl SZ _ Witness = \case {}
snequalToNoRefl (SS _) SZ Witness = \case {}
snequalToNoRefl (SS n) (SS m) Witness = \case
Refl -> snequalToNoRefl n m Witness Refl
sequalSym :: SNat n -> SNat m -> (n == m) :~: (m == n)
sequalSym SZ SZ = Refl
sequalSym SZ (SS _) = Refl
sequalSym (SS _) SZ = Refl
sequalSym (SS n) (SS m) = sequalSym n m
sleqFlip :: SNat n -> SNat m -> (n :~: m -> Void) -> (m <= n) :~: Not (n <= m)
sleqFlip SZ SZ neq = absurd $ neq Refl
sleqFlip SZ (SS _) _ = Refl
sleqFlip (SS _) SZ _ = Refl
sleqFlip (SS n) (SS m) neq = sleqFlip n m (neq . succCong)
sLeqReflexive :: SNat n -> SNat m -> IsTrue (n == m) -> IsTrue (n <= m)
sLeqReflexive SZ _ Witness = Witness
sLeqReflexive (SS n) (SS m) Witness = sLeqReflexive n m Witness
sLeqReflexive (SS _) SZ witness = case witness of {}
nonSLeqToLT :: (n <= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT
nonSLeqToLT n m = withRefl (sequalSym n m) $
case m %== n of
STrue -> case sLeqReflexive n m Witness of {}
SFalse ->
case m %<= n of
STrue -> Refl
SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {}
instance PeanoOrder Nat where
{-# SPECIALISE instance PeanoOrder Nat #-}
leqZero _ = Witness
leqSucc _ _ Witness = Witness
viewLeq SZ n Witness = LeqZero n
viewLeq (SS n) (SS m) Witness = LeqSucc n m Witness
viewLeq (SS _) SZ a = case a of {}
ltToLeq n m Refl =
case n %== m of
SFalse -> case n %<= m of
STrue -> Witness
eqlCmpEQ n m Refl =
case n %== m of
STrue -> Refl
SFalse -> absurd $ snequalToNoRefl n m Witness Refl
eqToRefl n m Refl =
case n %== m of
STrue -> sequalToRefl n m Witness
SFalse -> case n %<= m of {}
leqToCmp n m Witness =
case n %== m of
STrue -> Left $ sequalToRefl n m Witness
SFalse -> Right Refl
cmpZero _ = Refl
flipCompare n m =
case n %== m of
STrue -> withRefl (sequalSym n m) Refl
SFalse -> withRefl (sequalSym n m) $
case n %<= m of
STrue -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $
case m %<= n of
SFalse -> Refl
SFalse -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $
case m %<= n of
STrue -> Refl
minLeqL SZ SZ = Witness
minLeqL SZ (SS _) = Witness
minLeqL (SS _) SZ = Witness
minLeqL (SS n) (SS m) = minLeqL n m
minLeqR SZ SZ = Witness
minLeqR SZ (SS _) = Witness
minLeqR (SS _) SZ = Witness
minLeqR (SS n) (SS m) = minLeqR n m
minLargest SZ _ _ _ _ = Witness
minLargest (SS _) SZ SZ _ a = case a of {}
minLargest (SS _) SZ (SS _) a Witness = case a of {}
minLargest (SS _) (SS _) SZ _ a = case a of {}
minLargest (SS n) (SS m) (SS l) Witness Witness =
minLargest n m l Witness Witness
maxLeqL SZ SZ = Witness
maxLeqL SZ (SS _) = Witness
maxLeqL (SS n) SZ = leqRefl n
maxLeqL (SS n) (SS m) = maxLeqL n m
maxLeqR SZ SZ = Witness
maxLeqR (SS _) SZ = Witness
maxLeqR (SS n) (SS m) = maxLeqR n m
maxLeqR SZ (SS m) = leqRefl m
maxLeast _ SZ SZ _ _ = Witness
maxLeast _ SZ (SS _) _ a = a
maxLeast _ (SS _) SZ a _ = a
maxLeast SZ _ (SS n) _ a = absurd $ succLeqZeroAbsurd n a
maxLeast (SS k) (SS l) (SS m) slLEsk smLEsk =
coerce (leqSucc' (sMax l m) k) $
maxLeast k l m
(coerce (sym $ leqSucc' l k) slLEsk)
(coerce (sym $ leqSucc' m k) smLEsk)
leqReversed _ _ = Refl
lneqReversed _ _ = Refl
lneqSuccLeq _ _ = Refl
plusMinusEqL :: SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinusEqL = plusMinus
plusNeutralR :: SNat n -> SNat m -> n + m :~: n -> m :~: 'Z
plusNeutralR n m npmn = plusEqCancelL n m SZ (npmn `trans` sym (plusZeroR n))
plusNeutralL :: SNat n -> SNat m -> n + m :~: m -> n :~: 'Z
plusNeutralL n m npmm = plusNeutralR m n (plusComm m n `trans` npmm)
--------------------------------------------------
-- * 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 = foldr appE (conE 'Z) . flip replicate (conE 'S) . read
, quotePat = foldr (\a b -> conP a [b]) (conP 'Z []) . flip replicate 'S . read
, quoteType = foldr appT (conT 'Z) . flip replicate (conT 'S) . read
, quoteDec = error "not implemented"
}
-- | Quotesi-quoter for 'SNat'. This can be used for an expression.
--
-- For example: @[snat|12|] '%+' [snat| 5 |]@.
snat :: QuasiQuoter
snat = mkSNatQQ [t| Nat |]