type-natural 0.9.0.0 → 1.0.0.0
raw patch · 30 files changed
+2667/−3172 lines, 30 filesdep +QuickCheckdep +ghcdep +ghc-typelits-knownnatdep −singletonsdep −singletons-presburgerdep ~basedep ~equational-reasoningdep ~ghc-typelits-presburger
Dependencies added: QuickCheck, ghc, ghc-typelits-knownnat, integer-logarithms, quickcheck-instances, tasty, tasty-discover, tasty-expected-failure, tasty-hunit, tasty-quickcheck, type-natural
Dependencies removed: singletons, singletons-presburger
Dependency ranges changed: base, equational-reasoning, ghc-typelits-presburger, template-haskell
Files
- Data/Type/Natural.hs +0/−302
- Data/Type/Natural/Builtin.hs +0/−466
- Data/Type/Natural/Class.hs +0/−33
- Data/Type/Natural/Class/Arithmetic.hs +0/−576
- Data/Type/Natural/Class/Order.hs +0/−755
- Data/Type/Natural/Core.hs +0/−79
- Data/Type/Natural/Definitions.hs +0/−148
- Data/Type/Natural/Singleton/Compat.hs +0/−44
- Data/Type/Natural/Singleton/Compat/TH.hs +0/−39
- Data/Type/Ordinal.hs +0/−322
- Data/Type/Ordinal/Builtin.hs +0/−174
- Data/Type/Ordinal/Peano.hs +0/−167
- src/Data/Type/Natural.hs +168/−0
- src/Data/Type/Natural/Builtin.hs +7/−0
- src/Data/Type/Natural/Core.hs +237/−0
- src/Data/Type/Natural/Lemma/Arithmetic.hs +295/−0
- src/Data/Type/Natural/Lemma/Order.hs +1054/−0
- src/Data/Type/Natural/Lemma/Presburger.hs +37/−0
- src/Data/Type/Natural/Presburger/MinMaxSolver.hs +61/−0
- src/Data/Type/Natural/Utils.hs +10/−0
- src/Data/Type/Ordinal.hs +338/−0
- src/Data/Type/Ordinal/Builtin.hs +7/−0
- tests/Data/Type/Natural/Presburger/Cases.hs +27/−0
- tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs +71/−0
- tests/Data/Type/NaturalSpec.hs +124/−0
- tests/Data/Type/NaturalSpec/TH.hs +56/−0
- tests/Data/Type/OrdinalSpec.hs +1/−0
- tests/Shared.hs +83/−0
- tests/test.hs +1/−0
- type-natural.cabal +90/−67
− Data/Type/Natural.hs
@@ -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 |]-
− Data/Type/Natural/Builtin.hs
@@ -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 |]-
− Data/Type/Natural/Class.hs
@@ -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) |]
− Data/Type/Natural/Class/Arithmetic.hs
@@ -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 #-}
− Data/Type/Natural/Class/Order.hs
@@ -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-
− Data/Type/Natural/Core.hs
@@ -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-
− Data/Type/Natural/Definitions.hs
@@ -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- |]
− Data/Type/Natural/Singleton/Compat.hs
@@ -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-
− Data/Type/Natural/Singleton/Compat/TH.hs
@@ -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)-
− Data/Type/Ordinal.hs
@@ -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 |]-
− Data/Type/Ordinal/Builtin.hs
@@ -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 #-}
− Data/Type/Ordinal/Peano.hs
@@ -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'
+ src/Data/Type/Natural.hs view
@@ -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 (>=),+ (%>=?),+ 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
+ src/Data/Type/Natural/Builtin.hs view
@@ -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
+ src/Data/Type/Natural/Core.hs view
@@ -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
+ src/Data/Type/Natural/Lemma/Arithmetic.hs view
@@ -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
+ src/Data/Type/Natural/Lemma/Order.hs view
@@ -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 (>=),+ 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 <? m)+propToBoolLt ZeroLtSucc = Witness+propToBoolLt (SuccLtSucc lt) =+ withWitness (propToBoolLt lt) Witness++boolToPropLt :: n < m => 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 <? m = n + 1 <=? m++(%<?) :: SNat n -> SNat m -> SBool (n <? m)+(%<?) = (%<=?) . sSucc++type n < m = (n <? m) ~ 'True++type n >=? m = m <=? n++(%>=?) :: SNat n -> SNat m -> SBool (n >=? m)+(%>=?) = flip (%<=?)++type n >= m = (n >=? m) ~ 'True++type n >? m = m <? n++(%>?) :: SNat n -> SNat m -> SBool (n >? m)+(%>?) = flip (%<?)++type n > 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 <? m) ->+ 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 <? m)+ltToLneq n m nLTm =+ gcastWith (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm++lneqZero :: SNat a -> IsTrue (0 <? Succ a)+lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n++lneqSucc :: SNat n -> IsTrue (n <? Succ n)+lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n++succLneqSucc ::+ SNat n ->+ SNat m ->+ (n <? m) :~: (Succ n <? Succ m)+succLneqSucc _ _ = Refl++lneqRightPredSucc ::+ SNat n ->+ SNat m ->+ IsTrue (n <? m) ->+ m :~: Succ (Pred m)+lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm++lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)+lneqSuccStepL n m snLNEQm =+ gcastWith (sym $ lneqSuccLeq n m) $+ leqSuccStepL (sSucc n) m $+ gcastWith (lneqSuccLeq (sSucc n) m) snLNEQm++lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)+lneqSuccStepR n m nLNEQm =+ gcastWith (sym $ lneqSuccLeq n (sSucc m)) $+ leqSuccStepR (sSucc n) m $+ gcastWith (lneqSuccLeq n m) nLNEQm++plusStrictMonotone ::+ SNat n ->+ SNat m ->+ SNat l ->+ SNat k ->+ IsTrue (n <? m) ->+ IsTrue (l <? k) ->+ IsTrue ((n + l) <? (m + k))+plusStrictMonotone n m l k nLNm lLNk =+ gcastWith (sym $ lneqSuccLeq (n %+ l) (m %+ k)) $+ flip coerceLeqL (m %+ k) (plusSuccL n l) $+ plusMonotone+ (sSucc n)+ m+ l+ k+ (gcastWith (lneqSuccLeq n m) nLNm)+ ( leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $+ gcastWith (lneqSuccLeq l k) lLNk+ )++maxZeroL :: SNat n -> 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 <? 0) -> 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
+ src/Data/Type/Natural/Lemma/Presburger.hs view
@@ -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
+ src/Data/Type/Natural/Presburger/MinMaxSolver.hs view
@@ -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 "<?")+ singNatGeq <- 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+ }
+ src/Data/Type/Natural/Utils.hs view
@@ -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 @())
+ src/Data/Type/Ordinal.hs view
@@ -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 %<? sNat @n of+ STrue -> 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 <? n) :~: 'True) $+ OLt sk++{- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.++ Since 1.0.0.0+-}+sNatToOrd' :: (m < n) => 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 %<? sn of+ STrue -> 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
+ src/Data/Type/Ordinal/Builtin.hs view
@@ -0,0 +1,7 @@+module Data.Type.Ordinal.Builtin+ {-# DEPRECATED "Use Data.Type.Ordinal instead" #-}+ ( module Data.Type.Ordinal,+ )+where++import Data.Type.Ordinal
+ tests/Data/Type/Natural/Presburger/Cases.hs view
@@ -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
+ tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs view
@@ -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)
+ tests/Data/Type/NaturalSpec.hs view
@@ -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 "(<?)" $ \(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 "(>?)" $ \(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
+ tests/Data/Type/NaturalSpec/TH.hs view
@@ -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
+ tests/Data/Type/OrdinalSpec.hs view
@@ -0,0 +1,1 @@+module Data.Type.OrdinalSpec where
@@ -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
+ tests/test.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}
type-natural.cabal view
@@ -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