fin 0.0.2 → 0.0.3

raw patch · 7 files changed

+475/−7 lines, 7 filesdep +decPVP ok

version bump matches the API change (PVP)

Dependencies added: dec

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−1
• LICENSE +1/−1
• fin.cabal +9/−5
• src/Data/Type/Nat.hs +37/−0
• src/Data/Type/Nat/LE.hs +184/−0
• src/Data/Type/Nat/LE/ReflStep.hs +169/−0
• src/Data/Type/Nat/LT.hs +68/−0

@@ -1,4 +1,10 @@-# Revision history for boring+# Revision history for fin++## 0.0.3++- Add `Data.Type.Nat.LE`, `Data.Type.Nat.LT` and `Data.Type.Nat.LE.ReflStep`+  modules+- Add `withSNat` and `discreteNat`  ## 0.0.2 

@@ -1,4 +1,4 @@-Copyright (c) 2017, Oleg Grenrus+Copyright (c) 2017-2019, Oleg Grenrus  All rights reserved. 

@@ -1,8 +1,8 @@ cabal-version:      >=1.10 name:               fin-version:            0.0.2+version:            0.0.3 synopsis:           Nat and Fin: peano naturals and finite numbers-category:           Data+category:           Data, Dependent Types, Singletons description:   This package provides two simple types, and some tools to work with them.   Also on type level as @DataKinds@.@@ -52,7 +52,7 @@ license-file:       LICENSE author:             Oleg Grenrus <oleg.grenrus@iki.fi> maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright:          (c) 2017 Oleg Grenrus+copyright:          (c) 2017-2019 Oleg Grenrus build-type:         Simple extra-source-files: ChangeLog.md tested-with:@@ -68,17 +68,21 @@     Data.Fin.Enum     Data.Nat     Data.Type.Nat+    Data.Type.Nat.LE+    Data.Type.Nat.LE.ReflStep+    Data.Type.Nat.LT    build-depends:       base      >=4.7     && <4.13+    , dec       >=0.0.3   && <0.1     , deepseq   >=1.3.0.2 && <1.5-    , hashable  >=1.2.7.0 && <1.3+    , hashable  >=1.2.7.0 && <1.4    if !impl(ghc >=8.2)     build-depends: bifunctors >=5.5.3 && <5.6    if !impl(ghc >=8.0)-    build-depends: semigroups >=0.18.4 && <0.19+    build-depends: semigroups >=0.18.4 && <0.20    if !impl(ghc >=7.10)     build-depends:

@@ -1,5 +1,6 @@ {-# LANGUAGE CPP                  #-} {-# LANGUAGE DataKinds            #-}+{-# LANGUAGE EmptyCase            #-} {-# LANGUAGE GADTs                #-} {-# LANGUAGE KindSignatures       #-} {-# LANGUAGE RankNTypes           #-}@@ -26,12 +27,14 @@     snatToNatural,     -- * Implicit     SNatI(..),+    withSNat,     reify,     reflect,     reflectToNum,     -- * Equality     eqNat,     EqNat,+    discreteNat,     -- * Induction     induction,     induction1,@@ -63,6 +66,7 @@ import Data.Nat import Data.Proxy         (Proxy (..)) import Data.Type.Equality+import Data.Type.Dec import Numeric.Natural    (Natural)  import qualified GHC.TypeLits as GHC@@ -85,6 +89,13 @@ instance            SNatI 'Z         where snat = SZ instance SNatI n => SNatI ('S n)     where snat = SS +-- | Constructor 'SNatI' dictionary from 'SNat'.+--+-- @since 0.0.3+withSNat :: SNat n -> (SNatI n => r) -> r+withSNat SZ k = k+withSNat SS k = k+ -- | Reflect type-level 'Nat' to the term level. reflect :: forall n proxy. SNatI n => proxy n -> Nat reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)@@ -152,6 +163,32 @@         return Refl  newtype NatEq n = NatEq { getNatEq :: forall m. SNatI m => Maybe (n :~: m) }++-- | Decide equality of type-level numbers.+--+-- >>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))+-- "Yes Refl"+--+-- @since 0.0.3+discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)+discreteNat = getDiscreteNat $ induction (DiscreteNat start) (\p -> DiscreteNat (step p))+  where+    start :: forall p. SNatI p => Dec ('Z :~: p)+    start = case snat :: SNat p of+        SZ -> Yes Refl+        SS -> No $ \p -> case p of {}++    step :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: q)+    step rec = case snat :: SNat q of+        SZ -> No $ \p -> case p of {}+        SS -> step' rec++    step' :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: 'S q)+    step' (DiscreteNat rec) = case rec :: Dec (p :~: q) of+        Yes Refl -> Yes Refl+        No np    -> No $ \Refl -> np Refl++newtype DiscreteNat n = DiscreteNat { getDiscreteNat :: forall m. SNatI m => Dec (n :~: m) }  instance TestEquality SNat where     testEquality SZ SZ = Just Refl

@@ -0,0 +1,184 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE EmptyCase             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TypeOperators         #-}++{-# LANGUAGE UndecidableInstances  #-}+-- | Less-than-or-equal relation for (unary) natural numbers 'Nat'.+--+-- There are at least three ways to encode this relation.+--+-- * \(zero : 0 \le m\) and \(succ : n \le m \to 1 + n \le 1 + m\) (this module),+--+-- * \(refl : n \le n \) and \(step : n \le m \to n \le 1 + m\) ("Data.Type.Nat.LE.ReflStep"),+--+-- * \(ex : \exists p. n + p \equiv m \) (tricky in Haskell).+--+-- Depending on a situation, usage ergonomics are different.+--+module Data.Type.Nat.LE (+    -- * Relation+    LE (..),+    LEProof (..),+    withLEProof,+    -- * Decidability+    decideLE,+    -- * Lemmas+    -- ** Constructor like+    leZero,+    leSucc,+    leRefl,+    leStep,+    -- ** Partial order+    leAsym,+    leTrans,+    -- ** Total order+    leSwap,+    leSwap',+    -- ** More+    leStepL,+    lePred,+    proofZeroLEZero,+    ) where++import Data.Type.Dec      (Dec (..), Decidable (..), Neg)+import Data.Type.Equality+import Data.Type.Nat+import Data.Void          (absurd)++-------------------------------------------------------------------------------+-- Proof+-------------------------------------------------------------------------------++-- | An evidence of \(n \le m\). /zero+succ/ definition.+data LEProof n m where+    LEZero :: LEProof 'Z m+    LESucc :: LEProof n m -> LEProof ('S n) ('S m)++deriving instance Show (LEProof n m)++-- | 'LEProof' values are unique (not @'Boring'@ though!).+instance Eq (LEProof n m) where+    _ == _ = True++instance Ord (LEProof n m) where+    compare _ _ = EQ++-------------------------------------------------------------------------------+-- Class+-------------------------------------------------------------------------------++-- | Total order of 'Nat', less-than-or-Equal-to, \( \le \).+--+class LE n m where+    leProof :: LEProof n m++instance LE 'Z m where+    leProof = LEZero++instance (m ~ 'S m', LE n m') => LE ('S n) m where+    leProof = LESucc leProof++-- | Constructor 'LE' dictionary from 'LEProof'.+withLEProof :: LEProof n m -> (LE n m => r) -> r+withLEProof LEZero     k = k+withLEProof (LESucc p) k = withLEProof p k++-------------------------------------------------------------------------------+-- Lemmas+-------------------------------------------------------------------------------++-- | \(\forall n : \mathbb{N}, 0 \le n \)+leZero :: LEProof 'Z n+leZero = LEZero++-- | \(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)+leSucc :: LEProof n m -> LEProof ('S n) ('S m)+leSucc = LESucc++-- | \(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)+lePred :: LEProof ('S n) ('S m) -> LEProof n m+lePred (LESucc p) = p++-- | \(\forall n : \mathbb{N}, n \le n \)+leRefl :: forall n. SNatI n => LEProof n n+leRefl = case snat :: SNat n of+    SZ -> LEZero+    SS -> LESucc leRefl++-- | \(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)+leStep :: LEProof n m -> LEProof n ('S m)+leStep LEZero     = LEZero+leStep (LESucc p) = LESucc (leStep p)++-- | \(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)+leStepL :: LEProof ('S n) m -> LEProof n m+leStepL (LESucc p) = leStep p++-- | \(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)+leAsym :: LEProof n m -> LEProof m n -> n :~: m+leAsym LEZero     LEZero     = Refl+leAsym (LESucc p) (LESucc q) = case leAsym p q of Refl -> Refl+-- leAsym LEZero p = case p of {}+-- leAsym p LEZero = case p of {}++-- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)+leTrans :: LEProof n m -> LEProof m p -> LEProof n p+leTrans LEZero     _          = LEZero+leTrans (LESucc p) (LESucc q) = LESucc (leTrans p q)+-- leTrans (LESucc _) q = case q of {}++-- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)+leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n+leSwap np = case (snat :: SNat m, snat :: SNat n) of+    (_,  SZ) -> absurd (np LEZero)+    (SZ, SS) -> LESucc LEZero+    (SS, SS) -> LESucc $ leSwap $ \p -> np $ LESucc p++-- | \(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)+--+-- >>> leProof :: LEProof Nat2 Nat3+-- LESucc (LESucc LEZero)+--+-- >>> leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))+-- LESucc (LESucc (LESucc LEZero))+--+-- >>> lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))+-- LESucc (LESucc LEZero)+--+leSwap' :: LEProof n m -> LEProof ('S m) n -> void+leSwap' p (LESucc q) = case p of LESucc p' -> leSwap' p' q++-------------------------------------------------------------------------------+-- Dedidablity+-------------------------------------------------------------------------------++-- | Find the @'LEProof' n m@, i.e. compare numbers.+decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)+decideLE = case snat :: SNat n of+    SZ -> Yes leZero+    SS -> caseSnm+  where+    caseSnm :: forall n' m'. (SNatI n', SNatI m') => Dec (LEProof ('S n') m')+    caseSnm = case snat :: SNat m' of+        SZ -> No $ \p -> case p of {} -- ooh, GHC is smart!+        SS -> case decideLE of+            Yes p -> Yes (leSucc p)+            No  p -> No $ \p' -> p (lePred p')++instance (SNatI n, SNatI m) => Decidable (LEProof n m) where+    decide = decideLE++-------------------------------------------------------------------------------+-- More lemmas+-------------------------------------------------------------------------------++-- | \(\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 \)+proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z+proofZeroLEZero LEZero = Refl

@@ -0,0 +1,169 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE EmptyCase             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TypeOperators         #-}++{-# LANGUAGE UndecidableInstances  #-}+module Data.Type.Nat.LE.ReflStep (+    -- * Relation+    LEProof (..),+    fromZeroSucc,+    toZeroSucc,+    -- * Decidability+    decideLE,+    -- * Lemmas+    -- ** Constructor like+    leZero,+    leSucc,+    leRefl,+    leStep,+    -- ** Partial order+    leAsym,+    leTrans,+    -- ** Total order+    leSwap,+    leSwap',+    -- ** More+    leStepL,+    lePred,+    proofZeroLEZero,+    ) where++import Data.Type.Dec      (Dec (..), Decidable (..), Neg)+import Data.Type.Equality+import Data.Type.Nat+import Data.Void          (absurd)++import qualified Data.Type.Nat.LE as ZeroSucc++-------------------------------------------------------------------------------+-- Proof+-------------------------------------------------------------------------------++-- | An evidence of \(n \le m\). /refl+step/ definition.+data LEProof n m where+    LERefl :: LEProof n n+    LEStep :: LEProof n m -> LEProof n ('S m)++deriving instance Show (LEProof n m)++-- | 'LEProof' values are unique (not @'Boring'@ though!).+instance Eq (LEProof n m) where+    _ == _ = True++instance Ord (LEProof n m) where+    compare _ _ = EQ++-------------------------------------------------------------------------------+-- Conversion+-------------------------------------------------------------------------------++-- | Convert from /zero+succ/ to /refl+step/ definition.+--+-- Inverse of 'toZeroSucc'.+--+fromZeroSucc :: forall n m. SNatI m => ZeroSucc.LEProof n m -> LEProof n m+fromZeroSucc ZeroSucc.LEZero     = leZero+fromZeroSucc (ZeroSucc.LESucc p) = case snat :: SNat m of+    SS -> leSucc (fromZeroSucc p)+    -- q  -> case q of {} -- for older GHC++-- | Convert /refl+step/ to /zero+succ/ definition.+--+-- Inverse of 'fromZeroSucc'.+--+toZeroSucc :: SNatI n => LEProof n m -> ZeroSucc.LEProof n m+toZeroSucc LERefl     = ZeroSucc.leRefl+toZeroSucc (LEStep p) = ZeroSucc.leStep (toZeroSucc p)++-------------------------------------------------------------------------------+-- Lemmas+-------------------------------------------------------------------------------++-- | \(\forall n : \mathbb{N}, 0 \le n \)+leZero :: forall n. SNatI n => LEProof 'Z n+leZero = case snat :: SNat n of+    SZ -> LERefl+    SS -> LEStep leZero++-- | \(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)+leSucc :: LEProof n m -> LEProof ('S n) ('S m)+leSucc LERefl     = LERefl+leSucc (LEStep p) = LEStep (leSucc p)++-- | \(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)+lePred :: LEProof ('S n) ('S m) -> LEProof n m+lePred LERefl              = LERefl+lePred (LEStep LERefl)     = LEStep LERefl+lePred (LEStep (LEStep q)) = LEStep (leStepL q)++-- | \(\forall n : \mathbb{N}, n \le n \)+leRefl :: LEProof n n+leRefl = LERefl++-- | \(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)+leStep :: LEProof n m -> LEProof n ('S m)+leStep = LEStep++-- | \(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)+leStepL :: LEProof ('S n) m -> LEProof n m+leStepL LERefl     = LEStep LERefl+leStepL (LEStep p) = LEStep (leStepL p)++-- | \(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)+leAsym :: LEProof n m -> LEProof m n -> n :~: m+leAsym LERefl _ = Refl+leAsym _ LERefl = Refl+leAsym (LEStep p) (LEStep q) = case leAsym (leStepL p) (leStepL q) of+    Refl -> Refl++-- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)+leTrans :: LEProof n m -> LEProof m p -> LEProof n p+leTrans LERefl     q          = q+leTrans p          LERefl     = p+leTrans (LEStep p) (LEStep q) = LEStep $ leTrans p $ leStepL q++-- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)+leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n+leSwap np = case (snat :: SNat m, snat :: SNat n) of+    (_,  SZ) -> absurd (np leZero)+    (SZ, SS) -> leSucc leZero+    (SS, SS) -> leSucc $ leSwap $ \p -> np $ leSucc p++-- | \(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)+leSwap' :: LEProof n m -> LEProof ('S m) n -> void+leSwap' p LERefl     = case p of LEStep p' -> leSwap' (leStepL p') LERefl+leSwap' p (LEStep q) = leSwap' (leStepL p) q++-------------------------------------------------------------------------------+-- Decidability+-------------------------------------------------------------------------------++-- | Find the @'LEProof' n m@, i.e. compare numbers.+decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)+decideLE = case snat :: SNat n of+    SZ -> Yes leZero+    SS -> caseSnm+  where+    caseSnm :: forall n' m'. (SNatI n', SNatI m') => Dec (LEProof ('S n') m')+    caseSnm = case snat :: SNat m' of+        SZ -> No $ \p -> case p of {} -- ooh, GHC is smart!+        SS -> case decideLE of+            Yes p -> Yes (leSucc p)+            No  p -> No $ \p' -> p (lePred p')++instance (SNatI n, SNatI m) => Decidable (LEProof n m) where+    decide = decideLE++-------------------------------------------------------------------------------+-- More lemmas+---------------------------------------------------------------------------------++-- | \(\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 \)+proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z+proofZeroLEZero LERefl = Refl

@@ -0,0 +1,68 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}+module Data.Type.Nat.LT (+    LT (..),+    LTProof,+    withLTProof,+    -- * Lemmas+    ltReflAbsurd,+    ltSymAbsurd,+    ltTrans,+    ) where++import Data.Type.Nat+import Data.Type.Nat.LE++-- | An evidence \(n < m\) which is the same as (\1 + n \le m\).+type LTProof n m = LEProof ('S n) m++-------------------------------------------------------------------------------+-- Class+-------------------------------------------------------------------------------++-- | Less-Than-or. \(<\). Well-founded relation on 'Nat'.+--+-- GHC can solve this for us!+--+-- >>> ltProof :: LTProof Nat0 Nat4+-- LESucc LEZero+--+-- >>> ltProof :: LTProof Nat2 Nat4+-- LESucc (LESucc (LESucc LEZero))+--+-- >>> ltProof :: LTProof Nat3 Nat3+-- ...+-- ...error...+-- ...+--+class LT (n :: Nat) (m :: Nat) where+    ltProof :: LTProof n m++instance LE ('S n) m => LT n m where+    ltProof = leProof++withLTProof :: LTProof n m -> (LT n m => r) -> r+withLTProof p f = withLEProof p f -- eta expansion needed for old GHC++-------------------------------------------------------------------------------+-- Lemmas+-------------------------------------------------------------------------------++-- | \(\forall n : \mathbb{N}, n < n \to \bot \)+ltReflAbsurd :: LTProof n n -> a+ltReflAbsurd (LESucc p) = ltReflAbsurd p++-- | \(\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot \)+ltSymAbsurd :: LTProof n m -> LTProof m n -> a+ltSymAbsurd (LESucc p) (LESucc q) = ltSymAbsurd p q++-- | \(\forall n\, m\, p : \mathbb{N}, n < m \to m < p \to n < p \)+ltTrans :: LTProof n m -> LTProof m p -> LTProof n p+ltTrans p (LESucc q) = leStep $ leTrans p q