type-natural 0.4.2.0 → 0.5.0.0
raw patch · 9 files changed
+1840/−645 lines, 9 filesdep ~ghc-typelits-presburgerdep ~singletons
Dependency ranges changed: ghc-typelits-presburger, singletons
Files
- Data/Type/Natural.hs +204/−389
- Data/Type/Natural/Builtin.hs +193/−101
- Data/Type/Natural/Class.hs +7/−0
- Data/Type/Natural/Class/Arithmetic.hs +541/−0
- Data/Type/Natural/Class/Order.hs +643/−0
- Data/Type/Natural/Core.hs +11/−17
- Data/Type/Natural/Definitions.hs +26/−38
- Data/Type/Ordinal.hs +204/−96
- type-natural.cabal +11/−4
Data/Type/Natural.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, EmptyCase, LambdaCase #-}+{-# 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,@@ -25,34 +25,24 @@ (:-$), (:-$$), (:-$$$), (%:-), (%-), -- ** Type-level predicate & judgements- Leq(..), (:<=), (:<<=),- (:<<=$),(:<<=$$),(:<<=$$$),- (%:<<=), LeqInstance,+ Leq(..), (:<=),+ LeqInstance, boolToPropLeq, boolToClassLeq, propToClassLeq,- LeqTrueInstance, propToBoolLeq,+ propToBoolLeq, -- * Conversion functions natToInt, intToNat, sNatToInt, -- * Quasi quotes for natural numbers nat, snat, -- * Properties of natural numbers- succCongEq, eqPreservesS, succCong, plusCongR, plusCongL,- succPlusL, plusSuccL, succPlusR, plusSuccR,- plusZR, plusZL, plusAssociative, plusAssoc,- multAssociative, multAssoc, multComm, multZL, multZR, multOneL,- multOneR, snEqZAbsurd, succInjective, succInj,+ IsPeano(..),+ plusCongR, plusCongL, snEqZAbsurd, plusInjectiveL, plusInjectiveR,- plusMultDistr, plusMultDistrib, multPlusDistr, multPlusDistrib, multCongL, multCongR,- sAndPlusOne, succAndPlusOneR,- plusComm, plusCommutative, minusCongEq, minusCongL,- minusNilpotent,- eqSuccMinus, plusMinusEqL, plusMinusEqR,- zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL,- leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,+ plusMinusEqL, leqRhs, leqLhs,+ plusNeutralR, plusNeutralL, -- * Properties of ordering 'Leq'- leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,- minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR,- leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd,+ 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,@@ -70,24 +60,26 @@ 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+ )+ where+import Data.Type.Natural.Class hiding (One, Zero, sOne, sZero) import Data.Type.Natural.Core import Data.Type.Natural.Definitions hiding ((:<=)) -import Data.Singletons-import qualified Data.Singletons.Prelude as S-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-import Data.Constraint (Dict(..))+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+import Data.Kind+#endif +import Data.Singletons+import Data.Singletons.Prelude.Ord+import Data.Singletons.Decide+import Data.Type.Monomorphic+import Proof.Equational+import Proof.Propositional hiding (Not)+import Data.Void+import Language.Haskell.TH hiding (Type)+import Language.Haskell.TH.Quote+ -------------------------------------------------- -- * Conversion functions. --------------------------------------------------@@ -97,403 +89,225 @@ intToNat 0 = Z intToNat n | n < 0 = error "negative integer"- | otherwise = S $ intToNat (n P.- 1)+ | otherwise = S $ intToNat (n - 1) -- | Convert 'Nat' into normal integers. natToInt :: Integral n => Nat -> n natToInt Z = 0-natToInt (S n) = natToInt n P.+ 1+natToInt (S n) = natToInt n + 1 -- | Convert 'SNat n' into normal integers.-sNatToInt :: P.Num n => SNat x -> n+sNatToInt :: Num n => SNat x -> n sNatToInt SZ = 0-sNatToInt (SS n) = sNatToInt n P.+ 1+sNatToInt (SS n) = sNatToInt n + 1 instance Monomorphicable (Sing :: Nat -> *) where- type MonomorphicRep (Sing :: Nat -> *) = Int+ type MonomorphicRep (Sing :: Nat -> *) = Integer 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+ | otherwise = withPolymorhic (n - 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) -plusZL :: SNat n -> 'Z :+: n :=: n-plusZL _ = Refl+-- | Since 0.5.0.0+instance IsPeano ('KProxy :: KProxy Nat) where+ induction base _step SZ = base+ induction base step (SS n) = step n (induction base step n) -succCong, succCongEq, eqPreservesS :: n :=: m -> 'S n :=: 'S m-succCong Refl = Refl-succCongEq = succCong-{-# DEPRECATED succCongEq "Will be removed in @0.5.0.0@. Use @'succCong'@ instead." #-}-eqPreservesS = succCong-{-# DEPRECATED eqPreservesS "Will be removed in @0.5.0.0@. Use @'succCong'@ instead." #-}+ 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 -snEqZAbsurd :: 'S n :=: 'Z -> a-snEqZAbsurd _ = bugInGHC+ succInj Refl = Refl+ succOneCong = Refl+ succNonCyclic _ a = case a of {} -succInj, succInjective :: 'S n :=: 'S m -> n :=: m-succInj Refl = Refl-succInjective = succInj-{-# DEPRECATED succInjective "Will be removed in @0.5.0.0@. \- Use @'succInj'@ instead." #-}+ plusZeroL _ = Refl + plusSuccL _ _ = Refl -plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l+ 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 $ succInjective eq+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 :: 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+ === n %:+ l `because` plusComm l n === m %:+ l `because` eq- === l %:+ m `because` plusCommutative m l--succAndPlusOneR, sAndPlusOne :: SNat n -> 'S n :=: n :+: One-succAndPlusOneR SZ = Refl-succAndPlusOneR (SS n) =- start (SS (SS n))- === SS (n %+ sOne) `because` cong' SS (succAndPlusOneR n)- =~= SS n %+ sOne-sAndPlusOne = succAndPlusOneR-{-# DEPRECATED sAndPlusOne "Will be removed in @0.5.0.0@. Use @'succAndPlusOneR'@ instead." #-}--plusAssoc, plusAssociative :: SNat n -> SNat m -> SNat l- -> n :+: (m :+: l) :=: (n :+: m) :+: l-plusAssoc SZ _ _ = Refl-plusAssoc (SS n) m l =- start (SS n %+ (m %+ l))- =~= SS (n %+ (m %+ l))- === SS ((n %+ m) %+ l) `because` cong' SS (plusAssoc n m l)- =~= SS (n %+ m) %+ l- =~= (SS n %+ m) %+ l-plusAssociative = plusAssoc-{-# DEPRECATED plusAssociative "Will be removed in @0.5.0.0@. Use @'plusAssoc'@ instead." #-}--plusSR :: SNat n -> SNat m -> 'S (n :+: m) :=: n :+: 'S m-plusSR n m =- start (SS (n %+ m))- === (n %+ m) %+ sOne `because` succAndPlusOneR (n %+ m)- === n %+ (m %+ sOne) `because` symmetry (plusAssoc n m sOne)- === n %+ SS m `because` plusCongL n (symmetry $ succAndPlusOneR m)--{-# DEPRECATED plusSR "Will be removed in @0.5.0.0@. Use @'plusSuccR'@ instead." #-}---plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'-plusCongL _ Refl = Refl--plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n-plusCongR _ Refl = Refl--plusSuccL, succPlusL :: SNat n -> SNat m -> 'S n :+ m :=: 'S (n :+ m)-plusSuccL _ _ = Refl-succPlusL = plusSuccL-{-# DEPRECATED succPlusL "Will be removed in @0.5.0.0@. Use @'plusSuccL'@ instead." #-}--plusSuccR, succPlusR :: SNat n -> SNat m -> n :+ 'S m :=: 'S (n :+ m)-plusSuccR SZ _ = Refl-plusSuccR (SS n) m =- start (SS n %+ SS m)- =~= SS (n %+ SS m)- === SS (SS (n %+ m)) `because` succCong (plusSuccR n m)- =~= SS (SS n %+ m)--succPlusR = plusSuccR--{-# DEPRECATED succPlusR "Will be removed in @0.5.0.0@. Use @'plusSuccR'@ instead." #-}---minusCongEq, minusCongL :: n :=: m -> SNat l -> n :-: l :=: m :-: l-minusCongL Refl _ = Refl-minusCongEq = minusCongL-{-# DEPRECATED minusCongEq "Will be removed in @0.5.0.0@. Use @'minusCongL'@ instead." #-}--minusNilpotent :: SNat n -> n :-: n :=: Zero-minusNilpotent SZ = Refl-minusNilpotent (SS n) =- start (SS n %:- SS n)- =~= n %:- n- === SZ `because` minusNilpotent n---plusComm, plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n-plusComm SZ SZ = Refl-plusComm SZ (SS m) =- start (SZ %+ SS m)- =~= SS m- === SS (m %+ SZ) `because` cong' SS (plusCommutative SZ m)- =~= SS m %+ SZ-plusComm (SS n) m =- start (SS n %+ m)- =~= SS (n %+ m)- === SS (m %+ n) `because` cong' SS (plusCommutative n m)- === (m %+ n) %+ sOne `because` succAndPlusOneR (m %+ n)- === m %+ (n %+ sOne) `because` symmetry (plusAssoc m n sOne)- === m %+ SS n `because` plusCongL m (symmetry $ succAndPlusOneR n)--plusCommutative = plusComm-{-# DEPRECATED plusCommutative "Will be removed in @0.5.0.0@. Use @'plusComm'@ instead." #-}+ === l %:+ m `because` plusComm m l -eqSuccMinus :: ((m S.:<= 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+-- 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 +reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n :== m)+reflToSEqual SZ _ Refl = Witness+reflToSEqual (SS n) (SS m) Refl =+ case reflToSEqual n m Refl of+ Witness -> Witness+reflToSEqual (SS _) SZ refl = case refl of {} -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) (succCong $ plusMinusEqL n m)+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 {} -plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n-plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)+snequalToNoRefl :: SNat n -> SNat m -> IsTrue (Not (n :== m)) -> n :~: m -> Void+snequalToNoRefl SZ _ Witness = \case {}+snequalToNoRefl (SS _) _ Witness = \case {} -zAbsorbsMinR :: SNat n -> Min n 'Z :=: 'Z-zAbsorbsMinR SZ = Refl-zAbsorbsMinR (SS n) =- case zAbsorbsMinR n of+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) =+ case sequalSym n m 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, multPlusDistrib :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l)-multPlusDistrib SZ _ _ = Refl-multPlusDistrib (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) (multPlusDistrib 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 (plusAssoc (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) (plusAssoc (n %* l) l m)- =~= (SS n %* l) %+ m %+ n %* m- === (SS n %* l) %+ (m %+ (n %* m)) `because` symmetry (plusAssoc (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)-multPlusDistr = multPlusDistrib-{-# DEPRECATED multPlusDistr "Will be removed in @0.5.0.0@. Use @'multPlusDistrib'@ instead." #-}--plusMultDistr, plusMultDistrib :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l)-plusMultDistrib SZ _ _ = Refl-plusMultDistrib (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 (plusMultDistrib n m l)- === m %* l %+ n %* l %+ l `because` plusCongR l (plusCommutative (n %* l) (m %* l))- === m %* l %+ (n %* l %+ l) `because` symmetry (plusAssoc (m %* l) (n %*l) l)- =~= m %* l %+ (SS n %* l)- === (SS n %* l) %+ (m %* l) `because` plusCommutative (m %* l) (SS n %* l)--plusMultDistr = plusMultDistrib-{-# DEPRECATED plusMultDistr "Will be removed in @0.5.0.0@. Use @'plusMultDistrib'@ instead." #-}--multAssoc, multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l-multAssoc SZ _ _ = Refl-multAssoc (SS n) m l =- start (SS n %* (m %* l))- =~= n %* (m %* l) %+ (m %* l)- === (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssoc n m l)- === (n %* m %+ m) %* l `because` symmetry (plusMultDistrib (n %* m) m l)- =~= (SS n %* m) %* l-multAssociative = multAssoc-{-# DEPRECATED multAssociative "Will be removed in @0.5.0.0@. Use @'multAssoc'@ instead." #-}-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 (succAndPlusOneR 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 (multPlusDistrib m n sOne)- === m %* SS n `because` multCongL m (symmetry $ succAndPlusOneR 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+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 =+ case sleqFlip n m (neq . succCong) of+ Refl -> Refl ------------------------------------------------------ * Properties of 'Leq'---------------------------------------------------+sLeqReflexive :: SNat n -> SNat m -> IsTrue (n :== m) -> IsTrue (n :<= m)+sLeqReflexive SZ _ Witness = Witness+sLeqReflexive (SS n) (SS m) Witness =+ case sLeqReflexive n m Witness of+ Witness -> Witness+sLeqReflexive (SS _) SZ witness = case witness of {} -leqRefl :: SNat n -> Leq n n-leqRefl SZ = ZeroLeq SZ-leqRefl (SS n) = SuccLeqSucc $ leqRefl n+nonSLeqToLT :: (n :<= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT+nonSLeqToLT n m =+ case sequalSym n m of+ Refl -> + 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 {} -leqSucc :: SNat n -> Leq n ('S n)-leqSucc SZ = ZeroLeq sOne-leqSucc (SS n) = SuccLeqSucc $ leqSucc n+instance PeanoOrder ('KProxy :: KProxy Nat) where+ 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 {} -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+ ltToLeq n m Refl =+ case n %:== m of+ SFalse -> case n %:<= m of+ STrue -> Witness+ _ -> bugInGHC+ _ -> bugInGHC -instance Preorder Leq where- reflexivity = leqRefl- transitivity = leqTrans+ eqlCmpEQ n m Refl =+ case n %:== m of+ STrue -> Refl+ SFalse -> absurd $ snequalToNoRefl n m Witness Refl -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 sym $ plusSuccR m (leqRhs leq) of- Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq-plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'+ eqToRefl n m Refl =+ case n %:== m of+ STrue -> sequalToRefl n m Witness+ SFalse -> case n %:<= m of {} -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+ leqToCmp n m Witness =+ case n %:== m of+ STrue -> Left $ sequalToRefl n m Witness+ SFalse -> Right Refl -plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)-plusLeqR n m =- case plusCommutative n m of- Refl -> plusLeqL m n+ flipCompare n m =+ case n %:== m of+ STrue -> case sequalSym n m of+ Refl -> Refl+ SFalse ->+ case sequalSym n m of+ Refl -> + case n %:<= m of+ STrue ->+ case sleqFlip n m (snequalToNoRefl n m Witness) of+ Refl -> case m %:<= n of+ SFalse -> Refl+ SFalse ->+ case sleqFlip n m (snequalToNoRefl n m Witness) of+ Refl -> case m %:<= n of+ STrue -> Refl -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)+ minLeqL SZ SZ = Witness+ minLeqL SZ (SS _) = Witness+ minLeqL (SS _) SZ = Witness+ minLeqL (SS n) (SS m) = 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+ minLeqR SZ SZ = Witness+ minLeqR SZ (SS _) = Witness+ minLeqR (SS _) SZ = Witness+ minLeqR (SS n) (SS m) = minLeqR n m -leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m-leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl-leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = succCong $ leqAnitsymmetric leq1 leq2-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-leqAnitsymmetric _ _ = error "impossible!"-#endif+ 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 :: 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+ maxLeqL SZ SZ = Witness+ maxLeqL SZ (SS _) = Witness+ maxLeqL (SS n) SZ = leqRefl n+ maxLeqL (SS n) (SS m) = 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+ maxLeqR SZ SZ = Witness+ maxLeqR (SS _) SZ = Witness+ maxLeqR (SS n) (SS m) = maxLeqR n m+ maxLeqR SZ (SS m) = leqRefl m -leqSnZAbsurd :: Leq ('S n) 'Z -> a-leqSnZAbsurd = \case {}+ maxLeast SZ SZ SZ Witness _ = Witness+ maxLeast SZ SZ (SS _) a _ = case a of {}+ maxLeast SZ (SS _) SZ a _ = case a of {}+ maxLeast SZ (SS _) (SS _) a _ = case a of {}+ maxLeast (SS _) _ _ _ a = case a of {} -leqnZElim :: Leq n 'Z -> n :=: 'Z-leqnZElim (ZeroLeq SZ) = Refl+ leqReversed _ _ = Refl+ lneqReversed _ _ = Refl+ lneqSuccLeq _ _ = 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+plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :~: n+plusMinusEqL = plusMinus -leqPred :: Leq ('S n) ('S m) -> Leq n m-leqPred (SuccLeqSucc leq) = leq-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-leqPred _ = bugInGHC-#endif+plusNeutralR :: SNat n -> SNat m -> n :+ m :~: n -> m :~: 'Z+plusNeutralR n m npmn = plusEqCancelL n m SZ (npmn `trans` sym (plusZeroR n)) -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+plusNeutralL :: SNat n -> SNat m -> n :+ m :~: m -> n :~: 'Z+plusNeutralL n m npmm = plusNeutralR m n (plusComm m n `trans` npmm) -------------------------------------------------- -- * Quasi Quoter@@ -503,9 +317,9 @@ -- -- 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+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" } @@ -513,8 +327,9 @@ -- -- 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+snat = QuasiQuoter { quoteExp = foldr appE (conE 'SZ) . flip replicate (conE 'SS) . read+ , quotePat = foldr (\a b -> conP a [b]) (conP 'SZ []) . flip replicate 'SS . read+ , quoteType = appT (conT ''SNat) . foldr appT (conT 'Z) . flip replicate (conT 'S) . read , quoteDec = error "not implemented" }+
Data/Type/Natural/Builtin.hs view
@@ -1,5 +1,7 @@-{-# LANGUAGE ConstraintKinds, CPP, DataKinds, GADTs, PolyKinds, RankNTypes #-}-{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}+{-# LANGUAGE CPP, ConstraintKinds, DataKinds, EmptyCase, ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts, GADTs, InstanceSigs, PolyKinds, RankNTypes #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} -- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@@@ -20,34 +22,40 @@ fromPeanoMultCong, toPeanoMultCong, fromPeanoMonotone, toPeanoMonotone, -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@- plusZR, plusZL, plusSuccR, plusSuccL,- multZR, multZL, multSuccR, multSuccL,+ IsPeano(..), inductionNat,- plusComm, multComm, plusAssoc, multAssoc,- plusMultDistr, multPlusDistr ) where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+import Data.Type.Natural.Class import Data.Type.Natural.Compat-#endif -import Data.Promotion.Prelude.Enum (Succ)-import Data.Singletons (Sing, SingI, sing)-import Data.Singletons.Decide (Decision (..), (%~))-import Data.Singletons.Decide (Void)-import Data.Singletons.Prelude.Bool (Sing (..))-import Data.Singletons.Prelude.Ord (POrd(..), SOrd ((%:<=)))-import Data.Singletons.Prelude.Enum (Pred, sPred, sSucc)-import Data.Singletons.Prelude.Num (SNum (..))+import Data.Singletons.Decide (SDecide (..))+import Data.Singletons.Decide (Decision (..))+import Data.Singletons.Prelude (PNum (..), SNum (..), Sing (..))+import Data.Singletons.Prelude (SingI (..))+import Data.Singletons.Prelude (KProxy (..))+import Data.Singletons.Prelude (SingKind (..), SomeSing (..))+import Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..))+import Data.Singletons.Prelude.Ord (POrd (..), SOrd (..))+import Data.Singletons.TH (sCases)+import Data.Singletons.TypeLits (withKnownNat)+import Data.Type.Equality ((:~:) (..))+import Data.Type.Monomorphic (Monomorphic (..))+import Data.Type.Monomorphic (Monomorphicable (..)) import Data.Type.Natural (Nat (S, Z), Sing (SS, SZ))-import Data.Type.Natural (plusCongR) import qualified Data.Type.Natural as PN import Data.Void (absurd)+import Data.Void (Void)+import GHC.TypeLits (type (+), type (<=), type (<=?)) import qualified GHC.TypeLits as TL-import Proof.Equational ((:=:), (:~:) (Refl), coerce)+import Proof.Equational (coerce) import Proof.Equational (start, sym, (===), (=~=)) import Proof.Equational (because)+import Proof.Propositional (Empty (..), IsTrue (..)) import Unsafe.Coerce (unsafeCoerce)+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+import Data.Kind+#endif -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@. type Peano = PN.Nat@@ -60,11 +68,7 @@ ToPeano 0 = 'Z ToPeano n = 'S (ToPeano (Pred n)) -data NatView (n :: TL.Nat) where- IsZero :: NatView 0- IsSucc :: Sing n -> NatView (Succ n)--viewNat :: Sing n -> NatView n+viewNat :: Sing (n :: TL.Nat) -> ZeroOrSucc n viewNat n = case n %~ (sing :: Sing 0) of Proved Refl -> IsZero@@ -74,16 +78,16 @@ sFromPeano SZ = sing sFromPeano (SS sn) = sSucc (sFromPeano sn) -toPeanoInjective :: ToPeano n :=: ToPeano m -> n :=: m+toPeanoInjective :: ToPeano n :~: ToPeano m -> n :~: m toPeanoInjective Refl = Refl --- trustMe :: a :=: b--- trustMe = unsafeCoerce (Refl :: () :=: ())+-- trustMe :: a :~: b+-- trustMe = unsafeCoerce (Refl :: () :~: ()) -- {-# WARNING trustMe -- "Used unproven type-equalities; This may cause disastrous result..." #-} -toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :=: 'S (ToPeano n)-toPeanoSuccCong _ = unsafeCoerce (Refl :: () :=: ())+toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :~: 'S (ToPeano n)+toPeanoSuccCong _ = unsafeCoerce (Refl :: () :~: ()) -- We cannot prove this lemma within Haskell, so we assume it a priori. sToPeano :: Sing n -> Sing (ToPeano n)@@ -93,27 +97,27 @@ Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn))) -- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat).--- Succ n :=: Succ m -> n :=: m+-- Succ n :~: Succ m -> n :~: m -- litSuccInjective Refl = Refl -toFromPeano :: Sing n -> ToPeano (FromPeano n) :=: n+toFromPeano :: Sing n -> ToPeano (FromPeano n) :~: n toFromPeano SZ = Refl toFromPeano (SS sn) = start (sToPeano (sFromPeano (SS sn))) =~= sToPeano (sSucc (sFromPeano sn)) === SS (sToPeano (sFromPeano sn)) `because` toPeanoSuccCong (sFromPeano sn)- === SS sn `because` PN.succCong (toFromPeano sn)+ === SS sn `because` succCong (toFromPeano sn) -congFromPeano :: n :=: m -> FromPeano n :=: FromPeano m+congFromPeano :: n :~: m -> FromPeano n :~: FromPeano m congFromPeano Refl = Refl -congToPeano :: n :=: m -> ToPeano n :=: ToPeano m+congToPeano :: n :~: m -> ToPeano n :~: ToPeano m congToPeano Refl = Refl -congSucc :: n :=: m -> Succ n :=: Succ m+congSucc :: n :~: m -> Succ n :~: Succ m congSucc Refl = Refl -fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n+fromToPeano :: Sing n -> FromPeano (ToPeano n) :~: n fromToPeano sn = case viewNat sn of IsZero -> Refl@@ -126,7 +130,7 @@ === sSucc n1 `because` congSucc (fromToPeano n1) fromPeanoInjective :: forall n m. (SingI n, SingI m)- => FromPeano n :=: FromPeano m -> n :=: m+ => FromPeano n :~: FromPeano m -> n :~: m fromPeanoInjective frEq = let sn = sing :: Sing n sm = sing :: Sing m@@ -135,10 +139,10 @@ === sToPeano (sFromPeano sm) `because` congToPeano frEq === sm `because` toFromPeano sm -fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :=: Succ (FromPeano n)+fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :~: Succ (FromPeano n) fromPeanoSuccCong _sn = Refl -fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :=: FromPeano n TL.+ FromPeano m+fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :~: FromPeano n :+ FromPeano m fromPeanoPlusCong SZ _ = Refl fromPeanoPlusCong (SS sn) sm = start (sFromPeano (SS sn %:+ sm))@@ -148,7 +152,7 @@ =~= sSucc (sFromPeano sn) %:+ sFromPeano sm =~= sFromPeano (SS sn) %:+ sFromPeano sm -toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n TL.+ m) :=: ToPeano n PN.:+ ToPeano m+toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n :+ m) :~: ToPeano n :+ ToPeano m toPeanoPlusCong sn sm = case viewNat sn of IsZero -> Refl@@ -158,28 +162,28 @@ === SS (sToPeano (pn %:+ sm)) `because` toPeanoSuccCong (pn %:+ sm) === SS (sToPeano pn %:+ sToPeano sm)- `because` PN.succCong (toPeanoPlusCong pn sm)+ `because` succCong (toPeanoPlusCong pn sm) =~= SS (sToPeano pn) %:+ sToPeano sm === (sToPeano (sSucc pn) %:+ sToPeano sm)- `because` plusCongR (sToPeano sm) (sym (toPeanoSuccCong pn))+ `because` plusCongL (sym (toPeanoSuccCong pn)) (sToPeano sm) =~= sToPeano sn %:+ sToPeano sm -fromPeanoZeroCong :: FromPeano 'Z :=: 0+fromPeanoZeroCong :: FromPeano 'Z :~: 0 fromPeanoZeroCong = Refl -toPeanoZeroCong :: ToPeano 0 :=: 'Z+toPeanoZeroCong :: ToPeano 0 :~: 'Z toPeanoZeroCong = Refl -fromPeanoOneCong :: FromPeano PN.One :=: 1+fromPeanoOneCong :: FromPeano PN.One :~: 1 fromPeanoOneCong = Refl -toPeanoOneCong :: ToPeano 1 :=: PN.One+toPeanoOneCong :: ToPeano 1 :~: PN.One toPeanoOneCong = Refl -natPlusCongR :: Sing r -> n :=: m -> n TL.+ r :=: m TL.+ r+natPlusCongR :: Sing r -> n :~: m -> n + r :~: m + r natPlusCongR _ Refl = Refl -fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :=: FromPeano n TL.* FromPeano m+fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :~: FromPeano n :* FromPeano m fromPeanoMultCong SZ _ = Refl fromPeanoMultCong (SS psn) sm = start (sFromPeano (SS psn %:* sm))@@ -192,7 +196,7 @@ =~= sFromPeano (SS psn) %:* sFromPeano sm -toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n PN.:* m) :=: ToPeano n PN.:* ToPeano m+toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n PN.:* m) :~: ToPeano n PN.:* ToPeano m toPeanoMultCong sn sm = case viewNat sn of IsZero -> Refl@@ -202,33 +206,28 @@ === sToPeano (psn %:* sm) %:+ sToPeano sm `because` toPeanoPlusCong (psn %:* sm) sm === sToPeano psn %:* sToPeano sm %:+ sToPeano sm- `because` plusCongR (sToPeano sm) (toPeanoMultCong psn sm)+ `because` plusCongL (toPeanoMultCong psn sm) (sToPeano sm) =~= SS (sToPeano psn) %:* sToPeano sm === sToPeano (sSucc psn) %:* sToPeano sm- `because` PN.multCongR (sToPeano sm) (sym (toPeanoSuccCong psn))+ `because` multCongL (sym (toPeanoSuccCong psn)) (sToPeano sm) infix 4 %:<=?-(%:<=?) :: Sing n -> Sing m -> Sing (n TL.<=? m)-sn %:<=? sm =- case viewNat sn of- IsZero -> STrue- IsSucc pn -> case viewNat sm of- IsZero -> SFalse- IsSucc pm ->- case pn %:<=? pm of- STrue -> STrue- SFalse -> SFalse+(%:<=?) :: Sing (n :: TL.Nat) -> Sing m -> Sing (n <=? m)+n %:<=? m = case sCompare n m of+ SLT -> STrue+ SEQ -> STrue+ SGT -> SFalse -natLeqSuccEq :: Sing n -> Sing m -> ((n TL.+ 1) TL.<=? (m TL.+ 1)) :~: (n TL.<=? m)+natLeqSuccEq :: Sing n -> Sing m -> ((n + 1) <=? (m + 1)) :~: (n <=? m) natLeqSuccEq _ _ = Refl -leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? z)+leqqCong :: n :~: m -> l :~: z -> (n <=? l) :~: (m <=? z) leqqCong Refl Refl = Refl -leqCong :: n :=: m -> l :=: z -> (n :<= l) :~: (m :<= z)+leqCong :: n :~: m -> l :~: z -> (n :<= l) :~: (m :<= z) leqCong Refl Refl = Refl -fromPeanoMonotone :: ((n :<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True+fromPeanoMonotone :: ((n :<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :~: 'True fromPeanoMonotone SZ _ = Refl fromPeanoMonotone (SS n) (SS m) = start (sFromPeano (SS n) %:<=? sFromPeano (SS m))@@ -242,30 +241,31 @@ fromPeanoMonotone _ _ = bugInGHC #endif -natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0-natLeqZero _ = Refl+natLeqZero :: (n <= 0) => Sing n -> n :~: 0+natLeqZero Zero = Refl+natLeqZero _ = error "natLeqZero : bug in ghc" -- | Currently, ghc-typelits-natnormalise reduces @(0 - 1) + 1@ to @0@, -- which is contradictory to current GHC's behaviour. -- So our assumption @((n :~: 0) -> Void)@ is simply disregarded.-natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :=: n+natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :~: n natSuccPred _ = Refl -myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :=: (n :<= m)+myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :~: (n :<= m) myLeqPred SZ _ = Refl myLeqPred (SS _) (SS _) = Refl myLeqPred (SS _) SZ = Refl -toPeanoCong :: a :=: b -> ToPeano a :=: ToPeano b+toPeanoCong :: a :~: b -> ToPeano a :~: ToPeano b toPeanoCong Refl = Refl -toPeanoMonotone :: (n TL.<= m)+toPeanoMonotone :: (n <= m) => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True toPeanoMonotone sn sm = case sn %~ (sing :: Sing 0) of Proved Refl -> Refl Disproved nPos -> case sm %~ (sing :: Sing 0) of- Proved Refl -> absurd $ nPos $ natLeqZero sm+ Proved Refl -> absurd $ nPos $ natLeqZero sn Disproved mPos -> let pn = sPred sn pm = sPred sm@@ -280,50 +280,142 @@ === STrue `because` toPeanoMonotone pn pm -- | Induction scheme for built-in @'TL.Nat'@.-inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m TL.+ 1)) -> Sing n -> p n+inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n inductionNat base step snat = case viewNat snat of IsZero -> base IsSucc sl -> step (inductionNat base step sl) -plusZR :: Sing n -> n TL.+ 0 :~: n-plusZR _ = Refl -plusZL :: Sing n -> 0 TL.+ n :~: n-plusZL _ = Refl--plusSuccL :: Sing n -> Sing m -> (Succ n) TL.+ m :~: Succ (n TL.+ m)-plusSuccL _ _ = Refl+instance IsPeano ('KProxy :: KProxy TL.Nat) where+ predSucc _ = Refl+ plusMinus _ _ = Refl+ succInj Refl = Refl+ succOneCong = Refl+ succNonCyclic _ a = case a of { }+ plusZeroR _ = Refl+ plusZeroL _ = Refl+ plusSuccL _ _ = Refl+ plusSuccR _ _ = Refl+ multZeroL _ = Refl+ multZeroR _ = Refl+ multSuccL _ _ = Refl+ multSuccR _ _ = Refl+ plusComm _ _ = Refl+ multComm _ _ = Refl+ plusAssoc _ _ _ = Refl+ multAssoc _ _ _ = Refl+ plusMultDistrib _ _ _ = Refl+ multPlusDistrib _ _ _ = Refl+ induction base step snat =+ case viewNat snat of+ IsZero -> base+ IsSucc sl ->+ withKnownNat sl $ step sing (induction base step sl) -plusSuccR :: Sing n -> Sing m -> n TL.+ (Succ m) :~: Succ (n TL.+ m)-plusSuccR _ _ = Refl+maxCompareFlip :: Sing n -> Sing m -> TL.CmpNat m n :~: 'LT -> Max n m :~: n+maxCompareFlip n m mLTn =+ case sCompare n m of+ SLT -> eliminate $+ start SLT === sCompare m n `because` sym mLTn+ === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)+ =~= SGT+ SEQ -> eliminate $+ start SLT === sCompare m n `because` sym mLTn+ === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)+ =~= SEQ+ SGT -> Refl -multZL :: Sing n -> 0 TL.* n :~: 0-multZL _ = Refl+minCompareFlip :: Sing n -> Sing m -> TL.CmpNat m n :~: 'LT -> Min n m :~: m+minCompareFlip n m mLTn =+ case sCompare n m of+ SLT -> eliminate $+ start SLT === sCompare m n `because` sym mLTn+ === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)+ =~= SGT+ SEQ -> eliminate $+ start SLT === sCompare m n `because` sym mLTn+ === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)+ =~= SEQ+ SGT -> Refl -multZR :: Sing n -> n TL.* 0 :~: 0-multZR _ = Refl+type family MyLeqHelper n m o where+ MyLeqHelper n m 'LT = 'True+ MyLeqHelper n m 'EQ = 'True+ MyLeqHelper n m 'GT = 'False -multSuccL :: Sing n -> Sing m -> Succ n TL.* m :~: (n TL.* m) TL.+ m-multSuccL _ _ = Refl+instance PeanoOrder ('KProxy :: KProxy TL.Nat) where+ eqlCmpEQ _ _ Refl = Refl+ ltToLeq _ _ Refl = Witness+ succLeqToLT m n Witness =+ case sCompare (sSucc m) n of+ SLT -> Refl+ SEQ -> Refl+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+ _ -> bugInGHC+#endif+ cmpZero _ = Refl+ leqRefl _ = Witness+ eqToRefl _ _ Refl = Refl+ flipCompare n m = $(sCases ''Ordering [|sCompare n m|] [|Refl|])+ leqToCmp n m Witness =+ case sCompare n m of+ SLT -> Right Refl+ SEQ -> Left Refl+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+ _ -> bugInGHC+#endif -multSuccR :: Sing n -> Sing m -> n TL.* Succ m :~: (n TL.* m) TL.+ n-multSuccR _ _ = Refl+ leqToMin _ _ Witness = Refl+ leqToMax _ _ Witness = Refl+ geqToMax n m mLEQn =+ case leqToCmp m n mLEQn of+ Left Refl -> Refl+ Right mLTn ->+ maxCompareFlip n m mLTn+ geqToMin n m mLEQn =+ case leqToCmp m n mLEQn of+ Left Refl -> Refl+ Right mLTn ->+ minCompareFlip n m mLTn -plusComm :: Sing n -> Sing m -> (n TL.+ m) :~: (m TL.+ n)-plusComm _ _ = Refl+ lneqReversed n m =+ case flipCompare n m of+ Refl -> case sCompare n m of+ SEQ -> Refl+ SLT -> Refl+ SGT -> Refl -multComm :: Sing n -> Sing m -> (n TL.* m) :~: (m TL.* n)-multComm _ _ = Refl+ leqReversed n m =+ case flipCompare n m of+ Refl -> case sCompare n m of+ SEQ -> Refl+ SLT -> Refl+ SGT -> Refl -plusAssoc :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.+ l :~: n TL.+ (m TL.+ l)-plusAssoc _ _ _ = Refl+ lneqSuccLeq n m =+ case sCompare n m of+ SEQ ->+ start (n %:< m)+ =~= SFalse+ === (sSucc n %:<= n) `because` sym (succLeqAbsurd' n)+ === (sSucc n %:<= m) `because` sLeqCongR (sSucc n) (eqToRefl n m Refl)+ SLT ->+ case ltToSuccLeq n m Refl of+ Witness ->+ start (n %:< m)+ =~= STrue+ =~= (sSucc n %:<= m)+ SGT ->+ case sSucc n %:<= m of+ SFalse -> Refl+ STrue -> eliminate $ succLeqToLT n m Witness -multAssoc :: Sing n -> Sing m -> Sing l -> (n TL.* m) TL.* l :~: n TL.* (m TL.* l)-multAssoc _ _ _ = Refl+instance Monomorphicable (Sing :: TL.Nat -> *) where+ type MonomorphicRep (Sing :: TL.Nat -> *) = Integer+ demote (Monomorphic sn) = fromSing sn+ {-# INLINE demote #-} -plusMultDistr :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.* l :~: n TL.* l TL.+ m TL.* l-plusMultDistr _ _ _ = Refl+ promote n = case toSing n of SomeSing k -> Monomorphic k+ {-# INLINE promote #-} -multPlusDistr :: Sing n -> Sing m -> Sing l -> n TL.* (m TL.+ l) :~: n TL.* m TL.+ n TL.* l-multPlusDistr _ _ _ = Refl
+ Data/Type/Natural/Class.hs view
@@ -0,0 +1,7 @@+-- | Re-exports arithmetic and order structure for peano arithmetic.+module Data.Type.Natural.Class ( module Data.Type.Natural.Class.Arithmetic+ , module Data.Type.Natural.Class.Order+ ) where+import Data.Type.Natural.Class.Arithmetic+import Data.Type.Natural.Class.Order+
+ Data/Type/Natural/Class/Arithmetic.hs view
@@ -0,0 +1,541 @@+{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+module Data.Type.Natural.Class.Arithmetic+ (Zero, One, S, sZero, sOne, ZeroOrSucc(..),+ plusCong, plusCongR, plusCongL, succCong,+ multCong, multCongL, multCongR,+ minusCong, minusCongL, minusCongR,+ IsPeano(..), pattern Zero, pattern Succ+ ) where+import Data.Singletons.Decide+import Data.Singletons.Prelude+import Data.Singletons.Prelude.Enum+import Data.Type.Equality+import Data.Void+import Proof.Equational+import Proof.Propositional++type family Zero (kproxy :: KProxy nat) :: nat where+ Zero 'KProxy = FromInteger 0++sZero :: (SNum kproxy) => Sing (Zero kproxy)+sZero = sFromInteger (sing :: Sing 0)++type family One (kproxy :: KProxy nat) :: nat where+ One 'KProxy = FromInteger 1++sOne :: SNum kproxy => Sing (One kproxy)+sOne = sFromInteger (sing :: Sing 1)++type S n = Succ n++sS :: SEnum ('KProxy :: KProxy nat) => Sing (n :: nat) -> Sing (S n)+sS = sSucc++predCong :: n :~: m -> Pred n :~: Pred m+predCong Refl = Refl++plusCong :: n :~: m -> n' :~: m' -> n :+ n' :~: m :+ m'+plusCong Refl Refl = Refl++plusCongL :: n :~: m -> Sing k -> n :+ k :~: m :+ k+plusCongL Refl _ = Refl++plusCongR :: Sing k -> n :~: m -> k :+ n :~: k :+ m+plusCongR _ Refl = Refl++succCong :: n :~: m -> S n :~: S m+succCong Refl = Refl++multCong :: n :~: m -> l :~: k -> n :* l :~: m :* k+multCong Refl Refl = Refl++multCongL :: n :~: m -> Sing k -> n :* k :~: m :* k+multCongL Refl _ = Refl++multCongR :: Sing k -> n :~: m -> k :* n :~: k :* m+multCongR _ Refl = Refl++minusCong :: n :~: m -> l :~: k -> n :- l :~: m :- k+minusCong Refl Refl = Refl++minusCongL :: n :~: m -> Sing k -> n :- k :~: m :- k+minusCongL Refl _ = Refl++minusCongR :: Sing k -> n :~: m -> k :- n :~: k :- m+minusCongR _ Refl = Refl++data ZeroOrSucc (n :: nat) where+ IsZero :: ZeroOrSucc (Zero 'KProxy)+ IsSucc :: Sing n -> ZeroOrSucc (Succ n)++newtype Assoc op n = Assoc { assocProof :: forall k l. Sing k -> Sing l ->+ Apply (op (Apply (op n) k)) l :~:+ Apply (op n) (Apply (op k) l)+ }+++newtype IdentityR op e (n :: nat) = IdentityR { idRProof :: Apply (op n) e :~: n }+newtype IdentityL op e (n :: nat) = IdentityL { idLProof :: Apply (op e) n :~: n }++type PlusZeroR (n :: nat) = IdentityR (:+$$) (Zero 'KProxy) n+newtype PlusSuccR (n :: nat) =+ PlusSuccR { plusSuccRProof :: forall m. Sing m -> n :+ S m :~: S (n :+ m) }++type PlusZeroL (n :: nat) = IdentityL (:+$$) (Zero 'KProxy) n+newtype PlusSuccL (m :: nat) =+ PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n :+ m :~: S (n :+ m) }++newtype Comm op n = Comm { commProof :: forall m. Sing m -> Apply (op n) m :~: Apply (op m) n }++type PlusComm = Comm (:+$$)++data MultZeroL n =+ MultZeroL { multZeroLProof :: !(Zero ('KProxy :: KProxy nat) :* n :~: Zero 'KProxy) }+data MultZeroR (n :: nat) =+ MultZeroR { multZeroRProof :: !(n :* Zero ('KProxy :: KProxy nat) :~: Zero 'KProxy) }++newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n :* m :~: n :* m :+ m }+data MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n :* S m :~: n :* m :+ n }++data PlusMultDistrib n =+ PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l+ -> (n :+ m) :* l :~: n :* l :+ m :* l+ }++newtype PlusEqCancelL n = PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l+ -> n :+ m :~: n :+ l -> m :~: l }++data SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: !(Succ n :~: One 'KProxy :+ n) }+newtype MultEqCancelR n =+ MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l+ -> n :* Succ l :~: m :* Succ l+ -> n :~: m+ }++class (SDecide kproxy, SNum kproxy, SEnum kproxy, kproxy ~ 'KProxy)+ => IsPeano (kproxy :: KProxy nat) where+ {-# MINIMAL succOneCong, succNonCyclic, predSucc, plusMinus,+ succInj, ( (plusZeroL, plusSuccL) | (plusZeroR, plusZeroL))+ , ( (multZeroL, multSuccL) | (multZeroR, multSuccR)),+ induction #-}++ succOneCong :: Succ (Zero kproxy) :~: One kproxy+ succInj :: Succ n :~: Succ (m :: nat) -> n :~: m+ succInj' :: proxy n -> proxy' m -> Succ n :~: Succ (m :: nat) -> n :~: m+ succInj' _ _ = succInj+ succNonCyclic :: Sing n -> Succ n :~: Zero kproxy -> Void+ induction :: p (Zero kproxy) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k+ plusMinus :: Sing (n :: nat) -> Sing m -> n :+ m :- m :~: n++ plusZeroL :: Sing n -> (Zero kproxy :+ n) :~: n+ plusZeroL sn = idLProof (induction base step sn)+ where+ base :: PlusZeroL (Zero kproxy)+ base = IdentityL (plusZeroR sZero)++ step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n)+ step sk (IdentityL ih) = IdentityL $+ start (sZero %:+ sS sk)+ === sS (sZero %:+ sk) `because` plusSuccR sZero sk+ === sS sk `because` succCong ih++ plusSuccL :: Sing n -> Sing m -> S n :+ m :~: S (n :+ m :: nat)+ plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0+ where+ base :: PlusSuccL (Zero kproxy)+ base = PlusSuccL $ \sn ->+ start (sS sn %:+ sZero)+ === sS sn `because` plusZeroR (sS sn)+ === sS (sn %:+ sZero) `because` succCong (sym $ plusZeroR sn)++ step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n)+ step sm (PlusSuccL ih) = PlusSuccL $ \sn ->+ start (sS sn %:+ sS sm)+ === sS (sS sn %:+ sm) `because` plusSuccR (sS sn) sm+ === sS (sS (sn %:+ sm)) `because` succCong (ih sn)+ === sS (sn %:+ sS sm) `because` succCong (sym $ plusSuccR sn sm)++ plusZeroR :: Sing n -> (n :+ Zero kproxy) :~: n+ plusZeroR sn = idRProof (induction base step sn)+ where+ base :: PlusZeroR (Zero kproxy)+ base = IdentityR (plusZeroL sZero)++ step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n)+ step sk (IdentityR ih) = IdentityR $+ start (sS sk %:+ sZero)+ === sS (sk %:+ sZero) `because` plusSuccL sk sZero+ === sS sk `because` succCong ih++ plusSuccR :: Sing n -> Sing m -> n :+ S m :~: S (n :+ m :: nat)+ plusSuccR sn0 = plusSuccRProof (induction base step sn0)+ where+ base :: PlusSuccR (Zero kproxy)+ base = PlusSuccR $ \sk ->+ start (sZero %:+ sS sk)+ === sS sk `because` plusZeroL (sS sk)+ === sS (sZero %:+ sk) `because` succCong (sym $ plusZeroL sk)++ step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n)+ step sn (PlusSuccR ih) = PlusSuccR $ \sk ->+ start (sS sn %:+ sS sk)+ === sS (sn %:+ sS sk) `because` plusSuccL sn (sS sk)+ === sS (sS (sn %:+ sk)) `because` succCong (ih sk)+ === sS (sS sn %:+ sk) `because` succCong (sym $ plusSuccL sn sk)++ plusComm :: Sing n -> Sing m -> n :+ m :~: (m :: nat) :+ n+ plusComm sn0 = commProof (induction base step sn0)+ where+ base :: PlusComm (Zero kproxy)+ base = Comm $ \sk ->+ start (sZero %:+ sk)+ === sk `because` plusZeroL sk+ === (sk %:+ sZero) `because` sym (plusZeroR sk)++ step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n)+ step sn (Comm ih) = Comm $ \sk ->+ start (sS sn %:+ sk)+ === sS (sn %:+ sk) `because` plusSuccL sn sk+ === sS (sk %:+ sn) `because` succCong (ih sk)+ === sk %:+ sS sn `because` sym (plusSuccR sk sn)++ plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l+ -> (n :+ m) :+ l :~: n :+ (m :+ l)+ plusAssoc sn m l = assocProof (induction base step sn) m l+ where+ base :: Assoc (:+$$) (Zero kproxy)+ base = Assoc $ \ sk sl ->+ start ((sZero %:+ sk) %:+ sl)+ === sk %:+ sl+ `because` plusCongL (plusZeroL sk) sl+ === (sZero %:+ (sk %:+ sl))+ `because` sym (plusZeroL (sk %:+ sl))++ step :: forall k . Sing (k :: nat) -> Assoc (:+$$) k -> Assoc (:+$$) (S k)+ step sk (Assoc ih) = Assoc $ \ sl su ->+ start ((sS sk %:+ sl) %:+ su)+ === (sS (sk %:+ sl) %:+ su) `because` plusCongL (plusSuccL sk sl) su+ === sS (sk %:+ sl %:+ su) `because` plusSuccL (sk %:+ sl) su+ === sS (sk %:+ (sl %:+ su)) `because` succCong (ih sl su)+ === sS sk %:+ (sl %:+ su) `because` sym (plusSuccL sk (sl %:+ su))+++ multZeroL :: Sing n -> Zero kproxy :* n :~: Zero kproxy+ multZeroL sn0 = multZeroLProof $ induction base step sn0+ where+ base :: MultZeroL (Zero kproxy)+ base = MultZeroL (multZeroR sZero)++ step :: Sing (k :: nat) -> MultZeroL k -> MultZeroL (S k)+ step sk (MultZeroL ih) = MultZeroL $+ start (sZero %:* sS sk)+ === sZero %:* sk %:+ sZero `because` multSuccR sZero sk+ === sZero %:* sk `because` plusZeroR (sZero %:* sk)+ === sZero `because` ih++ multSuccL :: Sing (n :: nat) -> Sing m -> S n :* m :~: n :* m :+ m+ multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0+ where+ base :: MultSuccL (Zero kproxy)+ base = MultSuccL $ \sk ->+ start (sS sk %:* sZero)+ === sZero `because` multZeroR (sS sk)+ === sk %:* sZero `because` sym (multZeroR sk)+ === sk %:* sZero %:+ sZero `because` sym (plusZeroR (sk %:* sZero))++ step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m)+ step sm (MultSuccL ih) = MultSuccL $ \sk ->+ start (sS sk %:* sS sm)+ === sS sk %:* sm %:+ sS sk+ `because` multSuccR (sS sk) sm+ === (sk %:* sm %:+ sm) %:+ sS sk+ `because` plusCongL (ih sk) (sS sk)+ === sS ((sk %:* sm %:+ sm) %:+ sk)+ `because` plusSuccR (sk %:* sm %:+ sm) sk+ === sS (sk %:* sm %:+ (sm %:+ sk))+ `because` succCong (plusAssoc (sk %:* sm) sm sk)+ === sS (sk %:* sm %:+ (sk %:+ sm))+ `because` succCong (plusCongR (sk %:* sm) (plusComm sm sk))+ === sS ((sk %:* sm %:+ sk) %:+ sm)+ `because` succCong (sym $ plusAssoc (sk %:* sm) sk sm)+ === sS ((sk %:* sS sm) %:+ sm)+ `because` succCong (plusCongL (sym $ multSuccR sk sm) sm)+ === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm)++ multZeroR :: Sing n -> n :* Zero kproxy :~: Zero kproxy+ multZeroR sn0 = multZeroRProof $ induction base step sn0+ where+ base :: MultZeroR (Zero kproxy)+ base = MultZeroR (multZeroR sZero)++ step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k)+ step sk (MultZeroR ih) = MultZeroR $+ start (sS sk %:* sZero)+ === sk %:* sZero %:+ sZero `because` multSuccL sk sZero+ === sk %:* sZero `because` plusZeroR (sk %:* sZero)+ === sZero `because` ih++ multSuccR :: Sing n -> Sing m -> n :* S m :~: n :* m :+ (n :: nat)+ multSuccR sn0 = multSuccRProof $ induction base step sn0+ where+ base :: MultSuccR (Zero kproxy)+ base = MultSuccR $ \sk ->+ start (sZero %:* sS sk)+ === sZero+ `because` multZeroL (sS sk)+ === sZero %:* sk+ `because` sym (multZeroL sk)+ === sZero %:* sk %:+ sZero+ `because` sym (plusZeroR (sZero %:* sk))+++ step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n)+ step sn (MultSuccR ih) = MultSuccR $ \sk ->+ start (sS sn %:* sS sk)+ === sn %:* sS sk %:+ sS sk+ `because` multSuccL sn (sS sk)+ === sS (sn %:* sS sk %:+ sk)+ `because` plusSuccR (sn %:* sS sk) sk+ === sS (sn %:* sk %:+ sn %:+ sk)+ `because` succCong (plusCongL (ih sk) sk)+ === sS (sn %:* sk %:+ (sn %:+ sk))+ `because` succCong (plusAssoc (sn %:* sk) sn sk)+ === sS (sn %:* sk %:+ (sk %:+ sn))+ `because` succCong (plusCongR (sn %:* sk) (plusComm sn sk))+ === sS (sn %:* sk %:+ sk %:+ sn)+ `because` succCong (sym $ plusAssoc (sn %:* sk) sk sn)+ === sS (sS sn %:* sk %:+ sn)+ `because` succCong (plusCongL (sym $ multSuccL sn sk) sn)+ === sS sn %:* sk %:+ sS sn+ `because` sym (plusSuccR (sS sn %:* sk) sn)+++ multComm :: Sing (n :: nat) -> Sing m -> n :* m :~: m :* n+ multComm sn0 = commProof (induction base step sn0)+ where+ base :: Comm (:*$$) (Zero kproxy)+ base = Comm $ \sk ->+ start (sZero %:* sk)+ === sZero `because` multZeroL sk+ === sk %:* sZero `because` sym (multZeroR sk)++ step :: Sing (n :: nat) -> Comm (:*$$) n -> Comm (:*$$) (S n)+ step sn (Comm ih) = Comm $ \sk ->+ start (sS sn %:* sk)+ === sn %:* sk %:+ sk `because` multSuccL sn sk+ === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk+ === sk %:* sS sn `because` sym (multSuccR sk sn)++ multOneR :: Sing n -> n :* One kproxy :~: n+ multOneR sn =+ start (sn %:* sOne)+ === sn %:* sS sZero `because` multCongR sn (sym $ succOneCong)+ === sn %:* sZero %:+ sn `because` multSuccR sn sZero+ === sZero %:+ sn `because` plusCongL (multZeroR sn) sn+ === sn `because` plusZeroL sn++ multOneL :: Sing n -> One kproxy :* n :~: n+ multOneL sn =+ start (sOne %:* sn)+ === sn %:* sOne `because` multComm sOne sn+ === sn `because` multOneR sn++ plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l+ -> (n :+ m) :* l :~: n :* l :+ m :* l+ plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0+ where+ base :: PlusMultDistrib (Zero kproxy)+ base = PlusMultDistrib $ \sk sl ->+ start ((sZero %:+ sk) %:* sl)+ === (sk %:* sl)+ `because` multCongL (plusZeroL sk) sl+ === sZero %:+ (sk %:* sl)+ `because` sym (plusZeroL (sk %:* sl))+ === sZero %:* sl %:+ sk %:* sl+ `because` plusCongL (sym $ multZeroL sl) (sk %:* sl)++ step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n)+ step sn (PlusMultDistrib ih) = PlusMultDistrib $ \sk sl ->+ start ((sS sn %:+ sk) %:* sl)+ === (sS (sn %:+ sk) %:* sl) `because` multCongL (plusSuccL sn sk) sl+ === (sn %:+ sk) %:* sl %:+ sl `because` multSuccL (sn %:+ sk) sl+ === (sn %:* sl %:+ sk %:* sl) %:+ sl `because` plusCongL (ih sk sl) sl+ === sn %:* sl %:+ (sk %:* sl %:+ sl) `because` plusAssoc (sn %:* sl) (sk %:* sl) sl+ === sn %:* sl %:+ (sl %:+ sk %:* sl) `because` plusCongR (sn %:* sl) (plusComm (sk %:* sl) sl)+ === (sn %:* sl %:+ sl) %:+ sk %:* sl `because` sym (plusAssoc (sn %:* sl) sl (sk %:* sl))+ === (sS sn %:* sl) %:+ sk %:* sl `because` plusCongL (sym $ multSuccL sn sl) (sk %:* sl)++ multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l+ -> n :* (m :+ l) :~: n :* m :+ n :* l+ multPlusDistrib n m l =+ start (n %:* (m %:+ l))+ === (m %:+ l) %:* n `because` multComm n (m %:+ l)+ === m %:* n %:+ l %:* n `because` plusMultDistrib m l n+ === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n)++ minusNilpotent :: Sing n -> n :- n :~: Zero kproxy+ minusNilpotent n =+ start (n %:- n)+ === (sZero %:+ n) %:- n `because` minusCongL (sym $ plusZeroL n) n+ === sZero `because` plusMinus sZero n+++ multAssoc :: Sing (n :: nat) -> Sing m -> Sing l+ -> (n :* m) :* l :~: n :* (m :* l)+ multAssoc sn0 = assocProof $ induction base step sn0+ where+ base :: Assoc (:*$$) (Zero kproxy)+ base = Assoc $ \ m l ->+ start (sZero %:* m %:* l)+ === sZero %:* l `because` multCongL (multZeroL m) l+ === sZero `because` multZeroL l+ === sZero %:* (m %:* l) `because` sym (multZeroL (m %:* l))++ step :: Sing (n :: nat) -> Assoc (:*$$) n -> Assoc (:*$$) (S n)+ step n _ = Assoc $ \ m l ->+ start (sS n %:* m %:* l)+ === (n %:* m %:+ m) %:* l `because` multCongL (multSuccL n m) l+ === n %:* m %:* l %:+ m %:* l `because` plusMultDistrib (n %:* m) m l+ === n %:* (m %:* l) %:+ m %:* l `because` plusCongL (multAssoc n m l) (m %:* l)+ === sS n %:* (m %:* l) `because` sym (multSuccL n (m %:* l))++ plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ m :~: n :+ l -> m :~: l+ plusEqCancelL = plusEqCancelLProof . induction base step+ where+ base :: PlusEqCancelL (Zero kproxy)+ base = PlusEqCancelL $ \l m nlnm ->+ start l === sZero %:+ l `because` sym (plusZeroL l)+ === sZero %:+ m `because` nlnm+ === m `because` plusZeroL m++ step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n)+ step n (PlusEqCancelL ih) = PlusEqCancelL $ \l m snlsnm ->+ succInj $ ih (sS l) (sS m) $+ start (n %:+ sS l)+ === sS (n %:+ l) `because` plusSuccR n l+ === sS n %:+ l `because` sym (plusSuccL n l)+ === sS n %:+ m `because` snlsnm+ === sS (n %:+ m) `because` plusSuccL n m+ === n %:+ sS m `because` sym (plusSuccR n m)++ plusEqCancelR :: forall n m l . Sing (n :: nat) -> Sing m -> Sing l -> n :+ l :~: m :+ l -> n :~: m+ plusEqCancelR n m l nlml = plusEqCancelL l n m $+ start (l %:+ n)+ === (n %:+ l) `because` plusComm l n+ === (m %:+ l) `because` nlml+ === (l %:+ m) `because` plusComm m l++ succAndPlusOneL :: Sing n -> Succ n :~: One kproxy :+ n+ succAndPlusOneL = proofSuccPlusL . induction base step+ where+ base :: SuccPlusL (Zero kproxy)+ base = SuccPlusL $+ start (sSucc sZero)+ === sOne `because` succOneCong+ === sOne %:+ sZero `because` sym (plusZeroR sOne)++ step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n)+ step sn (SuccPlusL ih) = SuccPlusL $+ start (sSucc (sSucc sn))+ === sSucc (sOne %:+ sn) `because` succCong ih+ === sOne %:+ sSucc sn `because` sym (plusSuccR sOne sn)++ succAndPlusOneR :: Sing n -> Succ n :~: n :+ One kproxy+ succAndPlusOneR n =+ start (sSucc n)+ === sOne %:+ n `because` succAndPlusOneL n+ === n %:+ sOne `because` plusComm sOne n++ predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat)++ zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n+ zeroOrSucc = induction base step+ where+ base = IsZero+ step sn _ = IsSucc sn++ plusEqZeroL :: Sing n -> Sing m -> n :+ m :~: Zero kproxy -> n :~: Zero kproxy+ plusEqZeroL n m Refl =+ case zeroOrSucc n of+ IsZero -> Refl+ IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m)++ plusEqZeroR :: Sing n -> Sing m -> n :+ m :~: Zero kproxy -> m :~: Zero kproxy+ plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n)++ predUnique :: Sing (n :: nat) -> Sing m -> Succ n :~: m -> n :~: Pred m+ predUnique n m snEm =+ start n === (sPred (sSucc n)) `because` sym (predSucc n)+ === sPred m `because` predCong snEm++ multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> n :* m :~: Succ l -> n :~: Succ (Pred n)+ multEqSuccElimL n m l nmEsl =+ case zeroOrSucc n of+ IsZero -> absurd $ succNonCyclic l $ sym $+ start sZero === sZero %:* m `because` sym (multZeroL m)+ === sSucc l `because` nmEsl+ IsSucc pn -> succCong (predUnique pn n Refl)++ multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* m :~: Succ l -> m :~: Succ (Pred m)+ multEqSuccElimR n m l nmEsl =+ multEqSuccElimL m n l (multComm m n `trans` nmEsl)++ multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m+ multEqCancelR = proofMultEqCancelR . induction base step+ where+ base :: MultEqCancelR (Zero kproxy)+ base = MultEqCancelR $ \m l zslmsl ->+ sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero+ === sZero %:* l `because` sym (multZeroL l)+ === sZero %:* l %:+ sZero `because` sym (plusZeroR (sZero %:* l))+ === sZero %:* sSucc l `because` sym (multSuccR sZero l)+ === m %:* sSucc l `because` zslmsl+ === m %:* l %:+ m `because` multSuccR m l++ step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n)+ step n (MultEqCancelR ih) = MultEqCancelR $ \m l snmssnl ->+ let m' = sPred m+ pf = start (m %:* sSucc l)+ === sSucc n %:* sSucc l `because` sym snmssnl+ === n %:* sSucc l %:+ sSucc l `because` multSuccL n (sSucc l)+ === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l+ sm'Em = multEqSuccElimL m (sSucc l) (n %:* sSucc l %:+ l) pf+ pf' = ih m' l $ plusEqCancelR (n %:* sSucc l) (m' %:* sSucc l) (sSucc l) $+ start (n %:* sSucc l %:+ sSucc l)+ === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l+ === m %:* sSucc l `because` sym pf+ === sSucc m' %:* sSucc l `because` multCongL sm'Em (sSucc l)+ === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l)+ in succCong pf' `trans` sym sm'Em++ succPred :: Sing n -> (n :~: Zero kproxy -> Void) -> Succ (Pred n) :~: n+ succPred n nonZero =+ case zeroOrSucc n of+ IsZero -> absurd $ nonZero Refl+ IsSucc n' -> sym $ succCong $ predUnique n' n Refl++ multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> Succ n :* m :~: Succ n :* l -> m :~: l+ multEqCancelL n m l snmEsnl =+ multEqCancelR m l n $+ multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l++ sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)+ sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)++refute [t| 'LT :~: 'GT |]+refute [t| 'LT :~: 'EQ |]+refute [t| 'EQ :~: 'LT |]+refute [t| 'EQ :~: 'GT |]+refute [t| 'GT :~: 'LT |]+refute [t| 'GT :~: 'EQ |]+refute [t| 'True :~: 'False |]++pattern Zero <- (zeroOrSucc -> IsZero) where+ Zero = sZero++pattern Succ n <- (zeroOrSucc -> IsSucc n) where+ Succ n = sSucc n
+ Data/Type/Natural/Class/Order.hs view
@@ -0,0 +1,643 @@+{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-}+module Data.Type.Natural.Class.Order+ (PeanoOrder(..), DiffNat(..), LeqView(..),+ FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,+ sLeqCongL, sLeqCongR, sLeqCong+ ) where+import Data.Type.Natural.Class.Arithmetic++import Data.Singletons.Decide+import Data.Singletons.Prelude+import Data.Singletons.Prelude.Enum+import Data.Singletons.TH+import Data.Type.Equality+import Data.Void+import Proof.Equational+import Proof.Propositional++data LeqView (n :: nat) (m :: nat) where+ LeqZero :: Sing n -> LeqView (Zero 'KProxy) n+ LeqSucc :: Sing n -> Sing m -> IsTrue (n :<= m) -> LeqView (Succ n) (Succ m)++data DiffNat n m where+ DiffNat :: Sing n -> Sing m -> DiffNat n (n :+ m)++newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n :<= m) -> DiffNat n m }+newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m) }++succDiffNat :: IsPeano ('KProxy :: KProxy nat)+ => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m)+succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m++coerceLeqL :: forall (n :: nat) m l . IsPeano ('KProxy :: KProxy nat) => n :~: m -> Sing l+ -> IsTrue (n :<= l) -> IsTrue (m :<= l)+coerceLeqL Refl _ Witness = Witness++coerceLeqR :: forall (n :: nat) m l . IsPeano ('KProxy :: KProxy nat) => Sing l -> n :~: m+ -> IsTrue (l :<= n) -> IsTrue (l :<= m)+coerceLeqR _ Refl Witness = Witness++singletonsOnly [d|+ flipOrdering :: Ordering -> Ordering+ flipOrdering EQ = EQ+ flipOrdering LT = GT+ flipOrdering GT = LT+ |]++congFlipOrdering :: a :~: b -> FlipOrdering a :~: FlipOrdering b+congFlipOrdering Refl = Refl++compareCongR :: Sing (a :: k) -> b :~: c -> Compare a b :~: Compare a c+compareCongR _ Refl = Refl++sLeqCong :: a :~: b -> c :~: d -> (a :<= c) :~: (b :<= d)+sLeqCong Refl Refl = Refl++sLeqCongL :: a :~: b -> Sing c -> (a :<= c) :~: (b :<= c)+sLeqCongL Refl _ = Refl++sLeqCongR :: Sing a -> b :~: c -> (a :<= b) :~: (a :<= c)+sLeqCongR _ Refl = Refl++newtype LTSucc n = LTSucc { proofLTSucc :: Compare n (Succ n) :~: 'LT }+newtype CmpSuccStepR (n :: nat) =+ CmpSuccStepR { proofCmpSuccStepR :: forall (m :: nat). Sing m+ -> Compare n m :~: 'LT+ -> Compare n (Succ m) :~: 'LT+ }++newtype LeqViewRefl n = LeqViewRefl { proofLeqViewRefl :: LeqView n n }++class (SOrd kproxy, IsPeano kproxy) => PeanoOrder (kproxy :: KProxy nat) where+ {-# MINIMAL ( succLeqToLT, cmpZero, leqRefl+ | leqZero, leqSucc , viewLeq+ | leqWitness, leqStep+ ),+ eqlCmpEQ, ltToLeq, eqToRefl,+ flipCompare, leqToCmp,+ leqReversed, lneqSuccLeq, lneqReversed,+ (leqToMin, geqToMin | minLeqL, minLeqR, minLargest),+ (leqToMax, geqToMax | maxLeqL, maxLeqR, maxLeast) #-}++ leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a :<= b)+ -> Either (a :~: b) (Compare a b :~: 'LT)+ eqlCmpEQ :: Sing (a :: nat) -> Sing b -> a :~: b -> Compare a b :~: 'EQ+ eqToRefl :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'EQ -> a :~: b++ flipCompare :: Sing (a :: nat) -> Sing b+ -> FlipOrdering (Compare a b) :~: Compare b a++ ltToNeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT+ -> a :~: b -> Void+ ltToNeq a b aLTb aEQb = eliminate $+ start SLT+ === sCompare a b `because` sym aLTb+ === SEQ `because` eqlCmpEQ a b aEQb++ leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a :<= b) -> (a :~: b -> Void) -> Compare a b :~: 'LT+ leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb+++ succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a :<= b) -> Compare a b :~: 'LT+ succLeqToLT a b saLEQb =+ case leqWitness (sSucc a) b saLEQb of+ DiffNat _ k -> let aLEQb = leqStep a b (sSucc k) $+ start (a %:+ sSucc k)+ === sSucc (a %:+ k) `because` plusSuccR a k+ === sSucc a %:+ k `because` sym (plusSuccL a k)+ =~= b+ aNEQb aeqb = succNonCyclic k $ plusEqCancelL a (sSucc k) sZero $+ start (a %:+ sSucc k)+ === sSucc (a %:+ k) `because` plusSuccR a k+ === (sSucc a) %:+ k `because` sym (plusSuccL a k)+ =~= b+ === a `because` sym aeqb+ === a %:+ sZero `because` sym (plusZeroR a)+ in leqNeqToLT a b aLEQb aNEQb++ ltToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT+ -> IsTrue (a :<= b)++ gtToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'GT+ -> IsTrue (b :<= a)+ gtToLeq n m nGTm = ltToLeq m n $+ start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)+ === sFlipOrdering SGT `because` congFlipOrdering nGTm+ =~= SLT++ ltToSuccLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT+ -> IsTrue (Succ a :<= b)+ ltToSuccLeq n m nLTm =+ leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)++ cmpZero :: Sing a -> Compare (Zero kproxy) (Succ a) :~: 'LT+ cmpZero sn = leqToLT sZero (sSucc sn) $ leqStep (sSucc sZero) (sSucc sn) sn $+ start (sSucc sZero %:+ sn)+ === sSucc (sZero %:+ sn) `because` plusSuccL sZero sn+ === sSucc sn `because` succCong (plusZeroL sn)++ leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b :<= a)+ -> Compare a b :~: 'GT+ leqToGT a b sbLEQa =+ start (sCompare a b)+ === sFlipOrdering (sCompare b a) `because` sym (flipCompare b a)+ === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa)+ =~= SGT++ cmpZero' :: Sing a -> Either (Compare (Zero kproxy) a :~: 'EQ) (Compare (Zero kproxy) a :~: 'LT)+ cmpZero' n =+ case zeroOrSucc n of+ IsZero -> Left $ eqlCmpEQ sZero n Refl+ IsSucc n' -> Right $ cmpZero n'++ zeroNoLT :: Sing a -> Compare a (Zero kproxy) :~: 'LT -> Void+ zeroNoLT n eql =+ case cmpZero' n of+ Left cmp0nEQ -> eliminate $+ start SGT+ =~= sFlipOrdering SLT+ === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql)+ === sCompare sZero n `because` flipCompare n sZero+ === SEQ `because` cmp0nEQ+ Right cmp0nLT -> eliminate $+ start SGT+ =~= sFlipOrdering SLT+ === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql)+ === sCompare sZero n `because` flipCompare n sZero+ === SLT `because` cmp0nLT++ ltRightPredSucc :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT -> b :~: Succ (Pred b)+ ltRightPredSucc a b aLTb =+ case zeroOrSucc b of+ IsZero -> absurd $ zeroNoLT a aLTb+ IsSucc b' -> sym $+ start (sSucc (sPred b))+ =~= sSucc (sPred (sSucc b'))+ === sSucc b' `because` succCong (predSucc b')+ =~= b++ cmpSucc :: Sing (n :: nat) -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)+ cmpSucc n m =+ case sCompare n m of+ SEQ -> let nEQm = eqToRefl n m Refl+ in sym $ eqlCmpEQ (sSucc n) (sSucc m) $ succCong nEQm+ SLT -> case leqWitness (sSucc n) m $ ltToSuccLeq n m Refl of+ DiffNat _ k ->+ sym $ succLeqToLT (sSucc n) (sSucc m) $+ leqStep (sSucc (sSucc n)) (sSucc m) k $+ start (sSucc (sSucc n) %:+ k)+ === sSucc (sSucc n %:+ k) `because` plusSuccL (sSucc n) k+ =~= sSucc m+ SGT -> case leqWitness (sSucc m) n $ ltToSuccLeq m n (sym $ flipCompare n m) of+ DiffNat _ k ->+ let pf = (succLeqToLT (sSucc m) (sSucc n) $+ leqStep (sSucc (sSucc m)) (sSucc n) k $+ start (sSucc (sSucc m) %:+ k)+ === sSucc (sSucc m %:+ k) `because` plusSuccL (sSucc m) k+ =~= sSucc n)+ in start (sCompare n m)+ =~= SGT+ =~= sFlipOrdering SLT+ === sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf)+ === sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n)++ ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: 'LT+ ltSucc = proofLTSucc . induction base step+ where+ base :: LTSucc (Zero kproxy)+ base = LTSucc $ cmpZero (sZero :: Sing (Zero kproxy))++ step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n)+ step n (LTSucc ih) = LTSucc $+ start (sCompare (sSucc n) (sSucc (sSucc n)))+ === sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n))+ === SLT `because` ih++ cmpSuccStepR :: Sing (n :: nat) -> Sing m -> Compare n m :~: 'LT+ -> Compare n (Succ m) :~: 'LT+ cmpSuccStepR = proofCmpSuccStepR . induction base step+ where+ base :: CmpSuccStepR (Zero kproxy)+ base = CmpSuccStepR $ \m _ -> cmpZero m++ step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n)+ step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->+ case zeroOrSucc m of+ IsZero -> absurd $ zeroNoLT (sSucc n) snltm+ IsSucc m' ->+ let nLTm' = trans (cmpSucc n m') snltm+ in start (sCompare (sSucc n) (sSucc m))+ =~= sCompare (sSucc n) (sSucc (sSucc m'))+ === sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m'))+ === SLT `because` ih m' nLTm'++ ltSuccLToLT :: Sing (n :: nat) -> Sing m -> Compare (Succ n) m :~: 'LT+ -> Compare n m :~: 'LT+ ltSuccLToLT n m snLTm =+ case zeroOrSucc m of+ IsZero -> absurd $ zeroNoLT (sSucc n) snLTm+ IsSucc m' ->+ let nLTm = cmpSucc n m' `trans` snLTm+ in start (sCompare n (sSucc m'))+ === SLT `because` cmpSuccStepR n m' nLTm++ leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a :<= b)+ -> Compare a b :~: 'LT+ leqToLT n m snLEQm =+ case leqToCmp (sSucc n) m snLEQm of+ Left Refl ->+ start (sCompare n m)+ =~= sCompare n (sSucc n)+ === SLT `because` ltSucc n+ Right nLTm -> ltSuccLToLT n m nLTm++ leqZero :: Sing n -> IsTrue (Zero kproxy :<= n)+ leqZero sn =+ case zeroOrSucc sn of+ IsZero -> leqRefl sn+ IsSucc pn -> ltToLeq sZero sn $ cmpZero pn++ leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (Succ n :<= Succ m)+ leqSucc n m nLEQm =+ case leqToCmp n m nLEQm of+ Left Refl -> leqRefl (sSucc n)+ Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm++ fromLeqView :: LeqView (n :: nat) m -> IsTrue (n :<= m)+ fromLeqView (LeqZero n) = leqZero n+ fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm++ leqViewRefl :: Sing (n :: nat) -> LeqView n n+ leqViewRefl = proofLeqViewRefl . induction base step+ where+ base :: LeqViewRefl (Zero kproxy)+ base = LeqViewRefl $ LeqZero sZero+ step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n)+ step n (LeqViewRefl nLEQn) =+ LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn)++ viewLeq :: forall n m . Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> LeqView n m+ viewLeq n m nLEQm =+ case (zeroOrSucc n, leqToCmp n m nLEQm) of+ (IsZero, _) -> LeqZero m+ (_, Left Refl) -> leqViewRefl n+ (IsSucc n', Right nLTm) ->+ let sm'EQm = ltRightPredSucc n m nLTm+ m' = sPred m+ n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm+ in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm'++ leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> DiffNat n m+ leqWitness = leqWitPf . induction base step+ where+ base :: LeqWitPf (Zero kproxy)+ base = LeqWitPf $ \sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm++ step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n)+ step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->+ case viewLeq (sSucc n) m snLEQm of+ LeqZero _ -> absurd $ succNonCyclic n Refl+ LeqSucc (_ :: Sing n') pm nLEQpm ->+ succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm++ leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m)+ leqStep = leqStepPf . induction base step+ where+ base :: LeqStepPf (Zero kproxy)+ base = LeqStepPf $ \k _ _ -> leqZero k++ step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n)+ step n (LeqStepPf ih) =+ LeqStepPf $ \k l snPlEqk ->+ let kEQspk = start k+ === sSucc n %:+ l `because` sym snPlEqk+ === sSucc (n %:+ l) `because` plusSuccL n l+ pk = n %:+ l+ in coerceLeqR (sSucc n) (sym kEQspk) $ leqSucc n pk $ ih pk l Refl++ leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> (n :~: m -> Void) -> IsTrue (Succ n :<= m)+ leqNeqToSuccLeq n m nLEQm nNEQm =+ case leqWitness n m nLEQm of+ DiffNat _ k ->+ case zeroOrSucc k of+ IsZero -> absurd $ nNEQm $ sym $ plusZeroR n+ IsSucc k' -> leqStep (sSucc n) m k' $+ start (sSucc n %:+ k')+ === sSucc (n %:+ k') `because` plusSuccL n k'+ === n %:+ sSucc k' `because` sym (plusSuccR n k')+ =~= m++ leqRefl :: Sing (n :: nat) -> IsTrue (n :<= n)+ leqRefl sn = leqStep sn sn sZero (plusZeroR sn)++ leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (n :<= Succ m)+ leqSuccStepR n m nLEQm =+ case leqWitness n m nLEQm of+ DiffNat _ k -> leqStep n (sSucc m) (sSucc k) $+ start (n %:+ sSucc k) === sSucc (n %:+ k) `because` plusSuccR n k =~= sSucc m++ leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :<= m) -> IsTrue (n :<= m)+ leqSuccStepL n m snLEQm =+ leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm++ leqReflexive :: Sing (n :: nat) -> Sing m -> n :~: m -> IsTrue (n :<= m)+ leqReflexive n _ Refl = leqRefl n++ leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n :<= m) -> IsTrue (m :<= l) -> IsTrue (n :<= l)+ leqTrans n m k nLEm mLEk =+ case leqWitness n m nLEm of+ DiffNat _ mMn -> case leqWitness m k mLEk of+ DiffNat _ kMn -> leqStep n k (mMn %:+ kMn) (sym $ plusAssoc n mMn kMn)++ leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (m :<= n) -> n :~: m+ leqAntisymm n m nLEm mLEn =+ case (leqWitness n m nLEm, leqWitness m n mLEn) of+ (DiffNat _ mMn, DiffNat _ nMm) ->+ let pEQ0 = plusEqCancelL n (mMn %:+ nMm) sZero $+ start (n %:+ (mMn %:+ nMm))+ === (n %:+ mMn) %:+ nMm+ `because` sym (plusAssoc n mMn nMm)+ =~= m %:+ nMm+ =~= n+ === n %:+ sZero+ `because` sym (plusZeroR n)+ nMmEQ0 = plusEqZeroL mMn nMm pEQ0++ in sym $ start m+ =~= n %:+ mMn+ === n %:+ sZero `because` plusCongR n nMmEQ0+ === n `because` plusZeroR n++ plusMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k+ -> IsTrue (n :<= m) -> IsTrue (l :<= k)+ -> IsTrue (n :+ l :<= m :+ k)+ plusMonotone n m l k nLEm lLEk =+ case (leqWitness n m nLEm, leqWitness l k lLEk) of+ (DiffNat _ mMINn, DiffNat _ kMINl) ->+ let r = mMINn %:+ kMINl+ in leqStep (n %:+ l) (m %:+ k) r $+ start (n %:+ l %:+ r)+ === n %:+ (l %:+ r)+ `because` plusAssoc n l r+ =~= n %:+ (l %:+ (mMINn %:+ kMINl))+ === n %:+ (l %:+ (kMINl %:+ mMINn))+ `because` plusCongR n (plusCongR l (plusComm mMINn kMINl))+ === n %:+ ((l %:+ kMINl) %:+ mMINn)+ `because` plusCongR n (sym $ plusAssoc l kMINl mMINn)+ =~= n %:+ (k %:+ mMINn)+ === n %:+ (mMINn %:+ k)+ `because` plusCongR n (plusComm k mMINn)+ === n %:+ mMINn %:+ k+ `because` sym (plusAssoc n mMINn k)+ =~= m %:+ k++ leqZeroElim :: Sing n -> IsTrue (n :<= Zero kproxy) -> n :~: Zero kproxy+ leqZeroElim n nLE0 =+ case viewLeq n sZero nLE0 of+ LeqZero _ -> Refl+ LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl++ plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n :<= m)+ -> IsTrue (n :+ l :<= m :+ l)+ plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l)++ plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m :<= l)+ -> IsTrue (n :+ m :<= n :+ l)+ plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq++ plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= n :+ m)+ plusLeqL n m = leqStep n (n %:+ m) m Refl++ plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n :+ m)+ plusLeqR n m = leqStep m (n %:+ m) n $ plusComm m n++ plusCancelLeqR :: Sing (n :: nat) -> Sing m -> Sing l+ -> IsTrue (n :+ l :<= m :+ l)+ -> IsTrue (n :<= m)+ plusCancelLeqR n m l nlLEQml =+ case leqWitness (n %:+ l) (m %:+ l) nlLEQml of+ DiffNat _ k ->+ let pf = plusEqCancelR (n %:+ k) m l $+ start ((n %:+ k) %:+ l)+ === n %:+ (k %:+ l) `because` plusAssoc n k l+ === n %:+ (l %:+ k) `because` plusCongR n (plusComm k l)+ === n %:+ l %:+ k `because` sym (plusAssoc n l k)+ =~= m %:+ l+ in leqStep n m k pf++ plusCancelLeqL :: Sing (n :: nat) -> Sing m -> Sing l+ -> IsTrue (n :+ m :<= n :+ l)+ -> IsTrue (m :<= l)+ plusCancelLeqL n m l nmLEQnl =+ plusCancelLeqR m l n $+ coerceLeqL (plusComm n m) (l %:+ n) $+ coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl++ succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero kproxy) -> Void+ succLeqZeroAbsurd n leq =+ succNonCyclic n (leqZeroElim (sSucc n) leq)++ succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero kproxy) :~: 'False+ succLeqZeroAbsurd' n =+ case sSucc n %:<= sZero of+ STrue -> absurd $ succLeqZeroAbsurd n Witness+ SFalse -> Refl++ succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n :<= n) -> Void+ succLeqAbsurd n snLEQn =+ eliminate $+ start SLT+ === sCompare n n `because` sym (succLeqToLT n n snLEQn)+ === SEQ `because` eqlCmpEQ n n Refl++ succLeqAbsurd' :: Sing (n :: nat) -> (S n :<= n) :~: 'False+ succLeqAbsurd' n =+ case sSucc n %:<= n of+ STrue -> absurd $ succLeqAbsurd n Witness+ SFalse -> Refl++ notLeqToLeq :: ((n :<= m) ~ 'False) => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n)+ notLeqToLeq n m =+ case sCompare n m of+ SLT -> eliminate $ ltToLeq n m Refl+ SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl+ SGT -> gtToLeq n m Refl++ leqSucc' :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (Succ n :<= Succ m)+ leqSucc' n m =+ case n %:<= m of+ STrue ->+ case leqSucc n m Witness of+ Witness -> Refl+ SFalse ->+ case sSucc n %:<= sSucc m of+ SFalse -> Refl+ STrue ->+ case viewLeq (sSucc n) (sSucc m) Witness of+ LeqZero _ -> absurd $ succNonCyclic n Refl+ LeqSucc n' m' Witness ->+ eliminate $+ start STrue+ =~= (n' %:<= m')+ === (n %:<= m) `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl)+ =~= SFalse++ leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> Min n m :~: n+ leqToMin n m nLEQm =+ leqAntisymm (sMin n m) n (minLeqL n m)+ (minLargest n n m (leqRefl n) nLEQm)++ geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Min n m :~: m+ geqToMin n m mLEQn =+ leqAntisymm (sMin n m) m (minLeqR n m)+ (minLargest m n m mLEQn (leqRefl m))++ minComm :: Sing (n :: nat) -> Sing m -> Min n m :~: Min m n+ minComm n m =+ case n %:<= m of+ STrue -> start (sMin n m) === n `because` leqToMin n m Witness+ === sMin m n `because` sym (geqToMin m n Witness)+ SFalse -> start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m)+ === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m)++ minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m :<= n)+ minLeqL n m =+ case n %:<= m of+ STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness+ SFalse -> let mLEQn = notLeqToLeq n m+ in leqTrans (sMin n m) m n+ (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $+ mLEQn++ minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m :<= m)+ minLeqR n m = leqTrans (sMin n m) (sMin m n) m+ (leqReflexive (sMin n m) (sMin m n) $ minComm n m)+ (minLeqL m n)++ minLargest :: Sing (l :: nat) -> Sing n -> Sing m+ -> IsTrue (l :<= n) -> IsTrue (l :<= m)+ -> IsTrue (l :<= Min n m)+ minLargest l n m lLEQn lLEQm =+ withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $+ case n %:<= m of+ STrue -> leqTrans l n (sMin n m) lLEQn $+ leqReflexive sing sing $ sym $ leqToMin n m Witness+ SFalse ->+ let mLEQn = notLeqToLeq n m+ in leqTrans l m (sMin n m) lLEQm $+ leqReflexive sing sing $ sym $ geqToMin n m mLEQn++ leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> Max n m :~: m+ leqToMax n m nLEQm =+ leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m)++ geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Max n m :~: n+ geqToMax n m mLEQn =+ leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m)++ maxComm :: Sing (n :: nat) -> Sing m -> Max n m :~: Max m n+ maxComm n m =+ case n %:<= m of+ STrue -> start (sMax n m) === m `because` leqToMax n m Witness+ === sMax m n `because` sym (geqToMax m n Witness)+ SFalse -> start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m)+ === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m)++ maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= Max n m)+ maxLeqR n m =+ case n %:<= m of+ STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness+ SFalse -> let mLEQn = notLeqToLeq n m+ in leqTrans m n (sMax n m) mLEQn+ (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn))++ maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= Max n m)+ maxLeqL n m = leqTrans n (sMax m n) (sMax n m)+ (maxLeqR m n)+ (leqReflexive (sMax m n) (sMax n m) $ maxComm m n)++ maxLeast :: Sing (l :: nat) -> Sing n -> Sing m+ -> IsTrue (n :<= l) -> IsTrue (m :<= l)+ -> IsTrue (Max n m :<= l)+ maxLeast l n m lLEQn lLEQm =+ withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $+ case n %:<= m of+ STrue -> leqTrans (sMax n m) m l+ (leqReflexive sing sing $ leqToMax n m Witness)+ lLEQm+ SFalse ->+ let mLEQn = notLeqToLeq n m+ in leqTrans (sMax n m) n l+ (leqReflexive sing sing $ geqToMax n m mLEQn)+ lLEQn++ leqReversed :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (m :>= n)+ lneqSuccLeq :: Sing (n :: nat) -> Sing m -> (n :< m) :~: (Succ n :<= m)+ lneqReversed :: Sing (n :: nat) -> Sing m -> (n :< m) :~: (m :> n)++ lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n :< m)+ -> Compare n m :~: 'LT+ lneqToLT n m nLNEm =+ succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm++ ltToLneq :: Sing (n :: nat) -> Sing (m :: nat) -> Compare n m :~: 'LT+ -> IsTrue (n :< m)+ ltToLneq n m nLTm =+ coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm++ lneqZero :: Sing (a :: nat) -> IsTrue (Zero kproxy :< Succ a)+ lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n++ lneqSucc :: Sing (n :: nat) -> IsTrue (n :< Succ n)+ lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n++ succLneqSucc :: Sing (n :: nat) -> Sing (m :: nat)+ -> (n :< m) :~: (Succ n :< Succ m)+ succLneqSucc n m =+ start (n %:< m)+ === (sSucc n %:<= m) `because` lneqSuccLeq n m+ === (sSucc (sSucc n) %:<= sSucc m) `because` leqSucc' (sSucc n) m+ === (sSucc n %:< sSucc m) `because` sym (lneqSuccLeq (sSucc n) (sSucc m))++ lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n :< m)+ -> m :~: Succ (Pred m)+ lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm++ plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k+ -> IsTrue (n :< m) -> IsTrue (l :< k)+ -> IsTrue (n :+ l :< m :+ k)+ plusStrictMonotone n m l k nLNm lLNk =+ coerce (sym $ lneqSuccLeq (n %:+ l) (m %:+ k)) $+ flip coerceLeqL (m %:+ k) (plusSuccL n l) $+ plusMonotone (sSucc n) m l k+ (coerce (lneqSuccLeq n m) nLNm)+ (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $+ coerce (lneqSuccLeq l k) lLNk)++ maxZeroL :: Sing n -> Max (Zero kproxy) n :~: n+ maxZeroL n = leqToMax sZero n (leqZero n)++ maxZeroR :: Sing n -> Max n (Zero kproxy) :~: n+ maxZeroR n = geqToMax n sZero (leqZero n)++ minZeroL :: Sing n -> Min (Zero kproxy) n :~: Zero kproxy+ minZeroL n = leqToMin sZero n (leqZero n)++ minZeroR :: Sing n -> Min n (Zero kproxy) :~: Zero kproxy+ minZeroR n = geqToMin n sZero (leqZero n)++ minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Succ n :- m :~: Succ (n :- m)+ minusSucc n m mLEQn =+ case leqWitness m n mLEQn of+ DiffNat _ k ->+ start (sSucc n %:- m)+ =~= sSucc (m %:+ k) %:- m+ === (m %:+ sSucc k) %:- m `because` minusCongL (sym $ plusSuccR m k) m+ === (sSucc k %:+ m) %:- m `because` minusCongL (plusComm m (sSucc k)) m+ === sSucc k `because` plusMinus (sSucc k) m+ === sSucc (k %:+ m %:- m) `because` succCong (sym $ plusMinus k m)+ === sSucc (m %:+ k %:- m) `because` succCong (minusCongL (plusComm k m) m)+ =~= sSucc (n %:- m)
Data/Type/Natural/Core.hs view
@@ -8,30 +8,24 @@ import Data.Type.Natural.Compat #endif -import Data.Constraint hiding ((:-))-import qualified Data.Singletons.Prelude as S-import Data.Type.Natural.Definitions hiding ((:<=))-import Prelude (Bool (..), Eq (..), Show (..),- ($))-import Unsafe.Coerce+import Data.Constraint hiding ((:-))+import Data.Promotion.Prelude.Ord ((:<=))+import Data.Type.Natural.Definitions hiding ((:<=))+import Prelude (Bool (..), Eq (..), Show (..), ($))+import Proof.Propositional (IsTrue)+import Unsafe.Coerce -------------------------------------------------- -- ** Type-level predicate & judgements. ----------------------------------------------------- | Comparison via type-class.-class (n :: Nat) :<= (m :: Nat)-instance 'Z :<= n-instance (n :<= m) => 'S n :<= 'S m-{-# DEPRECATED (:<=) "This class will be removed in 0.5.0.0. Use @(n 'Data.Singletons.Prelude.Ord.:<=' m) ~ 'True@ instead" #-}- -- | Comparison via GADTs. data Leq (n :: Nat) (m :: Nat) where ZeroLeq :: SNat m -> Leq Zero m SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m) -type LeqTrueInstance a b = Dict ((a S.:<= b) ~ 'True)+type LeqTrueInstance a b = IsTrue (a :<= b) -(%-) :: (m S.:<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)+(%-) :: (m :<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m) n %- SZ = n SS n %- SS m = n %- m #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800@@ -55,7 +49,7 @@ propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE propToBoolLeq #-} -boolToClassLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq :: (n :<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE boolToClassLeq #-} @@ -79,9 +73,9 @@ propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict -} -type LeqInstance n m = Dict (n :<= m)+type LeqInstance n m = IsTrue (n :<= m) -boolToPropLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> Leq n m+boolToPropLeq :: (n :<= m) ~ 'True => SNat n -> SNat m -> Leq n m boolToPropLeq SZ m = ZeroLeq m boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
Data/Type/Natural/Definitions.hs view
@@ -1,21 +1,17 @@-{-# LANGUAGE DataKinds, DeriveDataTypeable, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, InstanceSigs, KindSignatures #-}-{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude, PolyKinds #-}-{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, GADTs, InstanceSigs, KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses, PolyKinds, RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}+{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-} module Data.Type.Natural.Definitions (module Data.Type.Natural.Definitions, module Data.Singletons.Prelude ) where-import Data.Singletons.Prelude-import Data.Singletons.TH (singletons)-import Data.Typeable (Typeable)-import Prelude (Num (..), Ord (..))-import Prelude (Bool (..), Eq (..), Show (..))-import qualified Prelude as P--+import Data.Promotion.Prelude.Enum+import Data.Singletons.Prelude+import Data.Singletons.Prelude.Enum+import Data.Singletons.TH (singletons)+import Data.Typeable (Typeable) -------------------------------------------------- -- * Natural numbers and its singleton type@@ -33,11 +29,15 @@ -------------------------------------------------- singletons [d|- instance P.Ord Nat where+ instance Ord Nat where Z <= _ = True S _ <= Z = False S n <= S m = n <= m + n >= m = m <= n+ n < m = S n <= m+ n > m = m < n+ min Z Z = Z min Z (S _) = Z min (S _) Z = Z@@ -48,9 +48,8 @@ max (S n) Z = S n max (S n) (S m) = S (max n m) |]- singletons [d|- instance P.Num Nat where+ instance Num Nat where Z + n = n S m + n = S (m + n) @@ -69,6 +68,16 @@ fromInteger n = if n == 0 then Z else S (fromInteger (n-1)) |] +singletons [d|+ instance Enum Nat where+ succ n = S n+ pred Z = Z+ pred (S n) = n+ toEnum n = if n == 0 then Z else S (toEnum (n - 1))+ fromEnum Z = 0+ fromEnum (S n) = 1 + fromEnum n+ |]+ type n :-: m = n :- m type n :+: m = n :+ m @@ -151,24 +160,3 @@ n19 = nineteen n20 = twenty |]---- | Boolean-valued type-level comparison function.-{-# DEPRECATED (<<=) "Use @'Ord'@ instance instead." #-}-(<<=) :: Nat -> Nat -> Bool-(<<=) = (<=)--{-# DEPRECATED (:<<=) "Use @'(:<=)'@ from @'POrd'@ instead." #-}-type n :<<= m = n :<= m--{-# DEPRECATED (%:<<=) "Use @'(%:<=)'@ from @'POrd'@ instead." #-}-(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)-(%:<<=) = (%:<=)--type (:<<=$) = (:<=$)-{-# DEPRECATED (:<<=$) "Use @(':<=$')@ instead." #-}--type (:<<=$$) = (:<=$$)-{-# DEPRECATED (:<<=$$) "Use @(':<=$$')@ instead." #-}--type (:<<=$$$) n m = (:<=$$$) n m-{-# DEPRECATED (:<<=$$$) "Use @(':<=$$$')@ instead." #-}
Data/Type/Ordinal.hs view
@@ -1,14 +1,15 @@-{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE LambdaCase, PolyKinds, ScopedTypeVariables, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}--- | Set-theoretic ordinal arithmetic+{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls #-}+{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PatternSynonyms, PolyKinds #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}+-- | Set-theoretic ordinals for general peano arithmetic models module Data.Type.Ordinal ( -- * Data-types- Ordinal (..),+ Ordinal (..), HasOrdinal, -- * Conversion from cardinals to ordinals.- sNatToOrd', sNatToOrd, ordToInt, ordToSNat,- ordToSNat', CastedOrdinal(..),+ sNatToOrd', sNatToOrd, ordToInt, ordToSing,+ ordToSing', CastedOrdinal(..), unsafeFromInt, inclusion, inclusion', -- * Ordinal arithmetics (@+), enumOrdinal,@@ -17,130 +18,222 @@ -- * Quasi Quoter od ) where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Type.Natural.Compat+import Control.Monad (liftM)+import Data.List (genericDrop, genericTake)+import Data.Ord (comparing)+import Data.Singletons.Prelude+import Data.Singletons.Prelude.Enum+import Data.Type.Equality+import Data.Type.Monomorphic+import qualified Data.Type.Natural as PN+import Data.Type.Natural.Builtin ()+import Data.Type.Natural.Class+import Data.Typeable (Typeable)+import GHC.TypeLits (type (+))+import qualified GHC.TypeLits as TL+import Language.Haskell.TH hiding (Type)+import Language.Haskell.TH.Quote+import Proof.Equational+import Proof.Propositional+import Unsafe.Coerce+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+import Data.Kind #endif -import Control.Monad (liftM)-import Data.Singletons.Prelude-import Data.Type.Monomorphic-import Data.Type.Natural-import Data.Constraint(Dict(..))-import Data.Typeable (Typeable)-import Language.Haskell.TH-import Language.Haskell.TH.Quote-import Unsafe.Coerce-import qualified Data.Singletons.Prelude as S -- | Set-theoretic (finite) ordinals: -- -- > n = {0, 1, ..., n-1} -- -- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@.-data Ordinal n where- OZ :: Ordinal ('S n)- OS :: Ordinal n -> Ordinal ('S n)+--+-- Since 0.5.0.0+data Ordinal (n :: nat) where+ OZ :: Sing n -> Ordinal (Succ n)+ OS :: Ordinal n -> Ordinal (Succ n)+ OLt :: (n :< m) ~ 'True => Sing n -> Ordinal m -- | Since 0.2.3.0 deriving instance Typeable Ordinal--- | Parsing always fails, because there are no inhabitant.-instance Read (Ordinal 'Z) where- readsPrec _ _ = [] -instance SingI n => Num (Ordinal n) where+-- | Class synonym for Peano numerals with ordinals.+--+-- Since 0.5.0.0+class (PeanoOrder kproxy, Monomorphicable (Sing :: nat -> *),+ Integral (MonomorphicRep (Sing :: nat -> *)),+ SingKind kproxy, kproxy ~ 'KProxy,+ Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal (kproxy :: KProxy nat)+instance (PeanoOrder ('KProxy :: KProxy nat), Monomorphicable (Sing :: nat -> *),+ Integral (MonomorphicRep (Sing :: nat -> *)),+ SingKind ('KProxy :: KProxy nat),+ Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal ('KProxy :: KProxy nat)++instance (HasOrdinal ('KProxy :: KProxy nat), SingI (n :: nat))+ => Num (Ordinal n) where+ {-# SPECIALISE instance SingI n => Num (Ordinal (n :: PN.Nat)) #-}+ {-# SPECIALISE instance SingI n => Num (Ordinal (n :: TL.Nat)) #-} _ + _ = error "Finite ordinal is not closed under addition." _ - _ = error "Ordinal subtraction is not defined"- negate OZ = OZ+ negate (OZ pxy) = OZ pxy negate _ = error "There are no negative oridnals!"- OZ * _ = OZ- _ * OZ = OZ+ OZ pxy * _ = OZ pxy+ _ * OZ pxy = OZ pxy _ * _ = error "Finite ordinal is not closed under multiplication" abs = id signum = error "What does Ordinal sign mean?"- fromInteger = unsafeFromInt . fromInteger+ fromInteger = unsafeFromInt' (Proxy :: Proxy ('KProxy :: KProxy nat)) . fromInteger -deriving instance Read (Ordinal n) => Read (Ordinal ('S n))-deriving instance Show (Ordinal n)-deriving instance Eq (Ordinal n)-deriving instance Ord (Ordinal n)+-- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n))+instance (SingI n, HasOrdinal ('KProxy :: KProxy nat))+ => Show (Ordinal (n :: nat)) where+ {-# SPECIALISE instance SingI n => Show (Ordinal (n :: PN.Nat)) #-}+ {-# SPECIALISE instance SingI n => Show (Ordinal (n :: TL.Nat)) #-}+ showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (demote $ Monomorphic (sing :: Sing n))) -instance SingI n => Enum (Ordinal n) where- fromEnum = ordToInt- toEnum = unsafeFromInt+instance (HasOrdinal ('KProxy :: KProxy nat))+ => Eq (Ordinal (n :: nat)) where+ {-# SPECIALISE instance Eq (Ordinal (n :: PN.Nat)) #-}+ {-# SPECIALISE instance Eq (Ordinal (n :: TL.Nat)) #-}+ o == o' = ordToInt o == ordToInt o'++instance (HasOrdinal ('KProxy :: KProxy nat)) => Ord (Ordinal (n :: nat)) where+ compare = comparing ordToInt++instance (HasOrdinal ('KProxy :: KProxy nat), SingI n)+ => Enum (Ordinal (n :: nat)) where+ fromEnum = fromIntegral . ordToInt+ toEnum = unsafeFromInt' (Proxy :: Proxy ('KProxy :: KProxy nat)) . fromIntegral enumFrom = enumFromOrd enumFromTo = enumFromToOrd -enumFromToOrd :: forall n. SingI n => Ordinal n -> Ordinal n -> [Ordinal n]+enumFromToOrd :: forall (n :: nat).+ (HasOrdinal ('KProxy :: KProxy nat), SingI n)+ => Ordinal n -> Ordinal n -> [Ordinal n] enumFromToOrd ok ol = let k = ordToInt ok l = ordToInt ol- in take (l - k + 1) $ enumFromOrd ok+ in genericTake (l - k + 1) $ enumFromOrd ok -enumFromOrd :: forall n. SingI n => Ordinal n -> [Ordinal n]-enumFromOrd ord = drop (ordToInt ord) $ enumOrdinal (sing :: SNat n)+enumFromOrd :: forall (n :: nat).+ (HasOrdinal ('KProxy :: KProxy nat), SingI n)+ => Ordinal n -> [Ordinal n]+enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n) -enumOrdinal :: SNat n -> [Ordinal n]-enumOrdinal SZ = []-enumOrdinal (SS n) = OZ : map OS (enumOrdinal n)+enumOrdinal :: (SingKind ('KProxy :: KProxy nat), PeanoOrder ('KProxy :: KProxy nat), SingI n) => Sing (n :: nat) -> [Ordinal n]+enumOrdinal (Succ n) = withSingI n $+ case lneqZero n of+ Witness ->+ OLt sZero : map succOrd (enumOrdinal n)+enumOrdinal _ = [] -instance SingI n => Bounded (Ordinal ('S n)) where- minBound = OZ+succOrd :: forall (n :: nat). (SingKind ('KProxy :: KProxy nat), PeanoOrder ('KProxy :: KProxy nat), SingI n) => Ordinal n -> Ordinal (Succ n)+succOrd (OLt n) =+ case succLneqSucc n (sing :: Sing n) of+ Refl -> OLt (sSucc n)+succOrd (OZ n) =+ case (succLneqSucc sZero (sSucc n), lneqZero n) of+ (Refl, Witness) -> OLt $ coerce (sym succOneCong) sOne+succOrd (OS o) =+ case (succLneqSucc sZero (sSucc (sing :: Sing n)), lneqZero (sing :: Sing n)) of+ (Refl, Witness) -> OS (OS o)++instance SingI n => Bounded (Ordinal ('PN.S n)) where+ minBound = OLt PN.SZ+ maxBound =- case propToBoolLeq $ leqRefl (sing :: SNat n) of- Dict -> sNatToOrd (sing :: SNat n)+ case leqRefl (sing :: Sing n) of+ Witness -> sNatToOrd (sing :: Sing n) -unsafeFromInt :: forall n. SingI n => Int -> Ordinal n+instance (SingI m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n) where+ minBound =+ case lneqZero (sing :: Sing m) of+ Witness -> OLt (sing :: Sing 0)+ {-# INLINE minBound #-}+ maxBound =+ case lneqSucc (sing :: Sing m) of+ Witness -> sNatToOrd (sing :: Sing m)+ {-# INLINE maxBound #-}+++unsafeFromInt :: forall (n :: nat). (HasOrdinal ('KProxy :: KProxy nat), SingI (n :: nat))+ => MonomorphicRep (Sing :: nat -> *) -> Ordinal n unsafeFromInt n =- case (promote n :: Monomorphic (Sing :: Nat -> *)) of+ case promote (n :: MonomorphicRep (Sing :: nat -> *)) of Monomorphic sn ->- case SS sn %:<= (sing :: SNat n) of- STrue -> sNatToOrd' (sing :: SNat n) sn+ case sn %:< (sing :: Sing n) of+ STrue -> sNatToOrd' (sing :: Sing n) sn SFalse -> error "Bound over!" +unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal ('KProxy :: KProxy nat), SingI n)+ => proxy ('KProxy :: KProxy nat) -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n+unsafeFromInt' _ n =+ case promote (n :: MonomorphicRep (Sing :: nat -> *)) of+ Monomorphic sn ->+ case sn %:< (sing :: Sing n) of+ STrue -> sNatToOrd' (sing :: Sing n) sn+ SFalse -> error "Bound over!"+ -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.-sNatToOrd' :: ('S m S.:<= n) ~ 'True => SNat n -> SNat m -> Ordinal n-sNatToOrd' (SS _) SZ = OZ-sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-sNatToOrd' _ _ = bugInGHC-#endif+--+-- Since 0.5.0.0+sNatToOrd' :: (PeanoOrder ('KProxy :: KProxy nat), (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n+sNatToOrd' _ m = OLt m -- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (SingI n, ('S m S.:<= n) ~ 'True) => SNat m -> Ordinal n+sNatToOrd :: (PeanoOrder ('KProxy :: KProxy nat), SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = sNatToOrd' sing data CastedOrdinal n where- CastedOrdinal :: ('S m S.:<= n) ~ 'True => SNat m -> CastedOrdinal n+ CastedOrdinal :: (m :< n) ~ 'True => Sing m -> CastedOrdinal n --- | Convert @Ordinal n@ into @SNat m@ with the proof of @'S m :<<= n@.-ordToSNat' :: Ordinal n -> CastedOrdinal n-ordToSNat' OZ = CastedOrdinal SZ-ordToSNat' (OS on) =- case ordToSNat' on of- CastedOrdinal m ->- CastedOrdinal (SS m)+-- | Convert @Ordinal n@ into @Sing m@ with the proof of @'S m :<= n@.+ordToSing' :: forall (n :: nat). (PeanoOrder ('KProxy :: KProxy nat), SingI n) => Ordinal n -> CastedOrdinal n+ordToSing' (OZ sk) =+ case lneqZero sk of+ (Witness) -> CastedOrdinal sZero+ordToSing' (OS (on :: Ordinal k)) =+ withSingI (sing :: Sing n) $+ withPredSingI (Proxy :: Proxy k) (sing :: Sing n) $+ case ordToSing' on of+ CastedOrdinal m ->+ case succLneqSucc m (sing :: Sing k) of+ Refl -> CastedOrdinal (Succ m)+ordToSing' (OLt s) = CastedOrdinal s --- | Convert @Ordinal n@ into monomorphic @SNat@-ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)-ordToSNat OZ = Monomorphic SZ-ordToSNat (OS n) =- case ordToSNat n of- Monomorphic sn ->+withPredSingI :: forall proxy (n :: nat) r. PeanoOrder ('KProxy :: KProxy nat)+ => proxy (n :: nat) -> Sing (Succ n) -> (SingI n => r) -> r+withPredSingI pxy sn r = withSingI (sPred' pxy sn) r+++-- | Convert @Ordinal n@ into monomorphic @Sing@+--+-- Since 0.5.0.0+ordToSing :: (PeanoOrder ('KProxy :: KProxy nat)) => Ordinal (n :: nat) -> SomeSing ('KProxy :: KProxy nat)+ordToSing (OLt n) = SomeSing n+ordToSing OZ{} = SomeSing sZero+ordToSing (OS n) =+ case ordToSing n of+ SomeSing sn -> case singInstance sn of- SingInstance -> Monomorphic (SS sn)+ SingInstance -> SomeSing (Succ sn) -- | Convert ordinal into @Int@.-ordToInt :: Ordinal n -> Int-ordToInt OZ = 0+ordToInt :: (HasOrdinal ('KProxy :: KProxy nat), int ~ MonomorphicRep (Sing :: nat -> *))+ => Ordinal (n :: nat)+ -> int+ordToInt OZ{} = 0 ordToInt (OS n) = 1 + ordToInt n+ordToInt (OLt n) = demote $ Monomorphic n+{-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Integer #-}+{-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-} -- | Inclusion function for ordinals.-inclusion' :: (n S.:<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m+inclusion' :: (n :< m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-} {- -- The "proof" of the correctness of the above-inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m+inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' (SS SZ) OZ = OZ inclusion' (SS (SS _)) OZ = OZ inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m@@ -148,34 +241,49 @@ -} -- | Inclusion function for ordinals with codomain inferred.-inclusion :: ((n S.:<= m) ~ 'True) => Ordinal n -> Ordinal m+inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m inclusion on = unsafeCoerce on {-# INLINE inclusion #-} + -- | Ordinal addition.-(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)-OZ @+ n =- let sn = sing :: SNat n- sm = sing :: SNat m- in case propToBoolLeq (plusLeqR sn sm) of- Dict -> inclusion n-OS n @+ m =- case sing :: SNat n of- SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800- _ -> bugInGHC-#endif+(@+) :: forall n m. (PeanoOrder ('KProxy :: KProxy nat), SingI (n :: nat), SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+OLt s @+ n =+ case ordToSing' n of+ CastedOrdinal n' ->+ case plusStrictMonotone s (sing :: Sing n) n' (sing :: Sing m) Witness Witness of+ Witness -> OLt $ s %:+ n'+OZ {} @+ n =+ let sn = sing :: Sing n+ sm = sing :: Sing m+ in case plusLeqR sn sm of+ Witness -> inclusion n+OS (n :: Ordinal k) @+ m =+ withPredSingI n (sing :: Sing n) $+ case sing :: Sing n of+ Zero -> absurdOrd (OS n)+ Succ sn ->+ case singInstance sn of+ SingInstance ->+ let sm = sing :: Sing m+ sn' = sing :: Sing n+ sk = sing :: Sing k+ pf = start (sSucc (sk %:+ sm))+ === sSucc sk %:+ sm `because` sym (plusSuccL sk sm)+ =~= sn' %:+ sm+ in coerce pf $ OS $ n @+ m+ _ -> error "inaccessible pattern" -- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. -- -- Since 0.2.3.0-absurdOrd :: Ordinal 'Z -> a-absurdOrd cs = case cs of {}+absurdOrd :: PeanoOrder ('KProxy :: KProxy nat) => Ordinal (Zero ('KProxy :: KProxy nat)) -> a+absurdOrd _cs = undefined -- case cs of {} -- | 'absurdOrd' for the value in 'Functor'. -- -- Since 0.2.3.0-vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a+vacuousOrd :: (PeanoOrder ('KProxy :: KProxy nat), Functor f) => f (Ordinal (Zero ('KProxy :: KProxy nat))) -> f a vacuousOrd = fmap absurdOrd -- | 'absurdOrd' for the value in 'Monad'.@@ -183,7 +291,7 @@ -- become the superclass of 'Monad'. -- -- Since 0.2.3.0-vacuousOrdM :: Monad m => m (Ordinal 'Z) -> m a+vacuousOrdM :: (PeanoOrder ('KProxy :: KProxy nat), Monad m) => m (Ordinal (Zero ('KProxy :: KProxy nat))) -> m a vacuousOrdM = liftM absurdOrd -- | Quasiquoter for ordinals
type-natural.cabal view
@@ -2,9 +2,13 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.4.2.0+version: 0.5.0.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties.+ .+ This version 0.5.0.0 supports __GHC 7.10.* only__.+ .+ __Use >= 0.6.0.0 with GHC 8.0.0+__. homepage: https://github.com/konn/type-natural license: BSD3 license-file: LICENSE@@ -14,7 +18,7 @@ category: Math build-type: Simple cabal-version: >= 1.10-tested-with: GHC == 7.10.3, GHC == 8.0.1+tested-with: GHC == 7.10.3 source-repository head Type: git@@ -28,6 +32,9 @@ exposed-modules: Data.Type.Natural , Data.Type.Ordinal , Data.Type.Natural.Builtin+ , Data.Type.Natural.Class+ , Data.Type.Natural.Class.Arithmetic+ , Data.Type.Natural.Class.Order other-modules: Data.Type.Natural.Definitions , Data.Type.Natural.Core , Data.Type.Natural.Compat@@ -37,8 +44,8 @@ , template-haskell >= 2.8 && < 3 , constraints >= 0.3 && < 0.9 , ghc-typelits-natnormalise == 0.4.*- , ghc-typelits-presburger == 0.1.*- , singletons >= 2.0 && < 2.3+ , ghc-typelits-presburger >= 0.1.1 && < 1+ , singletons == 2.1 default-language: Haskell2010 default-extensions: DataKinds