module Data.Type.Natural (
module Data.Singletons,
Nat(..),
SNat, Sing (SZ, SS)
, sZ, sS
, min, Min, sMin, max, Max, sMax
, (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*)
, (:-:), (:-), (%:-), (%-)
, Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, leqRefl, leqSucc
, boolToPropLeq, boolToClassLeq, propToClassLeq
, LeqTrueInstance(..), propToBoolLeq
, natToInt, intToNat, sNatToInt
, succCongEq, plusCongR, plusCongL, succPlusL, succPlusR
, plusZR, plusZL, eqPreservesS, plusAssociative
, multAssociative, multComm, multZL, multZR, multOneL, multOneR
, plusMultDistr, multPlusDistr, multCongL, multCongR
, sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent
, eqSuccMinus, plusMinusEqL, plusMinusEqR, plusLeqL, plusLeqR
, zAbsorbsMinR, zAbsorbsMinL, minLeqL, minLeqR, plusSR
, leqRhs, leqLhs, leqTrans, minComm, leqAnitsymmetric
, maxZL, maxComm, maxZR, maxLeqL, maxLeqR, plusMonotone
, 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
, 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
, sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14
, sN15, sN16, sN17, sN18, sN19, sN20
) where
import Data.Singletons
import Prelude (Bool (..), Eq (..), Integral (..), Ord ((<)),
Show (..), error, id, otherwise, ($), (.), undefined)
import qualified Prelude as P
import Proof.Equational
singletons [d|
data Nat = Z | S Nat
deriving (Show, Eq, Ord)
|]
singletons [d|
min :: Nat -> Nat -> Nat
min Z Z = Z
min Z (S _) = Z
min (S _) Z = Z
min (S m) (S n) = S (min m n)
max :: Nat -> Nat -> Nat
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|
(+) :: Nat -> Nat -> Nat
Z + n = n
S m + n = S (m + n)
() :: Nat -> Nat -> Nat
n Z = n
S n S m = n m
Z S _ = Z
(*) :: Nat -> Nat -> Nat
Z * _ = Z
S n * m = n * m + m
|]
instance P.Num Nat where
n m = n m
n + m = n + m
n * m = n * m
abs = id
signum Z = Z
signum _ = S Z
fromInteger 0 = Z
fromInteger n | n P.< 0 = error "negative integer"
| otherwise = S $ P.fromInteger (n P.- 1)
infixl 6 :-:, %:-,
type n :-: m = n :- m
infixl 6 :+:, %+, %:+, :+
type n :+: m = n :+ m
(%+) :: SNat n -> SNat m -> SNat (n :+: m)
(%+) = (%:+)
infixl 7 :*:, %*, %:*, :*
type n :*: m = n :* m
(%*) :: 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
|]
class (n :: Nat) :<= (m :: Nat)
instance Z :<= n
instance (n :<= m) => S n :<= S m
singletons [d|
(<<=) :: Nat -> Nat -> Bool
Z <<= _ = True
S _ <<= Z = False
S n <<= S m = n <<= m
|]
data Leq (n :: Nat) (m :: Nat) where
ZeroLeq :: SNat m -> Leq Zero m
SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
data LeqTrueInstance a b where
LeqTrueInstance :: (a :<<= b) ~ True => LeqTrueInstance a b
(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)
n %- SZ = n
SS n %- SS m = n %- m
_ %- _ = error "impossible!"
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)
propToBoolLeq :: Leq n m -> LeqTrueInstance n m
propToBoolLeq (ZeroLeq _) = LeqTrueInstance
propToBoolLeq (SuccLeqSucc leq) =
case propToBoolLeq leq of
LeqTrueInstance -> LeqTrueInstance
data LeqInstance n m where
LeqInstance :: (n :<= m) => LeqInstance n m
boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
boolToPropLeq SZ m = ZeroLeq m
boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
boolToPropLeq _ _ = bugInGHC
boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
boolToClassLeq SZ _ = LeqInstance
boolToClassLeq (SS n) (SS m) =
case boolToClassLeq n m of
LeqInstance -> LeqInstance
boolToClassLeq _ _ = bugInGHC
propToClassLeq :: Leq n m -> LeqInstance n m
propToClassLeq (ZeroLeq _) = LeqInstance
propToClassLeq (SuccLeqSucc leq) =
case propToClassLeq leq of
LeqInstance -> LeqInstance
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
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
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
leqTrans _ _ = error "impossible!"
instance Preorder Leq where
reflexivity = leqRefl
transitivity = leqTrans
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)
eqPreservesS :: n :=: m -> S n :=: S m
eqPreservesS Refl = Refl
plusZL :: SNat n -> Z :+: n :=: n
plusZL _ = Refl
succCongEq :: n :=: m -> S n :=: S m
succCongEq Refl = Refl
sAndPlusOne :: SNat n -> S n :=: n :+: One
sAndPlusOne SZ = Refl
sAndPlusOne (SS n) =
start (sS (sS n))
=== sS (n %+ sOne) `because` cong' sS (sAndPlusOne n)
=~= sS n %+ sOne
plusAssociative :: SNat n -> SNat m -> SNat l
-> n :+: (m :+: l) :=: (n :+: m) :+: l
plusAssociative SZ _ _ = Refl
plusAssociative (SS n) m l =
start (sS n %+ (m %+ l))
=~= sS (n %+ (m %+ l))
=== sS ((n %+ m) %+ l) `because` cong' sS (plusAssociative n m l)
=~= sS (n %+ m) %+ l
=~= (sS n %+ m) %+ l
plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m
plusSR n m =
start (sS (n %+ m))
=== (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)
=== n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)
=== n %+ sS m `because` plusCongL n (symmetry $ sAndPlusOne m)
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 plusSR m (leqRhs leq) of
Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq
plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'
infer :: Proxy a
infer = Proxy
plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'
plusCongL _ Refl = Refl
plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n
plusCongR _ Refl = Refl
succPlusL :: SNat n -> SNat m -> S n :+ m :=: S (n :+ m)
succPlusL _ _ = Refl
succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m)
succPlusR SZ _ = Refl
succPlusR (SS n) m =
start (sS n %+ sS m)
=~= sS (n %+ sS m)
=== sS (sS (n %+ m)) `because` succCongEq (succPlusR n m)
=~= sS (sS n %+ m)
minusCongEq :: n :=: m -> SNat l -> n :-: l :=: m :-: l
minusCongEq Refl _ = Refl
minusNilpotent :: SNat n -> n :-: n :=: Zero
minusNilpotent SZ = Refl
minusNilpotent (SS n) =
start (sS n %:- sS n)
=~= n %:- n
=== sZ `because` minusNilpotent n
plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n
plusCommutative SZ SZ = Refl
plusCommutative SZ (SS m) =
start (sZ %+ sS m)
=~= sS m
=== sS (m %+ sZ) `because` cong' sS (plusCommutative SZ m)
=~= sS m %+ sZ
plusCommutative (SS n) m =
start (sS n %+ m)
=~= sS (n %+ m)
=== sS (m %+ n) `because` cong' sS (plusCommutative n m)
=== (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)
=== m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)
=== m %+ sS n `because` plusCongL m (symmetry $ sAndPlusOne n)
eqSuccMinus :: ((m :<<= 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)
eqSuccMinus _ _ = bugInGHC
plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
plusLeqL SZ m = case plusZR m of Refl -> ZeroLeq m
plusLeqL (SS n) m = SuccLeqSucc $ plusLeqL n m
plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
plusLeqR n m =
case plusCommutative n m of
Refl -> plusLeqL m n
plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
plusMinusEqL SZ m = minusNilpotent m
plusMinusEqL (SS n) m =
case propToBoolLeq (plusLeqR n m) of
LeqTrueInstance -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ 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
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
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
leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl
leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2
leqAnitsymmetric _ _ = bugInGHC
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)
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
newtype MultPlusDistr l m n =
MultPlusDistr { unMultPlusDistr :: l :* (m :+ n) :=: l :* m :+ l :* n}
instance Proposition (MultPlusDistr l m) where
type OriginalProp (MultPlusDistr l m) n = l :* (m :+ n) :=: l :* m :+ l :* n
wrap = MultPlusDistr
unWrap = unMultPlusDistr
multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l
multPlusDistr SZ _ _ = Refl
multPlusDistr (SS n) m l =
start (sS n %* (m %+ l))
=~= n %* (m %+ l) %+ (m %+ l)
=== (n %* m) %+ (n %* l) %+ (m %+ l) `because` plusCongR (m %+ l) (multPlusDistr n m l)
=== (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)
=== n %* m %+ (n %*l %+ (l %+ m)) `because` symmetry (plusAssociative (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) (plusAssociative (n %* l) l m)
=~= (sS n %* l) %+ m %+ n %* m
=== (sS n %* l) %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (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)
plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: n :* l :+ m :* l
plusMultDistr SZ _ _ = Refl
plusMultDistr (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 (plusMultDistr n m l)
=== m %* l %+ n %* l %+ l `because` plusCongR l (plusCommutative (n %* l) (m %* l))
=== m %* l %+ (n %* l %+ l) `because` symmetry (plusAssociative (m %* l) (n %*l) l)
=~= m %* l %+ (sS n %* l)
=== (sS n %* l) %+ (m %* l) `because` plusCommutative (m %* l) (sS n %* l)
multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l
multAssociative SZ _ _ = Refl
multAssociative (SS n) m l =
start (sS n %* (m %* l))
=~= n %* (m %* l) %+ (m %* l)
=== (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssociative n m l)
=== (n %* m %+ m) %* l `because` symmetry (plusMultDistr (n %* m) m l)
=~= (sS n %* m) %* l
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 (sAndPlusOne 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 (multPlusDistr m n sOne)
=== m %* sS n `because` multCongL m (symmetry $ sAndPlusOne n)
intToNat :: (Integral a, Ord a) => a -> Nat
intToNat 0 = Z
intToNat n
| n < 0 = error "negative integer"
| otherwise = S $ intToNat (n P.- 1)
natToInt :: Integral n => Nat -> n
natToInt Z = 0
natToInt (S n) = natToInt n P.+ 1
sNatToInt :: P.Num n => SNat x -> n
sNatToInt SZ = 0
sNatToInt (SS n) = sNatToInt n P.+ 1