packages feed

type-natural 0.4.2.0 → 1.3.0.2

raw patch · 26 files changed

Files

+ 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,520 +0,0 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables                 #-}-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies          #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, EmptyCase, LambdaCase #-}--- | 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,-                          LeqTrueInstance, propToBoolLeq,-                          -- * Conversion functions-                          natToInt, intToNat, sNatToInt,-                          -- * Quasi quotes for natural numbers-                          nat, snat,-                          -- * Properties of natural numbers-                          succCongEq, eqPreservesS, succCong, plusCongR, plusCongL,-                          succPlusL, plusSuccL, succPlusR, plusSuccR,-                          plusZR, plusZL, plusAssociative, plusAssoc,-                          multAssociative, multAssoc, multComm, multZL, multZR, multOneL,-                          multOneR, snEqZAbsurd, succInjective, succInj,-                          plusInjectiveL, plusInjectiveR,-                          plusMultDistr, plusMultDistrib, multPlusDistr, multPlusDistrib,-                          multCongL, multCongR,-                          sAndPlusOne, succAndPlusOneR,-                          plusComm, plusCommutative, minusCongEq, minusCongL,-                          minusNilpotent,-                          eqSuccMinus, plusMinusEqL, plusMinusEqR,-                          zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL,-                          leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,-                          -- * Properties of ordering 'Leq'-                          leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,-                          minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR,-                          leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd,-                          -- * 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.Compat-import Data.Type.Natural.Core-import Data.Type.Natural.Definitions hiding ((:<=))--import           Data.Singletons-import qualified Data.Singletons.Prelude as S-import           Data.Type.Monomorphic-import           Language.Haskell.TH-import           Language.Haskell.TH.Quote-import           Prelude                   (Bool (..), Eq (..), Int,-                                            Integral (..), Ord ((<)), error,-                                            otherwise, ($), (.))-import           Prelude                   (Ord (..))-import qualified Prelude                   as P-import           Proof.Equational-import Data.Constraint (Dict(..))------------------------------------------------------- * Conversion functions.------------------------------------------------------- | Convert integral numbers into 'Nat'-intToNat :: (Integral a, Ord a) => a -> Nat-intToNat 0 = Z-intToNat n-    | n < 0     = error "negative integer"-    | otherwise = S $ intToNat (n P.- 1)---- | Convert 'Nat' into normal integers.-natToInt :: Integral n => Nat -> n-natToInt Z     = 0-natToInt (S n) = natToInt n P.+ 1---- | Convert 'SNat n' into normal integers.-sNatToInt :: P.Num n => SNat x -> n-sNatToInt SZ     = 0-sNatToInt (SS n) = sNatToInt n P.+ 1--instance Monomorphicable (Sing :: Nat -> *) where-  type MonomorphicRep (Sing :: Nat -> *) = Int-  demote  (Monomorphic sn) = sNatToInt sn-  promote n-      | n < 0     = error "negative integer!"-      | n == 0    = Monomorphic SZ-      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn------------------------------------------------------- * Properties----------------------------------------------------plusZR :: SNat n -> n :+: 'Z :=: n-plusZR SZ     = Refl-plusZR (SS n) =- start (SS n %+ SZ)-   =~= SS (n %+ SZ)-   === SS n          `because` cong' SS (plusZR n)--plusZL :: SNat n -> 'Z :+: n :=: n-plusZL _ = Refl--succCong, succCongEq, eqPreservesS :: n :=: m -> 'S n :=: 'S m-succCong Refl = Refl-succCongEq = succCong-{-# DEPRECATED succCongEq "Will be removed in @0.5.0.0@. Use @'succCong'@ instead." #-}-eqPreservesS = succCong-{-# DEPRECATED eqPreservesS "Will be removed in @0.5.0.0@. Use @'succCong'@ instead." #-}--snEqZAbsurd :: 'S n :=: 'Z -> a-snEqZAbsurd _ = bugInGHC--succInj, succInjective :: 'S n :=: 'S m -> n :=: m-succInj Refl = Refl-succInjective = succInj-{-# DEPRECATED succInjective "Will be removed in @0.5.0.0@. \-                              Use @'succInj'@ instead." #-}--plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l-plusInjectiveL SZ     _ _ Refl = Refl-plusInjectiveL (SS n) m l eq   = plusInjectiveL n m l $ succInjective eq--plusInjectiveR :: SNat n -> SNat m -> SNat l -> n :+ l :=: m :+ l -> n :=: m-plusInjectiveR n m l eq = plusInjectiveL l n m $-  start (l %:+ n)-    === n %:+ l   `because` plusCommutative l n-    === m %:+ l   `because` eq-    === l %:+ m   `because` plusCommutative m l--succAndPlusOneR, sAndPlusOne :: SNat n -> 'S n :=: n :+: One-succAndPlusOneR SZ = Refl-succAndPlusOneR (SS n) =-  start (SS (SS n))-    === SS (n %+ sOne) `because` cong' SS (succAndPlusOneR n)-    =~= SS n %+ sOne-sAndPlusOne = succAndPlusOneR-{-# DEPRECATED sAndPlusOne "Will be removed in @0.5.0.0@. Use @'succAndPlusOneR'@ instead." #-}--plusAssoc, plusAssociative :: SNat n -> SNat m -> SNat l-                -> n :+: (m :+: l) :=: (n :+: m) :+: l-plusAssoc SZ     _ _ = Refl-plusAssoc (SS n) m l =-  start (SS n %+ (m %+ l))-    =~= SS (n %+ (m %+ l))-    === SS ((n %+ m) %+ l)  `because` cong' SS (plusAssoc n m l)-    =~= SS (n %+ m) %+ l-    =~= (SS n %+ m) %+ l-plusAssociative = plusAssoc-{-# DEPRECATED plusAssociative "Will be removed in @0.5.0.0@. Use @'plusAssoc'@ instead." #-}--plusSR :: SNat n -> SNat m -> 'S (n :+: m) :=: n :+: 'S m-plusSR n m =-  start (SS (n %+ m))-    === (n %+ m) %+ sOne `because` succAndPlusOneR (n %+ m)-    === n %+ (m %+ sOne) `because` symmetry (plusAssoc n m sOne)-    === n %+ SS m        `because` plusCongL n (symmetry $ succAndPlusOneR m)--{-# DEPRECATED plusSR "Will be removed in @0.5.0.0@. Use @'plusSuccR'@ instead." #-}---plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'-plusCongL _ Refl = Refl--plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n-plusCongR _ Refl = Refl--plusSuccL, succPlusL :: SNat n -> SNat m -> 'S n :+ m :=: 'S (n :+ m)-plusSuccL _ _ = Refl-succPlusL = plusSuccL-{-# DEPRECATED succPlusL "Will be removed in @0.5.0.0@. Use @'plusSuccL'@ instead." #-}--plusSuccR, succPlusR :: SNat n -> SNat m -> n :+ 'S m :=: 'S (n :+ m)-plusSuccR SZ     _ = Refl-plusSuccR (SS n) m =-  start (SS n %+ SS m)-    =~= SS (n %+ SS m)-    === SS (SS (n %+ m)) `because` succCong (plusSuccR n m)-    =~= SS (SS n %+ m)--succPlusR = plusSuccR--{-# DEPRECATED succPlusR "Will be removed in @0.5.0.0@. Use @'plusSuccR'@ instead." #-}---minusCongEq, minusCongL :: n :=: m -> SNat l -> n :-: l :=: m :-: l-minusCongL Refl _ = Refl-minusCongEq = minusCongL-{-# DEPRECATED minusCongEq "Will be removed in @0.5.0.0@. Use @'minusCongL'@ instead." #-}--minusNilpotent :: SNat n -> n :-: n :=: Zero-minusNilpotent SZ = Refl-minusNilpotent (SS n) =-  start (SS n %:- SS n)-    =~= n %:- n-    === SZ     `because` minusNilpotent n---plusComm, plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n-plusComm SZ SZ     = Refl-plusComm SZ (SS m) =-  start (SZ %+ SS m)-    =~= SS m-    === SS (m %+ SZ) `because` cong' SS (plusCommutative SZ m)-    =~= SS m %+ SZ-plusComm (SS n) m =-  start (SS n %+ m)-    =~= SS (n %+ m)-    === SS (m %+ n)      `because` cong' SS (plusCommutative n m)-    === (m %+ n) %+ sOne `because` succAndPlusOneR (m %+ n)-    === m %+ (n %+ sOne) `because` symmetry (plusAssoc m n sOne)-    === m %+ SS n        `because` plusCongL m (symmetry $ succAndPlusOneR n)--plusCommutative = plusComm-{-# DEPRECATED plusCommutative "Will be removed in @0.5.0.0@. Use @'plusComm'@ instead." #-}--eqSuccMinus :: ((m S.:<= n) ~ 'True)-            => SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m))-eqSuccMinus _      SZ     = Refl-eqSuccMinus (SS n) (SS m) =-  start (SS (SS n) %:- SS m)-    =~= SS n %:- m-    === SS (n %:- m)       `because` eqSuccMinus n m-    =~= SS (SS n %:- SS m)-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-eqSuccMinus _ _ = bugInGHC-#endif---plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n-plusMinusEqL SZ     m = minusNilpotent m-plusMinusEqL (SS n) m =-  case propToBoolLeq (plusLeqR n m) of-    Dict -> transitivity (eqSuccMinus (n %+ m) m) (succCong $ plusMinusEqL n m)--plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n-plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)--zAbsorbsMinR :: SNat n -> Min n 'Z :=: 'Z-zAbsorbsMinR SZ     = Refl-zAbsorbsMinR (SS n) =-  case zAbsorbsMinR n of-    Refl -> Refl--zAbsorbsMinL :: SNat n -> Min 'Z n :=: 'Z-zAbsorbsMinL SZ     = Refl-zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl--minComm :: SNat n -> SNat m -> Min n m :=: Min m n-minComm SZ     SZ = Refl-minComm SZ     (SS _) = Refl-minComm (SS _) SZ = Refl-minComm (SS n) (SS m) = case minComm n m of Refl -> Refl--maxZL :: SNat n -> Max 'Z n :=: n-maxZL SZ = Refl-maxZL (SS _) = Refl--maxComm :: SNat n -> SNat m -> (Max n m) :=: (Max m n)-maxComm SZ SZ = Refl-maxComm SZ (SS _) = Refl-maxComm (SS _) SZ = Refl-maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl--maxZR :: SNat n -> Max n 'Z :=: n-maxZR n = transitivity (maxComm n SZ) (maxZL n)--multPlusDistr, multPlusDistrib :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l)-multPlusDistrib SZ     _ _ = Refl-multPlusDistrib (SS (n :: SNat n')) m l =-  start (SS n %* (m %+ l))-    =~= (n %* (m %+ l)) %+ (m %+ l)-    === ((n %* m) %+ (n %* l)) %+ (m %+ l)-        `because` plusCongR (m %+ l) (multPlusDistrib n m l :: n' :* (m :+ l) :=: (n' :* m) :+ (n' :* l))-    === (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)-    === n %* m %+ (n %*l %+ (l %+ m))    `because` symmetry (plusAssoc (n %* m) (n %* l) (l %+ m))-    === n %* l %+ (l %+ m) %+ n %* m     `because` plusCommutative (n %* m) (n %*l %+ (l %+ m))-    === (n %* l %+ l) %+ m %+ n %* m     `because` plusCongR (n %* m) (plusAssoc (n %* l) l m)-    =~= (SS n %* l)   %+ m %+ n %* m-    === (SS n %* l)   %+ (m %+ (n %* m)) `because` symmetry (plusAssoc (SS n %* l) m (n %* m))-    === (SS n %* l)   %+ ((n %* m) %+ m) `because` plusCongL (SS n %* l) (plusCommutative m (n %* m))-    =~= (SS n %* l)   %+ (SS n %* m)-    === (SS n %* m)   %+ (SS n %* l)     `because` plusCommutative (SS n %* l) (SS n %* m)-multPlusDistr = multPlusDistrib-{-# DEPRECATED multPlusDistr "Will be removed in @0.5.0.0@. Use @'multPlusDistrib'@ instead." #-}--plusMultDistr, plusMultDistrib :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l)-plusMultDistrib SZ _ _ = Refl-plusMultDistrib (SS n) m l =-  start ((SS n %+ m) %* l)-    =~= SS (n %+ m) %* l-    =~= (n %+ m) %* l %+ l-    === n %* l  %+  m %* l  %+  l   `because` plusCongR l (plusMultDistrib n m l)-    === m %* l  %+  n %* l  %+  l   `because` plusCongR l (plusCommutative (n %* l) (m %* l))-    === m %* l  %+ (n %* l  %+  l)  `because` symmetry (plusAssoc (m %* l) (n %*l) l)-    =~= m %* l  %+ (SS n %* l)-    === (SS n %* l)  %+  (m %* l)   `because` plusCommutative (m %* l) (SS n %* l)--plusMultDistr = plusMultDistrib-{-# DEPRECATED plusMultDistr "Will be removed in @0.5.0.0@. Use @'plusMultDistrib'@ instead." #-}--multAssoc, multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l-multAssoc SZ     _ _ = Refl-multAssoc (SS n) m l =-  start (SS n %* (m %* l))-    =~= n %* (m %* l) %+ (m %* l)-    === (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssoc n m l)-    === (n %* m %+ m) %* l        `because` symmetry (plusMultDistrib (n %* m) m l)-    =~= (SS n %* m) %* l-multAssociative = multAssoc-{-# DEPRECATED multAssociative "Will be removed in @0.5.0.0@. Use @'multAssoc'@ instead." #-}-multZL :: SNat m -> Zero :* m :=: Zero-multZL _ = Refl--multZR :: SNat m -> m :* Zero :=: Zero-multZR SZ = Refl-multZR (SS n) =-  start (SS n %* SZ)-    =~= n %* SZ %+ SZ-    === SZ %+ SZ      `because` plusCongR SZ (multZR n)-    =~= SZ--multOneL :: SNat n -> One :* n :=: n-multOneL n =-  start (sOne %* n)-    =~= sZero %* n %+ n-    =~= sZero %:+ n-    =~= n--multOneR :: SNat n -> n :* One :=: n-multOneR SZ = Refl-multOneR (SS n) =-  start (SS n %* sOne)-    =~= n %* sOne %+ sOne-    === n %+ sOne         `because` plusCongR sOne (multOneR n)-    === SS n              `because` symmetry (succAndPlusOneR n)--multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l-multCongL _ Refl = Refl--multCongR :: SNat n -> m :=: l -> m :* n :=: l :* n-multCongR _ Refl = Refl--multComm :: SNat n -> SNat m -> n :* m :=: m :* n-multComm SZ m =-  start (SZ %* m)-    =~= SZ-    === m %* SZ `because` symmetry (multZR m)-multComm (SS n) m =-  start (SS n %* m)-    =~= n %* m %+ m-    === m %* n %+ m          `because` plusCongR m (multComm n m)-    === m %* n %+ m %* sOne  `because` plusCongL (m %* n) (symmetry $ multOneR m)-    === m %* (n %+ sOne)     `because` symmetry (multPlusDistrib m n sOne)-    === m %* SS n            `because` multCongL m (symmetry $ succAndPlusOneR n)--plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: 'Z-plusNeutralR SZ m eq =-  start m-    =~= SZ %:+ m-    === SZ       `because` eq-plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq--plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: 'Z-plusNeutralL n m eq = plusNeutralR m n $-  start (m %:+ n)-    === n %:+ m   `because` plusCommutative m n-    === m         `because` eq------------------------------------------------------- * Properties of 'Leq'-----------------------------------------------------leqRefl :: SNat n -> Leq n n-leqRefl SZ = ZeroLeq SZ-leqRefl (SS n) = SuccLeqSucc $ leqRefl n--leqSucc :: SNat n -> Leq n ('S n)-leqSucc SZ = ZeroLeq sOne-leqSucc (SS n) = SuccLeqSucc $ leqSucc n--leqTrans :: Leq n m -> Leq m l -> Leq n l-leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq-leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-leqTrans _ _ = error "impossible!"-#endif--instance Preorder Leq where-  reflexivity = leqRefl-  transitivity = leqTrans--plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)-plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)-plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =-  case sym $ plusSuccR m (leqRhs leq) of-    Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq-plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'--plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)-plusLeqL SZ     m = ZeroLeq $ coerce (symmetry $ plusZL m) m-plusLeqL (SS n) m =-  start (SS n)-    =<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)-    =~= SS n %+ m--plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)-plusLeqR n m =-  case plusCommutative n m of-    Refl -> plusLeqL m n--minLeqL :: SNat n -> SNat m -> Leq (Min n m) n-minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq SZ-minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n-minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)--minLeqR :: SNat n -> SNat m -> Leq (Min n m) m-minLeqR n m = case minComm n m of Refl -> minLeqL m n--leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m-leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl-leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = succCong $ leqAnitsymmetric leq1 leq2-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-leqAnitsymmetric _ _ = error "impossible!"-#endif--maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)-maxLeqL SZ m = ZeroLeq (sMax SZ m)-maxLeqL n SZ = case maxZR n of-                 Refl -> leqRefl n-maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m--maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)-maxLeqR n m = case maxComm n m of-                Refl -> maxLeqL m n--leqSnZAbsurd :: Leq ('S n) 'Z -> a-leqSnZAbsurd = \case {}--leqnZElim :: Leq n 'Z -> n :=: 'Z-leqnZElim (ZeroLeq SZ) = Refl--leqSnLeq :: Leq ('S n) m -> Leq n m-leqSnLeq (SuccLeqSucc leq) =-  let n = leqLhs leq-      m = SS $ leqRhs leq-  in start n-       =<= SS n   `because` leqSucc n-       =<= m      `because` SuccLeqSucc leq-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-leqSnLeq _ = bugInGHC-#endif--leqPred :: Leq ('S n) ('S m) -> Leq n m-leqPred (SuccLeqSucc leq) = leq-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-leqPred _ = bugInGHC-#endif--leqSnnAbsurd :: Leq ('S n) n -> a-leqSnnAbsurd (SuccLeqSucc leq) =-  case leqLhs leq of-    SS _ -> leqSnnAbsurd leq-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-    _    -> bugInGHC "cannot be occured"-leqSnnAbsurd _ = bugInGHC-#endif------------------------------------------------------- * Quasi Quoter------------------------------------------------------- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type.------   for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@-nat :: QuasiQuoter-nat = QuasiQuoter { quoteExp = P.foldr appE (conE 'Z) . P.flip P.replicate (conE 'S) . P.read-                  , quotePat = P.foldr (\a b -> conP a [b]) (conP 'Z []) . P.flip P.replicate 'S . P.read-                  , quoteType = P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read-                  , quoteDec = error "not implemented"-                  }---- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.------  For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@-snat :: QuasiQuoter-snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read-                   , quotePat = P.foldr (\a b -> conP a [b]) (conP 'SZ []) . P.flip P.replicate 'SS . P.read-                   , quoteType = appT (conT ''SNat) . P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read-                   , quoteDec = error "not implemented"-                   }
− Data/Type/Natural/Builtin.hs 
@@ -1,329 +0,0 @@-{-# LANGUAGE ConstraintKinds, CPP, DataKinds, GADTs, PolyKinds, RankNTypes #-}-{-# LANGUAGE TypeFamilies, TypeOperators, 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'@-         plusZR, plusZL, plusSuccR, plusSuccL,-         multZR, multZL, multSuccR, multSuccL,-         inductionNat,-         plusComm, multComm, plusAssoc, multAssoc,-         plusMultDistr, multPlusDistr-       )-       where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Type.Natural.Compat-#endif--import Data.Promotion.Prelude.Enum (Succ)-import           Data.Singletons              (Sing, SingI, sing)-import           Data.Singletons.Decide       (Decision (..), (%~))-import           Data.Singletons.Decide       (Void)-import           Data.Singletons.Prelude.Bool (Sing (..))-import           Data.Singletons.Prelude.Ord  (POrd(..), SOrd ((%:<=)))-import           Data.Singletons.Prelude.Enum (Pred, sPred, sSucc)-import           Data.Singletons.Prelude.Num  (SNum (..))-import           Data.Type.Natural            (Nat (S, Z), Sing (SS, SZ))-import           Data.Type.Natural            (plusCongR)-import qualified Data.Type.Natural            as PN-import           Data.Void                    (absurd)-import qualified GHC.TypeLits                 as TL-import           Proof.Equational             ((:=:), (:~:) (Refl), coerce)-import           Proof.Equational             (start, sym, (===), (=~=))-import           Proof.Equational             (because)-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))--data NatView (n :: TL.Nat) where-  IsZero :: NatView 0-  IsSucc :: Sing n -> NatView (Succ n)--viewNat :: Sing n -> NatView n-viewNat n =-  case n %~ (sing :: Sing 0) of-    Proved Refl -> IsZero-    Disproved _ -> 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 Refl  -> 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` PN.succCong (toFromPeano sn)--congFromPeano :: n :=: m -> FromPeano n :=: FromPeano m-congFromPeano Refl = Refl--congToPeano :: n :=: m -> ToPeano n :=: ToPeano m-congToPeano Refl = Refl--congSucc :: n :=: m -> Succ n :=: Succ m-congSucc Refl = Refl--fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n-fromToPeano sn  =-  case viewNat sn of-    IsZero    -> Refl-    IsSucc n1 ->-      start (sFromPeano (sToPeano sn))-        =~= sFromPeano (sToPeano (sSucc n1))-        === sFromPeano (SS (sToPeano n1))-              `because` congFromPeano (toPeanoSuccCong n1)-        =~= sSucc (sFromPeano (sToPeano n1))-        === sSucc n1 `because` congSucc (fromToPeano n1)--fromPeanoInjective :: forall n m. (SingI n, SingI m)-                   => FromPeano n :=: FromPeano m -> n :=: m-fromPeanoInjective frEq =-  let sn = sing :: Sing n-      sm = sing :: Sing m-  in start sn-       === sToPeano (sFromPeano sn) `because` sym (toFromPeano sn)-       === sToPeano (sFromPeano sm) `because` congToPeano frEq-       === sm                       `because` toFromPeano sm--fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :=: Succ (FromPeano n)-fromPeanoSuccCong _sn = Refl--fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :=: FromPeano n TL.+ FromPeano m-fromPeanoPlusCong SZ _ = Refl-fromPeanoPlusCong (SS sn) sm =-  start (sFromPeano (SS sn %:+ sm))-    =~= sFromPeano (SS (sn %:+ sm))-    === sSucc (sFromPeano (sn %:+ sm))           `because` fromPeanoSuccCong (sn %:+ sm)-    === sSucc (sFromPeano sn  %:+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm)-    =~= sSucc (sFromPeano sn) %:+ sFromPeano sm-    =~= sFromPeano (SS sn)    %:+ sFromPeano sm--toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n TL.+ m) :=: ToPeano n PN.:+ ToPeano m-toPeanoPlusCong sn sm =-  case viewNat sn of-    IsZero -> Refl-    IsSucc pn ->-      start (sToPeano (sSucc pn %:+ sm))-        =~= sToPeano (sSucc (pn %:+ sm))-        === SS (sToPeano (pn %:+ sm))-            `because` toPeanoSuccCong (pn %:+ sm)-        === SS (sToPeano pn %:+ sToPeano sm)-            `because` PN.succCong (toPeanoPlusCong pn sm)-        =~= SS (sToPeano pn) %:+ sToPeano sm-        === (sToPeano (sSucc pn) %:+ sToPeano sm)-            `because` plusCongR (sToPeano sm) (sym (toPeanoSuccCong pn))-        =~= sToPeano sn %:+ sToPeano sm--fromPeanoZeroCong :: FromPeano 'Z :=: 0-fromPeanoZeroCong = Refl--toPeanoZeroCong :: ToPeano 0 :=: 'Z-toPeanoZeroCong = Refl--fromPeanoOneCong :: FromPeano PN.One :=: 1-fromPeanoOneCong = Refl--toPeanoOneCong :: ToPeano 1 :=: PN.One-toPeanoOneCong = Refl--natPlusCongR :: Sing r -> n :=: m -> n TL.+ r :=: m TL.+ r-natPlusCongR _ Refl = Refl--fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :=: FromPeano n TL.* FromPeano m-fromPeanoMultCong SZ _ = Refl-fromPeanoMultCong (SS psn) sm =-  start (sFromPeano (SS psn %:* sm))-    =~= sFromPeano (psn %:* sm %:+ sm)-    === sFromPeano (psn %:* sm) %:+ sFromPeano sm-        `because` fromPeanoPlusCong (psn %:* sm) sm-    === sFromPeano psn %:* sFromPeano sm %:+ sFromPeano sm-        `because` natPlusCongR (sFromPeano sm) (fromPeanoMultCong psn sm)-    =~= sSucc (sFromPeano psn) %:* sFromPeano sm-    =~= sFromPeano (SS psn)    %:* sFromPeano sm---toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n 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` plusCongR (sToPeano sm) (toPeanoMultCong psn sm)-        =~= SS (sToPeano psn) %:* sToPeano sm-        === sToPeano (sSucc psn) %:* sToPeano sm-            `because` PN.multCongR (sToPeano sm) (sym (toPeanoSuccCong psn))--infix 4 %:<=?-(%:<=?) :: Sing n -> Sing m -> Sing (n TL.<=? m)-sn %:<=? sm =-  case viewNat sn of-    IsZero -> STrue-    IsSucc pn -> case viewNat sm of-      IsZero -> SFalse-      IsSucc pm ->-        case pn %:<=? pm of-          STrue  -> STrue-          SFalse -> SFalse--natLeqSuccEq :: Sing n -> Sing m -> ((n TL.+ 1) TL.<=? (m TL.+ 1)) :~: (n TL.<=? m)-natLeqSuccEq _ _ = Refl--leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? 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 TL.<=? FromPeano m) :=: 'True-fromPeanoMonotone SZ _ = Refl-fromPeanoMonotone (SS n) (SS m) =-   start (sFromPeano (SS n) %:<=? sFromPeano (SS m))-     === (sSucc (sFromPeano n) %:<=? sSucc (sFromPeano m))-      `because` leqqCong  (fromPeanoSuccCong n) (fromPeanoSuccCong m)-     === (sFromPeano n %:<=? sFromPeano m)-      `because` natLeqSuccEq (sFromPeano n) (sFromPeano m)-     === STrue-      `because` fromPeanoMonotone n m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-fromPeanoMonotone _ _ = bugInGHC-#endif--natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0-natLeqZero _ = Refl---- | 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 TL.<= m)-                => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True-toPeanoMonotone sn sm =-  case sn %~ (sing :: Sing 0) of-    Proved Refl -> Refl-    Disproved nPos -> case sm %~ (sing :: Sing 0) of-      Proved Refl -> absurd $ nPos $ natLeqZero sm-      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 TL.+ 1)) -> Sing n -> p n-inductionNat base step snat =-  case viewNat snat of-    IsZero -> base-    IsSucc sl -> step (inductionNat base step sl)--plusZR :: Sing n -> n TL.+ 0 :~: n-plusZR _ = Refl--plusZL :: Sing n -> 0 TL.+ n :~: n-plusZL _ = Refl--plusSuccL :: Sing n -> Sing m -> (Succ n) TL.+ m :~: Succ (n TL.+ m)-plusSuccL _ _ =  Refl--plusSuccR :: Sing n -> Sing m -> n TL.+ (Succ m) :~: Succ (n TL.+ m)-plusSuccR _ _ =  Refl--multZL :: Sing n -> 0 TL.* n :~: 0-multZL _ = Refl--multZR :: Sing n -> n TL.* 0 :~: 0-multZR _ = Refl--multSuccL :: Sing n -> Sing m -> Succ n TL.* m :~: (n TL.* m) TL.+ m-multSuccL _ _ = Refl--multSuccR :: Sing n -> Sing m -> n TL.* Succ m :~: (n TL.* m) TL.+ n-multSuccR _ _ = Refl--plusComm :: Sing n -> Sing m -> (n TL.+ m) :~: (m TL.+ n)-plusComm _ _ = Refl--multComm :: Sing n -> Sing m -> (n TL.* m) :~: (m TL.* n)-multComm _ _ = Refl--plusAssoc :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.+ l :~: n TL.+ (m TL.+ l)-plusAssoc _ _ _ = Refl--multAssoc :: Sing n -> Sing m -> Sing l -> (n TL.* m) TL.* l :~: n TL.* (m TL.* l)-multAssoc _ _ _ = Refl--plusMultDistr :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.* l :~: n TL.* l TL.+  m TL.* l-plusMultDistr _ _ _ = Refl--multPlusDistr :: Sing n -> Sing m -> Sing l -> n TL.* (m TL.+ l) :~: n TL.* m TL.+  n TL.* l-multPlusDistr _ _ _ = Refl
− 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,97 +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 qualified Data.Singletons.Prelude       as S-import           Data.Type.Natural.Definitions hiding ((:<=))-import           Prelude                       (Bool (..), Eq (..), Show (..),-                                                ($))-import           Unsafe.Coerce------------------------------------------------------- ** Type-level predicate & judgements.------------------------------------------------------ | Comparison via type-class.-class (n :: Nat) :<= (m :: Nat)-instance 'Z :<= n-instance (n :<= m) => 'S n :<= 'S m-{-# DEPRECATED (:<=) "This class will be removed in 0.5.0.0. Use @(n 'Data.Singletons.Prelude.Ord.:<=' m) ~ 'True@ instead" #-}---- | Comparison via GADTs.-data Leq (n :: Nat) (m :: Nat) where-  ZeroLeq     :: SNat m -> Leq Zero m-  SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m)--type LeqTrueInstance a b = Dict ((a S.:<= b) ~ 'True)--(%-) :: (m S.:<= 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 S.:<= 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 = Dict (n :<= m)--boolToPropLeq :: (n S.:<= 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,174 +0,0 @@-{-# LANGUAGE DataKinds, DeriveDataTypeable, FlexibleContexts        #-}-{-# LANGUAGE FlexibleInstances, GADTs, InstanceSigs, KindSignatures #-}-{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude, PolyKinds    #-}-{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving    #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators           #-}-{-# LANGUAGE UndecidableInstances                                   #-}-module Data.Type.Natural.Definitions-       (module Data.Type.Natural.Definitions,-        module Data.Singletons.Prelude-       ) where-import           Data.Singletons.Prelude-import           Data.Singletons.TH      (singletons)-import           Data.Typeable           (Typeable)-import           Prelude                 (Num (..), Ord (..))-import           Prelude                 (Bool (..), Eq (..), Show (..))-import qualified Prelude                 as P--------------------------------------------------------- * 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 P.Ord Nat where-     Z   <= _   = True-     S _ <= Z   = False-     S n <= S m = n <= m--     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 P.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))- |]--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- |]---- | Boolean-valued type-level comparison function.-{-# DEPRECATED (<<=) "Use @'Ord'@ instance instead." #-}-(<<=) :: Nat -> Nat -> Bool-(<<=) = (<=)--{-# DEPRECATED (:<<=) "Use @'(:<=)'@ from @'POrd'@ instead." #-}-type n :<<= m = n :<= m--{-# DEPRECATED (%:<<=) "Use @'(%:<=)'@ from @'POrd'@ instead." #-}-(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)-(%:<<=) = (%:<=)--type (:<<=$) = (:<=$)-{-# DEPRECATED (:<<=$) "Use @(':<=$')@ instead." #-}--type (:<<=$$) = (:<=$$)-{-# DEPRECATED (:<<=$$) "Use @(':<=$$')@ instead." #-}--type (:<<=$$$) n m = (:<=$$$) n m-{-# DEPRECATED (:<<=$$$) "Use @(':<=$$$')@ instead." #-}
− Data/Type/Ordinal.hs 
@@ -1,195 +0,0 @@-{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls   #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures      #-}-{-# LANGUAGE LambdaCase, PolyKinds, ScopedTypeVariables, StandaloneDeriving  #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                    #-}--- | Set-theoretic ordinal arithmetic-module Data.Type.Ordinal-       ( -- * Data-types-         Ordinal (..),-         -- * Conversion from cardinals to ordinals.-         sNatToOrd', sNatToOrd, ordToInt, ordToSNat,-         ordToSNat', CastedOrdinal(..),-         unsafeFromInt, inclusion, inclusion',-         -- * Ordinal arithmetics-         (@+), enumOrdinal,-         -- * Elimination rules for @'Ordinal' 'Z'@.-         absurdOrd, vacuousOrd, vacuousOrdM,-         -- * Quasi Quoter-         od-       ) where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Type.Natural.Compat-#endif--import Control.Monad             (liftM)-import Data.Singletons.Prelude-import Data.Type.Monomorphic-import Data.Type.Natural-import Data.Constraint(Dict(..))-import Data.Typeable             (Typeable)-import Language.Haskell.TH-import Language.Haskell.TH.Quote-import Unsafe.Coerce-import qualified Data.Singletons.Prelude as S---- | Set-theoretic (finite) ordinals:------ > n = {0, 1, ..., n-1}------ So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@.-data Ordinal n where-  OZ :: Ordinal ('S n)-  OS :: Ordinal n -> Ordinal ('S n)---- | Since 0.2.3.0-deriving instance Typeable Ordinal--- | Parsing always fails, because there are no inhabitant.-instance Read (Ordinal 'Z) where-  readsPrec _ _ = []--instance SingI n => Num (Ordinal n) where-  _ + _ = 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 . fromInteger--deriving instance Read (Ordinal n) => Read (Ordinal ('S n))-deriving instance Show (Ordinal n)-deriving instance Eq (Ordinal n)-deriving instance Ord (Ordinal n)--instance SingI n => Enum (Ordinal n) where-  fromEnum = ordToInt-  toEnum   = unsafeFromInt-  enumFrom = enumFromOrd-  enumFromTo = enumFromToOrd--enumFromToOrd :: forall n. SingI n => Ordinal n -> Ordinal n -> [Ordinal n]-enumFromToOrd ok ol =-  let k = ordToInt ok-      l = ordToInt ol-  in take (l - k + 1) $ enumFromOrd ok--enumFromOrd :: forall n. SingI n => Ordinal n -> [Ordinal n]-enumFromOrd ord = drop (ordToInt ord) $ enumOrdinal (sing :: SNat n)--enumOrdinal :: SNat n -> [Ordinal n]-enumOrdinal SZ = []-enumOrdinal (SS n) = OZ : map OS (enumOrdinal n)--instance SingI n => Bounded (Ordinal ('S n)) where-  minBound = OZ-  maxBound =-    case propToBoolLeq $ leqRefl (sing :: SNat n) of-      Dict -> sNatToOrd (sing :: SNat n)--unsafeFromInt :: forall n. SingI n => Int -> Ordinal n-unsafeFromInt n =-    case (promote n :: Monomorphic (Sing :: Nat -> *)) of-      Monomorphic sn ->-           case SS sn %:<= (sing :: SNat n) of-             STrue -> sNatToOrd' (sing :: SNat n) sn-             SFalse -> error "Bound over!"---- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.-sNatToOrd' :: ('S m S.:<= n) ~ 'True => SNat n -> SNat m -> Ordinal n-sNatToOrd' (SS _) SZ = OZ-sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-sNatToOrd' _ _ = bugInGHC-#endif---- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (SingI n, ('S m S.:<= n) ~ 'True) => SNat m -> Ordinal n-sNatToOrd = sNatToOrd' sing--data CastedOrdinal n where-  CastedOrdinal :: ('S m S.:<= n) ~ 'True => SNat m -> CastedOrdinal n---- | Convert @Ordinal n@ into @SNat m@ with the proof of @'S m :<<= n@.-ordToSNat' :: Ordinal n -> CastedOrdinal n-ordToSNat' OZ = CastedOrdinal SZ-ordToSNat' (OS on) =-  case ordToSNat' on of-    CastedOrdinal m ->-      CastedOrdinal (SS m)---- | Convert @Ordinal n@ into monomorphic @SNat@-ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)-ordToSNat OZ = Monomorphic SZ-ordToSNat (OS n) =-  case ordToSNat n of-    Monomorphic sn ->-      case singInstance sn of-        SingInstance -> Monomorphic (SS sn)---- | Convert ordinal into @Int@.-ordToInt :: Ordinal n -> Int-ordToInt OZ = 0-ordToInt (OS n) = 1 + ordToInt n---- | Inclusion function for ordinals.-inclusion' :: (n S.:<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m-inclusion' _ = unsafeCoerce-{-# INLINE inclusion' #-}-{---- The "proof" of the correctness of the above-inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m-inclusion' (SS SZ) OZ = OZ-inclusion' (SS (SS _)) OZ = OZ-inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m-inclusion' _ _ = bugInGHC--}---- | Inclusion function for ordinals with codomain inferred.-inclusion :: ((n S.:<= m) ~ 'True) => Ordinal n -> Ordinal m-inclusion on = unsafeCoerce on-{-# INLINE inclusion #-}---- | Ordinal addition.-(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)-OZ @+ n =-  let sn = sing :: SNat n-      sm = sing :: SNat m-  in case propToBoolLeq (plusLeqR sn sm) of-      Dict -> inclusion n-OS n @+ m =-  case sing :: SNat n of-    SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-    _ -> bugInGHC-#endif---- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.------ Since 0.2.3.0-absurdOrd :: Ordinal 'Z -> a-absurdOrd cs = case cs of {}---- | 'absurdOrd' for the value in 'Functor'.------   Since 0.2.3.0-vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a-vacuousOrd = fmap absurdOrd---- | 'absurdOrd' for the value in 'Monad'.---   This function will become uneccesary once 'Applicative' (and hence 'Functor')---   become the superclass of 'Monad'.------   Since 0.2.3.0-vacuousOrdM :: Monad m => m (Ordinal 'Z) -> m a-vacuousOrdM = liftM absurdOrd---- | Quasiquoter for ordinals-od :: QuasiQuoter-od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read-                 , quoteType = error "No type quoter for Ordinals"-                 , quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read-                 , quoteDec = error "No declaration quoter for Ordinals"-                 }
+ 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
+ tests/Shared.hs view
@@ -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,55 +1,114 @@--- Initial type-natural.cabal generated by cabal init.  For further --- documentation, see http://haskell.org/cabal/users-guide/+cabal-version: 3.0+name: type-natural+version: 1.3.0.2+license: BSD-3-Clause+license-file: LICENSE+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. -name:                type-natural-version:             0.4.2.0-synopsis:            Type-level natural and proofs of their properties.-description:         Type-level natural numbers and proofs of their properties.-homepage:            https://github.com/konn/type-natural-license:             BSD3-license-file:        LICENSE-author:              Hiromi ISHII-maintainer:          konn.jinro_at_gmail.com-copyright:           (C) Hiromi ISHII 2013-2014-category:            Math-build-type:          Simple-cabal-version:       >= 1.10-tested-with:         GHC == 7.10.3, GHC == 8.0.1+category: Math+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-  ghc-options:         -Wall -O2 -fno-warn-orphans-  if impl(ghc >= 8.0.0)-    ghc-options:       -Wno-redundant-constraints-  exposed-modules:     Data.Type.Natural-                     , Data.Type.Ordinal-                     , Data.Type.Natural.Builtin-  other-modules:       Data.Type.Natural.Definitions-                     , Data.Type.Natural.Core-                     , Data.Type.Natural.Compat-  build-depends:       base                      >= 4       && < 5-                     , equational-reasoning      == 0.4.*-                     , monomorphic               >= 0.0.3-                     , template-haskell          >= 2.8     && < 3-                     , constraints               >= 0.3     && < 0.9-                     , ghc-typelits-natnormalise == 0.4.*-                     , ghc-typelits-presburger   == 0.1.*-                     , singletons                >= 2.0 && < 2.3+  -- 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 -  default-language:    Haskell2010-  default-extensions:  DataKinds-                       PolyKinds-                       ConstraintKinds-                       GADTs-                       ScopedTypeVariables-                       TemplateHaskell-                       TypeFamilies-                       TypeOperators-                       MultiParamTypeClasses-                       UndecidableInstances-                       FlexibleContexts-                       FlexibleInstances+  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