{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE DeriveLift #-}
module Morley.Util.Peano
(
Peano
, pattern S
, pattern Z
, ToPeano
, FromPeano
, SingNat (SZ, SS)
, peanoSing
, peanoSing'
, withPeanoSingI
, withSomePeano
, IsoNatPeano
, SingIPeano
, type (>)
, type (>=)
, peanoSingDecrement
, peanoSingAdd
, Decrement
, AddPeano
, SubPeano
, MinPeano
, MaxPeano
, Length
, At
, Drop
, LazyTake
, Take
, Head
, Tail
, IsLongerThan
, LongerThan
, RequireLongerThan
, IsLongerOrSameLength
, LongerOrSameLength
, RequireLongerOrSameLength
, requireLongerThan
, requireLongerOrSameLength
, isGreaterThan
, isGreaterEqualThan
, additivity
, associativity
, minIdempotency
, commutativity
, transitivity
, (|-)
, toNatural
, someSingNat
) where
import Data.Constraint (Dict(..), (\\))
import Data.Data (Data(..))
import Data.Singletons (Sing, SingI(..), SomeSing(..))
import Data.Type.Equality (gcastWith, type (:~:)(..))
import Data.Vinyl (Rec(..))
import Data.Vinyl.Core (Head, Tail)
import Data.Vinyl.TypeLevel (Nat(..), RLength)
import GHC.TypeLits (ErrorMessage(..), TypeError)
import GHC.TypeNats (type (+), type (-))
import GHC.TypeNats qualified as GHC
import Language.Haskell.TH.Syntax (Lift)
import Unsafe.Coerce (unsafeCoerce)
import Morley.Util.Sing (genSingletonsType)
import Morley.Util.StubbedProof
import Morley.Util.Type (FailUnless, MockableConstraint(..))
{-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
{-# ANN module ("HLint: ignore Use 'someNatVal' from Universum" :: Text) #-}
type Peano = Nat
deriving stock instance Eq Nat
deriving stock instance Show Nat
deriving stock instance Generic Nat
deriving stock instance Data Nat
deriving anyclass instance NFData Nat
$(genSingletonsType ''Nat)
deriving stock instance Show (SingNat (n :: Nat))
deriving stock instance Eq (SingNat (n :: Nat))
deriving stock instance Lift (SingNat (n :: Nat))
instance NFData (SingNat (n :: Nat)) where
rnf :: SingNat n -> ()
rnf SingNat n
SZ = ()
rnf (SS Sing n
n) = SingNat n -> ()
forall a. NFData a => a -> ()
rnf Sing n
SingNat n
n
type IsoNatPeano (n :: GHC.Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p)
type SingIPeano (n :: GHC.Nat) = SingI (ToPeano n)
type family ToPeano (n :: GHC.Nat) :: Peano where
ToPeano 0 = 'Z
ToPeano a = 'S (ToPeano (a - 1))
type family FromPeano (n :: Peano) :: GHC.Nat where
FromPeano 'Z = 0
FromPeano ('S a) = 1 + FromPeano a
peanoSing :: forall (n :: GHC.Nat). SingIPeano n => SingNat (ToPeano n)
peanoSing :: forall (n :: Nat). SingIPeano n => SingNat (ToPeano n)
peanoSing = forall {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @(ToPeano n)
peanoSing' :: forall (n :: GHC.Nat). KnownNat n => SingNat (ToPeano n)
peanoSing' :: forall (n :: Nat). KnownNat n => SingNat (ToPeano n)
peanoSing' = Natural -> SingNat (ToPeano n)
forall (m :: Nat). Natural -> SingNat m
go (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy)
where
go :: forall m. Natural -> SingNat m
go :: forall (m :: Nat). Natural -> SingNat m
go = \case
Natural
0 -> SingNat 'Z
(m ~ 'Z) => SingNat m
SZ ((m ~ 'Z) => SingNat m) -> (m :~: 'Z) -> SingNat m
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((Any :~: Any) -> m :~: 'Z
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'Z)
Natural
n -> Sing (Decrement m) -> SingNat ('S (Decrement m))
forall (n :: Nat). Sing n -> SingNat ('S n)
SS (forall (m :: Nat). Natural -> SingNat m
go @(Decrement m) (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)) ((m ~ 'S (Decrement m)) => SingNat m)
-> (m :~: 'S (Decrement m)) -> SingNat m
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((Any :~: Any) -> m :~: 'S (Decrement m)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'S (Decrement m))
withPeanoSingI :: forall (n :: GHC.Nat) r. KnownNat n => (SingIPeano n => r) -> r
withPeanoSingI :: forall (n :: Nat) r. KnownNat n => (SingIPeano n => r) -> r
withPeanoSingI SingI (ToPeano n) => r
act = SingI (ToPeano n) => r
act (SingI (ToPeano n) => r) -> Dict (SingI (ToPeano n)) -> r
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat). Natural -> Dict (SingI m)
go @(ToPeano n) (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy)
where
go :: forall (m :: Peano). Natural -> Dict (SingI m)
go :: forall (m :: Nat). Natural -> Dict (SingI m)
go = \case
Natural
0 -> (m ~ 'Z) => Dict (SingI m)
forall (a :: Constraint). a => Dict a
Dict ((m ~ 'Z) => Dict (SingI m)) -> (m :~: 'Z) -> Dict (SingI m)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((Any :~: Any) -> m :~: 'Z
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'Z)
Natural
n -> SingI (Decrement m) => Dict (SingI m)
forall (a :: Constraint). a => Dict a
Dict (SingI (Decrement m) => Dict (SingI m))
-> Dict (SingI (Decrement m)) -> Dict (SingI m)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat). Natural -> Dict (SingI m)
go @(Decrement m) (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) ((m ~ 'S (Decrement m)) => Dict (SingI m))
-> (m :~: 'S (Decrement m)) -> Dict (SingI m)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((Any :~: Any) -> m :~: 'S (Decrement m)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'S (Decrement m))
withSomePeano :: Natural -> (forall n. (KnownNat n, SingIPeano n) => Proxy n -> r) -> r
withSomePeano :: forall r.
Natural
-> (forall (n :: Nat). (KnownNat n, SingIPeano n) => Proxy n -> r)
-> r
withSomePeano Natural
n forall (n :: Nat). (KnownNat n, SingIPeano n) => Proxy n -> r
f = case Natural -> SomeNat
someNatVal Natural
n of
SomeNat (Proxy n
pn :: Proxy n) -> forall (n :: Nat) r. KnownNat n => (SingIPeano n => r) -> r
withPeanoSingI @n ((SingIPeano n => r) -> r) -> (SingIPeano n => r) -> r
forall a b. (a -> b) -> a -> b
$ Proxy n -> r
forall (n :: Nat). (KnownNat n, SingIPeano n) => Proxy n -> r
f Proxy n
pn
type family Decrement (a :: Peano) :: Peano where
Decrement 'Z = TypeError ('Text "Expected n > 0")
Decrement ('S n) = n
peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement :: forall (n :: Nat). Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement = \case
Sing n
SingNat n
SZ -> Maybe (Sing (Decrement n))
forall a. Maybe a
Nothing
SS Sing n
n -> SingNat n -> Maybe (SingNat n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sing n
SingNat n
n
type family (>) (x :: Peano) (y :: Peano) :: Bool where
'Z > _ = 'False
'S _ > 'Z = 'True
'S x > 'S y = x > y
type family (>=) (x :: Peano) (y :: Peano) :: Bool where
_ >= 'Z = 'True
'Z >= _ = 'False
('S x) >= ('S y) = x >= y
type family AddPeano (n :: Peano) (m :: Peano) :: Peano where
AddPeano 'Z x = x
AddPeano ('S x) y = 'S (AddPeano x y)
type family SubPeano (n :: Peano) (m :: Peano) :: Peano where
SubPeano 'Z ('S m) = TypeError ('Text "Subtracting " ':<>: 'ShowType (FromPeano ('S m))
':<>: 'Text " from zero")
SubPeano n 'Z = n
SubPeano ('S n) ('S m) = SubPeano n m
type family MinPeano (n :: Peano) (m :: Peano) :: Peano where
MinPeano _ 'Z = 'Z
MinPeano 'Z _ = 'Z
MinPeano ('S n) ('S m) = 'S (MinPeano n m)
type family MaxPeano (n :: Peano) (m :: Peano) :: Peano where
MaxPeano n 'Z = n
MaxPeano 'Z m = m
MaxPeano ('S n) ('S m) = 'S (MaxPeano n m)
peanoSingAdd :: SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd :: forall (n :: Nat) (m :: Nat).
SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd (SS Sing n
n) (SS (SingNat n
m :: SingNat m')) = Sing ('S (AddPeano n n)) -> SingNat ('S ('S (AddPeano n n)))
forall (n :: Nat). Sing n -> SingNat ('S n)
SS (Sing (AddPeano n n) -> SingNat ('S (AddPeano n n))
forall (n :: Nat). Sing n -> SingNat ('S n)
SS (SingNat n -> SingNat n -> SingNat (AddPeano n n)
forall (n :: Nat) (m :: Nat).
SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd Sing n
SingNat n
n SingNat n
m)) ((AddPeano n ('S n) ~ 'S (AddPeano n n)) =>
SingNat ('S (AddPeano n ('S n))))
-> (AddPeano n ('S n) :~: 'S (AddPeano n n))
-> SingNat ('S (AddPeano n ('S n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (y :: Nat) (x :: Nat).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity @m' Sing n
SingNat n
n
peanoSingAdd SingNat n
SZ SingNat m
m = SingNat m
SingNat (AddPeano n m)
m
peanoSingAdd SingNat n
n SingNat m
SZ = SingNat n
(AddPeano n 'Z ~ n) => SingNat (AddPeano n 'Z)
n ((AddPeano n 'Z ~ n) => SingNat (AddPeano n 'Z))
-> (AddPeano n 'Z :~: n) -> SingNat (AddPeano n 'Z)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n -> SingNat 'Z -> AddPeano n 'Z :~: AddPeano 'Z n
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat n
n SingNat 'Z
SZ
type family Length l :: Peano where
Length l = RLength l
type family At (n :: Peano) s where
At 'Z (x ': _) = x
At ('S n) (_ ': xs) = At n xs
At a '[] =
TypeError
('Text "You tried to access a non-existing element of the stack, n = " ':<>:
'ShowType (FromPeano a))
type family Drop (n :: Peano) (s :: [k]) :: [k] where
Drop 'Z s = s
Drop ('S _) '[] = '[]
Drop ('S n) (_ ': s) = Drop n s
type family Take (n :: Peano) (s :: [k]) :: [k] where
Take 'Z _ = '[]
Take _ '[] = '[]
Take ('S n) (a ': s) = a ': Take n s
type LazyTake :: Peano -> [k] -> [k]
type family LazyTake n xs where
LazyTake 'Z _ = '[]
LazyTake ('S n) xs = Head xs ': LazyTake n (Tail xs)
type family IsLongerThan (l :: [k]) (a :: Peano) :: Bool where
IsLongerThan (_ ': _) 'Z = 'True
IsLongerThan (_ ': xs) ('S a) = IsLongerThan xs a
IsLongerThan '[] _ = 'False
type LongerThan l a = IsLongerThan l a ~ 'True
type family IsLongerOrSameLength (l :: [k]) (a :: Peano) :: Bool where
IsLongerOrSameLength _ 'Z = 'True
IsLongerOrSameLength (_ ': xs) ('S a) = IsLongerOrSameLength xs a
IsLongerOrSameLength '[] ('S _) = 'False
type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True
type family OfLengthWithTail (acc :: GHC.Nat) (l :: [k]) :: GHC.Nat where
OfLengthWithTail a '[] = a
OfLengthWithTail a (_ ': xs) = OfLengthWithTail (a + 1) xs
type LengthWithTail l = OfLengthWithTail 0 l
type family RequireLongerThan' (l :: [k]) (a :: Nat) :: Constraint where
RequireLongerThan' l a =
FailUnless
(IsLongerThan l a)
('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:
'Text " is not accessible" ':$$:
'Text "Current stack has size of only " ':<>:
'ShowType (LengthWithTail l) ':<>:
'Text ":" ':$$: 'ShowType l
)
class (RequireLongerThan' l a, LongerThan l a) =>
RequireLongerThan (l :: [k]) (a :: Peano)
instance (RequireLongerThan' l a, LongerThan l a) =>
RequireLongerThan l a
type family RequireLongerOrSameLength' (l :: [k]) (a :: Peano) :: Constraint where
RequireLongerOrSameLength' l a =
FailUnless
(IsLongerOrSameLength l a)
('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
'Text "Current stack has size of only " ':<>:
'ShowType (LengthWithTail l) ':<>:
'Text ":" ':$$: 'ShowType l
)
class (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
RequireLongerOrSameLength (l :: [k]) (a :: Peano)
instance (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
RequireLongerOrSameLength l a
instance MockableConstraint (RequireLongerOrSameLength l a) where
unsafeProvideConstraint :: Dict (RequireLongerOrSameLength l a)
unsafeProvideConstraint = Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a)
forall a b. a -> b
unsafeCoerce (Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a))
-> Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(RequireLongerOrSameLength '[] 'Z)
instance MockableConstraint (RequireLongerThan l a) where
unsafeProvideConstraint :: Dict (RequireLongerThan l a)
unsafeProvideConstraint = Dict (RequireLongerThan '[()] 'Z) -> Dict (RequireLongerThan l a)
forall a b. a -> b
unsafeCoerce (Dict (RequireLongerThan '[()] 'Z) -> Dict (RequireLongerThan l a))
-> Dict (RequireLongerThan '[()] 'Z)
-> Dict (RequireLongerThan l a)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(RequireLongerThan '[()] 'Z)
requireLongerThan
:: Rec any stk
-> Sing n
-> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan :: forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any stk
RNil Sing n
_ = Maybe (Dict (RequireLongerThan stk n))
forall a. Maybe a
Nothing
requireLongerThan (any r
_ :& Rec any rs
_xs) Sing n
SingNat n
SZ = Dict (RequireLongerThan stk n)
-> Maybe (Dict (RequireLongerThan stk n))
forall a. a -> Maybe a
Just Dict (RequireLongerThan stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerThan (any r
_ :& Rec any rs
xs) (SS Sing n
n) = do
Dict (RequireLongerThan rs n)
Dict <- Rec any rs -> Sing n -> Maybe (Dict (RequireLongerThan rs n))
forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any rs
xs Sing n
n
Dict (RequireLongerThan stk n)
-> Maybe (Dict (RequireLongerThan stk n))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (RequireLongerThan stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerOrSameLength
:: Rec any stk
-> Sing n
-> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength :: forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any stk
_ Sing n
SingNat n
SZ = Dict (RequireLongerOrSameLength stk n)
-> Maybe (Dict (RequireLongerOrSameLength stk n))
forall a. a -> Maybe a
Just Dict (RequireLongerOrSameLength stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerOrSameLength Rec any stk
RNil (SS Sing n
_) = Maybe (Dict (RequireLongerOrSameLength stk n))
forall a. Maybe a
Nothing
requireLongerOrSameLength (any r
_ :& Rec any rs
xs) (SS Sing n
n) = do
Dict (RequireLongerOrSameLength rs n)
Dict <- Rec any rs
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength rs n))
forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any rs
xs Sing n
n
Dict (RequireLongerOrSameLength stk n)
-> Maybe (Dict (RequireLongerOrSameLength stk n))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (RequireLongerOrSameLength stk n)
forall (a :: Constraint). a => Dict a
Dict
isGreaterThan
:: Sing a -> Sing b
-> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing a
SingNat a
SZ Sing b
_ = Maybe (Dict ((a > b) ~ 'True))
forall a. Maybe a
Nothing
isGreaterThan (SS Sing n
_) Sing b
SingNat b
SZ = Dict ('True ~ 'True) -> Maybe (Dict ('True ~ 'True))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
isGreaterThan (SS Sing n
a) (SS Sing n
b) = Sing n -> Sing n -> Maybe (Dict ((n > n) ~ 'True))
forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing n
a Sing n
b
isGreaterEqualThan
:: Sing a -> Sing b
-> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan Sing a
_ Sing b
SingNat b
SZ = Dict ('True ~ 'True) -> Maybe (Dict ('True ~ 'True))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
isGreaterEqualThan Sing a
SingNat a
SZ Sing b
_ = Maybe (Dict ((a >= b) ~ 'True))
forall a. Maybe a
Nothing
isGreaterEqualThan (SS Sing n
a) (SS Sing n
b) = Sing n -> Sing n -> Maybe (Dict ((n >= n) ~ 'True))
forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan Sing n
a Sing n
b
(|-) :: forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- :: forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
(|-) = (a :~: b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
infixr 1 |-
{-# DEPRECATED (|-) "Just use (\\\\) from Data.Constraint." #-}
additivity :: forall k m n. AddPeano k ('S m) ~ n
=> SingNat k -> n > k :~: 'True
additivity :: forall (k :: Nat) (m :: Nat) (n :: Nat).
(AddPeano k ('S m) ~ n) =>
SingNat k -> (n > k) :~: 'True
additivity SingNat k
k = (Stubbed => (n > k) :~: 'True) -> (n > k) :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => (n > k) :~: 'True) -> (n > k) :~: 'True)
-> (Stubbed => (n > k) :~: 'True) -> (n > k) :~: 'True
forall a b. (a -> b) -> a -> b
$ case SingNat k
k of
SingNat k
SZ -> (n > k) :~: 'True
forall {k} (a :: k). a :~: a
Refl
SingNat k
_ -> (('S k > k) ~ 'True) => (n > k) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((('S k > k) ~ 'True) => (n > k) :~: 'True)
-> (('S k > k) :~: 'True) -> (n > k) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat k -> ('S k > k) :~: 'True
forall (k' :: Nat). SingNat k' -> ('S k' > k') :~: 'True
lemma SingNat k
k ((('S (AddPeano k m) > k) ~ 'True) => (n > k) :~: 'True)
-> (('S (AddPeano k m) > k) :~: 'True) -> (n > k) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k' :: Nat) (m' :: Nat).
SingNat k' -> ('S (AddPeano k' m') > k') :~: 'True
lemma2 @_ @m SingNat k
k ((n ~ 'S (AddPeano k m)) => (n > k) :~: 'True)
-> (n :~: 'S (AddPeano k m)) -> (n > k) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (y :: Nat) (x :: Nat).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity @m SingNat k
k
where
lemma2 :: forall k' m'. SingNat k' -> 'S (AddPeano k' m') > k' :~: 'True
lemma2 :: forall (k' :: Nat) (m' :: Nat).
SingNat k' -> ('S (AddPeano k' m') > k') :~: 'True
lemma2 SingNat k'
SZ = ('S (AddPeano k' m') > k') :~: 'True
forall {k} (a :: k). a :~: a
Refl
lemma2 (SS Sing n
k') = (('S (AddPeano n m') > n) ~ 'True) =>
('S (AddPeano n m') > n) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((('S (AddPeano n m') > n) ~ 'True) =>
('S (AddPeano n m') > n) :~: 'True)
-> (('S (AddPeano n m') > n) :~: 'True)
-> ('S (AddPeano n m') > n) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k' :: Nat) (m' :: Nat).
SingNat k' -> ('S (AddPeano k' m') > k') :~: 'True
lemma2 @_ @m' Sing n
SingNat n
k'
lemma :: SingNat k' -> 'S k' > k' :~: 'True
lemma :: forall (k' :: Nat). SingNat k' -> ('S k' > k') :~: 'True
lemma SingNat k'
SZ = ('S k' > k') :~: 'True
forall {k} (a :: k). a :~: a
Refl
lemma (SS Sing n
n') = (('S n > n) ~ 'True) => ('S n > n) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((('S n > n) ~ 'True) => ('S n > n) :~: 'True)
-> (('S n > n) :~: 'True) -> ('S n > n) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n -> ('S n > n) :~: 'True
forall (k' :: Nat). SingNat k' -> ('S k' > k') :~: 'True
lemma Sing n
SingNat n
n'
associativity :: forall y x. SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity :: forall (y :: Nat) (x :: Nat).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity SingNat x
x = (Stubbed => AddPeano x ('S y) :~: 'S (AddPeano x y))
-> AddPeano x ('S y) :~: 'S (AddPeano x y)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => AddPeano x ('S y) :~: 'S (AddPeano x y))
-> AddPeano x ('S y) :~: 'S (AddPeano x y))
-> (Stubbed => AddPeano x ('S y) :~: 'S (AddPeano x y))
-> AddPeano x ('S y) :~: 'S (AddPeano x y)
forall a b. (a -> b) -> a -> b
$ case SingNat x
x of
SingNat x
SZ -> AddPeano x ('S y) :~: 'S (AddPeano x y)
forall {k} (a :: k). a :~: a
Refl
SS Sing n
x' -> (AddPeano n ('S y) ~ 'S (AddPeano n y)) =>
AddPeano x ('S y) :~: 'S (AddPeano x y)
forall {k} (a :: k). a :~: a
Refl ((AddPeano n ('S y) ~ 'S (AddPeano n y)) =>
AddPeano x ('S y) :~: 'S (AddPeano x y))
-> (AddPeano n ('S y) :~: 'S (AddPeano n y))
-> AddPeano x ('S y) :~: 'S (AddPeano x y)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (y :: Nat) (x :: Nat).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity @y Sing n
SingNat n
x'
commutativity :: SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity :: forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat x
x SingNat y
y = (Stubbed => AddPeano x y :~: AddPeano y x)
-> AddPeano x y :~: AddPeano y x
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => AddPeano x y :~: AddPeano y x)
-> AddPeano x y :~: AddPeano y x)
-> (Stubbed => AddPeano x y :~: AddPeano y x)
-> AddPeano x y :~: AddPeano y x
forall a b. (a -> b) -> a -> b
$ case SingNat x
x of
SingNat x
SZ -> case SingNat y
y of
SingNat y
SZ -> AddPeano x y :~: AddPeano y x
forall {k} (a :: k). a :~: a
Refl
SS Sing n
y' -> (n ~ AddPeano n 'Z) => AddPeano x y :~: AddPeano y x
forall {k} (a :: k). a :~: a
Refl ((n ~ AddPeano n 'Z) => AddPeano x y :~: AddPeano y x)
-> (n :~: AddPeano n 'Z) -> AddPeano x y :~: AddPeano y x
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat x -> SingNat n -> AddPeano x n :~: AddPeano n x
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat x
x Sing n
SingNat n
y'
SS (SingNat n
x' :: SingNat x') -> (AddPeano y ('S n) ~ 'S (AddPeano y n)) =>
AddPeano x y :~: AddPeano y x
forall {k} (a :: k). a :~: a
Refl ((AddPeano y ('S n) ~ 'S (AddPeano y n)) =>
AddPeano x y :~: AddPeano y x)
-> (AddPeano y ('S n) :~: 'S (AddPeano y n))
-> AddPeano x y :~: AddPeano y x
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (y :: Nat) (x :: Nat).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity @x' SingNat y
y ((AddPeano n y ~ AddPeano y n) => AddPeano x y :~: AddPeano y x)
-> (AddPeano n y :~: AddPeano y n) -> AddPeano x y :~: AddPeano y x
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n -> SingNat y -> AddPeano n y :~: AddPeano y n
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat n
x' SingNat y
y
minIdempotency :: SingNat n -> MinPeano n n :~: n
minIdempotency :: forall (n :: Nat). SingNat n -> MinPeano n n :~: n
minIdempotency SingNat n
n = (Stubbed => MinPeano n n :~: n) -> MinPeano n n :~: n
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => MinPeano n n :~: n) -> MinPeano n n :~: n)
-> (Stubbed => MinPeano n n :~: n) -> MinPeano n n :~: n
forall a b. (a -> b) -> a -> b
$ case SingNat n
n of
SingNat n
SZ -> MinPeano n n :~: n
forall {k} (a :: k). a :~: a
Refl
SS Sing n
n' -> (MinPeano n n ~ n) => MinPeano n n :~: n
forall {k} (a :: k). a :~: a
Refl ((MinPeano n n ~ n) => MinPeano n n :~: n)
-> (MinPeano n n :~: n) -> MinPeano n n :~: n
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n -> MinPeano n n :~: n
forall (n :: Nat). SingNat n -> MinPeano n n :~: n
minIdempotency Sing n
SingNat n
n'
transitivity :: (x >= y ~ 'True, y > z ~ 'True)
=> SingNat x -> SingNat y -> SingNat z -> x > z :~: 'True
transitivity :: forall (x :: Nat) (y :: Nat) (z :: Nat).
((x >= y) ~ 'True, (y > z) ~ 'True) =>
SingNat x -> SingNat y -> SingNat z -> (x > z) :~: 'True
transitivity SingNat x
x SingNat y
y SingNat z
z = (Stubbed => (x > z) :~: 'True) -> (x > z) :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => (x > z) :~: 'True) -> (x > z) :~: 'True)
-> (Stubbed => (x > z) :~: 'True) -> (x > z) :~: 'True
forall a b. (a -> b) -> a -> b
$ case (SingNat x
x, SingNat y
y, SingNat z
z) of
(SS Sing n
_, SS Sing n
_, SingNat z
SZ) -> (x > z) :~: 'True
forall {k} (a :: k). a :~: a
Refl
(SS Sing n
x', SS Sing n
y', SS Sing n
z') -> ((n > n) ~ 'True) => (x > z) :~: 'True
forall {k} (a :: k). a :~: a
Refl (((n > n) ~ 'True) => (x > z) :~: 'True)
-> ((n > n) :~: 'True) -> (x > z) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n -> SingNat n -> SingNat n -> (n > n) :~: 'True
forall (x :: Nat) (y :: Nat) (z :: Nat).
((x >= y) ~ 'True, (y > z) ~ 'True) =>
SingNat x -> SingNat y -> SingNat z -> (x > z) :~: 'True
transitivity Sing n
SingNat n
x' Sing n
SingNat n
y' Sing n
SingNat n
z'
toNatural :: Peano -> Natural
toNatural :: Nat -> Natural
toNatural Nat
Z = Natural
0
toNatural (S Nat
x) = Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Nat -> Natural
toNatural Nat
x
someSingNat :: Natural -> SomeSing Peano
someSingNat :: Natural -> SomeSing Nat
someSingNat Natural
0 = Sing 'Z -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'Z
SingNat 'Z
SZ
someSingNat Natural
n = case Natural -> SomeSing Nat
someSingNat (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) of
SomeSing Sing a
sn -> Sing ('S a) -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> SingNat ('S a)
forall (n :: Nat). Sing n -> SingNat ('S n)
SS Sing a
sn)