diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs deleted file mode 100644 --- a/Data/Type/Natural.hs +++ /dev/null @@ -1,302 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, EmptyCase, FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE GADTs, KindSignatures, LambdaCase, MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-} -{-# LANGUAGE TypeOperators, UndecidableInstances #-} --- | Type level peano natural number, some arithmetic functions and their singletons. -module Data.Type.Natural (-- * Re-exported modules. - module Data.Singletons, - -- * Natural Numbers - -- | Peano natural numbers. It will be promoted to the type-level natural number. - Nat(..), - SSym0, SSym1, ZSym0, - -- | Singleton type for 'Nat'. - SNat, -#if MIN_VERSION_singletons(2,6,0) - SNat (SZ, SS), -#else - Sing(SZ,SS), -#endif - -- ** Arithmetic functions and their singletons. - min, Min, sMin, max, Max, sMax, - MinSym0, MinSym1, MinSym2, - MaxSym0, MaxSym1, MaxSym2, - type (+), - type (+@#@$), type (+@#@$$), type (+@#@$$$), - (%+), type (*), - type (*@#@$), type (*@#@$$), type (*@#@$$$), - (%*), type (-), - type (**), (%**), - type (-@#@$), type (-@#@$$), type (-@#@$$$), - (%-), - -- ** Type-level predicate & judgements - Leq(..), type (<=), LeqInstance, - boolToPropLeq, boolToClassLeq, propToClassLeq, - propToBoolLeq, - -- * Conversion functions - natToInt, intToNat, sNatToInt, - -- * Quasi quotes for natural numbers - nat, snat, - -- * Properties of natural numbers - IsPeano(..), - plusCong, plusCongR, plusCongL, - snEqZAbsurd, plusInjectiveL, plusInjectiveR, - multCongL, multCongR, multCong, - plusMinusEqL, - plusNeutralR, plusNeutralL, - -- * Properties of ordering 'Leq' - PeanoOrder(..), - reflToSEqual, sLeqReflexive, nonSLeqToLT, - -- * Useful type synonyms and constructors - zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven, - twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty, - Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten, - Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty, - ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0, - SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0, - ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0, - EighteenSym0, NineteenSym0, TwentySym0, - sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven, - sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty, - n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20, - N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20, - - N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0, - sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14, - sN15, sN16, sN17, sN18, sN19, sN20 - ) - where -import Data.Type.Natural.Singleton.Compat - -import Data.Singletons -import Data.Singletons.Decide -import Data.Type.Natural.Class hiding (One, Zero, sOne, sZero) -import Data.Type.Natural.Core -import Data.Type.Natural.Definitions hiding (type (<=)) -import Data.Void -import Language.Haskell.TH (appE, appT, conE, conP, conT) -import Language.Haskell.TH.Quote -import Proof.Equational -import Proof.Propositional hiding (Not) - --------------------------------------------------- --- * Conversion functions. --------------------------------------------------- - --- | Convert integral numbers into 'Nat' -intToNat :: (Integral a, Ord a) => a -> Nat -intToNat 0 = Z -intToNat n - | n < 0 = error "negative integer" - | otherwise = S $ intToNat (n - 1) - --- | Convert 'Nat' into normal integers. -natToInt :: Integral n => Nat -> n -natToInt Z = 0 -natToInt (S n) = natToInt n + 1 - --- | Convert 'SNat n' into normal integers. -sNatToInt :: Num n => SNat x -> n -sNatToInt SZ = 0 -sNatToInt (SS n) = sNatToInt n + 1 - --------------------------------------------------- --- * Properties --------------------------------------------------- - --- | Since 0.5.0.0 -instance IsPeano Nat where - {-# SPECIALISE instance IsPeano Nat #-} - induction base _step SZ = base - induction base step (SS n) = step n (induction base step n) - - plusMinus n SZ = - start (n %+ SZ %- SZ) - === (n %- SZ) `because` minusCongL (plusZeroR n) SZ - =~= n - plusMinus n (SS m) = - start (n %+ SS m %- SS m) - === SS (n %+ m) %- SS m `because` minusCongL (plusSuccR n m) (SS m) - =~= (n %+ m) %- m - === n `because` plusMinus n m - - succInj Refl = Refl - succOneCong = Refl - succNonCyclic _ a = case a of {} - - plusZeroL _ = Refl - plusSuccL _ _ = Refl - - multZeroL _ = Refl - multSuccL _ _ = Refl - - predSucc _ = Refl - -snEqZAbsurd :: SingI n => 'S n :~: 'Z -> a -snEqZAbsurd = absurd . succNonCyclic sing - -plusInjectiveL :: SNat n -> SNat m -> SNat l -> n + m :~: n + l -> m :~: l -plusInjectiveL SZ _ _ Refl = Refl -plusInjectiveL (SS n) m l eq = plusInjectiveL n m l $ succInj eq - -plusInjectiveR :: SNat n -> SNat m -> SNat l -> n + l :~: m + l -> n :~: m -plusInjectiveR n m l eq = plusInjectiveL l n m $ - start (l %+ n) - === n %+ l `because` plusComm l n - === m %+ l `because` eq - === l %+ m `because` plusComm m l - -reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n == m) -reflToSEqual SZ _ Refl = Witness -reflToSEqual (SS n) (SS m) Refl = reflToSEqual n m Refl -reflToSEqual (SS _) SZ refl = case refl of {} - -sequalToRefl :: SNat n -> SNat m -> IsTrue (n == m) -> n :~: m -sequalToRefl SZ SZ Witness = Refl -sequalToRefl SZ (SS _) witness = case witness of {} -sequalToRefl (SS n) (SS m) Witness = succCong $ sequalToRefl n m Witness -sequalToRefl (SS _) SZ witness = case witness of {} - -snequalToNoRefl :: SNat n -> SNat m -> IsTrue (Not (n == m)) -> n :~: m -> Void -snequalToNoRefl SZ _ Witness = \case {} -snequalToNoRefl (SS _) SZ Witness = \case {} -snequalToNoRefl (SS n) (SS m) Witness = \case - Refl -> snequalToNoRefl n m Witness Refl - -sequalSym :: SNat n -> SNat m -> (n == m) :~: (m == n) -sequalSym SZ SZ = Refl -sequalSym SZ (SS _) = Refl -sequalSym (SS _) SZ = Refl -sequalSym (SS n) (SS m) = sequalSym n m - -sleqFlip :: SNat n -> SNat m -> (n :~: m -> Void) -> (m <= n) :~: Not (n <= m) -sleqFlip SZ SZ neq = absurd $ neq Refl -sleqFlip SZ (SS _) _ = Refl -sleqFlip (SS _) SZ _ = Refl -sleqFlip (SS n) (SS m) neq = sleqFlip n m (neq . succCong) - -sLeqReflexive :: SNat n -> SNat m -> IsTrue (n == m) -> IsTrue (n <= m) -sLeqReflexive SZ _ Witness = Witness -sLeqReflexive (SS n) (SS m) Witness = sLeqReflexive n m Witness -sLeqReflexive (SS _) SZ witness = case witness of {} - -nonSLeqToLT :: (n <= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT -nonSLeqToLT n m = withRefl (sequalSym n m) $ - case m %== n of - STrue -> case sLeqReflexive n m Witness of {} - SFalse -> - case m %<= n of - STrue -> Refl - SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {} - -instance PeanoOrder Nat where - {-# SPECIALISE instance PeanoOrder Nat #-} - leqZero _ = Witness - leqSucc _ _ Witness = Witness - viewLeq SZ n Witness = LeqZero n - viewLeq (SS n) (SS m) Witness = LeqSucc n m Witness - viewLeq (SS _) SZ a = case a of {} - - ltToLeq n m Refl = - case n %== m of - SFalse -> case n %<= m of - STrue -> Witness - eqlCmpEQ n m Refl = - case n %== m of - STrue -> Refl - SFalse -> absurd $ snequalToNoRefl n m Witness Refl - - eqToRefl n m Refl = - case n %== m of - STrue -> sequalToRefl n m Witness - SFalse -> case n %<= m of {} - - leqToCmp n m Witness = - case n %== m of - STrue -> Left $ sequalToRefl n m Witness - SFalse -> Right Refl - - cmpZero _ = Refl - - flipCompare n m = - case n %== m of - STrue -> withRefl (sequalSym n m) Refl - SFalse -> withRefl (sequalSym n m) $ - case n %<= m of - STrue -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $ - case m %<= n of - SFalse -> Refl - SFalse -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $ - case m %<= n of - STrue -> Refl - - minLeqL SZ SZ = Witness - minLeqL SZ (SS _) = Witness - minLeqL (SS _) SZ = Witness - minLeqL (SS n) (SS m) = minLeqL n m - - minLeqR SZ SZ = Witness - minLeqR SZ (SS _) = Witness - minLeqR (SS _) SZ = Witness - minLeqR (SS n) (SS m) = minLeqR n m - - minLargest SZ _ _ _ _ = Witness - minLargest (SS _) SZ SZ _ a = case a of {} - minLargest (SS _) SZ (SS _) a Witness = case a of {} - minLargest (SS _) (SS _) SZ _ a = case a of {} - minLargest (SS n) (SS m) (SS l) Witness Witness = - minLargest n m l Witness Witness - - maxLeqL SZ SZ = Witness - maxLeqL SZ (SS _) = Witness - maxLeqL (SS n) SZ = leqRefl n - maxLeqL (SS n) (SS m) = maxLeqL n m - - maxLeqR SZ SZ = Witness - maxLeqR (SS _) SZ = Witness - maxLeqR (SS n) (SS m) = maxLeqR n m - maxLeqR SZ (SS m) = leqRefl m - - maxLeast _ SZ SZ _ _ = Witness - maxLeast _ SZ (SS _) _ a = a - maxLeast _ (SS _) SZ a _ = a - maxLeast SZ _ (SS n) _ a = absurd $ succLeqZeroAbsurd n a - maxLeast (SS k) (SS l) (SS m) slLEsk smLEsk = - coerce (leqSucc' (sMax l m) k) $ - maxLeast k l m - (coerce (sym $ leqSucc' l k) slLEsk) - (coerce (sym $ leqSucc' m k) smLEsk) - - leqReversed _ _ = Refl - lneqReversed _ _ = Refl - lneqSuccLeq _ _ = Refl - -plusMinusEqL :: SNat n -> SNat m -> ((n + m) - m) :~: n -plusMinusEqL = plusMinus - -plusNeutralR :: SNat n -> SNat m -> n + m :~: n -> m :~: 'Z -plusNeutralR n m npmn = plusEqCancelL n m SZ (npmn `trans` sym (plusZeroR n)) - -plusNeutralL :: SNat n -> SNat m -> n + m :~: m -> n :~: 'Z -plusNeutralL n m npmm = plusNeutralR m n (plusComm m n `trans` npmm) - --------------------------------------------------- --- * Quasi Quoter --------------------------------------------------- - --- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type. --- --- for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@ -nat :: QuasiQuoter -nat = QuasiQuoter { quoteExp = foldr appE (conE 'Z) . flip replicate (conE 'S) . read - , quotePat = foldr (\a b -> conP a [b]) (conP 'Z []) . flip replicate 'S . read - , quoteType = foldr appT (conT 'Z) . flip replicate (conT 'S) . read - , quoteDec = error "not implemented" - } - --- | Quotesi-quoter for 'SNat'. This can be used for an expression. --- --- For example: @[snat|12|] '%+' [snat| 5 |]@. -snat :: QuasiQuoter -snat = mkSNatQQ [t| Nat |] - diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs deleted file mode 100644 --- a/Data/Type/Natural/Builtin.hs +++ /dev/null @@ -1,466 +0,0 @@ -{-# LANGUAGE CPP, ConstraintKinds, DataKinds, EmptyCase, ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts, GADTs, InstanceSigs, PolyKinds, RankNTypes #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -#if MIN_VERSION_singletons(2,6,0) -{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-} -#else -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} -#endif -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} --- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@ -module Data.Type.Natural.Builtin - ( -- * Sysnonym to avoid confusion - Peano, - -- * Coercion between builtin type-level natural and peano numerals - FromPeano, ToPeano, sFromPeano, sToPeano, leqqAndLeq, - -- * Properties of @'FromPeano'@ and @'ToPeano'@. - fromPeanoInjective, toPeanoInjective, - -- ** Bijection - fromToPeano, toFromPeano, - -- ** Algebraic isomorphisms - fromPeanoZeroCong, toPeanoZeroCong, - fromPeanoOneCong, toPeanoOneCong, - fromPeanoSuccCong, toPeanoSuccCong, - fromPeanoPlusCong, toPeanoPlusCong, - fromPeanoMultCong, toPeanoMultCong, - fromPeanoMonotone, toPeanoMonotone, - -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@ - IsPeano(..), - inductionNat, - -- * QuasiQuotes - snat, - -- * Re-exports - module Data.Type.Natural.Singleton.Compat - ) - where -import Data.Type.Natural.Singleton.Compat -import Data.Type.Natural.Class - -import Data.Singletons.Decide (SDecide (..)) -import Data.Singletons.Decide (Decision (..)) -import Data.Singletons.Prelude (Sing (..), SingKind(..), SBool(..)) -import Data.Singletons.Prelude (SingI (..)) -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 ((:~:) (..)) -#if MIN_VERSION_singletons(2,6,0) -import Data.Type.Natural (Nat (S, Z), SNat (SS, SZ)) -#else -import Data.Type.Natural (Nat (S, Z), Sing (SS, SZ)) -#endif - -import qualified Data.Type.Natural as PN -import Data.Void (absurd) -import Data.Void (Void) -import GHC.TypeLits (type (<=?)) -import qualified GHC.TypeLits as TL -import Language.Haskell.TH.Quote (QuasiQuoter) -import Proof.Equational (coerce, withRefl) -import Proof.Equational (start, sym, (===), (=~=)) -import Proof.Equational (because) -import Proof.Propositional (Empty (..), IsTrue (..), - withEmpty, withWitness) -import Unsafe.Coerce (unsafeCoerce) - --- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@. -type Peano = PN.Nat - -type family FromPeano (n :: PN.Nat) :: TL.Nat where - FromPeano 'Z = 0 - FromPeano ('S n) = Succ (FromPeano n) - -type family ToPeano (n :: TL.Nat) :: PN.Nat where - ToPeano 0 = 'Z - ToPeano n = 'S (ToPeano (Pred n)) - -viewNat :: Sing (n :: TL.Nat) -> ZeroOrSucc n -viewNat n = - case n %~ (sing :: Sing 0) of - Proved Refl -> IsZero - Disproved t -> withEmpty t $ IsSucc (sPred n) - -sFromPeano :: Sing n -> Sing (FromPeano n) -sFromPeano SZ = sing -sFromPeano (SS sn) = sSucc (sFromPeano sn) - -toPeanoInjective :: forall n m. (TL.KnownNat n, TL.KnownNat m) - => ToPeano n :~: ToPeano m -> n :~: m -toPeanoInjective tPnEqtPm = - let sn = sing :: Sing n - sm = sing :: Sing m - in start sn - === sFromPeano (sToPeano sn) `because` sym (fromToPeano sn) - === sFromPeano (sToPeano sm) `because` congFromPeano tPnEqtPm - === sm `because` fromToPeano sm - --- 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 :: () :~: ()) - -- We cannot prove this lemma within Haskell, so we assume it a priori. - -infix 4 %<=? -(%<=?) :: 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) <=? (m TL.+ 1)) :~: (n <=? m) -natLeqSuccEq _ _ = Refl - -leqqCong :: n :~: m -> l :~: z -> (n <=? l) :~: (m <=? z) -leqqCong Refl Refl = Refl - -leqqAndLeq :: Sing n -> Sing m -> (n <=? m) :~: (n PN.<= m) -leqqAndLeq n m = - case sCompare n m of - SEQ -> Refl - SLT -> Refl - SGT -> Refl - -natSuccPred :: forall n. TL.KnownNat n => ((n :~: 0) -> Void) -> Succ (Pred n) :~: n -natSuccPred refute = - case sCompare (sing :: Sing 1) (sing :: Sing n) of - SLT -> Refl - SEQ -> Refl - SGT -> absurd $ refute Refl - -neqZero1leqq :: forall n. TL.KnownNat n => ((n :~: 0) -> Void) -> IsTrue (1 <=? n) -neqZero1leqq refute = - case sCompare (sing :: Sing 1) (sing :: Sing n) of - SLT -> Witness - SEQ -> Witness - SGT -> absurd $ refute Refl - -sToPeano :: Sing n -> Sing (ToPeano n) -sToPeano sn = - case sn %~ (sing :: Sing 0) of - Proved eq -> withRefl eq SZ - Disproved _pf -> - withKnownNat sn $ - withRefl (natSuccPred _pf) $ - coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn))) - --- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat). --- Succ n :~: Succ m -> n :~: m --- litSuccInjective Refl = Refl - -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` succCong (toFromPeano sn) - -congFromPeano :: n :~: m -> FromPeano n :~: FromPeano m -congFromPeano Refl = Refl - -congToPeano :: n :~: m -> ToPeano n :~: ToPeano m -congToPeano Refl = Refl - -congSucc :: n :~: m -> Succ n :~: Succ m -congSucc Refl = Refl - -fromToPeano :: Sing n -> FromPeano (ToPeano n) :~: n -fromToPeano sn = - case viewNat sn of - IsZero -> Refl - IsSucc n1 -> - start (sFromPeano (sToPeano sn)) - =~= sFromPeano (sToPeano (sSucc n1)) - === sFromPeano (SS (sToPeano n1)) - `because` congFromPeano (toPeanoSuccCong n1) - =~= sSucc (sFromPeano (sToPeano n1)) - === sSucc n1 `because` congSucc (fromToPeano n1) - -fromPeanoInjective :: forall n m. (SingI n, SingI m) - => FromPeano n :~: FromPeano m -> n :~: m -fromPeanoInjective frEq = - let sn = sing :: Sing n - sm = sing :: Sing m - in start sn - === sToPeano (sFromPeano sn) `because` sym (toFromPeano sn) - === sToPeano (sFromPeano sm) `because` congToPeano frEq - === sm `because` toFromPeano sm - -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 SZ _ = Refl -fromPeanoPlusCong (SS sn) sm = - start (sFromPeano (SS sn %+ sm)) - =~= sFromPeano (SS (sn %+ sm)) - === sSucc (sFromPeano (sn %+ sm)) `because` fromPeanoSuccCong (sn %+ sm) - === sSucc (sFromPeano sn %+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm) - =~= 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 sn sm = - case viewNat sn of - IsZero -> Refl - IsSucc pn -> - start (sToPeano (sSucc pn %+ sm)) - =~= sToPeano (sSucc (pn %+ sm)) - === SS (sToPeano (pn %+ sm)) - `because` toPeanoSuccCong (pn %+ sm) - === SS (sToPeano pn %+ sToPeano sm) - `because` succCong (toPeanoPlusCong pn sm) - =~= SS (sToPeano pn) %+ sToPeano sm - === (sToPeano (sSucc pn) %+ sToPeano sm) - `because` plusCongL (sym (toPeanoSuccCong pn)) (sToPeano sm) - =~= sToPeano sn %+ sToPeano sm - -fromPeanoZeroCong :: FromPeano 'Z :~: 0 -fromPeanoZeroCong = Refl - -toPeanoZeroCong :: ToPeano 0 :~: 'Z -toPeanoZeroCong = Refl - -fromPeanoOneCong :: FromPeano PN.One :~: 1 -fromPeanoOneCong = Refl - -toPeanoOneCong :: ToPeano 1 :~: PN.One -toPeanoOneCong = Refl - -natPlusCongR :: Sing r -> n :~: m -> n TL.+ r :~: m TL.+ r -natPlusCongR _ Refl = Refl - -fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.* m) :~: FromPeano n TL.* FromPeano m -fromPeanoMultCong SZ _ = Refl -fromPeanoMultCong (SS psn) sm = - start (sFromPeano (SS psn %* sm)) - =~= sFromPeano (psn %* sm %+ sm) - === sFromPeano (psn %* sm) %+ sFromPeano sm - `because` fromPeanoPlusCong (psn %* sm) sm - === sFromPeano psn %* sFromPeano sm %+ sFromPeano sm - `because` natPlusCongR (sFromPeano sm) (fromPeanoMultCong psn sm) - =~= sSucc (sFromPeano psn) %* sFromPeano sm - =~= sFromPeano (SS psn) %* sFromPeano sm - - -toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n TL.* m) :~: ToPeano n PN.* ToPeano m -toPeanoMultCong sn sm = - case viewNat sn of - IsZero -> Refl - IsSucc psn -> - start (sToPeano (sSucc psn %* sm)) - =~= sToPeano (psn %* sm %+ sm) - === sToPeano (psn %* sm) %+ sToPeano sm - `because` toPeanoPlusCong (psn %* sm) sm - === sToPeano psn %* sToPeano sm %+ sToPeano sm - `because` plusCongL (toPeanoMultCong psn sm) (sToPeano sm) - =~= SS (sToPeano psn) %* sToPeano sm - === sToPeano (sSucc psn) %* sToPeano sm - `because` multCongL (sym (toPeanoSuccCong psn)) (sToPeano sm) -leqCong :: n :~: m -> l :~: z -> (n PN.<= l) :~: (m PN.<= z) -leqCong Refl Refl = Refl - -fromPeanoMonotone :: ((n PN.<= 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)) - === (sSucc (sFromPeano n) %<=? sSucc (sFromPeano m)) - `because` leqqCong (fromPeanoSuccCong n) (fromPeanoSuccCong m) - === (sFromPeano n %<=? sFromPeano m) - `because` natLeqSuccEq (sFromPeano n) (sFromPeano m) - === STrue - `because` fromPeanoMonotone n m -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -fromPeanoMonotone _ _ = bugInGHC -#endif - -natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0 -natLeqZero Zero = Refl -natLeqZero _ = error "natLeqZero : bug in ghc" - -myLeqPred :: Sing n -> Sing m -> ('S n PN.<= 'S m) :~: (n PN.<= m) -myLeqPred SZ _ = Refl -myLeqPred (SS _) (SS _) = Refl -myLeqPred (SS _) SZ = Refl - -toPeanoCong :: a :~: b -> ToPeano a :~: ToPeano b -toPeanoCong Refl = Refl - -toPeanoMonotone :: (n TL.<= m) - => Sing n -> Sing m -> ((ToPeano n) PN.<= (ToPeano m)) :~: 'True -toPeanoMonotone sn sm = withKnownNat sn $ withKnownNat sm $ - case sn %~ (sing :: Sing 0) of - Proved eql -> withRefl eql Refl - Disproved nPos -> withWitness (neqZero1leqq nPos) $ case sm %~ (sing :: Sing 0) of - Proved mEq0 -> withRefl mEq0 $ absurd $ nPos $ natLeqZero sn - Disproved mPos -> withWitness (neqZero1leqq mPos) $ - let pn = sPred sn - pm = sPred sm - in start (sToPeano sn %<= sToPeano sm) - === (sToPeano (sSucc pn) %<= sToPeano (sSucc pm)) - `because` leqCong (toPeanoCong $ sym $ natSuccPred nPos) - (toPeanoCong $ sym $ natSuccPred mPos) - === (SS (sToPeano pn) %<= SS (sToPeano pm)) - `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm) - === (sToPeano pn %<= sToPeano pm) - `because` myLeqPred (sToPeano pn) (sToPeano pm) - === 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 base step sn = - case viewNat sn of - IsZero -> base - IsSucc sl -> step (inductionNat base step sl) - - -instance IsPeano TL.Nat where - {-# SPECIALISE instance IsPeano TL.Nat #-} - - toNatural = fromIntegral . fromSing - fromNatural = toSing . fromIntegral - - predSucc _ = Refl - plusMinus _ _ = Refl - succInj Refl = Refl - succOneCong = Refl - succNonCyclic _ a = case a of _ -> error "Bug in GHC!" - 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 sn = - case viewNat sn of - IsZero -> base - IsSucc sl -> - withKnownNat sl $ step sing (induction base step sl) - -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 - -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 - -type family MyLeqHelper n m o where - MyLeqHelper n m 'LT = 'True - MyLeqHelper n m 'EQ = 'True - MyLeqHelper n m 'GT = 'False - -instance PeanoOrder TL.Nat where - {-# SPECIALISE instance PeanoOrder TL.Nat #-} - eqlCmpEQ _ _ Refl = Refl - ltToLeq _ _ Refl = Witness - succLeqToLT n m w = case sCompare n m of - SEQ -> eliminate $ - start SLT === sCompare n m `because` sym (leqToLT n m w) - === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m) - =~= SEQ - SGT -> eliminate $ - start SLT === sCompare n m `because` sym (leqToLT n m w) - =~= SGT - SLT -> Refl - - 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 - - leqToMin _ _ Witness = Refl - leqToMax _ _ Witness = Refl - geqToMax n m mLEQn@Witness = - case leqToCmp m n mLEQn of - Left eql -> withRefl eql Refl - Right mLTn -> - maxCompareFlip n m mLTn - geqToMin n m mLEQn = - case leqToCmp m n mLEQn of - Left eql -> withRefl eql Refl - Right mLTn -> - minCompareFlip n m mLTn - - lneqReversed n m = - withRefl (flipCompare n m) $ - case sCompare n m of - SEQ -> Refl - SLT -> Refl - SGT -> Refl - - leqReversed n m = - withRefl (flipCompare n m) $ - case sCompare n m of - SEQ -> Refl - SLT -> Refl - SGT -> 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 -> withWitness (ltToSuccLeq n m Refl) $ - start (n %< m) - =~= STrue - =~= (sSucc n %<= m) - SGT -> - case sSucc n %<= m of - SFalse -> Refl - STrue -> eliminate $ succLeqToLT n m Witness - --- instance Monomorphicable (Sing :: TL.Nat -> *) where --- type MonomorphicRep (Sing :: TL.Nat -> *) = Integer --- demote (Monomorphic sn) = fromSing sn --- {-# INLINE demote #-} - --- promote n = case toSing n of SomeSing k -> Monomorphic k --- {-# INLINE promote #-} - --- | Quotesi-quoter for singleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression. --- --- For example: @[snat|12|] '%+' [snat| 5 |]@. -snat :: QuasiQuoter -snat = mkSNatQQ [t| TL.Nat |] - diff --git a/Data/Type/Natural/Class.hs b/Data/Type/Natural/Class.hs deleted file mode 100644 --- a/Data/Type/Natural/Class.hs +++ /dev/null @@ -1,33 +0,0 @@ -{-# LANGUAGE TemplateHaskell #-} --- | 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 - , -- * Quasi quoters generator for naturals - mkSNatQQ) where -import Data.Type.Natural.Class.Arithmetic -import Data.Type.Natural.Class.Order - -import Data.Singletons.Prelude (FromInteger, Sing, sing) -import Language.Haskell.TH (ExpQ, TypeQ, litT, numTyLit, sigT) -import Language.Haskell.TH.Quote (QuasiQuoter (..)) - --- | Quasiquoter generateor for specific peano-types. --- --- Since 0.7.0.0 -mkSNatQQ :: TypeQ -> QuasiQuoter -mkSNatQQ t = QuasiQuoter - { quoteExp = mkExpQuote - , quotePat = error "no pattern quoter for snats" - -- foldr (\a b -> conP a [b]) (conP 'SZ []) . flip replicate 'SS . read - , quoteType = mkTypeQuote - , quoteDec = error "not implemented" - } - where - mkExpQuote :: String -> ExpQ - mkExpQuote s = [| sing :: $(mkTypeQuote s) |] - - mkTypeQuote :: String -> TypeQ - mkTypeQuote s = - let n = read s - in [t| Sing $(sigT [t| FromInteger $(litT $ numTyLit n)|] =<< t) |] diff --git a/Data/Type/Natural/Class/Arithmetic.hs b/Data/Type/Natural/Class/Arithmetic.hs deleted file mode 100644 --- a/Data/Type/Natural/Class/Arithmetic.hs +++ /dev/null @@ -1,576 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} -{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-} -{-# LANGUAGE TypeInType, 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, - module Data.Type.Natural.Singleton.Compat - ) where -import Data.Type.Natural.Singleton.Compat (type (*), type (*@#@$), - type (*@#@$$), type (*@#@$$$), - type (+), type (+@#@$), - type (+@#@$$), type (+@#@$$$), - type (-), type (-@#@$), - type (-@#@$$), type (-@#@$$$), - type (/=), type (/=@#@$), - type (/=@#@$$), type (/=@#@$$$), - type (==), type (==@#@$), - type (==@#@$$), type (==@#@$$$), - FromInteger, FromIntegerSym0, - FromIntegerSym1, PNum (..), - SNum (..), (%*), (%+), (%-), (%/=), - (%==)) - -import Data.Functor.Const (Const (..)) -import Data.Singletons.Decide (SDecide (..)) -import Data.Singletons.Prelude (Apply, Sing, SingI (..), SingKind (..), - SomeSing (..)) -import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ, sPred, sSucc) -import Data.Type.Equality ((:~:) (..)) -import Data.Void (Void, absurd) -import Numeric.Natural (Natural) -import Proof.Equational (because, coerce, start, sym, trans, (===)) - -type family Zero nat :: nat where - Zero nat = FromInteger 0 - -sZero :: (SNum nat) => Sing (Zero nat) -sZero = sFromInteger (sing :: Sing 0) - -type family One nat :: nat where - One nat = FromInteger 1 - -sOne :: SNum nat => Sing (One nat) -sOne = sFromInteger (sing :: Sing 1) - -type S n = Succ n - -sS :: SEnum 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 nat) - 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 nat) n -newtype PlusSuccR (n :: nat) = - PlusSuccR { plusSuccRProof :: forall m. Sing m -> n + S m :~: S (n + m) } - -type PlusZeroL (n :: nat) = IdentityL (+@#@$$) (Zero nat) 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 (+@#@$$) - -newtype MultZeroL (n :: nat) = MultZeroL { multZeroLProof :: Zero nat * n :~: Zero nat } -newtype MultZeroR (n :: nat) = - MultZeroR { multZeroRProof :: n * Zero nat :~: Zero nat } - -newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n * m :~: n * m + m } -newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n * S m :~: n * m + n } - -newtype PlusMultDistrib (n :: nat) = - PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l - -> (n + m) * l :~: (n * l) + (m * l) - } - -newtype PlusEqCancelL (n :: nat) = - PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l - -> n + m :~: n + l -> m :~: l } - -newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat + n } -newtype MultEqCancelR n = - MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l - -> n * Succ l :~: m * Succ l - -> n :~: m - } - -class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) - => IsPeano nat where - {-# MINIMAL succOneCong, succNonCyclic, predSucc, plusMinus, - succInj, ( (plusZeroL, plusSuccL) | (plusZeroR, plusZeroL)) - , ( (multZeroL, multSuccL) | (multZeroR, multSuccR)), - induction #-} - - succOneCong :: Succ (Zero nat) :~: One nat - 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 nat -> Void - induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k - plusMinus :: Sing (n :: nat) -> Sing m -> n + m - m :~: n - - plusMinus' :: Sing (n :: nat) -> Sing m -> n + m - n :~: m - plusMinus' n m = - start (n %+ m %- n) - === m %+ n %- n `because` minusCongL (plusComm n m) n - === m `because` plusMinus m n - - plusZeroL :: Sing n -> (Zero nat + n) :~: n - plusZeroL sn = idLProof (induction base step sn) - where - base :: PlusZeroL (Zero nat) - 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 nat) - 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 nat) :~: n - plusZeroR sn = idRProof (induction base step sn) - where - base :: PlusZeroR (Zero nat) - 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 nat) - 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 nat) - 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 nat) - 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 nat * n :~: Zero nat - multZeroL sn0 = multZeroLProof $ induction base step sn0 - where - base :: MultZeroL (Zero nat) - 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 nat) - 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 nat :~: Zero nat - multZeroR sn0 = multZeroRProof $ induction base step sn0 - where - base :: MultZeroR (Zero nat) - base = MultZeroR (multZeroL 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 nat) - 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 nat) - 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 nat :~: 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 nat * 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 nat) - 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 nat - 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 nat) - 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 nat) - 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 nat + n - succAndPlusOneL = proofSuccPlusL . induction base step - where - base :: SuccPlusL (Zero nat) - 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 nat - 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 nat -> n :~: Zero nat - 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 nat -> m :~: Zero nat - 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) - - minusZero :: Sing n -> n - Zero nat :~: n - minusZero n = - start (n %- sZero) - === (n %+ sZero) %- sZero - `because` minusCongL (sym $ plusZeroR n) sZero - === n `because` plusMinus n sZero - - 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 nat) - 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 nat -> 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) - - toNatural :: Sing (n :: nat) -> Natural - toNatural = getConst . induction (Const 0) (\_ (Const k) -> (Const k + 1)) - - fromNatural :: Natural -> SomeSing nat - fromNatural 0 = SomeSing sZero - fromNatural n = - case fromNatural (n - 1) of - SomeSing sn -> SomeSing (Succ sn) - -pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n -pattern Zero <- (zeroOrSucc -> IsZero) where - Zero = sZero - -pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n -pattern Succ n <- (zeroOrSucc -> IsSucc n) where - Succ n = sSucc n - -{-# COMPLETE Zero, Succ #-} diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs deleted file mode 100644 --- a/Data/Type/Natural/Class/Order.hs +++ /dev/null @@ -1,755 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} -{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 -{-# LANGUAGE StandaloneKindSignatures #-} -#endif - -module Data.Type.Natural.Class.Order - (PeanoOrder(..), DiffNat(..), LeqView(..), - FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR, - sLeqCongL, sLeqCongR, sLeqCong, - type (-.), (%-.), minPlusTruncMinus, truncMinusLeq, - module Data.Type.Natural.Singleton.Compat - ) where -import Data.Type.Natural.Class.Arithmetic -import Data.Type.Natural.Singleton.Compat (type (<), type (<=), type (<=@#@$), - type (<=@#@$$), type (<=@#@$$$), - type (<@#@$), type (<@#@$$), - type (<@#@$$$), type (>), type (>=), - type (>=@#@$), type (>=@#@$$), - type (>=@#@$$$), type (>@#@$), - type (>@#@$$), type (>@#@$$$), - type Min, type Max, type Compare, - type MinSym0, type MinSym1, type MinSym2, - type MaxSym0, type MaxSym1, type MaxSym2, - type CompareSym0, type CompareSym1, type CompareSym2, -#if MIN_VERSION_singletons(2,6,0) - SOrdering (SLT, SEQ, SGT), -#else - Sing (SLT, SEQ, SGT), -#endif - - SOrd(..), POrd(..), - LTSym0, GTSym0, EQSym0, - (%<), (%<=), (%>), (%>=)) - -import Data.Singletons.Prelude - (Sing, -#if MIN_VERSION_singletons(2,6,0) - SBool (SFalse, STrue), -#else - Sing (SFalse, STrue), -#endif - sing, withSingI - ) -import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ) -import Data.Singletons.TH (singletonsOnly) -import Data.Type.Equality ((:~:) (..)) -import Data.Void (Void, absurd) -import Proof.Equational (because, coerce, start, sym, trans, - withRefl, (===), (=~=)) -import Proof.Propositional (IsTrue (..), eliminate, withWitness) - -data LeqView (n :: nat) (m :: nat) where - LeqZero :: Sing n -> LeqView (Zero nat) 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 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 - --- | Since 0.9.0.0 (type changed) -coerceLeqL -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 - :: forall nat (n :: nat) m l. -#else - :: forall (n :: nat) m l . -#endif - IsPeano nat - => n :~: m -> Sing l - -> IsTrue (n <= l) -> IsTrue (m <= l) -coerceLeqL Refl _ Witness = Witness - --- | Since 0.9.0.0 (type changed) -coerceLeqR -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 - :: forall nat (n :: nat) m l . -#else - :: forall (n :: nat) m l . -#endif - IsPeano 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 nat, IsPeano nat) => PeanoOrder 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 nat) (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 nat) a :~: 'EQ) (Compare (Zero nat) 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 nat) :~: '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 nat) - base = LTSucc $ cmpZero (sZero :: Sing (Zero nat)) - - 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 nat) - 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 eql -> withRefl eql $ - start (sCompare n m) - =~= sCompare n (sSucc n) - === SLT `because` ltSucc n - Right nLTm -> ltSuccLToLT n m nLTm - - leqZero :: Sing n -> IsTrue (Zero nat <= 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 eql -> withRefl eql $ 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 nat) - 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 nat) - 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 nat) - 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 nat) -> n :~: Zero nat - 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 nat) -> Void - succLeqZeroAbsurd n leq = - succNonCyclic n (leqZeroElim (sSucc n) leq) - - succLeqZeroAbsurd' :: Sing n -> (S n <= Zero nat) :~: '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 -> withWitness (leqSucc n m 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 nat < 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 - - lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m) - lneqSuccStepL n m snLNEQm = - coerce (sym $ lneqSuccLeq n m) $ - leqSuccStepL (sSucc n) m $ - coerce (lneqSuccLeq (sSucc n) m) snLNEQm - - lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m) - lneqSuccStepR n m nLNEQm = - coerce (sym $ lneqSuccLeq n (sSucc m)) $ - leqSuccStepR (sSucc n) m $ - coerce (lneqSuccLeq 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 nat) n :~: n - maxZeroL n = leqToMax sZero n (leqZero n) - - maxZeroR :: Sing n -> Max n (Zero nat) :~: n - maxZeroR n = geqToMax n sZero (leqZero n) - - minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat - minZeroL n = leqToMin sZero n (leqZero n) - - minZeroR :: Sing n -> Min n (Zero nat) :~: Zero nat - 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) - - lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero nat) -> Void - lneqZeroAbsurd n leq = - succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq) - - minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) - -> n - m + m :~: n - minusPlus n m mLEQn = - case leqWitness m n mLEQn of - DiffNat _ k -> - start (n %- m %+ m) - =~= m %+ k %- m %+ m - === k %+ m %- m %+ m `because` plusCongL (minusCongL (plusComm m k) m) m - === k %+ m `because` plusCongL (plusMinus k m) m - === m %+ k `because` plusComm k m - =~= n - --- | Natural subtraction, truncated to zero if m > n. -type n -. m = Subt n m (m <= n) -type family Subt (n :: nat) (m :: nat) (b :: Bool) :: nat where - Subt n m 'True = n - m - Subt (n :: nat) m 'False = Zero nat -infixl 6 -. - -(%-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n -. m) -n %-. m = - case m %<= n of - STrue -> n %- m - SFalse -> sZero - -minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat) - -> Min n m + (n -. m) :~: n -minPlusTruncMinus n m = - case m %<= n of - STrue -> - start (sMin n m %+ (n %-. m)) - === m %+ (n %-. m) `because` plusCongL (geqToMin n m Witness) (n %-. m) - =~= m %+ (n %- m) - === (n %- m) %+ m `because` plusComm m (n %- m) - === n `because` minusPlus n m Witness - SFalse -> - start (sMin n m %+ (n %-. m)) - =~= sMin n m %+ sZero - === sMin n m `because` plusZeroR (sMin n m) - === n `because` leqToMin n m (notLeqToLeq m n) - -truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue ((n -. m) <= n) -truncMinusLeq n m = - case m %<= n of - STrue -> leqStep (n %-. m) n m $ minusPlus n m Witness - SFalse -> leqZero n - diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs deleted file mode 100644 --- a/Data/Type/Natural/Core.hs +++ /dev/null @@ -1,79 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -module Data.Type.Natural.Core where -import Data.Type.Natural.Definitions - -import Data.Constraint (Dict (..)) -import Prelude (Bool (..), Eq (..), Show (..), ($)) -import Proof.Propositional (IsTrue) -import Unsafe.Coerce (unsafeCoerce) - --------------------------------------------------- --- ** Type-level predicate & judgements. --------------------------------------------------- --- | 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 = IsTrue (a <= b) - -#if !MIN_VERSION_singletons(2,4,0) -deriving instance Show (SNat n) -#endif -deriving instance Eq (SNat n) - -data (a :: Nat) :<: (b :: Nat) where - ZeroLtSucc :: Zero :<: 'S m - SuccLtSucc :: n :<: m -> 'S n :<: 'S m - -deriving instance Show (a :<: b) - --------------------------------------------------- --- * Total orderings on natural numbers. --------------------------------------------------- -propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m -propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) -{-# INLINE propToBoolLeq #-} - -boolToClassLeq :: (n <= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m -boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) -{-# INLINE boolToClassLeq #-} - -propToClassLeq :: Leq n m -> LeqInstance n m -propToClassLeq _ = unsafeCoerce (Dict :: Dict ()) -{-# INLINE propToClassLeq #-} - -{- --- | Below is the "proof" of the correctness of above: -propToBoolLeq :: Leq n m -> LeqTrueInstance n m -propToBoolLeq (ZeroLeq _) = Dict -propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict - -boolToClassLeq :: (n <<= m) ~ True => SNat n -> SNat m -> LeqInstance n m -boolToClassLeq SZ _ = Dict -boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict -boolToClassLeq _ _ = bugInGHC - -propToClassLeq :: Leq n m -> LeqInstance n m -propToClassLeq (ZeroLeq _) = Dict -propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict --} - -type LeqInstance n m = IsTrue (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 - -leqRhs :: Leq n m -> SNat m -leqRhs (ZeroLeq m) = m -leqRhs (SuccLeqSucc leq) = SS $ leqRhs leq - -leqLhs :: Leq n m -> SNat n -leqLhs (ZeroLeq _) = SZ -leqLhs (SuccLeqSucc leq) = SS $ leqLhs leq - diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs deleted file mode 100644 --- a/Data/Type/Natural/Definitions.hs +++ /dev/null @@ -1,148 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, InstanceSigs #-} -{-# LANGUAGE KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-} -{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 -{-# LANGUAGE StandaloneKindSignatures #-} -#endif - -module Data.Type.Natural.Definitions - (module Data.Type.Natural.Definitions, - module Data.Singletons.Prelude, - module Data.Type.Natural.Singleton.Compat - ) where -import Data.Type.Natural.Singleton.Compat - -import Data.Singletons.Prelude -import Data.Singletons.Prelude.Enum -import Data.Singletons.TH -import Data.Typeable - --------------------------------------------------- --- * Natural numbers and its singleton type --------------------------------------------------- -singletons [d| - data Nat = Z | S Nat - deriving (Show, Eq) - |] - -deriving instance Typeable 'S -deriving instance Typeable 'Z - --------------------------------------------------- --- ** Arithmetic functions. --------------------------------------------------- - -singletons [d| - 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 - min (S m) (S n) = S (min m n) - - max Z Z = Z - max Z (S n) = S n - max (S n) Z = S n - max (S n) (S m) = S (max n m) - |] - -singletons [d| - instance Num Nat where - Z + n = n - S m + n = S (m + n) - - n - Z = n - S n - S m = n - m - Z - S _ = Z - - Z * _ = Z - S n * m = n * m + m - - abs n = n - - signum Z = Z - signum (S _) = S Z - - fromInteger n = if n == 0 then Z else S (fromInteger (n-1)) - |] - -singletons [d| - instance Enum Nat where - succ = S - 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 - |] - -singletons [d| - (**) :: Nat -> Nat -> Nat - _ ** Z = S Z - n ** S m = (n ** m) * n - |] -#if !MIN_VERSION_singletons(2,4,0) -type (**) a b = a :** b - -(%**) :: SNat n -> SNat m -> SNat (n ** m) -(%**) = (%:**) -#endif - -singletons [d| - zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat - eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat - zero = Z - one = S zero - two = S one - three = S two - four = S three - five = S four - six = S five - seven = S six - eight = S seven - nine = S eight - ten = S nine - eleven = S ten - twelve = S eleven - thirteen = S twelve - fourteen = S thirteen - fifteen = S fourteen - sixteen = S fifteen - seventeen = S sixteen - eighteen = S seventeen - nineteen = S eighteen - twenty = S nineteen - n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat - n10, n11, n12, n13, n14, n15, n16, n17 :: Nat - n18, n19, n20 :: Nat - n0 = zero - n1 = one - n2 = two - n3 = three - n4 = four - n5 = five - n6 = six - n7 = seven - n8 = eight - n9 = nine - n10 = ten - n11 = eleven - n12 = twelve - n13 = thirteen - n14 = fourteen - n15 = fifteen - n16 = sixteen - n17 = seventeen - n18 = eighteen - n19 = nineteen - n20 = twenty - |] diff --git a/Data/Type/Natural/Singleton/Compat.hs b/Data/Type/Natural/Singleton/Compat.hs deleted file mode 100644 --- a/Data/Type/Natural/Singleton/Compat.hs +++ /dev/null @@ -1,44 +0,0 @@ -{-# LANGUAGE CPP, ExplicitNamespaces, TemplateHaskell, TypeInType #-} --- | Compatibility layer for singletons -module Data.Type.Natural.Singleton.Compat - ( - module Data.Singletons.Prelude.Eq, - module Data.Singletons.Prelude.Num, - module Data.Singletons.Prelude.Ord -#if MIN_VERSION_singletons(2,6,0) - ,SOrdering(..) -#endif -#if !MIN_VERSION_singletons(2,4,0) - ,module Data.Type.Natural.Singleton.Compat -#endif - ) - where - -#if !MIN_VERSION_singletons(2,4,0) -import Data.Type.Natural.Singleton.Compat.TH -#endif - -#if MIN_VERSION_singletons(2,6,0) -import Data.Singletons.Prelude (SOrdering (SEQ, SGT, SLT)) -#else - -#endif - -import Data.Singletons.Prelude.Eq -import Data.Singletons.Prelude.Num -import Data.Singletons.Prelude.Ord - -#if !MIN_VERSION_singletons(2,4,0) -generateCompat Nothing ''SOrd "<" -generateCompat Nothing ''SOrd ">" -generateCompat Nothing ''SOrd "<=" -generateCompat Nothing ''SOrd ">=" - -generateCompat Nothing ''SEq "/=" -generateCompat Nothing ''SEq "==" - -generateCompat Nothing ''SNum "+" -generateCompat Nothing ''SNum "-" -generateCompat Nothing ''SNum "*" -#endif - diff --git a/Data/Type/Natural/Singleton/Compat/TH.hs b/Data/Type/Natural/Singleton/Compat/TH.hs deleted file mode 100644 --- a/Data/Type/Natural/Singleton/Compat/TH.hs +++ /dev/null @@ -1,39 +0,0 @@ -{-# LANGUAGE TemplateHaskell #-} -module Data.Type.Natural.Singleton.Compat.TH where -import Control.Applicative ((<|>)) -import Control.Monad (forM, zipWithM) -import Data.Maybe (fromMaybe) -import Data.Singletons -import Language.Haskell.TH - -generateCompat :: Maybe Fixity -> Name -> String -> DecsQ -generateCompat mfix cls opname = do - mfix' <- reifyFixity (mkName opname) - Just oldOpName <- lookupTypeName $ ":" ++ opname - Just oldSingName <- lookupValueName $ "%:" ++ opname - Just oldCur1Name <- lookupTypeName $ ":" ++ opname ++ "$" - Just oldCur2Name <- lookupTypeName $ ":" ++ opname ++ "$$" - Just oldCur3Name <- lookupTypeName $ ":" ++ opname ++ "$$$" - let newOpName = mkName opname - newSingName = mkName $ "%" ++ opname - newCur1Name = mkName $ opname ++ "@#@$" - newCur2Name = mkName $ opname ++ "@#@$$" - newCur3Name = mkName $ opname ++ "@#@$$$" - cur12 <- zipWithM (\old new -> tySynD new [] (conT old)) - [oldCur1Name, oldCur2Name] - [newCur1Name, newCur2Name] - [a, b] <- mapM newName ["a", "b"] - cur3 <- tySynD newCur3Name (map PlainTV [a,b]) - $ infixT (varT a) oldCur3Name (varT b) - nat <- newName "nat" - tysyn <- tySynD newOpName [PlainTV a, PlainTV b] $ - infixT (varT a) oldOpName (varT b) - sig <- sigD newSingName $ - forallT [PlainTV nat, KindedTV a (VarT nat), KindedTV b (VarT nat)] - (sequence [[t| $(conT cls) $(varT nat) |]]) - [t| Sing $(varT a) -> Sing $(varT b) -> Sing $(infixT (varT a) newOpName (varT b)) |] - defn <- funD newSingName [clause [] (normalB $ varE oldSingName) [] ] - fixes <- fmap (fromMaybe []) $ forM (mfix <|> mfix') $ \fixity -> - return [InfixD fixity newOpName, InfixD fixity newSingName] - return (sig : defn : tysyn : cur12 ++ [cur3] ++ fixes) - diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs deleted file mode 100644 --- a/Data/Type/Ordinal.hs +++ /dev/null @@ -1,322 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls #-} -{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PatternSynonyms, PolyKinds #-} -{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} --- | Set-theoretic ordinals for general peano arithmetic models -module Data.Type.Ordinal - ( -- * Data-types - Ordinal (..), pattern OZ, pattern OS, HasOrdinal, - -- * Quasi Quoter - -- $quasiquotes - mkOrdinalQQ, odPN, odLit, - -- * Conversion from cardinals to ordinals. - sNatToOrd', sNatToOrd, - ordToNatural, unsafeNaturalToOrd', unsafeNaturalToOrd, - reallyUnsafeNaturalToOrd, - naturalToOrd, naturalToOrd', - ordToSing, inclusion, inclusion', - -- * Ordinal arithmetics - (@+), enumOrdinal, - -- * Elimination rules for @'Ordinal' 'Z'@. - absurdOrd, vacuousOrd, - -- * Deprecated combinators - ordToInt, unsafeFromInt, unsafeFromInt' - ) where -import Data.Type.Natural.Singleton.Compat - -import Data.List (genericDrop, genericTake) -import Data.Maybe (fromMaybe) -import Data.Ord (comparing) -import Data.Singletons.Decide -import Data.Singletons.Prelude -import Data.Singletons.Prelude.Enum -import Data.Type.Equality -import qualified Data.Type.Natural as PN -import Data.Type.Natural.Builtin () -import Data.Type.Natural.Class -import Data.Typeable (Typeable) -import Data.Void (absurd) -import qualified GHC.TypeLits as TL -import Language.Haskell.TH hiding (Type) -import Language.Haskell.TH.Quote -import Numeric.Natural -import Proof.Equational -import Proof.Propositional -import Unsafe.Coerce - --- | Set-theoretic (finite) ordinals: --- --- > n = {0, 1, ..., n-1} --- --- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. --- --- Since 0.6.0.0 -data Ordinal (n :: nat) where - OLt :: (IsPeano nat, (n < m) ~ 'True) => Sing (n :: nat) -> Ordinal m - -{-# COMPLETE OLt #-} - -fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n < Succ m) ~ 'True, SingI m) - => Sing (n :: nat) -> Ordinal m -fromOLt n = - withRefl (sym $ succLneqSucc n (sing :: Sing m)) $ - OLt n - --- | Pattern synonym representing the 0-th ordinal. --- --- Since 0.6.0.0 -pattern OZ :: forall nat (n :: nat). IsPeano nat - => (Zero nat < n) ~ 'True => Ordinal n -pattern OZ <- OLt Zero where - OZ = OLt sZero - --- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. --- --- Since 0.6.0.0 -pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t) - => (IsPeano nat) - => Ordinal t -> Ordinal (Succ t) -pattern OS n <- OLt (Succ (fromOLt -> n)) where - OS o = succOrd o - --- | Since 0.2.3.0 -deriving instance Typeable Ordinal - --- | Class synonym for Peano numerals with ordinals. --- --- Since 0.5.0.0 -class (PeanoOrder nat, SingKind nat) => HasOrdinal nat -instance (PeanoOrder nat, SingKind nat) => HasOrdinal nat - -instance (HasOrdinal nat, SingI (n :: nat)) - => Num (Ordinal n) where - _ + _ = error "Finite ordinal is not closed under addition." - _ - _ = error "Ordinal subtraction is not defined" - negate OZ = OZ - negate _ = error "There are no negative oridnals!" - OZ * _ = OZ - _ * OZ = OZ - _ * _ = error "Finite ordinal is not closed under multiplication" - abs = id - signum = error "What does Ordinal sign mean?" - fromInteger = unsafeFromInt' (Proxy :: Proxy nat) . fromInteger - --- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n)) -instance (SingI n, HasOrdinal nat) - => Show (Ordinal (n :: nat)) where - showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (toNatural (sing :: Sing n))) - -instance (HasOrdinal nat) - => Eq (Ordinal (n :: nat)) where - o == o' = ordToInt o == ordToInt o' - -instance (HasOrdinal nat) => Ord (Ordinal (n :: nat)) where - compare = comparing ordToInt - -instance (HasOrdinal nat, SingI n) - => Enum (Ordinal (n :: nat)) where - fromEnum = fromIntegral . ordToInt - toEnum = unsafeFromInt' (Proxy :: Proxy nat) . fromIntegral - enumFrom = enumFromOrd - enumFromTo = enumFromToOrd - --- | Since 0.9.0.0 (type changed) -enumFromToOrd :: forall nat (n :: nat). - (HasOrdinal nat, SingI n) - => Ordinal n -> Ordinal n -> [Ordinal n] -enumFromToOrd ok ol = - let k = ordToInt ok - l = ordToInt ol - in genericTake (l - k + 1) $ enumFromOrd ok - --- | Since 0.9.0.0 (type changed) -enumFromOrd :: forall nat (n :: nat). - (HasOrdinal nat, SingI n) - => Ordinal n -> [Ordinal n] -enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n) - --- | Enumerate all @'Ordinal'@s less than @n@. -enumOrdinal :: (PeanoOrder nat) => Sing (n :: nat) -> [Ordinal n] -enumOrdinal sn = withSingI sn $ map (reallyUnsafeNaturalToOrd Proxy) [0..toNatural sn - 1] - --- | Since 0.9.0.0 (type changed) -succOrd :: forall nat (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n) -succOrd (OLt n) = - withRefl (succLneqSucc n (sing :: Sing n)) $ - OLt (sSucc n) -{-# INLINE succOrd #-} - -instance SingI n => Bounded (Ordinal ('PN.S n)) where - minBound = OLt PN.SZ - - maxBound = - withWitness (leqRefl (sing :: Sing n)) $ - sNatToOrd (sing :: Sing n) - -instance (SingI m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n) where - minBound = - withWitness (lneqZero (sing :: Sing m)) $ - OLt (sing :: Sing 0) - {-# INLINE minBound #-} - maxBound = - withWitness (lneqSucc (sing :: Sing m)) $ - sNatToOrd (sing :: Sing m) - {-# INLINE maxBound #-} - -{-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-} --- | Since 0.9.0.0 (type changed) -unsafeFromInt :: forall nat (n :: nat). (HasOrdinal nat, SingI (n :: nat)) - => Int -> Ordinal n -unsafeFromInt = unsafeNaturalToOrd . fromIntegral - --- | Converts @'Natural'@s into @'Ordinal n'@. --- If the given natural is greater or equal to @n@, raises exception. --- --- Since 0.8.0.0 -unsafeNaturalToOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI (n :: nat)) - => Natural -> Ordinal n -unsafeNaturalToOrd k = - fromMaybe (error "unsafeNaturalToOrd Out of bound") $ - naturalToOrd k - -{-# DEPRECATED unsafeFromInt' "Use unsafeNaturalToOrd' instead" #-} --- | Since 0.8.0.0 -unsafeFromInt' :: forall proxy nat (n :: nat). (HasOrdinal nat, SingI n) - => proxy nat -> Int -> Ordinal n -unsafeFromInt' p = unsafeNaturalToOrd' p . fromIntegral - --- | Since 0.8.0.0 -unsafeNaturalToOrd' :: forall proxy nat (n :: nat). (HasOrdinal nat, SingI n) - => proxy nat -> Natural -> Ordinal n -unsafeNaturalToOrd' _ n = - case fromNatural n of - SomeSing sn -> - case sn %< (sing :: Sing n) of - STrue -> sNatToOrd' (sing :: Sing n) sn - SFalse -> error "Bound over!" - -{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-} --- | Converts @'Natural'@s into @'Ordinal' n@, WITHOUT any boundary check. --- This function may easily violate type-safety. Use with care! -reallyUnsafeNaturalToOrd :: forall pxy nat (n :: nat). (HasOrdinal nat, SingI n) - => pxy nat -> Natural -> Ordinal n -reallyUnsafeNaturalToOrd _ k = - case fromNatural k of - SomeSing (sk :: Sing (k :: nat)) -> - withRefl (unsafeCoerce (Refl :: () :~: ()) :: (k < n) :~: 'True) $ - OLt sk - --- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. --- --- Since 0.5.0.0 -sNatToOrd' :: (PeanoOrder nat, (m < n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n -sNatToOrd' _ = OLt -{-# INLINE sNatToOrd' #-} - --- | 'sNatToOrd'' with @n@ inferred. -sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m < n) ~ 'True) => Sing m -> Ordinal n -sNatToOrd = sNatToOrd' sing - --- | Since 0.8.0.0 -naturalToOrd :: forall nat n. (HasOrdinal nat, SingI n) - => Natural -> Maybe (Ordinal (n :: nat)) -naturalToOrd = naturalToOrd' (sing :: Sing n) - -naturalToOrd' :: HasOrdinal nat - => Sing (n :: nat) -> Natural -> Maybe (Ordinal n) -naturalToOrd' sn k = - case fromNatural k of - SomeSing sk -> - case sk %< sn of - STrue -> Just (OLt sk) - _ -> Nothing - --- | Convert @Ordinal n@ into monomorphic @Sing@ --- --- Since 0.5.0.0 -ordToSing :: (PeanoOrder nat) => Ordinal (n :: nat) -> SomeSing nat -ordToSing (OLt n) = SomeSing n -{-# INLINE ordToSing #-} - -{-# DEPRECATED ordToInt "Use ordToNatural instead." #-} --- | Convert ordinal into @'Int'@. -ordToInt :: (HasOrdinal nat) - => Ordinal (n :: nat) - -> Int -ordToInt = fromIntegral . ordToNatural -{-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Int #-} -{-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Int #-} - -ordToNatural :: HasOrdinal nat - => Ordinal (n :: nat) - -> Natural -ordToNatural (OLt n) = toNatural n -{-# SPECIALISE ordToNatural :: Ordinal (n :: PN.Nat) -> Natural #-} -{-# SPECIALISE ordToNatural :: Ordinal (n :: TL.Nat) -> Natural #-} - --- | Inclusion function for ordinals. --- --- Since 0.7.0.0 (constraint was weakened since last released) -inclusion' :: (n <= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m -inclusion' _ = unsafeCoerce -{-# INLINE inclusion' #-} - --- | Inclusion function for ordinals with codomain inferred. --- --- Since 0.7.0.0 (constraint was weakened since last released) -inclusion :: ((n <= m) ~ 'True) => Ordinal n -> Ordinal m -inclusion = unsafeCoerce -{-# INLINE inclusion #-} - - --- | Ordinal addition. --- --- Since 0.9.0.0 (type changed) -(@+) :: forall nat (n :: nat) m. (PeanoOrder nat, SingI n, SingI m) - => Ordinal n -> Ordinal m -> Ordinal (n + m) -OLt k @+ OLt l = - let (n, m) = (n :: Sing n, m :: Sing m) - in withWitness (plusStrictMonotone k n l m Witness Witness) $ OLt $ k %+ l - --- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. --- --- Since 0.2.3.0 -absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a -absurdOrd (OLt n) = absurd $ lneqZeroAbsurd n Witness - --- | @'absurdOrd'@ for value in 'Functor'. --- --- Since 0.2.3.0 -vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a -vacuousOrd = fmap absurdOrd - -{-$quasiquotes #quasiquoters# - - This section provides QuasiQuoter and general generator for ordinals. - Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT - checks boundary; with @'od'@, we can use literal with - boundary check. - For example, with @-XQuasiQuotes@ language extension enabled, - @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, - whilst @12 :: Ordinal 1@ compiles but raises run-time error. - So, to enforce correctness, we recommend to use these quoters - instead of bare @'Num'@ numerals. --} - --- | Quasiquoter generator for ordinals -mkOrdinalQQ :: TypeQ -> QuasiQuoter -mkOrdinalQQ t = - QuasiQuoter { quoteExp = \s -> [| OLt $(quoteExp (mkSNatQQ t) s) |] - , quoteType = error "No type quoter for Ordinals" - , quotePat = \s -> [p| OLt ((%~ $(quoteExp (mkSNatQQ t) s)) -> Proved Refl) |] - , quoteDec = error "No declaration quoter for Ordinals" - } - -odPN, odLit :: QuasiQuoter --- | Quasiquoter for ordinal indexed by Peano numeral @'Data.Type.Natural.Nat'@. -odPN = mkOrdinalQQ [t| PN.Nat |] --- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@. -odLit = mkOrdinalQQ [t| TL.Nat |] - diff --git a/Data/Type/Ordinal/Builtin.hs b/Data/Type/Ordinal/Builtin.hs deleted file mode 100644 --- a/Data/Type/Ordinal/Builtin.hs +++ /dev/null @@ -1,174 +0,0 @@ -{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-} -{-# OPTIONS_GHC -Wno-warnings-deprecations #-} --- | Module providing the same API as 'Data.Type.Ordinal' but specialised to --- GHC's builtin @'Nat'@. --- --- Since 0.7.1.0 -module Data.Type.Ordinal.Builtin - ( -- * Data-types and pattern synonyms - Ordinal, pattern OLt, pattern OZ, pattern OS, - -- * Quasi Quoter - -- $quasiquotes - od, - -- * Conversion from cardinals to ordinals. - sNatToOrd', sNatToOrd, ordToNatural, - unsafeNaturalToOrd, naturalToOrd, naturalToOrd', - inclusion, inclusion', - -- * Ordinal arithmetics - (@+), enumOrdinal, - -- * Elimination rules for @'Ordinal' 0'@. - absurdOrd, vacuousOrd, - -- * Deprecated combinators - ordToInt, unsafeFromInt - ) where -import qualified Data.Type.Natural.Singleton.Compat as SC - -import Numeric.Natural (Natural) -import Data.Singletons (SingI, Sing) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Ordinal as O -import GHC.TypeLits -import Language.Haskell.TH.Quote (QuasiQuoter) - --- | Set-theoretic (finite) ordinals: --- --- > n = {0, 1, ..., n-1} --- --- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 0@ is isomorphic to @Void@. --- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@ --- specialised to GHC's builtin numeral @'Nat'@. --- --- Since 0.7.0.0 -type Ordinal (n :: Nat) = O.Ordinal n - --- | We provide specialised version of constructor @'O.OLt'@ as type synonym @'OLt'@. --- In some case, GHC warns about incomplete pattern using pattern @'OLt'@, --- but it is due to the limitation of GHC's current exhaustiveness checker. --- --- Since 0.7.0.0 -pattern OLt :: () => forall (n1 :: Nat). ((n1 SC.< t) ~ 'True) - => Sing n1 -> O.Ordinal t -pattern OLt n = O.OLt n -{-# COMPLETE OLt #-} - --- | Pattern synonym representing the 0-th ordinal. --- --- Since 0.7.0.0 -pattern OZ :: forall (n :: Nat). () - => (0 SC.< n) ~ 'True => O.Ordinal n -pattern OZ = O.OZ - --- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. --- --- Since 0.7.0.0 -pattern OS :: forall (t :: Nat). (KnownNat t) - => () => O.Ordinal t -> O.Ordinal (Succ t) -pattern OS n = O.OS n - -{-$quasiquotes #quasiquoters# - - This section provides QuasiQuoter for ordinals. - Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT - checks boundary; with @'od'@, we can use literal with - boundary check. - For example, with @-XQuasiQuotes@ language extension enabled, - @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, - whilst @12 :: Ordinal 1@ compiles but raises run-time error. - So, to enforce correctness, we recommend to use these quoters - instead of bare @'Num'@ numerals. --} - --- | Quasiquoter for ordinal indexed by GHC's built-n @'Data.Type.Natural.Nat'@. --- --- Since 0.7.0.0 -od :: QuasiQuoter -od = O.odLit -{-# INLINE od #-} - --- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. --- --- Since 0.7.0.0 -sNatToOrd' :: (m SC.< n) ~ 'True => Sing n -> Sing m -> Ordinal n -sNatToOrd' = O.sNatToOrd' -{-# INLINE sNatToOrd' #-} - --- | 'sNatToOrd'' with @n@ inferred. --- --- Since 0.7.0.0 -sNatToOrd :: (KnownNat n, (m SC.< n) ~ 'True) => Sing m -> Ordinal n -sNatToOrd = O.sNatToOrd -{-# INLINE sNatToOrd #-} - -{-# DEPRECATED ordToInt "Use ordToNatural instead" #-} --- | Convert ordinal into @Int@. --- --- Since 0.7.0.0 -ordToInt :: Ordinal n -> Int -ordToInt = O.ordToInt -{-# INLINE ordToInt #-} - -{-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-} -unsafeFromInt :: KnownNat n - => Int -> Ordinal n -unsafeFromInt = O.unsafeFromInt -{-# INLINE unsafeFromInt #-} - -ordToNatural :: Ordinal (n :: Nat) -> Natural -ordToNatural = O.ordToNatural -{-# INLINE ordToNatural #-} - - -naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n) -naturalToOrd = O.naturalToOrd -{-# INLINE naturalToOrd #-} - -naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n) -naturalToOrd' = O.naturalToOrd' -{-# INLINE naturalToOrd' #-} - -unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n -unsafeNaturalToOrd = O.unsafeNaturalToOrd -{-# INLINE unsafeNaturalToOrd #-} - --- | Inclusion function for ordinals. --- --- Since 0.7.0.0 -inclusion :: (n SC.<= m) ~ 'True => Ordinal n -> Ordinal m -inclusion = O.inclusion -{-# INLINE inclusion #-} - --- | Inclusion function for ordinals with codomain inferred. --- --- Since 0.7.0.0 -inclusion' :: (n SC.<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m -inclusion' = O.inclusion' -{-# INLINE inclusion' #-} - --- | Ordinal addition. --- --- Since 0.7.0.0 -(@+) :: (KnownNat n, KnownNat m) => Ordinal n -> Ordinal m -> Ordinal (n + m) -(@+) = (O.@+) -{-# INLINE (@+) #-} - --- | Enumerate all @'Ordinal'@s less than @n@. --- --- Since 0.7.0.0 -enumOrdinal :: Sing n -> [Ordinal n] -enumOrdinal = O.enumOrdinal -{-# INLINE enumOrdinal #-} - --- | Since @Ordinal 0@ is logically not inhabited, we can coerce it to any value. --- --- Since 0.7.0.0 -absurdOrd :: Ordinal 0 -> a -absurdOrd = O.absurdOrd -{-# INLINE absurdOrd #-} - --- | @'absurdOrd'@ for values in 'Functor'. --- --- Since 0.7.0.0 -vacuousOrd :: Functor f => f (Ordinal 0) -> f a -vacuousOrd = O.vacuousOrd -{-# INLINE vacuousOrd #-} diff --git a/Data/Type/Ordinal/Peano.hs b/Data/Type/Ordinal/Peano.hs deleted file mode 100644 --- a/Data/Type/Ordinal/Peano.hs +++ /dev/null @@ -1,167 +0,0 @@ -{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-} -{-# OPTIONS_GHC -Wno-warnings-deprecations #-} --- | Module providing the same API as 'Data.Type.Ordinal' but specialised to --- peano numeral @'Nat'@. --- --- Since 0.7.0.0 -module Data.Type.Ordinal.Peano - ( -- * Data-types and pattern synonyms - Ordinal, pattern OLt, pattern OZ, pattern OS, - -- * Quasi Quoter - -- $quasiquotes - od, - -- * Conversion from cardinals to ordinals. - sNatToOrd', sNatToOrd, inclusion, inclusion', - ordToNatural, unsafeNaturalToOrd, naturalToOrd, naturalToOrd', - -- * Ordinal arithmetics - (@+), enumOrdinal, - -- * Elimination rules for @'Ordinal' 'Z'@. - absurdOrd, vacuousOrd, - -- * Deprecated Combinators - ordToInt, unsafeFromInt - ) where -import Data.Type.Natural.Singleton.Compat - -import Numeric.Natural (Natural) -import Data.Singletons.Prelude (SingI, Sing (..)) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Ordinal as O -import Data.Type.Natural -import Language.Haskell.TH.Quote (QuasiQuoter) - --- | Set-theoretic (finite) ordinals: --- --- > n = {0, 1, ..., n-1} --- --- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. --- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@ --- specialised to Peano numeral @'Nat'@. --- --- Since 0.7.0.0 -type Ordinal (n :: Nat) = O.Ordinal n - --- | We provide specialised version of constructor @'O.OLt'@ as type synonym @'OLt'@. --- In some case, GHC warns about incomplete pattern using pattern @'OLt'@, --- but it is due to the limitation of GHC's current exhaustiveness checker. --- --- Since 0.7.0.0 -pattern OLt :: () => forall (n1 :: Nat). ((n1 < t) ~ 'True) - => Sing n1 -> O.Ordinal t -pattern OLt n = O.OLt n -{-# COMPLETE OLt #-} - --- | Pattern synonym representing the 0-th ordinal. --- --- Since 0.7.0.0 -pattern OZ :: forall (n :: Nat). () - => ('Z < n) ~ 'True => O.Ordinal n -pattern OZ = O.OZ - --- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. --- --- Since 0.7.0.0 -pattern OS :: forall (t :: Nat). (SingI t) - => () => O.Ordinal t -> O.Ordinal (Succ t) -pattern OS n = O.OS n - -{-$quasiquotes #quasiquoters# - - This section provides QuasiQuoter for ordinals. - Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT - checks boundary; with @'od'@, we can use literal with - boundary check. - For example, with @-XQuasiQuotes@ language extension enabled, - @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, - whilst @12 :: Ordinal 1@ compiles but raises run-time error. - So, to enforce correctness, we recommend to use these quoters - instead of bare @'Num'@ numerals. --} - --- | Quasiquoter for ordinal indexed by Peano numeral @'Data.Type.Natural.Nat'@. --- --- Since 0.7.0.0 -od :: QuasiQuoter -od = O.odLit -{-# INLINE od #-} - --- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. --- --- Since 0.7.0.0 -sNatToOrd' :: (m < n) ~ 'True => Sing n -> Sing m -> Ordinal n -sNatToOrd' = O.sNatToOrd' -{-# INLINE sNatToOrd' #-} - --- | 'sNatToOrd'' with @n@ inferred. --- --- Since 0.7.0.0 -sNatToOrd :: (SingI n, (m < n) ~ 'True) => Sing m -> Ordinal n -sNatToOrd = O.sNatToOrd -{-# INLINE sNatToOrd #-} - --- | Convert ordinal into @Int@. --- --- Since 0.7.0.0 -ordToInt :: Ordinal n -> Int -ordToInt = O.ordToInt -{-# INLINE ordToInt #-} - -unsafeFromInt :: SingI n - => Int -> Ordinal n -unsafeFromInt = O.unsafeFromInt -{-# INLINE unsafeFromInt #-} - --- | Inclusion function for ordinals. --- --- Since 0.7.0.0 -inclusion :: (n <= m) ~ 'True => Ordinal n -> Ordinal m -inclusion = O.inclusion -{-# INLINE inclusion #-} - --- | Inclusion function for ordinals with codomain inferred. --- --- Since 0.7.0.0 -inclusion' :: (n <= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m -inclusion' = O.inclusion' -{-# INLINE inclusion' #-} - --- | Ordinal addition. --- --- Since 0.7.0.0 -(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m) -(@+) = (O.@+) -{-# INLINE (@+) #-} - --- | Enumerate all @'Ordinal'@s less than @n@. --- --- Since 0.7.0.0 -enumOrdinal :: Sing n -> [Ordinal n] -enumOrdinal = O.enumOrdinal -{-# INLINE enumOrdinal #-} - --- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. --- --- Since 0.7.0.0 -absurdOrd :: Ordinal 'Z -> a -absurdOrd = O.absurdOrd -{-# INLINE absurdOrd #-} - --- | @'absurdOrd'@ for values in 'Functor'. --- --- Since 0.7.0.0 -vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a -vacuousOrd = O.vacuousOrd -{-# INLINE vacuousOrd #-} - -ordToNatural :: Ordinal (n :: Nat) -> Natural -ordToNatural = O.ordToNatural -{-# INLINE ordToNatural #-} - -unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n -unsafeNaturalToOrd = O.unsafeNaturalToOrd - -naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n) -naturalToOrd = O.naturalToOrd - -naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n) -naturalToOrd' = O.naturalToOrd' diff --git a/src/Data/Type/Natural.hs b/src/Data/Type/Natural.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural.hs @@ -0,0 +1,168 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +-- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@ +module Data.Type.Natural + ( -- * Type-level naturals + + -- ** @Nat@, singletons and KnownNat manipulation, + Nat, + KnownNat, + SNat (Succ, Zero), + sNat, + sNatP, + toNatural, + SomeSNat (..), + toSomeSNat, + withSNat, + withKnownNat, + natVal, + natVal', + someNatVal, + SomeNat (..), + (%~), + Equality (..), + type (===), + + -- *** Pattens and Views + viewNat, + zeroOrSucc, + ZeroOrSucc (..), + + -- ** Promtoed and singletonised operations + + -- *** Arithmetic + Succ, + sSucc, + S, + Pred, + sPred, + sS, + Zero, + sZero, + One, + sOne, + type (+), + (%+), + type (-), + (%-), + type (*), + (%*), + Div, + sDiv, + Mod, + sMod, + type (^), + (%^), + type (-.), + (%-.), + Log2, + sLog2, + + -- *** Ordering + type (<=?), + type (<=), + (%<=?), + type (=?), + type (>=), + (%>=?), + type (>?), + type (>), + (%>?), + CmpNat, + sCmpNat, + sCompare, + Min, + sMin, + Max, + sMax, + induction, + + -- * QuasiQuotes + snat, + + -- * Singletons for auxiliary types + SBool (..), + SOrdering (..), + FlipOrdering, + sFlipOrdering, + ) +where + +import Data.Coerce (coerce) +import Data.Proxy (Proxy) +import Data.Type.Natural.Core +import Data.Type.Natural.Lemma.Arithmetic +import Data.Type.Natural.Lemma.Order +import Language.Haskell.TH (litT, numTyLit) +import Language.Haskell.TH.Quote +import Numeric.Natural +import Text.Read (readMaybe) + +{- | Quotesi-quoter for SNatleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression. + + For example: @[snat|12|] '%+' [snat| 5 |]@. +-} +snat :: QuasiQuoter +snat = + QuasiQuoter + { quoteExp = \str -> + case readMaybe str of + Just n -> [|sNat :: SNat $(litT $ numTyLit n)|] + Nothing -> error "Must be natural literal" + , quotePat = \str -> + case readMaybe str of + Just n -> [p|((%~ (sNat :: SNat $(litT $ numTyLit n))) -> Equal)|] + Nothing -> error "Must be natural literal" + , quoteType = \str -> + case readMaybe str of + Just n -> litT $ numTyLit n + Nothing -> error "Must be natural literal" + , quoteDec = error "No declaration Quotes for Nat" + } + +toNatural :: SNat n -> Natural +toNatural = coerce + +data SomeSNat where + SomeSNat :: KnownNat n => SNat n -> SomeSNat + +deriving instance Show SomeSNat + +instance Eq SomeSNat where + SomeSNat (SNat n) == SomeSNat (SNat m) = n == m + SomeSNat (SNat n) /= SomeSNat (SNat m) = n /= m + +toSomeSNat :: Natural -> SomeSNat +toSomeSNat n = case someNatVal n of + SomeNat pn -> withKnownNat sn $ SomeSNat sn + where + sn = sNatP pn + +withSNat :: Natural -> (forall n. KnownNat n => SNat n -> r) -> r +withSNat n act = case someNatVal n of + SomeNat (pn :: Proxy n) -> withKnownNat sn $ act sn + where + sn = sNatP pn + +sNatP :: KnownNat n => pxy n -> SNat n +sNatP = const sNat diff --git a/src/Data/Type/Natural/Builtin.hs b/src/Data/Type/Natural/Builtin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Builtin.hs @@ -0,0 +1,7 @@ +-- | Since 1.0.0.0 +module Data.Type.Natural.Builtin + {-# DEPRECATED "Use Data.Type.Natural instead" #-} + (module Data.Type.Natural) +where + +import Data.Type.Natural diff --git a/src/Data/Type/Natural/Core.hs b/src/Data/Type/Natural/Core.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Core.hs @@ -0,0 +1,237 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module Data.Type.Natural.Core + ( SNat (.., Zero, Succ), + ZeroOrSucc (..), + viewNat, + sNat, + withKnownNat, + (%+), + (%-), + (%*), + (%^), + sDiv, + sMod, + sLog2, + (%<=?), + sCmpNat, + sCompare, + Succ, + S, + sSucc, + sS, + Pred, + sPred, + Zero, + One, + sZero, + sOne, + Equality (..), + type (===), + (%~), + sFlipOrdering, + FlipOrdering, + SOrdering (..), + SBool (..), + -- Re-exports + module GHC.TypeNats, + ) +where + +import Data.Coerce (coerce) +import Data.Proxy (Proxy) +import Data.Type.Equality + ( TestEquality (..), + gcastWith, + type (:~:) (..), + type (==), + ) +import Data.Type.Natural.Utils +import GHC.Exts (Proxy#, proxy#) +import GHC.TypeNats +import Math.NumberTheory.Logarithms (naturalLog2) +import Numeric.Natural (Natural) +import Proof.Propositional (Empty) +import Type.Reflection (Typeable) +import Unsafe.Coerce (unsafeCoerce) + +-- | A singleton for type-level naturals +newtype SNat (n :: Nat) = SNat Natural + deriving newtype (Show, Eq, Ord) + +withKnownNat :: forall n r. SNat n -> (KnownNat n => r) -> r +withKnownNat (SNat n) act = + case someNatVal n of + SomeNat (_ :: Proxy m) -> + gcastWith (unsafeCoerce (Refl @()) :: n :~: m) act + +(%+) :: SNat n -> SNat m -> SNat (n + m) +(%+) = coerce $ (+) @Natural + +(%-) :: SNat n -> SNat m -> SNat (n - m) +(%-) = coerce $ (-) @Natural + +(%*) :: SNat n -> SNat m -> SNat (n * m) +(%*) = coerce $ (*) @Natural + +sDiv :: SNat n -> SNat m -> SNat (Div n m) +sDiv = coerce $ div @Natural + +sMod :: SNat n -> SNat m -> SNat (Mod n m) +sMod = coerce $ mod @Natural + +(%^) :: SNat n -> SNat m -> SNat (n ^ m) +(%^) = coerce $ (^) @Natural @Natural + +sLog2 :: SNat n -> SNat (Log2 n) +sLog2 = coerce $ fromIntegral @Int @Natural . naturalLog2 + +sNat :: forall n. KnownNat n => SNat n +sNat = SNat $ natVal' (proxy# :: Proxy# n) + +infixl 6 %+, %- + +infixl 7 %*, `sDiv`, `sMod` + +infixr 8 %^ + +instance TestEquality SNat where + testEquality (SNat l) (SNat r) = + if l == r + then Just trustMe + else Nothing + +data Equality n m where + Equal :: ((n == n) ~ 'True) => Equality n n + NonEqual :: + ((n === m) ~ 'False, (n == m) ~ 'False, Empty (n :~: m)) => + Equality n m + +type family a === b where + a === a = 'True + _ === _ = 'False + +infix 4 ===, %~ + +(%~) :: SNat l -> SNat r -> Equality l r +SNat l %~ SNat r = + if l == r + then unsafeCoerce (Equal @()) + else unsafeCoerce (NonEqual @0 @1) + +type Zero = 0 + +type One = 1 + +sZero :: SNat 0 +sZero = sNat + +sOne :: SNat 1 +sOne = sNat + +type Succ n = n + 1 + +type S n = Succ n + +sSucc, sS :: SNat n -> SNat (Succ n) +sS = (%+ sOne) +sSucc = sS + +sPred :: SNat n -> SNat (Pred n) +sPred = (%- sOne) + +type Pred n = n - 1 + +data ZeroOrSucc n where + IsZero :: ZeroOrSucc 0 + IsSucc :: + SNat n -> + ZeroOrSucc (n + 1) + +pattern Zero :: forall n. () => n ~ 0 => SNat n +pattern Zero <- + (viewNat -> IsZero) + where + Zero = sZero + +pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n +pattern Succ n <- + (viewNat -> IsSucc n) + where + Succ n = sSucc n + +{-# COMPLETE Zero, Succ #-} + +viewNat :: forall n. SNat n -> ZeroOrSucc n +viewNat n = + case n `testEquality` sNat @0 of + Just Refl -> IsZero + Nothing -> gcastWith (trustMe @(1 <=? n) @ 'True) $ IsSucc (sPred n) + +type family FlipOrdering ord where + FlipOrdering 'LT = 'GT + FlipOrdering 'GT = 'LT + FlipOrdering 'EQ = 'EQ + +sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord) +sFlipOrdering SLT = SGT +sFlipOrdering SEQ = SEQ +sFlipOrdering SGT = SLT + +data SOrdering (ord :: Ordering) where + SLT :: SOrdering 'LT + SEQ :: SOrdering 'EQ + SGT :: SOrdering 'GT + +deriving instance Show (SOrdering ord) + +deriving instance Eq (SOrdering ord) + +deriving instance Typeable SOrdering + +data SBool (b :: Bool) where + SFalse :: SBool 'False + STrue :: SBool 'True + +deriving instance Show (SBool ord) + +deriving instance Eq (SBool ord) + +deriving instance Typeable SBool + +infix 4 %<=? + +(%<=?) :: SNat n -> SNat m -> SBool (n <=? m) +SNat n %<=? SNat m = + if n <= m + then unsafeCoerce STrue + else unsafeCoerce SFalse + +sCmpNat, sCompare :: SNat n -> SNat m -> SOrdering (CmpNat n m) +sCompare = sCmpNat +sCmpNat (SNat n) (SNat m) = + case compare n m of + LT -> unsafeCoerce SLT + EQ -> unsafeCoerce SEQ + GT -> unsafeCoerce SGT diff --git a/src/Data/Type/Natural/Lemma/Arithmetic.hs b/src/Data/Type/Natural/Lemma/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Lemma/Arithmetic.hs @@ -0,0 +1,295 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} + +module Data.Type.Natural.Lemma.Arithmetic + ( Zero, + One, + S, + sZero, + sOne, + ZeroOrSucc (..), + plusCong, + plusCongR, + plusCongL, + predCong, + Succ, + sS, + sSucc, + Pred, + sPred, + sPred', + succCong, + multCong, + multCongL, + multCongR, + minusCong, + minusCongL, + minusCongR, + succOneCong, + succInj, + succInj', + succNonCyclic, + induction, + plusMinus, + plusMinus', + plusZeroL, + plusSuccL, + plusZeroR, + plusSuccR, + plusComm, + plusAssoc, + multZeroL, + multSuccL, + multSuccL', + multZeroR, + multSuccR, + multComm, + multOneR, + multOneL, + plusMultDistrib, + multPlusDistrib, + minusNilpotent, + multAssoc, + plusEqCancelL, + plusEqCancelR, + succAndPlusOneL, + succAndPlusOneR, + predSucc, + viewNat, + zeroOrSucc, + plusEqZeroL, + plusEqZeroR, + predUnique, + multEqSuccElimL, + multEqSuccElimR, + minusZero, + multEqCancelR, + succPred, + multEqCancelL, + pattern Zero, + pattern Succ, + ) +where + +import Data.Type.Equality + ( gcastWith, + (:~:) (..), + ) +import Data.Type.Natural.Core +import Data.Type.Natural.Lemma.Presburger + ( plusEqZeroL, + plusEqZeroR, + succNonCyclic, + ) +import Data.Void (Void, absurd) +import Proof.Equational (because, start, sym, trans, (===)) + +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 -> SNat k -> n + k :~: m + k +plusCongL Refl _ = Refl + +plusCongR :: SNat 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 -> SNat k -> n * k :~: m * k +multCongL Refl _ = Refl + +multCongR :: SNat 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 -> SNat k -> n - k :~: m - k +minusCongL Refl _ = Refl + +minusCongR :: SNat k -> n :~: m -> k - n :~: k - m +minusCongR _ Refl = Refl + +succOneCong :: Succ 0 :~: 1 +succOneCong = Refl + +succInj :: Succ n :~: Succ m -> n :~: m +succInj Refl = Refl + +succInj' :: proxy n -> proxy' m -> Succ n :~: Succ m -> n :~: m +succInj' _ _ = succInj + +induction :: forall p k. p 0 -> (forall n. SNat n -> p n -> p (S n)) -> SNat k -> p k +induction base step = go + where + go :: SNat m -> p m + go sn = case viewNat sn of + IsZero -> base + IsSucc n -> withKnownNat n $ step n (go n) + +plusMinus :: SNat n -> SNat m -> n + m - m :~: n +plusMinus _ _ = Refl + +plusMinus' :: SNat n -> SNat m -> n + m - n :~: m +plusMinus' n m = + start (n %+ m %- n) + === m %+ n %- n `because` minusCongL (plusComm n m) n + === m `because` plusMinus m n + +plusZeroL :: SNat n -> (0 + n) :~: n +plusZeroL _ = Refl + +plusSuccL :: SNat n -> SNat m -> S n + m :~: S (n + m) +plusSuccL _ _ = Refl + +plusZeroR :: SNat n -> (n + 0) :~: n +plusZeroR _ = Refl + +plusSuccR :: SNat n -> SNat m -> n + S m :~: S (n + m) +plusSuccR _ _ = Refl + +plusComm :: SNat n -> SNat m -> n + m :~: m + n +plusComm _ _ = Refl + +plusAssoc :: + forall n m l. + SNat n -> + SNat m -> + SNat l -> + (n + m) + l :~: n + (m + l) +plusAssoc _ _ _ = Refl + +multZeroL :: SNat n -> 0 * n :~: 0 +multZeroL _ = Refl + +multSuccL :: SNat n -> SNat m -> S n * m :~: n * m + m +multSuccL _ _ = Refl + +multSuccL' :: SNat n -> SNat m -> S n * m :~: n * m + 1 * m +multSuccL' _ _ = Refl + +multZeroR :: SNat n -> n * 0 :~: 0 +multZeroR _ = Refl + +multSuccR :: SNat n -> SNat m -> n * S m :~: n * m + n +multSuccR _ _ = Refl + +multComm :: SNat n -> SNat m -> n * m :~: m * n +multComm _ _ = Refl + +multOneR :: SNat n -> n * 1 :~: n +multOneR _ = Refl + +multOneL :: SNat n -> 1 * n :~: n +multOneL _ = Refl + +plusMultDistrib :: + SNat n -> + SNat m -> + SNat l -> + (n + m) * l :~: (n * l) + (m * l) +plusMultDistrib _ _ _ = Refl + +multPlusDistrib :: + SNat n -> + SNat m -> + SNat l -> + n * (m + l) :~: (n * m) + (n * l) +multPlusDistrib _ _ _ = Refl + +minusNilpotent :: SNat n -> n - n :~: 0 +minusNilpotent _ = Refl + +multAssoc :: + SNat n -> + SNat m -> + SNat l -> + (n * m) * l :~: n * (m * l) +multAssoc _ _ _ = Refl + +plusEqCancelL :: SNat n -> SNat m -> SNat l -> n + m :~: n + l -> m :~: l +plusEqCancelL _ _ _ Refl = Refl + +plusEqCancelR :: forall n m l. SNat n -> SNat m -> SNat 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 :: SNat n -> Succ n :~: 1 + n +succAndPlusOneL _ = Refl + +succAndPlusOneR :: SNat n -> Succ n :~: n + 1 +succAndPlusOneR _ = Refl + +predSucc :: SNat n -> Pred (Succ n) :~: n +predSucc _ = Refl + +zeroOrSucc :: SNat n -> ZeroOrSucc n +zeroOrSucc = viewNat + +predUnique :: SNat n -> SNat m -> Succ n :~: m -> n :~: Pred m +predUnique _ _ Refl = Refl + +minusZero :: SNat n -> n - 0 :~: n +minusZero _ = Refl + +multEqCancelR :: forall n m l. SNat n -> SNat m -> SNat l -> n * Succ l :~: m * Succ l -> n :~: m +multEqCancelR _ _ = go + where + go :: forall k. SNat k -> n * Succ k :~: m * Succ k -> n :~: m + go Zero Refl = Refl + go (Succ n) Refl = gcastWith (go n Refl) Refl + +succPred :: SNat n -> (n :~: 0 -> 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 :: SNat n -> SNat m -> SNat 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 -> SNat (Succ n) -> SNat n +sPred' pxy sn = gcastWith (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn) + +multEqSuccElimL :: + SNat n -> + SNat m -> + SNat l -> + n * m :~: Succ l -> + n :~: Succ (Pred n) +multEqSuccElimL Zero _ l Refl = absurd $ succNonCyclic l Refl +multEqSuccElimL (Succ _) _ _ Refl = Refl + +multEqSuccElimR :: SNat n -> SNat m -> SNat l -> n * m :~: Succ l -> m :~: Succ (Pred m) +multEqSuccElimR _ Zero l Refl = absurd $ succNonCyclic l Refl +multEqSuccElimR _ (Succ _) _ Refl = Refl diff --git a/src/Data/Type/Natural/Lemma/Order.hs b/src/Data/Type/Natural/Lemma/Order.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Lemma/Order.hs @@ -0,0 +1,1054 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module Data.Type.Natural.Lemma.Order + ( DiffNat (..), + LeqView (..), + type (<), + type (), + type (>?), + (%>?), + type (>=), + type (>=?), + (%>=?), + FlipOrdering, + Min, + sMin, + Max, + sMax, + + -- * Lemmas + sFlipOrdering, + coerceLeqL, + coerceLeqR, + sLeqCongL, + sLeqCongR, + sLeqCong, + succDiffNat, + compareCongR, + leqToCmp, + eqlCmpEQ, + eqToRefl, + flipCmpNat, + ltToNeq, + leqNeqToLT, + succLeqToLT, + ltToLeq, + gtToLeq, + congFlipOrdering, + ltToSuccLeq, + cmpZero, + leqToGT, + cmpZero', + zeroNoLT, + ltRightPredSucc, + cmpSucc, + ltSucc, + cmpSuccStepR, + ltSuccLToLT, + leqToLT, + leqZero, + leqSucc, + fromLeqView, + leqViewRefl, + viewLeq, + leqWitness, + leqStep, + leqNeqToSuccLeq, + leqRefl, + leqSuccStepR, + leqSuccStepL, + leqReflexive, + leqTrans, + leqAntisymm, + plusMonotone, + leqZeroElim, + plusMonotoneL, + plusMonotoneR, + plusLeqL, + plusLeqR, + plusCancelLeqR, + plusCancelLeqL, + succLeqZeroAbsurd, + succLeqZeroAbsurd', + succLeqAbsurd, + succLeqAbsurd', + notLeqToLeq, + leqSucc', + leqToMin, + geqToMin, + minComm, + minLeqL, + minLeqR, + minLargest, + leqToMax, + geqToMax, + maxComm, + maxLeqR, + maxLeqL, + maxLeast, + lneqSuccLeq, + lneqReversed, + lneqToLT, + ltToLneq, + lneqZero, + lneqSucc, + succLneqSucc, + lneqRightPredSucc, + lneqSuccStepL, + lneqSuccStepR, + plusStrictMonotone, + maxZeroL, + maxZeroR, + minZeroL, + minZeroR, + minusSucc, + lneqZeroAbsurd, + minusPlus, + minPlusTruncMinus, + truncMinusLeq, + type (-.), + (%-.), + + -- * Various witnesses for orderings + LeqWitness, + (:<:), + Leq (..), + leqRhs, + leqLhs, + + -- ** conversions between lax orders + propToBoolLeq, + boolToPropLeq, + + -- ** conversions between strict orders + propToBoolLt, + boolToPropLt, + ) +where + +import Data.Coerce (coerce) +import Data.Type.Equality (gcastWith, (:~:) (..)) +import Data.Type.Natural.Core +import Data.Type.Natural.Lemma.Arithmetic +import Data.Void (Void, absurd) +import Numeric.Natural (Natural) +import Proof.Equational + ( because, + start, + sym, + trans, + withRefl, + (===), + (=~=), + ) +import Proof.Propositional (IsTrue (..), eliminate, withWitness) + +-------------------------------------------------- + +-- ** Type-level predicate & judgements. + +-------------------------------------------------- + +-- | Comparison via GADTs. +data Leq n m where + ZeroLeq :: SNat m -> Leq 0 m + SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1) + +type LeqWitness n m = IsTrue (n <=? m) + +data a :<: b where + ZeroLtSucc :: 0 :<: (m + 1) + SuccLtSucc :: n :<: m -> (n + 1) :<: (m + 1) + +deriving instance Show (a :<: b) + +-------------------------------------------------- + +-- * Total orderings on natural numbers. + +-------------------------------------------------- +propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m +propToBoolLeq (ZeroLeq _) = Witness +propToBoolLeq (SuccLeqSucc leq) = withWitness (propToBoolLeq leq) Witness +{-# INLINE propToBoolLeq #-} + +boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m +boolToPropLeq Zero m = ZeroLeq m +boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m +boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness + +leqRhs :: Leq n m -> SNat m +leqRhs (ZeroLeq m) = m +leqRhs (SuccLeqSucc leq) = sSucc $ leqRhs leq + +leqLhs :: Leq n m -> SNat n +leqLhs (ZeroLeq _) = Zero +leqLhs (SuccLeqSucc leq) = sSucc $ leqLhs leq + +propToBoolLt :: n :<: m -> IsTrue (n SNat n -> SNat m -> n :<: m +boolToPropLt Zero (Succ _) = ZeroLtSucc +boolToPropLt (Succ _) Zero = eliminate (Refl :: 0 :~: 1) +boolToPropLt (Succ n) (Succ m) = SuccLtSucc (boolToPropLt n m) + +type Min n m = MinAux (n <=? m) n m + +sMin :: SNat n -> SNat m -> SNat (Min n m) +sMin = coerce $ min @Natural + +sMax :: SNat n -> SNat m -> SNat (Max n m) +sMax = coerce $ max @Natural + +type family MinAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where + MinAux 'True n _ = n + MinAux 'False _ m = m + +type Max n m = MaxAux (n >=? m) n m + +type family MaxAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where + MaxAux 'True n _ = n + MaxAux 'False _ m = m + +infix 4 =?, >=, >, >? + +type n SNat m -> SBool (n =? m = m <=? n + +(%>=?) :: SNat n -> SNat m -> SBool (n >=? m) +(%>=?) = flip (%<=?) + +type n >= m = (n >=? m) ~ 'True + +type n >? m = m ?) :: SNat n -> SNat m -> SBool (n >? m) +(%>?) = flip (% m = (n >? m) ~ 'True + +infix 4 %>?, %=? + +data LeqView n m where + LeqZero :: SNat n -> LeqView 0 n + LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m) + +data DiffNat n m where + DiffNat :: SNat n -> SNat m -> DiffNat n (n + m) + +newtype LeqWitPf n = LeqWitPf {leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m} + +newtype LeqStepPf n = LeqStepPf {leqStepPf :: forall m l. SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)} + +succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m) +succDiffNat _ _ (DiffNat n m) = gcastWith (plusSuccL n m) $ DiffNat (sSucc n) m + +-- | Since 1.0.0.0 (type changed) +coerceLeqL :: + forall n m l. + n :~: m -> + SNat l -> + IsTrue (n <=? l) -> + IsTrue (m <=? l) +coerceLeqL Refl _ Witness = Witness + +-- | Since 1.0.0.0 (type changed) +coerceLeqR :: + forall n m l. + SNat l -> + n :~: m -> + IsTrue (l <=? n) -> + IsTrue (l <=? m) +coerceLeqR _ Refl Witness = Witness + +compareCongR :: SNat a -> b :~: c -> CmpNat a b :~: CmpNat a c +compareCongR _ Refl = Refl + +sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d) +sLeqCong Refl Refl = Refl + +sLeqCongL :: a :~: b -> SNat c -> (a <= c) :~: (b <= c) +sLeqCongL Refl _ = Refl + +sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c) +sLeqCongR _ Refl = Refl + +newtype LTSucc n = LTSucc {proofLTSucc :: CmpNat n (Succ n) :~: 'LT} + +newtype CmpSuccStepR n = CmpSuccStepR + { proofCmpSuccStepR :: + forall m. + SNat m -> + CmpNat n m :~: 'LT -> + CmpNat n (Succ m) :~: 'LT + } + +newtype LeqViewRefl n = LeqViewRefl {proofLeqViewRefl :: LeqView n n} + +leqToCmp :: + SNat a -> + SNat b -> + IsTrue (a <=? b) -> + Either (a :~: b) (CmpNat a b :~: 'LT) +leqToCmp n m Witness = + case n %~ m of + Equal -> Left Refl + NonEqual -> Right Refl + +eqlCmpEQ :: SNat a -> SNat b -> a :~: b -> CmpNat a b :~: 'EQ +eqlCmpEQ _ _ Refl = Refl + +eqToRefl :: SNat a -> SNat b -> CmpNat a b :~: 'EQ -> a :~: b +eqToRefl _ _ Refl = Refl + +flipCmpNat :: + SNat a -> + SNat b -> + FlipOrdering (CmpNat a b) :~: CmpNat b a +flipCmpNat n m = case sCmpNat n m of + SGT -> Refl + SLT -> Refl + SEQ -> Refl + +ltToNeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'LT -> + a :~: b -> + Void +ltToNeq a b aLTb aEQb = + eliminate $ + start SLT + === sCmpNat a b `because` sym aLTb + === SEQ `because` eqlCmpEQ a b aEQb + +leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> (a :~: b -> Void) -> CmpNat a b :~: 'LT +leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb + +succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat 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 :: + SNat a -> + SNat b -> + CmpNat a b :~: 'LT -> + IsTrue (a <=? b) +ltToLeq _ _ Refl = Witness + +gtToLeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'GT -> + IsTrue (b <=? a) +gtToLeq n m nGTm = + ltToLeq m n $ + start (sCmpNat m n) === sFlipOrdering (sCmpNat n m) `because` sym (flipCmpNat n m) + === sFlipOrdering SGT `because` congFlipOrdering nGTm + =~= SLT + +congFlipOrdering :: + a :~: b -> FlipOrdering a :~: FlipOrdering b +congFlipOrdering Refl = Refl + +ltToSuccLeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'LT -> + IsTrue (Succ a <=? b) +ltToSuccLeq n m nLTm = + leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm) + +cmpZero :: SNat a -> CmpNat 0 (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 :: + SNat a -> + SNat b -> + IsTrue (Succ b <=? a) -> + CmpNat a b :~: 'GT +leqToGT a b sbLEQa = + start (sCmpNat a b) + === sFlipOrdering (sCmpNat b a) `because` sym (flipCmpNat b a) + === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa) + =~= SGT + +cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT) +cmpZero' n = + case zeroOrSucc n of + IsZero -> Left $ eqlCmpEQ sZero n Refl + IsSucc n' -> Right $ cmpZero n' + +zeroNoLT :: SNat a -> CmpNat a 0 :~: 'LT -> Void +zeroNoLT n eql = + case cmpZero' n of + Left cmp0nEQ -> + eliminate $ + start SGT + =~= sFlipOrdering SLT + === sFlipOrdering (sCmpNat n sZero) `because` congFlipOrdering (sym eql) + === sCmpNat sZero n `because` flipCmpNat n sZero + === SEQ `because` cmp0nEQ + Right cmp0nLT -> + eliminate $ + start SGT + =~= sFlipOrdering SLT + === sFlipOrdering (sCmpNat n sZero) `because` congFlipOrdering (sym eql) + === sCmpNat sZero n `because` flipCmpNat n sZero + === SLT `because` cmp0nLT + +ltRightPredSucc :: SNat a -> SNat b -> CmpNat 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 :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m) +cmpSucc n m = + case sCmpNat 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 $ flipCmpNat 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 (sCmpNat n m) + =~= SGT + =~= sFlipOrdering SLT + === sFlipOrdering (sCmpNat (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf) + === sCmpNat (sSucc n) (sSucc m) `because` flipCmpNat (sSucc m) (sSucc n) + +ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT +ltSucc = proofLTSucc . induction base step + where + base :: LTSucc 0 + base = LTSucc $ cmpZero (sZero :: SNat 0) + + step :: SNat n -> LTSucc n -> LTSucc (Succ n) + step n (LTSucc ih) = + LTSucc $ + start (sCmpNat (sSucc n) (sSucc (sSucc n))) + === sCmpNat n (sSucc n) `because` sym (cmpSucc n (sSucc n)) + === SLT `because` ih + +cmpSuccStepR :: + SNat n -> + SNat m -> + CmpNat n m :~: 'LT -> + CmpNat n (Succ m) :~: 'LT +cmpSuccStepR = proofCmpSuccStepR . induction base step + where + base :: CmpSuccStepR 0 + base = CmpSuccStepR $ \m _ -> cmpZero m + + step :: SNat n -> 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 (sCmpNat (sSucc n) (sSucc m)) + =~= sCmpNat (sSucc n) (sSucc (sSucc m')) + === sCmpNat n (sSucc m') `because` sym (cmpSucc n (sSucc m')) + === SLT `because` ih m' nLTm' + +ltSuccLToLT :: + SNat n -> + SNat m -> + CmpNat (Succ n) m :~: 'LT -> + CmpNat 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 (sCmpNat n (sSucc m')) + === SLT `because` cmpSuccStepR n m' nLTm + +leqToLT :: + SNat a -> + SNat b -> + IsTrue (Succ a <=? b) -> + CmpNat a b :~: 'LT +leqToLT n m snLEQm = + case leqToCmp (sSucc n) m snLEQm of + Left eql -> + withRefl eql $ + start (sCmpNat n m) + =~= sCmpNat n (sSucc n) + === SLT `because` ltSucc n + Right nLTm -> ltSuccLToLT n m nLTm + +leqZero :: SNat n -> IsTrue (0 <=? n) +leqZero _ = Witness + +leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m) +leqSucc _ _ Witness = Witness + +fromLeqView :: LeqView n m -> IsTrue (n <=? m) +fromLeqView (LeqZero n) = leqZero n +fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm + +leqViewRefl :: SNat n -> LeqView n n +leqViewRefl = proofLeqViewRefl . induction base step + where + base :: LeqViewRefl 0 + base = LeqViewRefl $ LeqZero sZero + step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n) + step n (LeqViewRefl nLEQn) = + LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) + +viewLeq :: forall n m. SNat n -> SNat 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 gcastWith (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' + +leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m +leqWitness = leqWitPf . induction base step + where + base :: LeqWitPf 0 + base = LeqWitPf $ \sm _ -> gcastWith (plusZeroL sm) $ DiffNat sZero sm + + step :: SNat n -> LeqWitPf n -> LeqWitPf (Succ n) + step (n :: SNat n) (LeqWitPf ih) = LeqWitPf $ \m snLEQm -> + case viewLeq (sSucc n) m snLEQm of + LeqZero _ -> absurd $ succNonCyclic n Refl + LeqSucc (_ :: SNat n') pm nLEQpm -> + succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm + +leqStep :: SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m) +leqStep = leqStepPf . induction base step + where + base :: LeqStepPf 0 + base = LeqStepPf $ \k _ _ -> leqZero k + + step :: SNat n -> 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 :: SNat n -> SNat 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 :: SNat n -> IsTrue (n <=? n) +leqRefl sn = leqStep sn sn sZero (plusZeroR sn) + +leqSuccStepR :: SNat n -> SNat 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 :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m) +leqSuccStepL n m snLEQm = + leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm + +leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m) +leqReflexive n _ Refl = leqRefl n + +leqTrans :: SNat n -> SNat m -> SNat 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 :: SNat n -> SNat 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 :: + SNat n -> + SNat m -> + SNat l -> + SNat 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 :: SNat n -> IsTrue (n <=? 0) -> n :~: 0 +leqZeroElim n nLE0 = + case viewLeq n sZero nLE0 of + LeqZero _ -> Refl + LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl + +plusMonotoneL :: + SNat n -> + SNat m -> + SNat l -> + IsTrue (n <=? m) -> + IsTrue ((n + l) <=? (m + l)) +plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l) + +plusMonotoneR :: + SNat n -> + SNat m -> + SNat l -> + IsTrue (m <=? l) -> + IsTrue ((n + m) <=? (n + l)) +plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq + +plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m)) +plusLeqL n m = leqStep n (n %+ m) m Refl + +plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m)) +plusLeqR n m = leqStep m (n %+ m) n $ plusComm m n + +plusCancelLeqR :: + SNat n -> + SNat m -> + SNat 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 :: + SNat n -> + SNat m -> + SNat 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 :: SNat n -> IsTrue (S n <=? 0) -> Void +succLeqZeroAbsurd n leq = + succNonCyclic n (leqZeroElim (sSucc n) leq) + +succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False +succLeqZeroAbsurd' n = + case sSucc n %<=? sZero of + STrue -> absurd $ succLeqZeroAbsurd n Witness + SFalse -> Refl + +succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void +succLeqAbsurd n snLEQn = + eliminate $ + start SLT + === sCmpNat n n `because` sym (succLeqToLT n n snLEQn) + === SEQ `because` eqlCmpEQ n n Refl + +succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False +succLeqAbsurd' n = + case sSucc n %<=? n of + STrue -> absurd $ succLeqAbsurd n Witness + SFalse -> Refl + +notLeqToLeq :: ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n) +notLeqToLeq n m = + case sCmpNat n m of + SLT -> eliminate $ ltToLeq n m Refl + SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl + SGT -> gtToLeq n m Refl + +leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m) +leqSucc' _ _ = Refl + +leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n +leqToMin _ _ Witness = Refl + +geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m +geqToMin n m Witness = + case n %<=? m of + SFalse -> Refl + STrue -> Refl + +minComm :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: + SNat l -> + SNat n -> + SNat m -> + IsTrue (l <=? n) -> + IsTrue (l <=? m) -> + IsTrue (l <=? Min n m) +minLargest l n m lLEQn lLEQm = + withKnownNat l $ + withKnownNat n $ + withKnownNat m $ + withKnownNat (sMin n m) $ + case n %<=? m of + STrue -> lLEQn + SFalse -> lLEQm + +leqToMax :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: + SNat l -> + SNat n -> + SNat m -> + IsTrue (n <=? l) -> + IsTrue (m <=? l) -> + IsTrue (Max n m <=? l) +maxLeast l n m lLEQn lLEQm = + withKnownNat l $ + withKnownNat n $ + withKnownNat m $ + withKnownNat (sMax n m) $ + case n %>=? m of + STrue -> lLEQn + SFalse -> lLEQm + +lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m) +lneqSuccLeq _ _ = Refl + +lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n) +lneqReversed _ _ = Refl + +lneqToLT :: + SNat n -> + SNat m -> + IsTrue (n + CmpNat n m :~: 'LT +lneqToLT n m nLNEm = + succLeqToLT n m $ gcastWith (lneqSuccLeq n m) nLNEm + +ltToLneq :: + SNat n -> + SNat m -> + CmpNat n m :~: 'LT -> + IsTrue (n IsTrue (0 IsTrue (n + SNat m -> + (n + SNat m -> + IsTrue (n + m :~: Succ (Pred m) +lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm + +lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n IsTrue (n SNat m -> IsTrue (n IsTrue (n + SNat m -> + SNat l -> + SNat k -> + IsTrue (n + IsTrue (l + IsTrue ((n + l) Max 0 n :~: n +maxZeroL n = leqToMax sZero n (leqZero n) + +maxZeroR :: SNat n -> Max n 0 :~: n +maxZeroR n = geqToMax n sZero (leqZero n) + +minZeroL :: SNat n -> Min 0 n :~: 0 +minZeroL n = leqToMin sZero n (leqZero n) + +minZeroR :: SNat n -> Min n 0 :~: 0 +minZeroR n = geqToMin n sZero (leqZero n) + +minusSucc :: SNat n -> SNat 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) + +lneqZeroAbsurd :: SNat n -> IsTrue (n Void +lneqZeroAbsurd n leq = + succLeqZeroAbsurd n (gcastWith (lneqSuccLeq n sZero) leq) + +minusPlus :: + forall n m. + SNat n -> + SNat m -> + IsTrue (m <=? n) -> + n - m + m :~: n +minusPlus n m mLEQn = + case leqWitness m n mLEQn of + DiffNat _ k -> + start (n %- m %+ m) + =~= m %+ k %- m %+ m + === k %+ m %- m %+ m `because` plusCongL (minusCongL (plusComm m k) m) m + === k %+ m `because` plusCongL (plusMinus k m) m + === m %+ k `because` plusComm k m + =~= n + +-- | Natural subtraction, truncated to zero if m > n. +type n -. m = Subt n m (m <=? n) + +type family Subt n m (b :: Bool) where + Subt n m 'True = n - m + Subt n m 'False = 0 + +infixl 6 -. + +(%-.) :: SNat n -> SNat m -> SNat (n -. m) +n %-. m = + case m %<=? n of + STrue -> n %- m + SFalse -> sZero + +minPlusTruncMinus :: + SNat n -> + SNat m -> + Min n m + (n -. m) :~: n +minPlusTruncMinus n m = + case m %<=? n of + STrue -> + start (sMin n m %+ (n %-. m)) + === m %+ (n %-. m) `because` plusCongL (geqToMin n m Witness) (n %-. m) + =~= m %+ (n %- m) + === (n %- m) %+ m `because` plusComm m (n %- m) + === n `because` minusPlus n m Witness + SFalse -> + start (sMin n m %+ (n %-. m)) + =~= sMin n m %+ sZero + === sMin n m `because` plusZeroR (sMin n m) + === n `because` leqToMin n m (notLeqToLeq m n) + +truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n) +truncMinusLeq n m = + case m %<=? n of + STrue -> leqStep (n %-. m) n m $ minusPlus n m Witness + SFalse -> leqZero n diff --git a/src/Data/Type/Natural/Lemma/Presburger.hs b/src/Data/Type/Natural/Lemma/Presburger.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Lemma/Presburger.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module Data.Type.Natural.Lemma.Presburger where + +import Data.Type.Equality +import Data.Type.Natural.Core +import Data.Void + +plusEqZeroL :: SNat n -> SNat m -> n + m :~: 0 -> n :~: 0 +plusEqZeroL _ _ Refl = Refl + +plusEqZeroR :: SNat n -> SNat m -> n + m :~: 0 -> m :~: 0 +plusEqZeroR _ _ Refl = Refl + +succNonCyclic :: SNat n -> Succ n :~: 0 -> Void +succNonCyclic Zero r = case r of +succNonCyclic (Succ n) Refl = succNonCyclic n Refl diff --git a/src/Data/Type/Natural/Presburger/MinMaxSolver.hs b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs @@ -0,0 +1,61 @@ +{- | This module provides a variant of `ghc-typelits-presburger`, + which can be also solve symbols added in this package, such as + @Min@, @Max@, @<@, @>@, and @>=@. +-} +module Data.Type.Natural.Presburger.MinMaxSolver (plugin) where + +import Control.Monad (mzero) +import GHC.TypeLits.Presburger.Compat (lookupModule) +import GHC.TypeLits.Presburger.Types +import GhcPlugins + ( Plugin, + fsLit, + mkModuleName, + mkTcOcc, + splitTyConApp_maybe, + ) +import TcPluginM + +plugin :: Plugin +plugin = + pluginWith $ + (<>) <$> defaultTranslation <*> genTypeNatsTranslation + +genTypeNatsTranslation :: TcPluginM Translation +genTypeNatsTranslation = do + orderMod <- lookupModule (mkModuleName "Data.Type.Natural.Lemma.Order") (fsLit "type-natural") + singNatLt <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "=?") + singNatGt <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc ">?") + + singNatLtProp <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "<") + singNatGeqProp <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc ">=") + singNatGtProp <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc ">") + + singMin <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Min") + singMax <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Max") + caseMinAux <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "MinAux") + caseMaxAux <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "MaxAux") + return + mempty + { natGeqBool = [singNatGeq] + , natLtBool = [singNatLt] + , natGtBool = [singNatGt] + , natMin = [singMin] + , natMax = [singMax] + , parsePred = \toE ty -> + case splitTyConApp_maybe ty of + Just (con, [l, r]) + | con == singNatLtProp -> (:<) <$> toE l <*> toE r + | con == singNatGtProp -> (:>) <$> toE l <*> toE r + | con == singNatGeqProp -> (:>=) <$> toE l <*> toE r + _ -> mzero + , parseExpr = \toE ty -> + case splitTyConApp_maybe ty of + Just (con, [_, n, m]) + | con == caseMinAux -> + Min <$> toE n <*> toE m + | con == caseMaxAux -> + Max <$> toE n <*> toE m + _ -> mzero + } diff --git a/src/Data/Type/Natural/Utils.hs b/src/Data/Type/Natural/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Utils.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Type.Natural.Utils where + +import Data.Type.Equality (type (:~:) (..)) +import Unsafe.Coerce (unsafeCoerce) + +trustMe :: x :~: y +trustMe = unsafeCoerce (Refl @()) diff --git a/src/Data/Type/Ordinal.hs b/src/Data/Type/Ordinal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Ordinal.hs @@ -0,0 +1,338 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +{- | Set-theoretic ordinals for built-in type-level naturals + + Since 1.0.0.0 +-} +module Data.Type.Ordinal + ( -- * Data-types + Ordinal (..), + pattern OZ, + pattern OS, + + -- * Quasi Quoter + -- $quasiquotes + od, + + -- * Conversion from cardinals to ordinals. + sNatToOrd', + sNatToOrd, + ordToNatural, + unsafeNaturalToOrd', + unsafeNaturalToOrd, + reallyUnsafeNaturalToOrd, + naturalToOrd, + naturalToOrd', + ordToSNat, + inclusion, + inclusion', + + -- * Ordinal arithmetics + (@+), + enumOrdinal, + + -- * Elimination rules for @'Ordinal' 'Z'@. + absurdOrd, + vacuousOrd, + ) +where + +import Data.Maybe (fromMaybe) +import Data.Ord (comparing) +import Data.Proxy (Proxy (Proxy)) +import Data.Type.Equality +import Data.Type.Natural +import Data.Type.Natural.Core (SNat (..)) +import Data.Typeable (Typeable) +import Language.Haskell.TH.Quote +import Numeric.Natural +import Unsafe.Coerce + +{- | Set-theoretic (finite) ordinals: + + > n = {0, 1, ..., n-1} + + So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. + + Since 1.0.0.0 +-} +data Ordinal (n :: Nat) where + OLt :: (n < m) => SNat (n :: Nat) -> Ordinal m + +{-# COMPLETE OLt #-} + +fromOLt :: + forall n m. + ((Succ n < Succ m), KnownNat m) => + SNat (n :: Nat) -> + Ordinal m +fromOLt n = OLt n + +{- | Pattern synonym representing the 0-th ordinal. + + Since 1.0.0.0 +-} +pattern OZ :: forall (n :: Nat). (0 < n) => Ordinal n +pattern OZ <- OLt Zero where OZ = OLt sZero + +{- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. + + Since 1.0.0.0 +-} +pattern OS :: forall (t :: Nat). (KnownNat t) => Ordinal t -> Ordinal (Succ t) +pattern OS n <- + OLt (Succ (fromOLt -> n)) + where + OS o = succOrd o + +-- | Since 1.0.0.0 +deriving instance Typeable Ordinal + +{- | Class synonym for Peano numerals with ordinals. + + Since 1.0.0.0 +-} +instance (KnownNat n) => Num (Ordinal n) where + _ + _ = error "Finite ordinal is not closed under addition." + _ - _ = error "Ordinal subtraction is not defined" + negate _ = error "There are no negative oridnals!" + _ * _ = error "Finite ordinal is not closed under multiplication" + abs = id + signum = error "What does Ordinal sign mean?" + fromInteger = unsafeFromNatural' . fromIntegral + +unsafeFromNatural' :: forall n. KnownNat n => Natural -> Ordinal n +unsafeFromNatural' k = withSNat k $ \sk -> + case sk % OLt sk + SFalse -> error $ "Index out of bounds: " ++ show (k, natVal @n Proxy) + +-- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n)) +instance + (KnownNat n) => + Show (Ordinal (n :: Nat)) + where + showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToNatural o) . showString " / " . showsPrec d (toNatural (sNat :: SNat n))) + +instance Eq (Ordinal (n :: Nat)) where + o == o' = ordToNatural o == ordToNatural o' + +instance Ord (Ordinal (n :: Nat)) where + compare = comparing ordToNatural + +instance + (KnownNat n) => + Enum (Ordinal (n :: Nat)) + where + fromEnum = fromEnum . ordToNatural + toEnum = unsafeFromNatural' . fromIntegral + enumFrom = enumFromOrd + enumFromTo = enumFromToOrd + +-- | Since 1.0.0.0 (type changed) +enumFromToOrd :: + forall (n :: Nat). + (KnownNat n) => + Ordinal n -> + Ordinal n -> + [Ordinal n] +enumFromToOrd ok ol = + map + (reallyUnsafeNaturalToOrd $ sNat @n) + [ordToNatural ok .. ordToNatural ol] + +-- | Since 1.0.0.0 (type changed) +enumFromOrd :: + forall (n :: Nat). + (KnownNat n) => + Ordinal n -> + [Ordinal n] +enumFromOrd ord = + map + (reallyUnsafeNaturalToOrd Proxy) + [ordToNatural ord .. natVal @n Proxy - 1] + +-- | Enumerate all @'Ordinal'@s less than @n@. +enumOrdinal :: SNat (n :: Nat) -> [Ordinal n] +enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. toNatural sn - 1] + +-- | Since 1.0.0.0(type changed) +succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n) +succOrd (OLt n) = + OLt (sSucc n) +{-# INLINE succOrd #-} + +instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where + minBound = OLt sZero + + maxBound = OLt $ sNat @(n - 1) + +{- | Converts @'Natural'@s into @'Ordinal n'@. + If the given natural is greater or equal to @n@, raises exception. + + Since 1.0.0.0 +-} +unsafeNaturalToOrd :: + forall (n :: Nat). + (KnownNat n) => + Natural -> + Ordinal n +unsafeNaturalToOrd k = + fromMaybe (error "unsafeNaturalToOrd Out of bound") $ + naturalToOrd k + +-- | Since 1.0.0.0 +unsafeNaturalToOrd' :: + forall proxy (n :: Nat). + (KnownNat n) => + proxy n -> + Natural -> + Ordinal n +unsafeNaturalToOrd' _ = unsafeNaturalToOrd + +{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-} + +{- | Converts @'Natural'@s into @'Ordinal' n@, WITHOUT any boundary check. + This function may easily violate type-safety. Use with care! +-} +reallyUnsafeNaturalToOrd :: + forall pxy (n :: Nat). + (KnownNat n) => + pxy -> + Natural -> + Ordinal n +reallyUnsafeNaturalToOrd _ k = + withSNat k $ \(sk :: SNat k) -> + gcastWith (unsafeCoerce (Refl :: () :~: ()) :: (k SNat (n :: Nat) -> SNat m -> Ordinal n +sNatToOrd' _ = OLt +{-# INLINE sNatToOrd' #-} + +-- | 'sNatToOrd'' with @n@ inferred. +sNatToOrd :: (KnownNat n, m < n) => SNat m -> Ordinal n +sNatToOrd = sNatToOrd' sNat + +-- | Since 1.0.0.0 +naturalToOrd :: + forall n. + (KnownNat n) => + Natural -> + Maybe (Ordinal (n :: Nat)) +naturalToOrd = naturalToOrd' (sNat :: SNat n) + +naturalToOrd' :: + SNat (n :: Nat) -> + Natural -> + Maybe (Ordinal n) +naturalToOrd' sn k = withSNat k $ \(sk :: SNat pk) -> + case sk % Just (OLt sk) + _ -> Nothing + +{- | Convert @Ordinal n@ into monomorphic @SNat@ + + Since 1.0.0.0 +-} +ordToSNat :: Ordinal (n :: Nat) -> SomeSNat +ordToSNat (OLt n) = withKnownNat n $ SomeSNat n +{-# INLINE ordToSNat #-} + +ordToNatural :: + Ordinal (n :: Nat) -> + Natural +ordToNatural (OLt n) = toNatural n + +{- | Inclusion function for ordinals. + + Since 1.0.0.0(constraint was weakened since last released) +-} +inclusion' :: (n <= m) => SNat m -> Ordinal n -> Ordinal m +inclusion' _ = unsafeCoerce +{-# INLINE inclusion' #-} + +{- | Inclusion function for ordinals with codomain inferred. + + Since 1.0.0.0(constraint was weakened since last released) +-} +inclusion :: (n <= m) => Ordinal n -> Ordinal m +inclusion (OLt a) = OLt a +{-# INLINE inclusion #-} + +{- | Ordinal addition. + + Since 1.0.0.0(type changed) +-} +(@+) :: + forall (n :: Nat) m. + (KnownNat n, KnownNat m) => + Ordinal n -> + Ordinal m -> + Ordinal (n + m) +OLt k @+ OLt l = OLt $ k %+ l + +{- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. + + Since 1.0.0.0 +-} +absurdOrd :: Ordinal 0 -> a +absurdOrd (OLt _) = case (Refl :: 0 :~: 1) of + +{- | @'absurdOrd'@ for value in 'Functor'. + + Since 1.0.0.0 +-} +vacuousOrd :: (Functor f) => f (Ordinal 0) -> f a +vacuousOrd = fmap absurdOrd + +{- $quasiquotes #quasiquoters# + + This section provides QuasiQuoter and general generator for ordinals. + Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT + checks boundary; with @'od'@, we can use literal with + boundary check. + For example, with @-XQuasiQuotes@ language extension enabled, + @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, + whilst @12 :: Ordinal 1@ compiles but raises run-time error. + So, to enforce correctness, we recommend to use these quoters + instead of bare @'Num'@ numerals. +-} + +-- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@. +od :: QuasiQuoter +od = + QuasiQuoter + { quoteExp = \s -> [|OLt $(quoteExp snat s)|] + , quoteType = error "No type quoter for Ordinals" + , quotePat = \s -> [p|OLt ((%~ $(quoteExp snat s)) -> Equal)|] + , quoteDec = error "No declaration quoter for Ordinals" + } + +-- >>> 42 diff --git a/src/Data/Type/Ordinal/Builtin.hs b/src/Data/Type/Ordinal/Builtin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Ordinal/Builtin.hs @@ -0,0 +1,7 @@ +module Data.Type.Ordinal.Builtin + {-# DEPRECATED "Use Data.Type.Ordinal instead" #-} + ( module Data.Type.Ordinal, + ) +where + +import Data.Type.Ordinal diff --git a/tests/Data/Type/Natural/Presburger/Cases.hs b/tests/Data/Type/Natural/Presburger/Cases.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/Natural/Presburger/Cases.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-} + +module Data.Type.Natural.Presburger.Cases where + +import Data.Proxy (Proxy (Proxy)) +import Data.Type.Equality +import Data.Type.Natural +import GHC.TypeNats + +minFlip :: n <= m => p n -> q m -> Min m n :~: n +minFlip _ _ = Refl + +maxFlip :: n <= m => p n -> q m -> Max m n :~: m +maxFlip _ _ = Refl + +minComm :: q m -> p n -> Min n m :~: Min m n +minComm _ _ = Refl + +maxComm :: q m -> p n -> Max n m :~: Max m n +maxComm _ _ = Refl + +falsity :: n <= m => p n -> q m -> Min n m :~: m +falsity = Refl diff --git a/tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs b/tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Type.Natural.Presburger.MinMaxSolverSpec where + +import Control.Exception +import Control.Monad +import Data.Type.Equality +import Data.Type.Natural +import Data.Type.Natural.Presburger.Cases +import Shared +import Test.QuickCheck (ioProperty) +import Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.QuickCheck +import Unsafe.Coerce (unsafeCoerce) + +test_MinMaxSolver :: TestTree +test_MinMaxSolver = + testGroup + "Data.Type.Natural.Presburger.MinMaxSolver" + [ testProperty @(SomeLeq -> Property) "rejects errornousInputs" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ falsity n m + case eith of + Left {} -> pure True + Right {} -> pure False + , testProperty @(SomeLeq -> Property) "minFlip" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ minFlip n m + case eith of + Left {} -> pure False + Right {} -> pure True + , testProperty @(SomeLeq -> Property) "maxFlip" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ maxFlip n m + case eith of + Left {} -> pure False + Right {} -> pure True + , testProperty @(SomeLeq -> Property) "maxComm" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ maxComm n m + case eith of + Left {} -> pure False + Right {} -> pure True + , testProperty @(SomeLeq -> Property) "minComm" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ minComm n m + case eith of + Left {} -> pure False + Right {} -> pure True + ] + +data SomeLeq where + SomeLeq :: n <= m => SNat n -> SNat m -> SomeLeq + +deriving instance Show SomeLeq + +instance Arbitrary SomeLeq where + arbitrary = do + n <- arbitrary + dn <- arbitrary + withSNat n $ + withSNat (n + dn) $ \(sn :: SNat n) (sm :: SNat m) -> + gcastWith (unsafeCoerce (Refl @()) :: (n <=? m) :~: 'True) $ + pure (SomeLeq sn sm) diff --git a/tests/Data/Type/NaturalSpec.hs b/tests/Data/Type/NaturalSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/NaturalSpec.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Type.NaturalSpec where + +import Data.Type.Natural +import Data.Type.NaturalSpec.TH +import Math.NumberTheory.Logarithms (naturalLog2, naturalLogBase) +import Numeric.Natural +import GHC.TypeNats +import Shared +import Test.Tasty +import Test.Tasty.QuickCheck +import Test.QuickCheck +import Control.Monad (join) + +test_arith :: TestTree +test_arith = + testGroup + "Arithmetic operations on singletons behaves correctly" + [ testProperty "(+), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + toNatural (n %+ m) === (natVal n + natVal m) + , $(testBinary "(+)" ''(+) '(%+)) + , testProperty "(-), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + disjoin + [ natVal n < natVal m .&&. toNatural (m %- n) === (natVal m - natVal n) + , toNatural (n %- m) === (natVal n - natVal m) + ] + , $(testBinaryP (>=) "(-)" ''(-) '(%-)) + , testProperty "(*), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + toNatural (n %* m) === (natVal n * natVal m) + , $(testBinary "(*)" ''(*) '(%*)) + , testProperty "Div, compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + label "divide by zero" (natVal m === 0) + .||. toNatural (n `sDiv` m) === (natVal n `div` natVal m) + , $(testBinaryP (const $ (/= 0)) "Div" ''Div 'sDiv) + , testProperty "Mod, compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + label "divide by zero" (natVal m === 0) + .||. toNatural (n `sMod` m) === (natVal n `mod` natVal m) + , $(testBinaryP (const $ (/= 0)) "Mod" ''Mod 'sMod) + , testProperty "(^), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + toNatural (n %^ m) === (natVal n ^ natVal m) + , $(testBinaryP (\a b -> a /= 0 && b /= 0) "(^)" ''(^) '(%^)) + , testProperty "(-.), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + toNatural (n %-. m) === (if natVal n < natVal m then 0 else natVal n - natVal m) + , $(testBinary "(-.)" ''(-.) '(%-.)) + , testProperty "Log2" $ \(SomeSNat n) -> + tabulateDigits [natVal n] $ + label "undefined" (natVal n === 0) + .||. toNatural (sLog2 n) === fromIntegral (naturalLog2 (natVal n)) + , $(testUnary False "Log2" ''Log2 'sLog2) + , testProperty "succ" $ \(SomeSNat n) -> + tabulateDigits [natVal n] $ + toNatural (sSucc n) === succ (natVal n) + , $(testUnary True "Succ" ''Succ 'sSucc) + , testProperty "pred" $ \(SomeSNat n) -> + tabulateDigits [natVal n] $ + label "undefiend" (natVal n === 0) + .||. toNatural (sPred n) === pred (natVal n) + , $(testUnary False "Pred" ''Pred 'sPred) + ] + +demoteBool :: SBool b -> Bool +demoteBool SFalse = False +demoteBool STrue = True + +demoteOrdering :: SOrdering sord -> Ordering +demoteOrdering SLT = LT +demoteOrdering SEQ = EQ +demoteOrdering SGT = GT + +test_order :: TestTree +test_order = + testGroup + "Order operations on singletons coincides with expression-leven ops" + [ testProperty "(<=?)" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %<=? m) === (natVal n <= natVal m) + , $(testBinary "(<=?)" ''(<=?) '(%<=?)) + , testProperty "( + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %=?)" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %>=? m) === (natVal n >= natVal m) + , $(testBinary "(>=?)" ''(>=?) '(%>=?)) + , testProperty "(>?)" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %>? m) === (natVal n > natVal m) + , $(testBinary "(>?)" ''(>?) '(%>?)) + , testProperty "sCmpNat" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteOrdering (n `sCmpNat` m) === compare (natVal n) (natVal m) + , $(testBinary "CmpNat" ''CmpNat 'sCmpNat) + , testProperty "min" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + toNatural (n `sMin` m) === (natVal n `min` natVal m) + , $(testBinary "min" ''Min 'sMin) + , testProperty "max" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + toNatural (n `sMax` m) === (natVal n `max` natVal m) + , $(testBinary "max" ''Max 'sMax) + ] + +tabulateDigits :: Testable prop => [Natural] -> prop -> Property +tabulateDigits = +#if MIN_VERSION_QuickCheck(2,12,0) + tabulate + "# of input digits" + . map (show . succ . naturalLogBase 10 . (+ 1)) +#else + const property +#endif diff --git a/tests/Data/Type/NaturalSpec/TH.hs b/tests/Data/Type/NaturalSpec/TH.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/NaturalSpec/TH.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Type.NaturalSpec.TH where + +import Data.Type.Natural +import Language.Haskell.TH +import Numeric.Natural +import Shared +import Test.Tasty +import Test.Tasty.HUnit + +allCombs :: [(Integer, Integer)] +allCombs = [(n, m) | n <- range, m <- range] + +range :: [Integer] +range = [0] ++ [50] ++ [63 .. 65] ++ [98, 99, 100, 200] ++ [1024, 1023, 1025] + +testUnary :: Bool -> String -> Name -> Name -> ExpQ +testUnary allowZero label tyName singName = + [|testCase (label ++ ", compared to fixed type-level")|] + `appE` doE + [ noBindS + [| + demote ($(varE singName) (sNat @($tyN))) + @?= demote (sing @($(conT tyName) $tyN)) + |] + | nat <- range + , let tyN = litT $ numTyLit nat + , allowZero || nat /= 0 + ] + +testBinary :: String -> Name -> Name -> ExpQ +testBinary = testBinaryP (const $ const True) + +testBinaryP :: (Integer -> Integer -> Bool) -> String -> Name -> Name -> ExpQ +testBinaryP ok label tyName singName = + [|testCase (label ++ ", compared to fixed type-level")|] + `appE` doE + [ noBindS + [| + demote ($(varE singName) (sNat @($tyL)) (sNat @($tyR))) + @?= demote (sing @($(conT tyName) $tyL $tyR)) + |] + | l <- range + , let tyL = litT $ numTyLit l + , r <- range + , let tyR = litT $ numTyLit r + , ok l r + ] + +-- >>> length allCombs +-- 289 diff --git a/tests/Data/Type/OrdinalSpec.hs b/tests/Data/Type/OrdinalSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/OrdinalSpec.hs @@ -0,0 +1,1 @@ +module Data.Type.OrdinalSpec where diff --git a/tests/Shared.hs b/tests/Shared.hs new file mode 100644 --- /dev/null +++ b/tests/Shared.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Shared where + +import Data.Kind (Type) +import Data.Type.Natural +import Data.Type.Ordinal +import GHC.TypeNats +import Numeric.Natural +import Test.QuickCheck +import Test.QuickCheck.Instances () + +instance (KnownNat n, 0 < n) => Arbitrary (Ordinal n) where + arbitrary = elements $ enumOrdinal sNat + shrink 0 = [] + shrink n = [0 .. pred n] + +instance Arbitrary SomeNat where + arbitrary = sized $ \n -> someNatVal <$> resize n arbitrary + shrink (SomeNat pn) = + someNatVal <$> shrink (natVal pn) + +instance Arbitrary SomeSNat where + arbitrary = sized $ \n -> toSomeSNat <$> resize n arbitrary + shrink (SomeSNat pn) = + toSomeSNat <$> shrink (natVal pn) + +type family Sing = (r :: k -> Type) + +class Demote k where + type Demoted k + type Demoted k = k + demote :: Sing (a :: k) -> Demoted k + +class Known a where + sing :: Sing a + +instance KnownNat n => Known n where + sing = sNat + +instance Known 'True where + sing = STrue + +instance Known 'False where + sing = SFalse + +instance Known 'LT where + sing = SLT + +instance Known 'GT where + sing = SGT + +instance Known 'EQ where + sing = SEQ + +type instance Sing = SNat + +instance Demote Nat where + type Demoted Nat = Natural + demote = toNatural + +type instance Sing = SOrdering + +instance Demote Ordering where + demote SLT = LT + demote SEQ = EQ + demote SGT = GT + +type instance Sing = SBool + +instance Demote Bool where + demote STrue = True + demote SFalse = False diff --git a/tests/test.hs b/tests/test.hs new file mode 100644 --- /dev/null +++ b/tests/test.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-} diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -1,74 +1,97 @@ --- Initial type-natural.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/ +cabal-version: >=1.10 +name: type-natural +version: 1.0.0.0 +license: BSD3 +license-file: LICENSE +copyright: (C) Hiromi ISHII 2013-2014 +maintainer: konn.jinro_at_gmail.com +author: Hiromi ISHII +tested-with: + ghc ==8.4.3 ghc ==8.6.5 ghc ==8.8.3 ghc ==8.10.3 -name: type-natural -version: 0.9.0.0 -synopsis: Type-level natural and proofs of their properties. -description: Type-level natural numbers and proofs of their properties. - . - Version 0.6+ supports __GHC 8+ only__. - . - __Use 0.5.* with ~ GHC 7.10.3__. -homepage: https://github.com/konn/type-natural -license: BSD3 -license-file: LICENSE -author: Hiromi ISHII -maintainer: konn.jinro_at_gmail.com -copyright: (C) Hiromi ISHII 2013-2014 -category: Math -build-type: Simple -cabal-version: >= 1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, - GHC == 8.6.3, GHC == 8.8.3, GHC == 8.10.1 +homepage: https://github.com/konn/type-natural +synopsis: Type-level natural and proofs of their properties. +description: + Type-level natural numbers and proofs of their properties. + . + Version 0.6+ supports __GHC 8+ only__. + . + __Use 0.5.* with ~ GHC 7.10.3__. -source-repository head - Type: git - Location: git://github.com/konn/type-natural.git +category: Math +build-type: Simple +source-repository head + type: git + location: git://github.com/konn/type-natural.git library - ghc-options: -Wall -O2 -fno-warn-orphans - if impl(ghc >= 8.0.0) - ghc-options: -Wno-redundant-constraints + exposed-modules: + Data.Type.Natural + Data.Type.Ordinal + Data.Type.Ordinal.Builtin + Data.Type.Natural.Builtin + Data.Type.Natural.Lemma.Arithmetic + Data.Type.Natural.Lemma.Order + Data.Type.Natural.Presburger.MinMaxSolver - exposed-modules: Data.Type.Natural - , Data.Type.Ordinal - , Data.Type.Ordinal.Builtin - , Data.Type.Ordinal.Peano - , 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.Singleton.Compat - , Data.Type.Natural.Singleton.Compat.TH - build-depends: base == 4.* - , equational-reasoning >= 0.4.1.1 - , template-haskell >= 2.8 - , constraints >= 0.3 - , ghc-typelits-natnormalise >= 0.4 - , singletons >= 2.2 && < 2.8 + hs-source-dirs: src + other-modules: + Data.Type.Natural.Core + Data.Type.Natural.Utils + Data.Type.Natural.Lemma.Presburger - default-language: Haskell2010 - default-extensions: DataKinds - PolyKinds - ConstraintKinds - GADTs - ScopedTypeVariables - TemplateHaskell - TypeFamilies - TypeOperators - MultiParamTypeClasses - UndecidableInstances - FlexibleContexts - FlexibleInstances - if impl(ghc >= 8.6) - default-extensions: NoStarIsType - if impl(ghc >= 8.8) - default-extensions: NoStarIsType, TypeApplications - build-depends: singletons-presburger >= 0.3 && <0.4 - if impl(ghc >= 8.4) - build-depends: ghc-typelits-presburger >= 0.3 && <0.4 - else - build-depends: ghc-typelits-presburger >= 0.2 && <0.3 + default-language: Haskell2010 + default-extensions: + DataKinds PolyKinds ConstraintKinds GADTs ScopedTypeVariables + TemplateHaskell TypeFamilies TypeOperators MultiParamTypeClasses + UndecidableInstances FlexibleContexts FlexibleInstances + + ghc-options: -Wall -O2 -fno-warn-orphans + build-depends: + base ==4.*, + ghc, + equational-reasoning >=0.4.1.1, + template-haskell >=2.8, + constraints >=0.3, + ghc-typelits-natnormalise >=0.4, + ghc-typelits-presburger >=0.5, + ghc-typelits-knownnat -any, + integer-logarithms -any + + if impl(ghc >=8.0.0) + ghc-options: -Wno-redundant-constraints + + if impl(ghc >=8.6) + default-extensions: NoStarIsType + +test-suite type-natural-test + type: exitcode-stdio-1.0 + main-is: test.hs + build-tools: tasty-discover -any + hs-source-dirs: tests + default-language: Haskell2010 + other-modules: + Shared + Data.Type.NaturalSpec + Data.Type.NaturalSpec.TH + Data.Type.Natural.Presburger.MinMaxSolverSpec + Data.Type.Natural.Presburger.Cases + Data.Type.OrdinalSpec + + build-depends: + tasty -any, + QuickCheck -any, + tasty-quickcheck -any, + quickcheck-instances -any, + integer-logarithms -any, + tasty-hunit -any, + tasty-discover -any, + template-haskell -any, + tasty-expected-failure -any, + base -any, + type-natural -any, + equational-reasoning -any + + if impl(ghc >=8.6) + default-extensions: NoStarIsType