packages feed

type-natural (empty) → 0.0.1.0

raw patch · 4 files changed

+688/−0 lines, 4 filesdep +basedep +equational-reasoningdep +singletonssetup-changed

Dependencies added: base, equational-reasoning, singletons

Files

+ Data/Type/Natural.hs view
@@ -0,0 +1,629 @@+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs    #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies     #-}+{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving  #-}+-- | Type level peano natural number, some arithmetic functions and their singletons.+module Data.Type.Natural (-- * Re-exported modules.+                          module Data.Singletons,+                     -- * Natural Numbers+                     -- | Peano natural numbers. It will be promoted to the type-level natural number.+                     Nat(..),+                     -- | Singleton type for 'Nat'.+                     SNat+                    -- ** Smart constructors+                    , sZ, sS+                    -- ** Arithmetic functions and thir singletons.+                    , min, Min, sMin, max, Max, sMax+                    , (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*)+                    , (:-:), (:-), (%:-), (%-)+                    -- ** Type-level predicate & judgements+                    , Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, leqRefl, leqSucc+                    , boolToPropLeq, boolToClassLeq, propToClassLeq+                    , LeqTrueInstance(..), propToBoolLeq+                    -- * Conversion functions+                    , natToInt, intToNat, sNatToInt+                    -- * Properties of natural numbers+                    , succCongEq, plusCongR, plusCongL, succPlusL, succPlusR+                    , plusZR, plusZL, eqPreservesS, plusAssociative+                    , multAssociative, multComm, multZL, multZR, multOneL, multOneR+                    , plusMultDistr, multPlusDistr, multCongL, multCongR+                    , sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent+                    , eqSuccMinus, plusMinusEqL, plusMinusEqR, plusLeqL, plusLeqR+                    , zAbsorbsMinR, zAbsorbsMinL, minLeqL, minLeqR, plusSR+                    , leqRhs, leqLhs, leqTrans, minComm, leqAnitsymmetric+                    , maxZL, maxComm, maxZR, maxLeqL, maxLeqR, plusMonotone+                    -- * Useful type synonyms and constructors+                    , zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven+                    , twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty+                    , Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten+                    , Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty+                    , sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven+                    , sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty+                    , n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20+                    , N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20+                    , sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14+                    , sN15, sN16, sN17, sN18, sN19, sN20+                    ) where+import           Data.Singletons+import           Prelude          (Bool (..), Eq (..), Integral (..), Ord ((<)),+                                   Show (..), error, id, otherwise, ($), (.), undefined)+import qualified Prelude          as P+import           Proof.Equational++--------------------------------------------------+-- * Natural numbers and its singleton type+--------------------------------------------------+singletons [d|+ data Nat = Z | S Nat+            deriving (Show, Eq, Ord)+ |]++--------------------------------------------------+-- ** Arithmetic functions.+--------------------------------------------------++singletons [d|+ -- | Minimum function.+ min :: Nat -> Nat -> Nat+ min Z     Z     = Z+ min Z     (S _) = Z+ min (S _) Z     = Z+ min (S m) (S n) = S (min m n)++ -- | Maximum function.+ max :: Nat -> Nat -> Nat+ max Z     Z     = Z+ max Z     (S n) = S n+ max (S n) Z     = S n+ max (S n) (S m) = S (max n m)+ |]++singletons [d|+ (+) :: Nat -> Nat -> Nat+ Z   + n = n+ S m + n = S (m + n)++ (-) :: Nat -> Nat -> Nat+ n   - Z   = n+ S n - S m = n - m+ Z   - S _ = Z++ (*) :: Nat -> Nat -> Nat+ Z   * _ = Z+ S n * m = n * m + m+ |]++instance P.Num Nat where+  n - m = n - m+  n + m = n + m+  n * m = n * m+  abs = id+  signum Z = Z+  signum _ = S Z+  fromInteger 0             = Z+  fromInteger n | n P.< 0   = error "negative integer"+                | otherwise = S $ P.fromInteger (n P.- 1)++infixl 6 :-:, %:-, -++type n :-: m = n :- m+infixl 6 :+:, %+, %:+, :+++type n :+: m = n :+ m++-- | Addition for singleton numbers.+(%+) :: SNat n -> SNat m -> SNat (n :+: m)+(%+) = (%:+)++infixl 7 :*:, %*, %:*, :*++-- | Type-level multiplication.+type n :*: m = n :* m++-- | Multiplication for singleton numbers.+(%*) :: SNat n -> SNat m -> SNat (n :*: m)+(%*) = (%:*)++--------------------------------------------------+-- ** Convenient synonyms+--------------------------------------------------+singletons [d|+ zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat           + eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat           + zero      = Z+ one       = S zero+ two       = S one+ three     = S two+ four      = S three+ five      = S four+ six       = S five+ seven     = S six+ eight     = S seven+ nine      = S eight+ ten       = S nine+ eleven    = S ten+ twelve    = S eleven+ thirteen  = S twelve+ fourteen  = S thirteen+ fifteen   = S fourteen+ sixteen   = S fifteen+ seventeen = S sixteen+ eighteen  = S seventeen+ nineteen  = S eighteen+ twenty    = S nineteen+ n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat+ n10, n11, n12, n13, n14, n15, n16, n17 :: Nat+ n18, n19, n20 :: Nat+ n0  = zero+ n1  = one+ n2  = two+ n3  = three+ n4  = four+ n5  = five+ n6  = six+ n7  = seven+ n8  = eight+ n9  = nine+ n10 = ten+ n11 = eleven+ n12 = twelve+ n13 = thirteen+ n14 = fourteen+ n15 = fifteen+ n16 = sixteen+ n17 = seventeen+ n18 = eighteen+ n19 = nineteen+ n20 = twenty+ |]++--------------------------------------------------+-- ** Type-level predicate & judgements.+--------------------------------------------------+-- | Comparison via type-class.+class (n :: Nat) :<= (m :: Nat)+instance Z :<= n+instance (n :<= m) => S n :<= S m++-- | Boolean-valued type-level comparison function.+singletons [d|+ (<<=) :: Nat -> Nat -> Bool+ Z   <<= _   = True+ S _ <<= Z   = False+ S n <<= S m = n <<= m+ |]++-- | 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)++data LeqTrueInstance a b where+  LeqTrueInstance :: (a :<<= b) ~ True => LeqTrueInstance a b++(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)+n   %- SZ    = n+SS n %- SS m = n %- m+_    %- _    = error "impossible!"++infixl 6 %-+deriving instance Show (SNat n)+deriving instance Eq (SNat n)++data (a :: Nat) :<: (b :: Nat) where+  ZeroLtSucc :: Zero :<: S m+  SuccLtSucc :: n :<: m -> S n :<: S m++deriving instance Show (a :<: b)++--------------------------------------------------+-- * Total orderings on natural numbers.+--------------------------------------------------+propToBoolLeq :: Leq n m -> LeqTrueInstance n m+propToBoolLeq (ZeroLeq _) = LeqTrueInstance+propToBoolLeq (SuccLeqSucc leq) =+  case propToBoolLeq leq of+    LeqTrueInstance -> LeqTrueInstance++data LeqInstance n m where+  LeqInstance :: (n :<= m) => LeqInstance 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+boolToPropLeq _      _      = bugInGHC++boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq SZ     _      = LeqInstance+boolToClassLeq (SS n) (SS m) =+  case boolToClassLeq n m of+    LeqInstance -> LeqInstance+boolToClassLeq _ _ = bugInGHC++propToClassLeq :: Leq n m -> LeqInstance n m+propToClassLeq (ZeroLeq _) = LeqInstance+propToClassLeq (SuccLeqSucc leq) =+  case propToClassLeq leq of+    LeqInstance -> LeqInstance++leqRefl :: SNat n -> Leq n n+leqRefl SZ = ZeroLeq sZ+leqRefl (SS n) = SuccLeqSucc $ leqRefl n++leqSucc :: SNat n -> Leq n (S n)+leqSucc SZ = ZeroLeq sOne+leqSucc (SS n) = SuccLeqSucc $ leqSucc n++leqRhs :: Leq n m -> SNat m+leqRhs (ZeroLeq m) = m+leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq++leqLhs :: Leq n m -> SNat n+leqLhs (ZeroLeq _) = sZ+leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq++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+leqTrans _ _ = error "impossible!"++instance Preorder Leq where+  reflexivity = leqRefl+  transitivity = leqTrans++{-+singletons [d|+  (<<) :: Nat -> Nat -> Bool+  Zero   << Succ n = True+  n      << Zero   = False+  Succ n << Succ m = n << m+  (<<=) :: Nat -> Nat -> Bool+  Zero   <<= _      = True+  Succ n <<= Zero   = False+  Succ n <<= Succ m = n <<= m+ |]++type a :>> b = b :<< a+type a :> b  = b :<: a++type a :<=: b = a :<: b :\/: a :=: b++instance FromBool (n :<: m) where+  type Predicate (n :<: m) = n :<< m+  type Args (n :<: m) = '[Sing n, Sing m]+  fromBool = boolToPropLt++boolToPropLt :: (x :<< y) ~ True => SNat x -> SNat y -> x :<: y+boolToPropLt SZ (SS _)     = ZeroLtSucc+boolToPropLt (SS n) (SS m) = SuccLtSucc $ boolToPropLt n m+boolToPropLt _ _         = bugInGHC++instance FromBool (n :<=: m) where+  type Predicate (n :<=: m) = n :<<= m+  type Args (n :<=: m) = '[Sing n, Sing m]+  fromBool = boolToPropLe++boolToPropLe :: (x :<<= y) ~ True => SNat x -> SNat y -> x :<=: y+boolToPropLe SZ SZ         = Right Refl+boolToPropLe SZ (SS _)     = Left ZeroLtSucc+boolToPropLe (SS n) (SS m) =+    case boolToPropLe n m of+      Left reason -> Left $ SuccLtSucc reason+      Right Refl  -> Right Refl+boolToPropLe _ _         = bugInGHC++rev :: (n :<<= m) ~ False => SNat n -> SNat m -> m :<: n+rev (SS _) SZ     = ZeroLtSucc+rev (SS n) (SS m) = SuccLtSucc $ rev n m+rev _         _         = bugInGHC++leTrans :: forall n m l. n :<=: m -> m :<=: l -> n :<=: l+leTrans (Right Refl) a = a+leTrans a (Right Refl) = a+leTrans (Left ZeroLtSucc) (Left (SuccLtSucc _)) = Left ZeroLtSucc+leTrans (Left (SuccLtSucc a)) (Left (SuccLtSucc b)) =+  case leTrans (Left a) (Left b) of+    Right Refl -> Right Refl+    Left le -> Left $ SuccLtSucc le+leTrans _ _ = bugInGHC++nLtSn :: SNat n -> n :<: Succ n+nLtSn SZ     = ZeroLtSucc+nLtSn (SS n) = SuccLtSucc (nLtSn n)++comparable :: SNat n -> SNat m -> n :<: m :\/: n :=: m :\/: m :<: n+comparable SZ SZ         = orIntroR (orIntroL Refl)+comparable SZ (SS _)     = orIntroL ZeroLtSucc+comparable (SS _) SZ     = orIntroR (orIntroR ZeroLtSucc)+comparable (SS n) (SS m) =+  case comparable n m of+    Left nLTm          -> orIntroL $ SuccLtSucc nLTm+    Right (Left Refl)  -> orIntroR $ orIntroL Refl+    Right (Right mLTn) -> orIntroR $ orIntroR $ SuccLtSucc mLTn+-}++--------------------------------------------------+-- * Properties+--------------------------------------------------+plusZR :: SNat n -> n :+: Z :=: n+plusZR SZ     = Refl+plusZR (SS n) =+ start (sS n %+ sZ)+   =~= sS (n %+ sZ)+   === sS n          `because` cong' sS (plusZR n)++eqPreservesS :: n :=: m -> S n :=: S m+eqPreservesS Refl = Refl++plusZL :: SNat n -> Z :+: n :=: n+plusZL _ = Refl++succCongEq :: n :=: m -> S n :=: S m+succCongEq Refl = Refl++sAndPlusOne :: SNat n -> S n :=: n :+: One+sAndPlusOne SZ = Refl+sAndPlusOne (SS n) =+  start (sS (sS n))+    === sS (n %+ sOne) `because` cong' sS (sAndPlusOne n)+    =~= sS n %+ sOne++plusAssociative :: SNat n -> SNat m -> SNat l+                -> n :+: (m :+: l) :=: (n :+: m) :+: l+plusAssociative SZ     _ _ = Refl+plusAssociative (SS n) m l =+  start (sS n %+ (m %+ l))+    =~= sS (n %+ (m %+ l))+    === sS ((n %+ m) %+ l)  `because` cong' sS (plusAssociative n m l)+    =~= sS (n %+ m) %+ l+    =~= (sS n %+ m) %+ l++plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m+plusSR n m =+  start (sS (n %+ m))+    === (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)+    === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)+    === n %+ sS m        `because` plusCongL n (symmetry $ sAndPlusOne m)++plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)+plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)+plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =+  case plusSR m (leqRhs leq) of+    Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq+plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'++infer :: Proxy a+infer = Proxy++plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'+plusCongL _ Refl = Refl++plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n+plusCongR _ Refl = Refl++succPlusL :: SNat n -> SNat m -> S n :+ m :=: S (n :+ m)+succPlusL _ _ = Refl++succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m)+succPlusR SZ     _ = Refl+succPlusR (SS n) m =+  start (sS n %+ sS m)+    =~= sS (n %+ sS m)+    === sS (sS (n %+ m)) `because` succCongEq (succPlusR n m)+    =~= sS (sS n %+ m)++minusCongEq :: n :=: m -> SNat l -> n :-: l :=: m :-: l+minusCongEq Refl _ = Refl++minusNilpotent :: SNat n -> n :-: n :=: Zero+minusNilpotent SZ = Refl+minusNilpotent (SS n) =+  start (sS n %:- sS n)+    =~= n %:- n+    === sZ     `because` minusNilpotent n++plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n+plusCommutative SZ SZ     = Refl+plusCommutative SZ (SS m) =+  start (sZ %+ sS m)+    =~= sS m+    === sS (m %+ sZ) `because` cong' sS (plusCommutative SZ m)+    =~= sS m %+ sZ+plusCommutative (SS n) m =+  start (sS n %+ m)+    =~= sS (n %+ m)+    === sS (m %+ n)      `because` cong' sS (plusCommutative n m)+    === (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)+    === m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)+    === m %+ sS n        `because` plusCongL m (symmetry $ sAndPlusOne n)++eqSuccMinus :: ((m :<<= n) ~ True)+            => SNat n -> SNat m -> (S n :-: m) :=: (S (n :-: m))+eqSuccMinus _      SZ     = Refl+eqSuccMinus (SS n) (SS m) =+  start (sS (sS n) %:- sS m)+    =~= sS n %:- m+    === sS (n %:- m)       `because` eqSuccMinus n m+    =~= sS (sS n %:- sS m)+eqSuccMinus _ _ = bugInGHC++plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)+plusLeqL SZ     m = case plusZR m of Refl -> ZeroLeq m+plusLeqL (SS n) m = SuccLeqSucc $ plusLeqL n m++plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)+plusLeqR n m =+  case plusCommutative n m of+    Refl -> plusLeqL m n++plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n+plusMinusEqL SZ     m = minusNilpotent m+plusMinusEqL (SS n) m =+  case propToBoolLeq (plusLeqR n m) of+    LeqTrueInstance -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)++plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n+plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)++zAbsorbsMinR :: SNat n -> Min n Z :=: Z+zAbsorbsMinR SZ     = Refl+zAbsorbsMinR (SS n) =+  case zAbsorbsMinR n of+    Refl -> Refl++zAbsorbsMinL :: SNat n -> Min Z n :=: Z+zAbsorbsMinL SZ     = Refl+zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl++minLeqL :: SNat n -> SNat m -> Leq (Min n m) n+minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq sZ+minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n+minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)++minLeqR :: SNat n -> SNat m -> Leq (Min n m) m+minLeqR n m = case minComm n m of Refl -> minLeqL m n++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++leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m+leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl+leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2+leqAnitsymmetric _ _ = bugInGHC++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)++maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)+maxLeqL SZ m = ZeroLeq (sMax sZ m)+maxLeqL n SZ = case maxZR n of+                 Refl -> leqRefl n+maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m++maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)+maxLeqR n m = case maxComm n m of+                Refl -> maxLeqL m n++newtype MultPlusDistr l m n =+    MultPlusDistr { unMultPlusDistr :: l :* (m :+ n) :=: l :* m :+ l :* n}++instance Proposition (MultPlusDistr l m) where+  type OriginalProp (MultPlusDistr l m) n = l :* (m :+ n) :=: l :* m :+ l :* n+  wrap = MultPlusDistr+  unWrap = unMultPlusDistr++multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l+multPlusDistr SZ     _ _ = Refl+multPlusDistr (SS n) m l = +  start (sS n %* (m %+ l))+    =~= n %* (m %+ l) %+ (m %+ l)+    === (n %* m) %+ (n %* l) %+ (m %+ l) `because` plusCongR (m %+ l) (multPlusDistr n m l)+    === (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)+    === n %* m %+ (n %*l %+ (l %+ m))    `because` symmetry (plusAssociative (n %* m) (n %* l) (l %+ m))+    === n %* l %+ (l %+ m) %+ n %* m     `because` plusCommutative (n %* m) (n %*l %+ (l %+ m))+    === (n %* l %+ l) %+ m %+ n %* m     `because` plusCongR (n %* m) (plusAssociative (n %* l) l m)+    =~= (sS n %* l)   %+ m %+ n %* m+    === (sS n %* l)   %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (sS n %* l) m (n %* m))+    === (sS n %* l)   %+ ((n %* m) %+ m) `because` plusCongL (sS n %* l) (plusCommutative m (n %* m))+    =~= (sS n %* l)   %+ (sS n %* m)+    === (sS n %* m)   %+ (sS n %* l)     `because` plusCommutative (sS n %* l) (sS n %* m)++plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: n :* l :+ m :* l+plusMultDistr SZ _ _ = Refl+plusMultDistr (SS n) m l =+  start ((SS n %+ m) %* l)+    =~= sS (n %+ m) %* l+    =~= (n %+ m) %* l %+ l+    === n %* l  %+  m %* l  %+  l   `because` plusCongR l (plusMultDistr n m l)+    === m %* l  %+  n %* l  %+  l   `because` plusCongR l (plusCommutative (n %* l) (m %* l))+    === m %* l  %+ (n %* l  %+  l)  `because` symmetry (plusAssociative (m %* l) (n %*l) l)+    =~= m %* l  %+ (sS n %* l)+    === (sS n %* l)  %+  (m %* l)   `because` plusCommutative (m %* l) (sS n %* l)++multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l+multAssociative SZ     _ _ = Refl+multAssociative (SS n) m l =+  start (sS n %* (m %* l))+    =~= n %* (m %* l) %+ (m %* l)+    === (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssociative n m l)+    === (n %* m %+ m) %* l        `because` symmetry (plusMultDistr (n %* m) m l)+    =~= (sS n %* m) %* l++multZL :: SNat m -> Zero :* m :=: Zero+multZL _ = Refl++multZR :: SNat m -> m :* Zero :=: Zero+multZR SZ = Refl+multZR (SS n) =+  start (sS n %* sZ)+    =~= n %* sZ %+ sZ+    === sZ %+ sZ      `because` plusCongR sZ (multZR n)+    =~= sZ++multOneL :: SNat n -> One :* n :=: n+multOneL n =+  start (sOne %* n)+    =~= sZero %* n %+ n+    =~= sZero %:+ n+    =~= n++multOneR :: SNat n -> n :* One :=: n+multOneR SZ = Refl+multOneR (SS n) =+  start (sS n %* sOne)+    =~= n %* sOne %+ sOne+    === n %+ sOne         `because` plusCongR sOne (multOneR n)+    === sS n              `because` symmetry (sAndPlusOne n)++multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l+multCongL _ Refl = Refl++multCongR :: SNat n -> m :=: l -> m :* n :=: l :* n+multCongR _ Refl = Refl++multComm :: SNat n -> SNat m -> n :* m :=: m :* n+multComm SZ m =+  start (sZ %* m)+    =~= sZ+    === m %* sZ `because` symmetry (multZR m)+multComm (SS n) m =+  start (sS n %* m)+    =~= n %* m %+ m+    === m %* n %+ m          `because` plusCongR m (multComm n m)+    === m %* n %+ m %* sOne  `because` plusCongL (m %* n) (symmetry $ multOneR m)+    === m %* (n %+ sOne)     `because` symmetry (multPlusDistr m n sOne)+    === m %* sS n            `because` multCongL m (symmetry $ sAndPlusOne n)++--------------------------------------------------+-- * Conversion functions.+--------------------------------------------------++-- | Convert integral numbers into 'Nat'+intToNat :: (Integral a, Ord a) => a -> Nat+intToNat 0 = Z+intToNat n+    | n < 0     = error "negative integer"+    | otherwise = S $ intToNat (n P.- 1)++-- | Convert 'Nat' into normal integers.+natToInt :: Integral n => Nat -> n+natToInt Z     = 0+natToInt (S n) = natToInt n P.+ 1++-- | Convert 'SNat n' into normal integers.+sNatToInt :: P.Num n => SNat x -> n+sNatToInt SZ     = 0+sNatToInt (SS n) = sNatToInt n P.+ 1
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013, Hiromi ISHII++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Hiromi ISHII nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ type-natural.cabal view
@@ -0,0 +1,27 @@+-- Initial type-natural.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                type-natural+version:             0.0.1.0+synopsis:            Type-level natural and proofs of their properties.+description:         Type-level natural numbers and proofs of their properties.+homepage:            https://github.com/konn/type-natural+license:             BSD3+license-file:        LICENSE+author:              Hiromi ISHII+maintainer:          konn.jinro_at_gmail.com+copyright:           (C) Hiromi ISHII 2013+category:            Math+build-type:          Simple+cabal-version:       >=1.8+source-repository head+  Type: git+  Location: git://github.com/konn/type-natural.git+++library+  exposed-modules:     Data.Type.Natural+  -- other-modules:       +  build-depends:       base ==4.6.*+               ,       singletons ==0.8.*+               ,       equational-reasoning ==0.0.*