diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs --- a/Data/Type/Natural.hs +++ b/Data/Type/Natural.hs @@ -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" } + diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs --- a/Data/Type/Natural/Builtin.hs +++ b/Data/Type/Natural/Builtin.hs @@ -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 diff --git a/Data/Type/Natural/Class.hs b/Data/Type/Natural/Class.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Class.hs @@ -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 + diff --git a/Data/Type/Natural/Class/Arithmetic.hs b/Data/Type/Natural/Class/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Class/Arithmetic.hs @@ -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 diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Class/Order.hs @@ -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) diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs --- a/Data/Type/Natural/Core.hs +++ b/Data/Type/Natural/Core.hs @@ -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 diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs --- a/Data/Type/Natural/Definitions.hs +++ b/Data/Type/Natural/Definitions.hs @@ -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." #-} diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -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 diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -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