type-natural 0.7.1.4 → 1.3.0.2
raw patch · 31 files changed
Files
- Changelog.md +11/−0
- Data/Type/Natural.hs +0/−292
- Data/Type/Natural/Builtin.hs +0/−425
- Data/Type/Natural/Class.hs +0/−33
- Data/Type/Natural/Class/Arithmetic.hs +0/−547
- Data/Type/Natural/Class/Order.hs +0/−706
- Data/Type/Natural/Compat.hs +0/−8
- Data/Type/Natural/Core.hs +0/−91
- Data/Type/Natural/Definitions.hs +0/−162
- Data/Type/Ordinal.hs +0/−274
- Data/Type/Ordinal/Builtin.hs +0/−149
- Data/Type/Ordinal/Peano.hs +0/−149
- src/Data/Type/Natural.hs +178/−0
- src/Data/Type/Natural/Builtin.hs +7/−0
- src/Data/Type/Natural/Core.hs +314/−0
- src/Data/Type/Natural/Lemma/Arithmetic.hs +296/−0
- src/Data/Type/Natural/Lemma/Order.hs +1004/−0
- src/Data/Type/Natural/Lemma/Presburger.hs +37/−0
- src/Data/Type/Natural/Presburger/MinMaxSolver.hs +60/−0
- src/Data/Type/Natural/Utils.hs +10/−0
- src/Data/Type/Ordinal.hs +340/−0
- src/Data/Type/Ordinal/Builtin.hs +7/−0
- tests/Data/Type/Natural/Lemma/OrderSpec.hs +485/−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 +84/−0
- tests/test.hs +1/−0
- type-natural.cabal +102/−45
+ Changelog.md view
@@ -0,0 +1,11 @@+# Changelog++## 1.3.0.1++* Supports GHC 9.8+* Drops support for GHC <9++## 1.3.0.0++* Supports GHC 9.6+* Adds compatibility layer for `SNat` singleton provided since base 4.18
− Data/Type/Natural.hs
@@ -1,292 +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, Sing (SZ, SS),- -- ** Arithmetic functions and their singletons.- min, Min, sMin, max, Max, sMax,- MinSym0, MinSym1, MinSym2,- MaxSym0, MaxSym1, MaxSym2,- (:+:), (:+),- (:+$), (:+$$), (:+$$$),- (%+), (%:+), (:*), (:*:),- (:*$), (:*$$), (:*$$$),- (%:*), (%*), (:-:), (:-),- (:**:), (:**), (%:**), (%**),- (:-$), (:-$$), (:-$$$),- (%:-), (%-),- -- ** Type-level predicate & judgements- Leq(..), (:<=), LeqInstance,- boolToPropLeq, boolToClassLeq, propToClassLeq,- propToBoolLeq,- -- * Conversion functions- natToInt, intToNat, sNatToInt,- -- * Quasi quotes for natural numbers- 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.Class hiding (One, Zero, sOne, sZero)-import Data.Type.Natural.Core-import Data.Type.Natural.Definitions hiding ((:<=))-import Data.Singletons-import Data.Singletons.Prelude.Ord-import Data.Singletons.Decide-import Data.Type.Monomorphic-import Proof.Equational-import Proof.Propositional hiding (Not)-import Data.Void-import Language.Haskell.TH.Quote------------------------------------------------------- * 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--instance Monomorphicable (Sing :: Nat -> *) where- type MonomorphicRep (Sing :: Nat -> *) = Integer- demote (Monomorphic sn) = sNatToInt sn- promote n- | n < 0 = error "negative integer!"- | n == 0 = Monomorphic SZ- | otherwise = withPolymorhic (n - 1) $ \sn -> Monomorphic $ SS sn------------------------------------------------------- * 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 _) _ Witness = \case {}--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 '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,425 +0,0 @@-{-# LANGUAGE CPP, ConstraintKinds, DataKinds, EmptyCase, ExplicitNamespaces #-}-{-# LANGUAGE FlexibleContexts, GADTs, InstanceSigs, PolyKinds, RankNTypes #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}--- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@-module Data.Type.Natural.Builtin- ( -- * Sysnonym to avoid confusion- Peano,- -- * Coercion between builtin type-level natural and peano numerals- FromPeano, ToPeano, sFromPeano, sToPeano,- -- * 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- )- where-import Data.Type.Natural.Class--import Data.Singletons.Decide (SDecide (..))-import Data.Singletons.Decide (Decision (..))-import Data.Singletons.Prelude (PNum (..), SNum (..), Sing (..))-import Data.Singletons.Prelude (SingI (..))-import Data.Singletons.Prelude (SingKind (..), SomeSing (..))-import Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..))-import Data.Singletons.Prelude.Ord (POrd (..), SOrd (..))-import Data.Singletons.TH (sCases)-import Data.Singletons.TypeLits (withKnownNat)-import Data.Type.Equality ((:~:) (..))-import Data.Type.Monomorphic (Monomorphic (..))-import Data.Type.Monomorphic (Monomorphicable (..))-import Data.Type.Natural (Nat (S, Z), Sing (SS, SZ))-import qualified Data.Type.Natural as PN-import Data.Void (absurd)-import Data.Void (Void)-import GHC.TypeLits (type (+), type (<=), type (<=?))-import qualified GHC.TypeLits as TL-import 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 :: ToPeano n :~: ToPeano m -> n :~: m-toPeanoInjective Refl = Refl---- trustMe :: a :~: b--- trustMe = unsafeCoerce (Refl :: () :~: ())--- {-# WARNING trustMe--- "Used unproven type-equalities; This may cause disastrous result..." #-}--toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :~: 'S (ToPeano n)-toPeanoSuccCong _ = unsafeCoerce (Refl :: () :~: ())- -- We cannot prove this lemma within Haskell, so we assume it a priori.--sToPeano :: Sing n -> Sing (ToPeano n)-sToPeano sn =- case sn %~ (sing :: Sing 0) of- Proved eq -> withRefl eq SZ- Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn)))---- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat).--- Succ n :~: Succ m -> n :~: m--- 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 :+ m) :~: FromPeano n :+ 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 + m) :~: ToPeano n :+ 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 + r :~: m + r-natPlusCongR _ Refl = Refl--fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :~: FromPeano n :* FromPeano m-fromPeanoMultCong SZ _ = Refl-fromPeanoMultCong (SS psn) sm =- start (sFromPeano (SS psn %:* sm))- =~= 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 PN.:* 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)--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 + 1) <=? (m + 1)) :~: (n <=? m)-natLeqSuccEq _ _ = Refl--leqqCong :: n :~: m -> l :~: z -> (n <=? l) :~: (m <=? z)-leqqCong Refl Refl = Refl--leqCong :: n :~: m -> l :~: z -> (n :<= l) :~: (m :<= z)-leqCong Refl Refl = Refl--fromPeanoMonotone :: ((n :<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :~: 'True-fromPeanoMonotone SZ _ = Refl-fromPeanoMonotone (SS n) (SS m) =- start (sFromPeano (SS n) %:<=? sFromPeano (SS m))- === (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 <= 0) => Sing n -> n :~: 0-natLeqZero Zero = Refl-natLeqZero _ = error "natLeqZero : bug in ghc"---- | Currently, ghc-typelits-natnormalise reduces @(0 - 1) + 1@ to @0@,--- which is contradictory to current GHC's behaviour.--- So our assumption @((n :~: 0) -> Void)@ is simply disregarded.-natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :~: n-natSuccPred _ = Refl--myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :~: (n :<= m)-myLeqPred SZ _ = Refl-myLeqPred (SS _) (SS _) = Refl-myLeqPred (SS _) SZ = Refl--toPeanoCong :: a :~: b -> ToPeano a :~: ToPeano b-toPeanoCong Refl = Refl--toPeanoMonotone :: (n <= m)- => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True-toPeanoMonotone sn sm =- case sn %~ (sing :: Sing 0) of- Proved eql -> withRefl eql Refl- Disproved nPos -> case sm %~ (sing :: Sing 0) of- Proved mEq0 -> withRefl mEq0 $ absurd $ nPos $ natLeqZero sn- Disproved 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 + 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 #-}- 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 m n Witness =- case sCompare (sSucc m) n of- SLT -> Refl- SEQ -> Refl-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800- _ -> bugInGHC-#endif- cmpZero _ = Refl- leqRefl _ = Witness- eqToRefl _ _ Refl = Refl- flipCompare n m = $(sCases ''Ordering [|sCompare n m|] [|Refl|])- leqToCmp n m Witness =- case sCompare n m of- SLT -> Right Refl- SEQ -> Left Refl-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800- _ -> bugInGHC-#endif-- leqToMin _ _ Witness = Refl- leqToMax _ _ Witness = Refl- geqToMax n m mLEQn =- 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-import Language.Haskell.TH.Quote---- | 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,547 +0,0 @@-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}-{-# LANGUAGE 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,- ) where-import Data.Singletons.Decide-import Data.Singletons.Prelude-import Data.Singletons.Prelude.Enum-import Data.Type.Equality-import Data.Void-import Proof.Equational--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)- => 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 (multZeroR sZero)-- step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k)- step sk (MultZeroR ih) = MultZeroR $- start (sS sk %:* sZero)- === sk %:* sZero %:+ sZero `because` multSuccL sk sZero- === sk %:* sZero `because` plusZeroR (sk %:* sZero)- === sZero `because` ih-- multSuccR :: Sing n -> Sing m -> n :* S m :~: n :* m :+ (n :: nat)- multSuccR sn0 = multSuccRProof $ induction base step sn0- where- base :: MultSuccR (Zero 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)--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-
− Data/Type/Natural/Class/Order.hs
@@ -1,706 +0,0 @@-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}-module Data.Type.Natural.Class.Order- (PeanoOrder(..), DiffNat(..), LeqView(..),- FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,- sLeqCongL, sLeqCongR, sLeqCong,- (:-.), (%:-.), minPlusTruncMinus, truncMinusLeq- ) where-import Data.Type.Natural.Class.Arithmetic--import Data.Singletons.Decide-import Data.Singletons.Prelude-import Data.Singletons.Prelude.Enum-import Data.Singletons.TH-import Data.Type.Equality-import Data.Void-import Proof.Equational-import Proof.Propositional--data LeqView (n :: nat) (m :: nat) where- LeqZero :: Sing n -> LeqView (Zero 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--coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l- -> IsTrue (n :<= l) -> IsTrue (m :<= l)-coerceLeqL Refl _ Witness = Witness--coerceLeqR :: forall (n :: nat) m l . 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/Compat.hs
@@ -1,8 +0,0 @@-{-# LANGUAGE CPP #-}-module Data.Type.Natural.Compat (bugInGHC) where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Singletons.Prelude (bugInGHC)-#else-bugInGHC :: a-bugInGHC = error "GHC case-analysis error!"-#endif
− Data/Type/Natural/Core.hs
@@ -1,91 +0,0 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-}-{-# LANGUAGE TypeOperators, UndecidableInstances #-}-module Data.Type.Natural.Core where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Type.Natural.Compat-#endif--import Data.Constraint hiding ((:-))-import Data.Promotion.Prelude.Ord ((:<=))-import Data.Type.Natural.Definitions hiding ((:<=))-import Prelude (Bool (..), Eq (..), Show (..), ($))-import Proof.Propositional (IsTrue)-import Unsafe.Coerce------------------------------------------------------- ** Type-level predicate & judgements.------------------------------------------------------ | Comparison via 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)--(%-) :: (m :<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)-n %- SZ = n-SS n %- SS m = n %- m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-_ %- _ = bugInGHC-#endif--infixl 6 %--deriving instance Show (SNat n)-deriving instance Eq (SNat n)--data (a :: Nat) :<: (b :: Nat) where- ZeroLtSucc :: Zero :<: 'S m- SuccLtSucc :: n :<: m -> 'S n :<: 'S m--deriving instance Show (a :<: b)------------------------------------------------------- * Total orderings on natural numbers.----------------------------------------------------propToBoolLeq :: 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-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-boolToPropLeq _ _ = bugInGHC-#endif--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,162 +0,0 @@-{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, InstanceSigs, KindSignatures #-}-{-# LANGUAGE MultiParamTypeClasses, PolyKinds, RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}-{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}-module Data.Type.Natural.Definitions- (module Data.Type.Natural.Definitions,- module Data.Singletons.Prelude- ) where-import Data.Promotion.Prelude.Enum-import Data.Singletons.Prelude-import Data.Singletons.Prelude.Enum-import Data.Singletons.TH (singletons)-import Data.Typeable (Typeable)------------------------------------------------------- * Natural numbers and its singleton type----------------------------------------------------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 n = S n- pred Z = Z- pred (S n) = n- toEnum n = if n == 0 then Z else S (toEnum (n - 1))- fromEnum Z = 0- fromEnum (S n) = 1 + fromEnum n- |]--type n :-: m = n :- m-type n :+: m = n :+ m--infixl 6 :-:, :+:--singletons [d|- (**) :: Nat -> Nat -> Nat- _ ** Z = S Z- n ** S m = (n ** m) * n- |]----- | Addition for singleton numbers.-(%+) :: SNat n -> SNat m -> SNat (n :+: m)-(%+) = (%:+)-infixl 6 %+---- | Type-level multiplication.-type n :*: m = n :* m-infixl 7 :*:---- | Multiplication for singleton numbers.-(%*) :: SNat n -> SNat m -> SNat (n :*: m)-(%*) = (%:*)-infixl 7 %*---- | Type-level exponentiation.-type n :**: m = n :** m---- | Exponentiation for singleton numbers.-(%**) :: SNat n -> SNat m -> SNat (n :**: m)-(%**) = (%:**)--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/Ordinal.hs
@@ -1,274 +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, ordToInt, ordToSing,- unsafeFromInt, inclusion, inclusion',- -- * Ordinal arithmetics- (@+), enumOrdinal,- -- * Elimination rules for @'Ordinal' 'Z'@.- absurdOrd, vacuousOrd- ) where-import Data.Kind-import Data.List (genericDrop, genericTake)-import Data.Ord (comparing)-import Data.Singletons.Decide-import Data.Singletons.Prelude-import Data.Singletons.Prelude.Enum-import Data.Type.Equality-import Data.Type.Monomorphic-import qualified Data.Type.Natural as PN-import Data.Type.Natural.Builtin ()-import Data.Type.Natural.Class-import Data.Typeable (Typeable)-import Data.Void (absurd)-import GHC.TypeLits (type (+))-import qualified GHC.TypeLits as TL-import Language.Haskell.TH hiding (Type)-import Language.Haskell.TH.Quote-import Proof.Equational-import Proof.Propositional-import Unsafe.Coerce---- | 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--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, Monomorphicable (Sing :: nat -> *),- Integral (MonomorphicRep (Sing :: nat -> *)),- Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat-instance (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),- Integral (MonomorphicRep (Sing :: nat -> *)),- Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat--instance (HasOrdinal nat, SingI (n :: nat))- => Num (Ordinal n) where- {-# SPECIALISE instance SingI n => Num (Ordinal (n :: PN.Nat)) #-}- {-# SPECIALISE instance SingI n => Num (Ordinal (n :: TL.Nat)) #-}- _ + _ = error "Finite ordinal is not closed under addition."- _ - _ = error "Ordinal subtraction is not defined"- negate OZ = OZ- negate _ = 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- {-# SPECIALISE instance SingI n => Show (Ordinal (n :: PN.Nat)) #-}- {-# SPECIALISE instance SingI n => Show (Ordinal (n :: TL.Nat)) #-}- showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (demote $ Monomorphic (sing :: Sing n)))--instance (HasOrdinal nat)- => Eq (Ordinal (n :: nat)) where- {-# SPECIALISE instance Eq (Ordinal (n :: PN.Nat)) #-}- {-# SPECIALISE instance Eq (Ordinal (n :: TL.Nat)) #-}- o == o' = ordToInt o == ordToInt o'--instance (HasOrdinal 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--enumFromToOrd :: forall (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--enumFromOrd :: forall (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 (Succ n) = withSingI n $- withWitness (lneqZero n) $- OLt sZero : map succOrd (enumOrdinal n)-enumOrdinal _ = []--succOrd :: forall (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 #-}--unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))- => MonomorphicRep (Sing :: nat -> *) -> Ordinal n-unsafeFromInt n =- case promote (n :: MonomorphicRep (Sing :: nat -> *)) of- Monomorphic sn ->- case sn %:< (sing :: Sing n) of- STrue -> sNatToOrd' (sing :: Sing n) sn- SFalse -> error "Bound over!"--unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)- => proxy nat -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n-unsafeFromInt' _ n =- case promote (n :: MonomorphicRep (Sing :: nat -> *)) of- Monomorphic sn ->- case sn %:< (sing :: Sing n) of- STrue -> sNatToOrd' (sing :: Sing n) sn- SFalse -> error "Bound over!"---- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.------ Since 0.5.0.0-sNatToOrd' :: (PeanoOrder nat, (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n-sNatToOrd' _ m = OLt m-{-# INLINE sNatToOrd' #-}---- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n-sNatToOrd = sNatToOrd' sing---- | 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 #-}---- | Convert ordinal into @Int@.-ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *))- => Ordinal (n :: nat)- -> int-ordToInt (OLt n) = demote $ Monomorphic n-{-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Integer #-}-{-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-}---- | 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 on = unsafeCoerce on-{-# INLINE inclusion #-}----- | Ordinal addition.-(@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), 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,149 +0,0 @@-{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}--- | 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, ordToInt,- unsafeFromInt, inclusion, inclusion',- -- * Ordinal arithmetics- (@+), enumOrdinal,- -- * Elimination rules for @'Ordinal' 0'@.- absurdOrd, vacuousOrd- ) where-import Data.Kind-import Data.Singletons.Prelude (POrd (..), Sing (..))-import Data.Singletons.Prelude.Enum (PEnum (..))-import qualified Data.Type.Ordinal as O-import GHC.TypeLits-import Language.Haskell.TH.Quote (QuasiQuoter)-import Data.Type.Monomorphic---- | 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 :< t) ~ 'True)- => Sing n1 -> O.Ordinal t-pattern OLt n = O.OLt n---- | Pattern synonym representing the 0-th ordinal.--- --- Since 0.7.0.0-pattern OZ :: forall (n :: Nat). ()- => (0 :< 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 :< 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 :< n) ~ 'True) => Sing m -> Ordinal n-sNatToOrd = O.sNatToOrd-{-# INLINE sNatToOrd #-}---- | Convert ordinal into @Int@.--- --- Since 0.7.0.0-ordToInt :: Ordinal n -> Integer-ordToInt = O.ordToInt-{-# INLINE ordToInt #-}--unsafeFromInt :: KnownNat n- => MonomorphicRep (Sing :: Nat -> Type) -> 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-(@+) :: (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,149 +0,0 @@-{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}--- | 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, ordToInt,- unsafeFromInt, inclusion, inclusion',- -- * Ordinal arithmetics- (@+), enumOrdinal,- -- * Elimination rules for @'Ordinal' 'Z'@.- absurdOrd, vacuousOrd- ) where-import Data.Kind-import Data.Singletons.Prelude (POrd (..), 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)-import Data.Type.Monomorphic---- | 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---- | 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 -> Integer-ordToInt = O.ordToInt-{-# INLINE ordToInt #-}--unsafeFromInt :: SingI n- => MonomorphicRep (Sing :: Nat -> Type) -> 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 #-}
+ src/Data/Type/Natural.hs view
@@ -0,0 +1,178 @@+{-# LANGUAGE CPP #-}+{-# 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,+ fromSNat,+ 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 (..),+ OrderingI(..),+ fromOrderingI,+ toOrderingI,+ FlipOrdering,+ sFlipOrdering,+ )+where++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 Text.Read (readMaybe)+import Data.Ord (comparing)+import Data.Function (on)++{- | 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+{-# DEPRECATED toNatural "Use fromSNat instead" #-}+toNatural = fromSNat++data SomeSNat where+ SomeSNat :: KnownNat n => SNat n -> SomeSNat++deriving instance Show SomeSNat++instance Eq SomeSNat where+ (==) = (==) `on` \(SomeSNat n) -> fromSNat n+ {-# INLINE (==) #-}++instance Ord SomeSNat where+ compare = comparing (\(SomeSNat n) -> fromSNat n)+ {-# INLINE compare #-}++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,314 @@+{-# LANGUAGE CPP #-}+{-# 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 #-}+{-# LANGUAGE NoStarIsType #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}++module Data.Type.Natural.Core+ ( SNat (Zero, Succ),+#if !MIN_VERSION_base(4,18,0)+ fromSNat,+ withKnownNat,+ withSomeSNat,+#endif+ unsafeLiftSBin,+ ZeroOrSucc (..),+ viewNat,+ sNat,+ (%+),+ (%-),+ (%*),+ (%^),+ sDiv,+ sMod,+ sLog2,+ (%<=?),+ sCmpNat,+ sCompare,+ Succ,+ S,+ sSucc,+ sS,+ Pred,+ sPred,+ Zero,+ One,+ sZero,+ sOne,+ Equality (..),+ equalAbsurdFromBool,+ type (===),+ (%~),+ sFlipOrdering,+ FlipOrdering,+ SOrdering (..),+ SBool (..),+ Natural,+ OrderingI(..),+ fromOrderingI,+ toOrderingI,+ -- Re-exports+ module GHC.TypeNats,+ )+where++import Data.Type.Equality+ ( type (:~:) (..),+ type (==),+ )+import GHC.TypeNats+import Math.NumberTheory.Logarithms (naturalLog2)+import Type.Reflection (Typeable)+import Unsafe.Coerce (unsafeCoerce)+import Numeric.Natural++#if MIN_VERSION_base(4,16,0)+import Data.Type.Ord (OrderingI(..))+#endif++#if !MIN_VERSION_base(4,18,0)+import Data.Proxy+import Data.Type.Equality+import GHC.Exts+#endif++#if !MIN_VERSION_base(4,18,0)+-- | A singleton for type-level naturals+newtype SNat (n :: Nat) = UnsafeSNat Natural+ deriving newtype (Show, Eq, Ord)++fromSNat :: SNat n -> Natural+fromSNat = coerce++withKnownNat :: forall n rep (r :: TYPE rep). SNat n -> (KnownNat n => r) -> r+withKnownNat (UnsafeSNat n) act =+ case someNatVal n of+ SomeNat (_ :: Proxy m) ->+ case unsafeCoerce (Refl @()) :: n :~: m of+ Refl -> act++data KnownNatInstance (n :: Nat) where+ KnownNatInstance :: KnownNat n => KnownNatInstance n++-- An internal function that is only used for defining the SNat pattern+-- synonym.+knownNatInstance :: SNat n -> KnownNatInstance n+knownNatInstance sn = withKnownNat sn KnownNatInstance++pattern SNat :: forall n. () => KnownNat n => SNat n+pattern SNat <- (knownNatInstance -> KnownNatInstance) + where SNat = sNat++withSomeSNat :: forall rep (r :: TYPE rep). Natural -> (forall n. SNat n -> r) -> r+withSomeSNat n f = f (UnsafeSNat n)+#endif++unsafeLiftSBin :: (Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat k+{-# INLINE unsafeLiftSBin #-}+unsafeLiftSBin f = \l r -> withSomeSNat (fromSNat l `f` fromSNat r) unsafeCoerce++unsafeLiftSUnary :: (Natural -> Natural) -> SNat n -> SNat k+{-# INLINE unsafeLiftSUnary #-}+unsafeLiftSUnary f = \l -> withSomeSNat (f $ fromSNat l) unsafeCoerce++(%+) :: SNat n -> SNat m -> SNat (n + m)+{-# INLINE (%+) #-}+(%+) = unsafeLiftSBin (+)++(%-) :: SNat n -> SNat m -> SNat (n - m)+(%-) = unsafeLiftSBin (-)++(%*) :: SNat n -> SNat m -> SNat (n * m)+(%*) = unsafeLiftSBin (*)++sDiv :: SNat n -> SNat m -> SNat (Div n m)+sDiv = unsafeLiftSBin quot++sMod :: SNat n -> SNat m -> SNat (Mod n m)+sMod = unsafeLiftSBin rem++(%^) :: SNat n -> SNat m -> SNat (n ^ m)+(%^) = unsafeLiftSBin (^)++sLog2 :: SNat n -> SNat (Log2 n)+sLog2 = unsafeLiftSUnary $ fromIntegral . naturalLog2++sNat :: forall n. KnownNat n => SNat n+#if MIN_VERSION_base(4,18,0)+sNat = SNat+#else+sNat = UnsafeSNat $ natVal' (proxy# :: Proxy# n)+#endif+++infixl 6 %+, %-++infixl 7 %*, `sDiv`, `sMod`++infixr 8 %^++#if !MIN_VERSION_ghc(4,18,0)+instance TestEquality SNat where+ testEquality (UnsafeSNat l) (UnsafeSNat r) =+ if l == r+ then Just trustMe+ else Nothing+#endif+++-- | Since 1.1.0.0 (Type changed)+data Equality n m where+ Equal :: ((n == n) ~ 'True) => Equality n n+ NonEqual ::+ ((n === m) ~ 'False, (n == m) ~ 'False) =>+ Equality n m++equalAbsurdFromBool ::+ (x === y) ~ 'False => x :~: y -> a+equalAbsurdFromBool = \case {}++type family a === b where+ a === a = 'True+ _ === _ = 'False++infix 4 ===, %~++(%~) :: SNat l -> SNat r -> Equality l r+l %~ r =+ if fromSNat l == fromSNat 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 %~ sNat @0 of+ Equal -> IsZero+ NonEqual -> IsSucc (sPred n)+++#if !MIN_VERSION_base(4,16,0)+data OrderingI (a :: Nat) (b :: Nat) where+ LTI :: CmpNat a b ~ 'LT => OrderingI a b+ EQI :: CmpNat a b ~ 'EQ => OrderingI a b+ GTI :: CmpNat a b ~ 'GT => OrderingI a b+#endif++type family FlipOrdering ord where+ FlipOrdering 'LT = 'GT+ FlipOrdering 'GT = 'LT+ FlipOrdering 'EQ = 'EQ++data SOrdering (ord :: Ordering) where+ SLT :: SOrdering 'LT+ SEQ :: SOrdering 'EQ+ SGT :: SOrdering 'GT++fromOrderingI :: OrderingI n m -> SOrdering (CmpNat n m)+fromOrderingI LTI = SLT+fromOrderingI EQI = SEQ+fromOrderingI GTI = SGT++toOrderingI :: SOrdering (CmpNat n m) -> OrderingI n m+toOrderingI SLT = LTI+toOrderingI SEQ = EQI+toOrderingI SGT = GTI++deriving instance Show (SOrdering ord)++deriving instance Eq (SOrdering ord)++deriving instance Typeable SOrdering++sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)+sFlipOrdering SLT = SGT+sFlipOrdering SEQ = SEQ+sFlipOrdering SGT = SLT++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)+n %<=? m =+ if fromSNat n <= fromSNat m+ then unsafeCoerce STrue+ else unsafeCoerce SFalse++sCmpNat, sCompare :: SNat n -> SNat m -> SOrdering (CmpNat n m)+sCompare = sCmpNat+sCmpNat n m =+ case compare (fromSNat n) (fromSNat m) of+ LT -> unsafeCoerce SLT+ EQ -> unsafeCoerce SEQ+ GT -> unsafeCoerce SGT+
+ src/Data/Type/Natural/Lemma/Arithmetic.hs view
@@ -0,0 +1,296 @@+{-# 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 #-}+{-# LANGUAGE NoStarIsType #-}+{-# 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,1004 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE CPP #-}+{-# 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,+ OrdCond,+ sOrdCond,++ -- * Lemmas+ ordCondDistrib,+ leqOrdCond,+ sFlipOrdering,+ coerceLeqL,+ coerceLeqR,+ sLeqCongL,+ sLeqCongR,+ sLeqCong,+ succDiffNat,+ compareCongR,+ leqToCmp,+ eqlCmpEQ,+ eqToRefl,+ flipCmpNat,+ ltToNeq,+ leqNeqToLT,+ succLeqToLT,+ ltToLeq,+ gtToLeq,+ congFlipOrdering,+ ltToSuccLeq,+ cmpZero,+ cmpSuccZeroGT,+ 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,+ minCase,+ maxCase,+ 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.Type.Equality (gcastWith, (:~:) (..))+import Data.Type.Natural.Core+import Data.Type.Natural.Lemma.Arithmetic+import Data.Void (Void, absurd)+import Proof.Equational+ ( because,+ start,+ sym,+ trans,+ (===),+ (=~=),+ )+import Proof.Propositional (IsTrue (..), eliminate, withWitness)+#if MIN_VERSION_ghc(9,2,1)+import qualified Data.Type.Ord as DTO+import Data.Type.Ord (OrdCond)+#endif+++--------------------------------------------------++-- ** Type-level predicate & judgements.++--------------------------------------------------++#if !MIN_VERSION_ghc(9,2,1)+type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) where+ OrdCond 'LT lt eq gt = lt+ OrdCond 'EQ lt eq gt = eq+ OrdCond 'GT lt eq gt = gt+#endif++sOrdCond :: SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)+sOrdCond SLT lt _ _ = lt+sOrdCond SEQ _ eq _ = eq+sOrdCond SGT _ _ gt = gt++minCase :: SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)+minCase n m =+ case sCmpNat n m of+ SLT -> Left Refl+ SEQ -> Left Refl+ SGT -> Right Refl++maxCase :: SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)+maxCase n m =+ case sCmpNat n m of+ SLT -> Left Refl+ SEQ -> Left Refl+ SGT -> Right Refl++-- | 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)++-- | Since 1.2.0 (argument changed)+data a :<: b where+ ZeroLtSucc :: SNat m -> 0 :<: (m + 1)+ SuccLtSucc :: SNat n -> SNat m -> 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 (sm :: SNat m)) = + gcastWith (cmpZero sm) Witness+propToBoolLt (SuccLtSucc sn sm lt) =+ gcastWith (cmpSucc sn sm) $+ withWitness (propToBoolLt lt) Witness++boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m+boolToPropLt Zero (Succ sn) = ZeroLtSucc sn+boolToPropLt (Succ n) Zero = eliminate $+ start STrue+ =~= (Succ n %<? Zero)+ =~= sOrdCond (sCmpNat (Succ n) Zero) STrue SFalse SFalse+ === sOrdCond SGT STrue SFalse SFalse+ `because` sOrdCondCong1 (cmpSuccZeroGT n) STrue SFalse SFalse+ =~= SFalse+boolToPropLt (Succ n) (Succ m) = + gcastWith (cmpSucc n m) $+ SuccLtSucc n m (boolToPropLt n m)++#if MIN_VERSION_ghc(9,2,1)+type Min m n = DTO.Min @Nat m n+#else+type Min m n = OrdCond (CmpNat m n) m m n+#endif++sMin :: SNat n -> SNat m -> SNat (Min n m)+{-# INLINE sMin #-}+sMin = unsafeLiftSBin min++sMax :: SNat n -> SNat m -> SNat (Max n m)+{-# INLINE sMax #-}+sMax = unsafeLiftSBin max++#if MIN_VERSION_ghc(9,2,1)+type Max m n = DTO.Max @Nat m n+#else+type Max m n = OrdCond (CmpNat m n) n n m+#endif++infix 4 <?, <, >=?, >=, >, >?++#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) <? m = n DTO.<? m+#else+type n <? m = OrdCond (CmpNat n m) 'True 'False 'False+#endif++(%<?) :: SNat n -> SNat m -> SBool (n <? m)+n %<? m = sOrdCond (sCmpNat n m) STrue SFalse SFalse++#if MIN_VERSION_ghc(9,2,2)+type (n :: Nat) < m = n DTO.< m+#else+type n < m = (n <? m) ~ 'True+#endif++#if MIN_VERSION_ghc(9,2,1)+type n >=? m = (DTO.>=?) @Nat n m+#else+type n >=? m = OrdCond (CmpNat n m) 'False 'True 'True+#endif++(%>=?) :: SNat n -> SNat m -> SBool (n >=? m)+n %>=? m = sOrdCond (sCmpNat n m) SFalse STrue STrue++#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) >= m = n DTO.>= m+#else+type n >= m = (n >=? m) ~ 'True+#endif++#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) >? m = n DTO.>? m+#else+type n >? m = OrdCond (CmpNat n m) 'False 'False 'True+#endif++(%>?) :: SNat n -> SNat m -> SBool (n >? m)+n %>? m = sOrdCond (sCmpNat n m) SFalse SFalse STrue++#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) > m = n DTO.> m+#else+type n > m = (n >? m) ~ 'True+#endif++infix 4 %>?, %<?, %>=?++ordCondDistrib :: proxy f -> SOrdering o -> p l -> p' e -> p'' g ->+ OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)+ordCondDistrib _ SLT _ _ _ = Refl+ordCondDistrib _ SEQ _ _ _ = Refl+ordCondDistrib _ SGT _ _ _ = Refl++leqOrdCond+ :: SNat n -> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False+#if MIN_VERSION_ghc(9,2,1)+leqOrdCond _ _ = Refl+#else+leqOrdCond Zero n =+ case cmpZero' n of+ Left Refl -> Refl+ Right Refl -> Refl+leqOrdCond (Succ m) Zero = + gcastWith (succLeqZeroAbsurd' m) $+ gcastWith (cmpSuccZeroGT m) $+ Refl+leqOrdCond (Succ m) (Succ n) =+ gcastWith (cmpSucc m n) $+ start (Succ m %<=? Succ n)+ === (m %<=? n) `because` sym (leqSucc' m n)+ === sOrdCond (sCmpNat m n) STrue STrue SFalse `because` leqOrdCond m n+#endif++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}++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 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 _ _ Witness = Refl++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 _ _ Refl = Witness++congFlipOrdering ::+ a :~: b -> FlipOrdering a :~: FlipOrdering b+congFlipOrdering Refl = Refl++ltToSuccLeq ::+ SNat a ->+ SNat b ->+ CmpNat a b :~: 'LT ->+ IsTrue (Succ a <=? b)+ltToSuccLeq _ _ Refl = Witness++cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT+cmpZero _ = Refl++cmpSuccZeroGT :: SNat a -> CmpNat (Succ a) 0 :~: 'GT+cmpSuccZeroGT _ = Refl++leqToGT ::+ SNat a ->+ SNat b ->+ IsTrue (Succ b <=? a) ->+ CmpNat a b :~: 'GT+leqToGT _ _ Witness = Refl++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 _ _ Refl = Refl++cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)+cmpSucc _ _ = Refl++ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT+ltSucc _ = Refl++cmpSuccStepR ::+ forall n m.+ SNat n ->+ SNat m ->+ CmpNat n m :~: 'LT ->+ CmpNat n (Succ m) :~: 'LT+cmpSuccStepR _ _ Refl = Refl++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 _ _ Witness = Refl++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 :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m+leqWitness = \sn -> leqWitPf (induction base step sn) @m+ where+ base :: LeqWitPf 0+ base = LeqWitPf $ \sm _ -> gcastWith (plusZeroL sm) $ DiffNat sZero sm++ step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)+ step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->+ case viewLeq (sSucc n) m snLEQm of+#if !MIN_VERSION_ghc(9,2,0) || MIN_VERSION_ghc(9,4,0)+ LeqZero _ -> absurd $ succNonCyclic n Refl+#endif+ LeqSucc (_ :: SNat n') pm nLEQpm ->+ succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm++leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)+leqStep _ _ _ Refl = Witness++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 _ = Witness++leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)+leqSuccStepR _ _ Witness = Witness++leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)+leqSuccStepL _ _ Witness = Witness++leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)+leqReflexive _ _ Refl = Witness++leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)+leqTrans _ _ _ Witness Witness = Witness++leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m+leqAntisymm _ _ Witness Witness = Refl++plusMonotone ::+ SNat n ->+ SNat m ->+ SNat l ->+ SNat k ->+ IsTrue (n <=? m) ->+ IsTrue (l <=? k) ->+ IsTrue ((n + l) <=? (m + k))+plusMonotone _ _ _ _ Witness Witness = Witness++leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0+leqZeroElim _ Witness = Refl++plusMonotoneL ::+ SNat n ->+ SNat m ->+ SNat l ->+ IsTrue (n <=? m) ->+ IsTrue ((n + l) <=? (m + l))+plusMonotoneL _ _ _ Witness = Witness++plusMonotoneR ::+ SNat n ->+ SNat m ->+ SNat l ->+ IsTrue (m <=? l) ->+ IsTrue ((n + m) <=? (n + l))+plusMonotoneR _ _ _ Witness = Witness++plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))+plusLeqL _ _ = Witness++plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))+plusLeqR _ _ = Witness++plusCancelLeqR ::+ SNat n ->+ SNat m ->+ SNat l ->+ IsTrue ((n + l) <=? (m + l)) ->+ IsTrue (n <=? m)+plusCancelLeqR _ _ _ Witness = Witness++plusCancelLeqL ::+ SNat n ->+ SNat m ->+ SNat l ->+ IsTrue ((n + m) <=? (n + l)) ->+ IsTrue (m <=? l)+plusCancelLeqL _ _ _ Witness = Witness++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' _ = 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' _ = Refl++notLeqToLeq :: forall n m. ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)+notLeqToLeq _ _ = Witness++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 n m Witness =+ case leqToCmp n m Witness of+ Left Refl -> Refl+ Right Refl -> Refl++geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m+geqToMin n m Witness =+ case leqToCmp m n Witness of+ Left Refl -> Refl+ Right Refl -> + gcastWith (flipCmpNat m n) 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 _ n m lLEQn lLEQm =+ case minCase n m of+ Left Refl -> lLEQn+ Right Refl -> lLEQm++leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m+leqToMax n m lLeqm =+ case leqToCmp n m lLeqm of+ Left Refl -> Refl+ Right Refl -> Refl++geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n+geqToMax n m Witness =+ case sCmpNat n m of+ SLT -> Refl+ SEQ -> Refl+ SGT -> Refl++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 _ n m nLEQl mLEQl =+ case maxCase n m of+ Left Refl -> mLEQl+ Right Refl -> nLEQl+++-- | Since 1.2.0.0 (type changed)+lneqSuccLeq :: SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)+#if MIN_VERSION_ghc(9,2,1)+lneqSuccLeq _ _ = Refl+#else+lneqSuccLeq n m = isTrueRefl (n %<? m) (Succ n %<=? m)+ (ltToSuccLeq n m . lneqToLT n m)+ (ltToLneq n m . succLeqToLT n m)++isTrueRefl :: SBool a -> SBool b + -> (IsTrue a -> IsTrue b)+ -> (IsTrue b -> IsTrue a)+ -> a :~: b+isTrueRefl SFalse SFalse _ _ = Refl+isTrueRefl STrue _ f _ = withWitness (f Witness) Refl+isTrueRefl _ STrue _ g = withWitness (g Witness) Refl+#endif++-- | Since 1.2.0.0 (type changed)+lneqReversed :: SNat n -> SNat m -> (n <? m) :~: (m >? n)+#if MIN_VERSION_ghc(9,2,1)+lneqReversed _ _ = Refl+#else+lneqReversed n m = + case sCmpNat n m of+ SLT -> gcastWith (flipCmpNat n m) Refl+ SEQ -> gcastWith (flipCmpNat n m) Refl+ SGT -> gcastWith (flipCmpNat n m) Refl+#endif++lneqToLT ::+ SNat n ->+ SNat m ->+ IsTrue (n <? m) ->+ CmpNat n m :~: 'LT+lneqToLT n m Witness =+ case sCmpNat n m of+ SLT -> Refl++ltToLneq ::+ SNat n ->+ SNat m ->+ CmpNat n m :~: 'LT ->+ IsTrue (n <? m)+ltToLneq _ _ Refl = Witness++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 n m = + start (n %<? m)+ =~=+ sOrdCond (sCmpNat n m) STrue SFalse SFalse+ === sOrdCond (sCmpNat (Succ n) (Succ m)) STrue SFalse SFalse + `because` sOrdCondCong1 (cmpSucc n m) STrue SFalse SFalse+ =~= (Succ n %<? Succ m)++sOrdCondCong1 :: o :~: o' -> proxy a -> proxy' b -> proxy' c + -> OrdCond o a b c :~: OrdCond o' a b c+sOrdCondCong1 Refl _ _ _ = 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,60 @@+{-# LANGUAGE CPP #-}++{- | 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+import GHC.TypeLits.Presburger.Types++import GHC.Plugins+ ( Plugin,+ fsLit,+ mkModuleName,+ mkTcOcc,+ splitTyConApp_maybe,+ )+import GHC.Tc.Plugin++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")+#if !MIN_VERSION_ghc(9,2,1)+ ordCondTyCon <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "OrdCond")+#endif+ return+ mempty+ { natGeqBool = [singNatGeq]+ , natLtBool = [singNatLt]+ , natGtBool = [singNatGt]+ , natMin = [singMin]+#if !MIN_VERSION_ghc(9,2,1)+ , ordCond = [ordCondTyCon]+#endif+ , 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+ }
+ 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,340 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE CPP #-}+{-# 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 Data.Type.Natural.Presburger.MinMaxSolver #-}+{-# OPTIONS_GHC -fobject-code #-}++{- | 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.Typeable (Typeable)+import Language.Haskell.TH.Quote+import Numeric.Natural ( Natural )+import Unsafe.Coerce+import Proof.Propositional (IsTrue (Witness))+import Data.Type.Natural.Lemma.Order (lneqZeroAbsurd)+import Data.Void (absurd)++{- | 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 (fromSNat (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 .. fromSNat sn - 1]++-- | Since 1.0.0.0 (type changed)+succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)+succOrd (OLt k) = OLt (sSucc k)+{-# INLINE succOrd #-}++instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where+ minBound = OLt sZero++ maxBound = withKnownNat (sNat @n %- sNat @1) $ 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) = fromSNat 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 sn) = absurd $ lneqZeroAbsurd sn Witness++{- | @'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/Lemma/OrderSpec.hs view
@@ -0,0 +1,485 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Data.Type.Natural.Lemma.OrderSpec where++import Control.Exception (SomeException (..), evaluate, try)+import Data.Functor ((<&>))+import Data.List (isInfixOf, isPrefixOf)+import Data.Type.Natural+import Data.Type.Natural.Lemma.Order+import Data.Void (Void)+import Proof.Propositional (IsTrue (Witness))+import Shared ()+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck+import Type.Reflection+import Unsafe.Coerce (unsafeCoerce)++someNat' :: NonNegative Integer -> SomeSNat+someNat' = toSomeSNat . fromInteger . getNonNegative++data SomeLeqNat where+ MkSomeLeqNat :: (n <=? m) ~ 'True => SNat n -> SNat m -> SomeLeqNat++data SomeLtNat where+ MkSomeLtNat ::+ CmpNat n m ~ 'LT =>+ SNat n ->+ SNat m ->+ SomeLtNat++data SomeLneqNat where+ MkSomeLneqNat ::+ (n <? m) ~ 'True =>+ SNat n ->+ SNat m ->+ SomeLneqNat++data SomeGtNat where+ MkSomeGtNat ::+ CmpNat n m ~ 'GT =>+ SNat n ->+ SNat m ->+ SomeGtNat++deriving instance Show SomeLeqNat++deriving instance Show SomeLtNat++deriving instance Show SomeLneqNat++deriving instance Show SomeGtNat++instance Arbitrary SomeLeqNat where+ arbitrary = do+ SomeSNat n <- someNat' <$> arbitrary+ SomeSNat m <- someNat' <$> arbitrary+ case n %<=? m of+ STrue -> pure $ MkSomeLeqNat n m+ SFalse ->+ case m %<=? n of+ STrue -> pure $ MkSomeLeqNat m n+ SFalse -> error "Impossible!"++instance Arbitrary SomeLtNat where+ arbitrary = do+ MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary+ let m' = Succ m+ case sCmpNat n m' of+ SLT -> pure $ MkSomeLtNat n m'+ _ -> error "impossible"++instance Arbitrary SomeLneqNat where+ arbitrary = do+ MkSomeLtNat (n :: SNat n) (m :: SNat m) <- arbitrary+ let m' = Succ m+ case n %<? m' of+ STrue -> pure $ MkSomeLneqNat n m'+ _ -> error "impossible"++instance Arbitrary SomeGtNat where+ arbitrary = do+ MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary+ let m' = Succ m+ case sCmpNat m' n of+ SGT -> pure $ MkSomeGtNat m' n+ _ -> error "impossible"++data SomeLeqView where+ MkSomeLeqView :: LeqView n m -> SomeLeqView++instance Show SomeLeqView where+ showsPrec d (MkSomeLeqView (LeqZero n)) =+ showParen (d > 10) $+ showString "LeqZero "+ . showsPrec 11 n+ showsPrec d (MkSomeLeqView (LeqSucc n m w)) =+ showParen (d > 10) $+ showString "LeqSucc "+ . showsPrec 11 n+ . showChar ' '+ . showsPrec 11 m+ . showChar ' '+ . showsPrec 11 w++instance Arbitrary SomeLeqView where+ arbitrary = sized $ \n ->+ if n <= 0+ then+ arbitrary <&> \case+ SomeSNat sn -> MkSomeLeqView (LeqZero sn)+ else+ arbitrary <&> \case+ MkSomeLeqNat sn sm -> MkSomeLeqView $ LeqSucc sn sm Witness++givesImpossibleVoid :: Void -> Property+givesImpossibleVoid contradiction = ioProperty $ do+ eith <- try @SomeException $ evaluate contradiction+ case eith of+ Left someE -> do+ pure $ counterexample (show someE) $+ property $+ "Impossible" `isPrefixOf` show someE+ || "Non-exhaustive" `isInfixOf` show someE+ || "missingAlt" `isInfixOf` show someE+ Right v -> + pure $ counterexample "Value of void returned..." + $ property False++test_Lemmas :: TestTree+test_Lemmas =+ testGroup+ "Lemmas"+ [ testProperty @(SomeLeqNat -> Property) "coerceLeqL terminates" $ \(MkSomeLeqNat (_ :: SNat n) sm) -> totalWitness $ coerceLeqL (Refl :: n :~: n) sm Witness+ , testProperty @(SomeLeqNat -> Property) "coerceLeqR terminates" $ \(MkSomeLeqNat sn (_ :: SNat m)) -> totalWitness $ coerceLeqR sn (Refl :: m :~: m) Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "sLeqCong terminates" $+ \(SomeSNat (_ :: SNat n)) (SomeSNat (_ :: SNat m)) ->+ totalRefl $ sLeqCong (Refl @n) (Refl @m)+ , testProperty @(SomeSNat -> SomeSNat -> Property) "succDiffNat terminates and gives the correct value" $+ \(SomeSNat sn) (SomeSNat sm) ->+ case succDiffNat sn (sn %+ sm) (DiffNat sn sm) of+ DiffNat sns sms ->+ fromSNat (sns %+ sms)+ === fromSNat sn + fromSNat sm + 1+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "compareCongR terminates"+ $ \(SomeSNat a) (SomeSNat (_ :: SNat b)) ->+ totalRefl $ compareCongR a (Refl @b)+ , testProperty @(SomeLeqNat -> Property)+ "leqToCmp works properly"+ $ \case+ MkSomeLeqNat a b ->+ case leqToCmp a b Witness of+ Left Refl -> fromSNat a === fromSNat b+ Right Refl ->+ property $ fromSNat a < fromSNat b+ , testProperty @(SomeSNat -> Property)+ "eqlCmpEQ terminates"+ $ \(SomeSNat n) ->+ totalRefl $ eqlCmpEQ n n Refl+ , testProperty @(SomeSNat -> Property)+ "eqToRefl terminates"+ $ \(SomeSNat n) ->+ totalRefl $ eqToRefl n n Refl+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "flipCmpNat terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ flipCmpNat n m+ , testProperty @(SomeSNat -> Property)+ "ltToNeq works as expected"+ $ \(SomeSNat n) ->+ givesImpossibleVoid $+ ltToNeq n n (unsafeCoerce $ Refl @()) Refl+ , testProperty @(SomeLeqNat -> Property)+ "leqNeqToLT terminates"+ $ \(MkSomeLeqNat n m) ->+ case n %~ m of+ Equal -> discard+ NonEqual ->+ totalRefl $ leqNeqToLT n m Witness (\case {})+ , testProperty @(SomeLeqNat -> Property)+ "succLeqToLT terminates"+ $ \(MkSomeLeqNat n' m) ->+ case n' of+ Succ n ->+ totalRefl $ succLeqToLT n m Witness+ _ -> discard+ , testProperty @(SomeLtNat -> Property)+ "ltToLeq terminates"+ $ \(MkSomeLtNat n m) ->+ totalWitness $ ltToLeq n m Refl+ , testProperty @(SomeGtNat -> Property)+ "gtToLeq terminates"+ $ \(MkSomeGtNat n m) ->+ totalWitness $ gtToLeq n m Refl+ , testCase "congFlipOrdering" $ do+ Refl <- evaluate (congFlipOrdering (Refl @( 'LT)))+ Refl <- evaluate (congFlipOrdering (Refl @( 'GT)))+ Refl <- evaluate (congFlipOrdering (Refl @( 'EQ)))+ pure ()+ , testProperty @(SomeLtNat -> Property) "ltToSuccLeq terminates" $ \(MkSomeLtNat n m) ->+ totalWitness $ ltToSuccLeq n m Refl+ , testProperty @(SomeSNat -> Property) "cmpZero terminates" $ \(SomeSNat n) ->+ totalRefl $ cmpZero n+ , testProperty @(SomeLeqNat -> Property) "leqToGT terminates" $ \(MkSomeLeqNat b0 a) ->+ case b0 of+ Succ b ->+ totalRefl $ leqToGT a b Witness+ Zero -> discard+ , testProperty @(SomeSNat -> Property) "cmpZero' works as expected" $ \(SomeSNat n) ->+ case n of+ Zero -> cmpZero' n === Left Refl+ Succ {} -> case cmpZero' n of+ Right Refl -> property True+ l -> counterexample ("Left Refl expected, but got: " <> show l) False+ , testProperty @(SomeSNat -> Property)+ "zeroNoLT works as expected"+ $ \(SomeSNat n) ->+ givesImpossibleVoid $ zeroNoLT n (unsafeCoerce $ Refl @())+ , testProperty @(SomeLtNat -> Property) "ltRightPredSucc terminates" $ \(MkSomeLtNat a b) ->+ totalRefl $ ltRightPredSucc a b Refl+ , testProperty @(SomeSNat -> SomeSNat -> Property) "cmpSucc terminates" $ \(SomeSNat a) (SomeSNat b) ->+ totalRefl $ cmpSucc a b+ , testProperty @(SomeSNat -> Property) "ltSucc terminates" $ \(SomeSNat a) ->+ totalRefl $ ltSucc a+ , testProperty @(SomeLtNat -> Property) "cmpSuccStepR terminates" $ \(MkSomeLtNat a b) ->+ totalRefl $ cmpSuccStepR a b Refl+ , testProperty @(SomeLtNat -> Property) "ltSuccLToLT terminates" $ \(MkSomeLtNat a0 b) ->+ case a0 of+ Succ a -> totalRefl $ ltSuccLToLT a b Refl+ Zero -> discard+ , testProperty @(SomeLeqNat -> Property) "leqToLT terminates" $ \(MkSomeLeqNat a0 b) ->+ case a0 of+ Succ a -> totalRefl $ leqToLT a b Witness+ Zero -> discard+ , testProperty @(SomeSNat -> Property) "leqZero terminates" $ \(SomeSNat n) ->+ totalWitness $ leqZero n+ , testProperty @(SomeLeqNat -> Property) "leqSucc terminates" $ \(MkSomeLeqNat n m) ->+ totalWitness $ leqSucc n m Witness+ , testProperty @(SomeLeqView -> Property) "fromLeqView terminates" $ \(MkSomeLeqView lview) ->+ totalWitness $ fromLeqView lview+ , testProperty @(SomeSNat -> Property) "leqViewRefl works properly" $ \(SomeSNat sn) ->+ case leqViewRefl sn of+ LeqZero sn' ->+ fromSNat sn' === fromSNat sn .&&. fromSNat sn' === 0+ LeqSucc sn' sm' Witness ->+ fromSNat sn' === fromSNat sm'+ .&&. fromSNat sn' + 1 === fromSNat sn+ , testProperty @(SomeLeqNat -> Property) "viewLeq works properly" $ \(MkSomeLeqNat sn sm) ->+ case viewLeq sn sm Witness of+ LeqZero sm' ->+ fromSNat sn === 0 .&&. fromSNat sm === fromSNat sm'+ LeqSucc sn' sm' Witness ->+ fromSNat sn' + 1 === fromSNat sn+ .&&. fromSNat sm' + 1 === fromSNat sm+ .&&. fromSNat sn' <= fromSNat sm'+ , testProperty @(SomeLeqNat -> Property) "leqWitness gives the difference as a witness" $+ \(MkSomeLeqNat sn sm) ->+ case leqWitness sn sm Witness of+ DiffNat sn' delta ->+ fromSNat sn === fromSNat sn'+ .&&. fromSNat sn' + fromSNat delta === fromSNat sm+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "leqStep terminates"+ $ \(SomeSNat n) (SomeSNat l) ->+ let m = n %+ l+ in totalWitness $ leqStep n m l Refl+ , testProperty @(SomeLeqNat -> Property) "leqNeqToSuccLeq terminates" $+ \(MkSomeLeqNat n m) ->+ case n %~ m of+ Equal -> discard+ NonEqual ->+ totalWitness $ leqNeqToSuccLeq n m Witness (\case {})+ , testProperty @(SomeSNat -> Property) "leqRefl terminates" $+ \(SomeSNat n) ->+ totalWitness $ leqRefl n+ , testProperty @(SomeLeqNat -> Property) "leqSuccStepR and leqSuccStepL terminates" $+ \(MkSomeLeqNat n m) ->+ totalWitness (leqSuccStepR n m Witness)+ .&&. case n of+ Succ n' ->+ label "leqSuccStepL tested" $+ totalWitness (leqSuccStepL n' m Witness)+ _ -> property True+ , testProperty @(SomeSNat -> Property) "leqReflexive terminates" $+ \(SomeSNat n) ->+ totalWitness $ leqReflexive n n Refl+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "leqTrans terminates" $+ \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat (l0 :: SNat lMinsM)) ->+ let l = m %+ l0+ in case m %<=? l of+ STrue ->+ totalWitness $+ leqTrans n m l Witness (Witness :: IsTrue (m <=? (m + lMinsM)))+ SFalse -> error "impossible"+ , testProperty @(SomeSNat -> Property) "leqAntisymm terminates" $+ \(SomeSNat n) ->+ totalRefl $ leqAntisymm n n Witness Witness+ , testProperty @(SomeLeqNat -> SomeLeqNat -> Property) "plusMonotone terminates" $+ \(MkSomeLeqNat n m) (MkSomeLeqNat l k) ->+ totalWitness $ plusMonotone n m l k Witness Witness+ , testCase "leqZeroElim terminates" $+ leqZeroElim (sNat @0) Witness @?= Refl+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneL terminates" $+ \(MkSomeLeqNat n m) (SomeSNat l) ->+ totalWitness $ plusMonotoneL n m l Witness+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneR terminates" $+ \(MkSomeLeqNat n m) (SomeSNat l) ->+ totalWitness $ plusMonotoneR l n m Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqL terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ plusLeqL n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqR terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ plusLeqR n m+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqL terminates" $+ \(MkSomeLeqNat (m :: SNat m) (l :: SNat l)) (SomeSNat n) ->+ totalWitness $+ plusCancelLeqR+ n+ m+ l+ (unsafeCoerce (Witness :: IsTrue (m <=? l)))+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqR terminates" $+ \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat l) ->+ totalWitness $+ plusCancelLeqR+ n+ m+ l+ (unsafeCoerce (Witness :: IsTrue (n <=? m)))+ , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd works properly" $ \(SomeSNat n) ->+ givesImpossibleVoid $ succLeqZeroAbsurd n (unsafeCoerce Witness)+ , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd' works properly" $ \(SomeSNat n) ->+ totalRefl $ succLeqZeroAbsurd' n+ , testProperty @(SomeSNat -> Property) "succLeqAbsurd works properly" $ \(SomeSNat n) ->+ givesImpossibleVoid $ succLeqAbsurd n (unsafeCoerce Witness)+ , testProperty @(SomeSNat -> Property) "succLeqAbsurd' works properly" $ \(SomeSNat n) ->+ totalRefl $ succLeqAbsurd' n+ , testProperty @(SomeGtNat -> Property)+ "notLeqToLeq terminates"+ $ \(MkSomeGtNat n m) ->+ case n %<=? m of+ STrue -> error "impossible!"+ SFalse ->+ totalWitness $ notLeqToLeq n m+ , testProperty+ @(SomeSNat -> SomeSNat -> Property)+ "leqSucc' terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ leqSucc' n m+ , testProperty @(SomeLeqNat -> Property) "leqToMin terminates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ leqToMin n m Witness+ , testProperty @(SomeLeqNat -> Property) "geqToMin terminates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ geqToMin m n Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "minComm terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ minComm n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqL terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ minLeqL n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqR terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ minLeqR n m+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "minLargest terminates" $+ \(MkSomeLeqNat l n) (SomeSNat lm) ->+ let m = l %+ lm+ in totalWitness $+ minLargest l n m Witness (unsafeCoerce Witness)+ , testProperty @(SomeLeqNat -> Property) "leqToMax termaxates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ leqToMax n m Witness+ , testProperty @(SomeLeqNat -> Property) "geqToMax termaxates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ geqToMax m n Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "maxComm termaxates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ maxComm n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqL termaxates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ maxLeqL n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqR termaxates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ maxLeqR n m+ , testProperty @(SomeLeqNat -> Property) "maxLeast termaxates" $+ \(MkSomeLeqNat n l) ->+ forAll (elements [0 .. fromSNat l]) $ \m0 ->+ case toSomeSNat m0 of+ SomeSNat m ->+ totalWitness $+ maxLeast l n m Witness (unsafeCoerce Witness)+ , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqSuccLeq terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ lneqSuccLeq n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqReversed terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ lneqReversed n m+ , testProperty @(SomeLneqNat -> Property) "lneqToLT terminates" $+ \(MkSomeLneqNat n m) ->+ totalRefl $ lneqToLT n m Witness+ , testProperty @(SomeLtNat -> Property) "ltToLneq terminates" $+ \(MkSomeLtNat n m) ->+ totalWitness $ ltToLneq n m Refl+ , testProperty @(SomeSNat -> Property) "lneqZero terminates" $+ \(SomeSNat n) -> totalWitness $ lneqZero n+ , testProperty @(SomeSNat -> Property) "lneqSucc terminates" $+ \(SomeSNat n) -> totalWitness $ lneqSucc n+ , testProperty @(SomeSNat -> SomeSNat -> Property) "succLneqSucc terminates" $+ \(SomeSNat n) (SomeSNat m) -> totalRefl $ succLneqSucc n m+ , testProperty @(SomeLneqNat -> Property) "lneqRightPredSucc terminates" $+ \(MkSomeLneqNat n m) ->+ totalRefl $ lneqRightPredSucc n m Witness+ , testProperty @(SomeLneqNat -> Property) "lneqSuccStepL and lneqSuccStepR works properly" $+ \(MkSomeLneqNat n m) ->+ conjoin+ [ totalWitness (lneqSuccStepR n m Witness)+ , case n of+ Succ n' ->+ label "lneqSuccStepL checked" $+ totalWitness (lneqSuccStepL n' m Witness)+ Zero -> property True+ ]+ , testProperty @(SomeLneqNat -> SomeLneqNat -> Property)+ "plusStrictMonotone terminates"+ $ \(MkSomeLneqNat n m) (MkSomeLneqNat l k) ->+ totalWitness $+ plusStrictMonotone n m l k Witness Witness+ , testProperty @(SomeSNat -> Property) "maxZeroL terminates" $+ \(SomeSNat n) -> totalRefl $ maxZeroL n+ , testProperty @(SomeSNat -> Property) "maxZeroR terminates" $+ \(SomeSNat n) -> totalRefl $ maxZeroR n+ , testProperty @(SomeSNat -> Property) "minZeroL terminates" $+ \(SomeSNat n) -> totalRefl $ minZeroL n+ , testProperty @(SomeSNat -> Property) "minZeroR terminates" $+ \(SomeSNat n) -> totalRefl $ minZeroR n+ , testProperty @(SomeLeqNat -> Property) "minusSucc terminates" $+ \(MkSomeLeqNat m n) ->+ totalRefl $ minusSucc n m Witness+ , testProperty @(SomeSNat -> Property) "lneqZeroAbsurd is absurd" $+ \(SomeSNat n) ->+ givesImpossibleVoid $+ lneqZeroAbsurd n $ unsafeCoerce Witness+ , testProperty @(SomeLeqNat -> Property)+ "minusPlus terminates"+ $ \(MkSomeLeqNat m n) ->+ totalRefl $+ minusPlus n m Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "minPlusTruncMinus terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ minPlusTruncMinus n m+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "truncMinusLeq terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ truncMinusLeq n m+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "leqOrdCond terminates"+ $ \(SomeSNat n) (SomeSNat m) -> totalRefl $ leqOrdCond n m+ , testProperty @(SomeSNat -> Property)+ "cmpSuccZeroGT terminates"+ $ \(SomeSNat n) -> totalRefl $ cmpSuccZeroGT n+ ]++totalWitness :: IsTrue p -> Property+totalWitness w =+ counterexample "Witness is not totalRefl!" $+ within+ 10000+ ( (case w of Witness -> True :: Bool) ::+ Bool+ )++totalRefl :: a :~: b -> Property+totalRefl = within 10000 . total
+ 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] $+ fromSNat (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 .&&. fromSNat (m %- n) === (natVal m - natVal n)+ , fromSNat (n %- m) === (natVal n - natVal m)+ ]+ , $(testBinaryP (>=) "(-)" ''(-) '(%-))+ , testProperty "(*), compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->+ tabulateDigits [natVal n, natVal m] $+ fromSNat (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)+ .||. fromSNat (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)+ .||. fromSNat (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] $+ fromSNat (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] $+ fromSNat (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)+ .||. fromSNat (sLog2 n) === fromIntegral (naturalLog2 (natVal n))+ , $(testUnary False "Log2" ''Log2 'sLog2)+ , testProperty "succ" $ \(SomeSNat n) ->+ tabulateDigits [natVal n] $+ fromSNat (sSucc n) === succ (natVal n)+ , $(testUnary True "Succ" ''Succ 'sSucc)+ , testProperty "pred" $ \(SomeSNat n) ->+ tabulateDigits [natVal n] $+ label "undefiend" (natVal n === 0)+ .||. fromSNat (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] $+ fromSNat (n `sMin` m) === (natVal n `min` natVal m)+ , $(testBinary "min" ''Min 'sMin)+ , testProperty "max" $ \(SomeSNat n) (SomeSNat m) ->+ tabulateDigits [natVal n, natVal m] $+ fromSNat (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,84 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# 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 = fromSNat++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,57 +1,114 @@+cabal-version: 3.0 name: type-natural-version: 0.7.1.4-cabal-version: >=1.10-build-type: Simple-license: BSD3+version: 1.3.0.2+license: BSD-3-Clause license-file: LICENSE-copyright: (C) Hiromi ISHII 2013-2014+copyright: (C) Hiromi ISHII 2013-2024 maintainer: konn.jinro_at_gmail.com+author: Hiromi ISHII+tested-with: ghc ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.4 || ==9.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__.+ Type-level natural numbers and proofs of their properties.+ category: Math-author: Hiromi ISHII-tested-with: GHC ==8.0.2 GHC ==8.2.2+build-type: Simple+extra-source-files: Changelog.md source-repository head- type: git- location: git://github.com/konn/type-natural.git+ type: git+ location: git://github.com/konn/type-natural.git library- - 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.Ordinal.Peano- Data.Type.Natural.Builtin- Data.Type.Natural.Class- Data.Type.Natural.Class.Arithmetic- Data.Type.Natural.Class.Order- build-depends:- base >=4 && <4.10,- equational-reasoning >=0.4.1.1 && <0.6,- monomorphic >=0.0.3 && <0.1,- template-haskell >=2.8 && <2.12,- constraints >=0.3 && <0.10,- ghc-typelits-natnormalise >=0.4 && <0.6,- ghc-typelits-presburger >=0.1.1 && <0.2,- singletons >=2.2 && <2.4- default-language: Haskell2010- default-extensions: DataKinds PolyKinds ConstraintKinds GADTs- ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators- MultiParamTypeClasses UndecidableInstances FlexibleContexts- FlexibleInstances- other-modules:- Data.Type.Natural.Definitions- Data.Type.Natural.Core- Data.Type.Natural.Compat- ghc-options: -Wall -O2 -fno-warn-orphans+ -- cabal-gild: discover src --exclude src/**/Core.hs --exclude src/**/Utils.hs --exclude src/Data/Type/Natural/Lemma/Presburger.hs+ exposed-modules:+ Data.Type.Natural+ Data.Type.Natural.Builtin+ Data.Type.Natural.Lemma.Arithmetic+ Data.Type.Natural.Lemma.Order+ Data.Type.Natural.Presburger.MinMaxSolver+ Data.Type.Ordinal+ Data.Type.Ordinal.Builtin + hs-source-dirs: src+ other-modules:+ Data.Type.Natural.Core+ Data.Type.Natural.Lemma.Presburger+ Data.Type.Natural.Utils++ default-language: Haskell2010+ default-extensions:+ ConstraintKinds+ DataKinds+ FlexibleContexts+ FlexibleInstances+ GADTs+ MultiParamTypeClasses+ PolyKinds+ ScopedTypeVariables+ TemplateHaskell+ TypeFamilies+ TypeOperators+ UndecidableInstances++ default-extensions: NoStarIsType+ ghc-options:+ -Wall+ -Wno-orphans+ -Wno-redundant-constraints++ build-depends:+ base >=4 && <5,+ constraints >=0.3,+ equational-reasoning >=0.4.1.1,+ ghc,+ ghc-typelits-knownnat,+ ghc-typelits-natnormalise >=0.4,+ integer-logarithms,+ template-haskell >=2.8,++ if impl(ghc >=9.8.4)+ build-depends: ghc-typelits-presburger >=0.7.4.1+ else+ if impl(ghc >=9.8)+ build-depends: ghc-typelits-presburger >=0.7.3+ else+ if impl(ghc >=9.6)+ build-depends: ghc-typelits-presburger >=0.7.2+ else+ if impl(ghc >=9.4)+ build-depends: ghc-typelits-presburger >=0.7.1+ else+ build-depends: ghc-typelits-presburger++test-suite type-natural-test+ type: exitcode-stdio-1.0+ main-is: test.hs+ build-tool-depends: tasty-discover:tasty-discover+ hs-source-dirs: tests+ default-language: Haskell2010+ ghc-options: -Wall+ other-modules:+ Data.Type.Natural.Lemma.OrderSpec+ Data.Type.Natural.Presburger.Cases+ Data.Type.Natural.Presburger.MinMaxSolverSpec+ Data.Type.NaturalSpec+ Data.Type.NaturalSpec.TH+ Data.Type.OrdinalSpec+ Shared++ build-depends:+ QuickCheck,+ base,+ equational-reasoning,+ integer-logarithms,+ quickcheck-instances,+ tasty,+ tasty-discover,+ tasty-hunit,+ tasty-quickcheck,+ template-haskell,+ type-natural,++ default-extensions: NoStarIsType