Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

OAlg.Entity.Natural

Contents

Natrual Numbers
Attest
Induction
Propositions
- Addition
- Multiplication
Some attests
X

Description

natural numbers promotable to type-level. They serve to parameterize the length of finite lists on type-level (see OAlg.Entity.FinList).

Note We need the language extension UndecidableInstances for type checking the definition

N0 * m = N0
S n * m = m + n * m

for the type family *.

Using UndecidableInstances could cause the type checker to not terminate, but this will obviously not happen for the given definition (we also use the same definition for the multiplicative structure of N').

Synopsis

data N'
- = N0
- | S N'
toN' :: N -> N'
type family (n :: N') + (m :: k) :: N'
type family (n :: k) * (m :: N') :: N'
class Typeable n => Attestable n where
- attest :: W n
data Ats n where
- Ats :: Attestable n => Ats n
nValue :: Attestable n => p n -> N
data W n where
- W0 :: W N0
- SW :: W n -> W (n + 1)
cmpW :: W n -> W m -> Ordering
(++) :: W n -> W m -> W (n + m)
(**) :: W n -> W m -> W (n * m)
data W' = forall n. W' (W n)
toW' :: N -> W'
data SomeNatural where
- SomeNatural :: Attestable n => W n -> SomeNatural
succSomeNatural :: SomeNatural -> SomeNatural
someNatural :: N -> SomeNatural
naturals :: [SomeNatural]
induction :: Any n -> f N0 -> (forall i. f i -> f (i + 1)) -> f n
type Any = W
type Some = W'
refl :: Any x -> x :~: x
lemma1 :: (x :~: y) -> f x :~: f y
sbstAdd :: (a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
prpAdd0 :: (a + 0) :~: a
prpAdd1 :: (a + 1) :~: S a
prpAdd2 :: (a + 2) :~: S (S a)
prpEqlAny :: (Any n :~: Any m) -> n :~: m
prpEqlAny' :: (n :~: m) -> Any n :~: Any m
prpSuccInjective :: (S n :~: S m) -> n :~: m
prpAddNtrlL :: p a -> (N0 + a) :~: a
prpAddNtrlR :: Any a -> (a + N0) :~: a
prpAddAssoc :: Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
lemmaAdd1 :: Any a -> Any b -> (S a + b) :~: (a + S b)
prpAddComm :: Any a -> Any b -> (a + b) :~: (b + a)
prpMltNtrlL :: Any a -> (N1 * a) :~: a
prpMltNtrlR :: Any a -> (a * N1) :~: a
prpDstrL :: Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpMltAssoc :: Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
lemmaMlt1 :: Any a -> (a * N0) :~: N0
lemmaAdd2 :: Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
prpDstrR :: Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpMltComm :: Any a -> Any b -> (a * b) :~: (b * a)
codeW :: N -> N -> String
itfW :: N -> N -> String
type N0 = 'N0
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9
xSomeNatural :: X N -> X SomeNatural

Natrual Numbers

data N' Source #

natural number promotable to type-level.

Constructors

N0
S N'

Instances

Instances details

Enum N' Source #
Instance details Defined in OAlg.Entity.Natural Methods succ :: N' -> N' # pred :: N' -> N' # toEnum :: Int -> N' # fromEnum :: N' -> Int # enumFrom :: N' -> [N'] # enumFromThen :: N' -> N' -> [N'] # enumFromTo :: N' -> N' -> [N'] # enumFromThenTo :: N' -> N' -> N' -> [N'] #
Show N' Source #
Instance details Defined in OAlg.Entity.Natural Methods showsPrec :: Int -> N' -> ShowS # show :: N' -> String # showList :: [N'] -> ShowS #
Eq N' Source #
Instance details Defined in OAlg.Entity.Natural Methods (==) :: N' -> N' -> Bool # (/=) :: N' -> N' -> Bool #
Ord N' Source #
Instance details Defined in OAlg.Entity.Natural Methods compare :: N' -> N' -> Ordering # (<) :: N' -> N' -> Bool # (<=) :: N' -> N' -> Bool # (>) :: N' -> N' -> Bool # (>=) :: N' -> N' -> Bool # max :: N' -> N' -> N' # min :: N' -> N' -> N' #
LengthN N' Source #
Instance details Defined in OAlg.Entity.Natural Methods lengthN :: N' -> N Source #
Validable N' Source #
Instance details Defined in OAlg.Entity.Natural Methods valid :: N' -> Statement Source #
Entity N' Source #
Instance details Defined in OAlg.Entity.Natural
Additive N' Source #
Instance details Defined in OAlg.Entity.Natural Methods zero :: Root N' -> N' Source # (+) :: N' -> N' -> N' Source # ntimes :: N -> N' -> N' Source #
Distributive N' Source #
Instance details Defined in OAlg.Entity.Natural
Fibred N' Source #
Instance details Defined in OAlg.Entity.Natural Associated Types type Root N' Source # Methods root :: N' -> Root N' Source #
FibredOriented N' Source #
Instance details Defined in OAlg.Entity.Natural
Commutative N' Source #
Instance details Defined in OAlg.Entity.Natural
Multiplicative N' Source #
Instance details Defined in OAlg.Entity.Natural Methods one :: Point N' -> N' Source # (*) :: N' -> N' -> N' Source # npower :: N' -> N -> N' Source #
Oriented N' Source #
Instance details Defined in OAlg.Entity.Natural Associated Types type Point N' Source # Methods orientation :: N' -> Orientation (Point N') Source # start :: N' -> Point N' Source # end :: N' -> Point N' Source #
Total N' Source #
Instance details Defined in OAlg.Entity.Natural
type Root N' Source #
Instance details Defined in OAlg.Entity.Natural type Root N' = Orientation ()
type Point N' Source #
Instance details Defined in OAlg.Entity.Natural type Point N' = ()
type N0 * m Source #
Instance details Defined in OAlg.Entity.Natural type N0 * m = N0
type N0 + (n :: N') Source #
Instance details Defined in OAlg.Entity.Natural type N0 + (n :: N') = n
type ('S n :: N') * m Source #
Instance details Defined in OAlg.Entity.Natural type ('S n :: N') * m = m + (n * m)
type ('S n) + (m :: N') Source #
Instance details Defined in OAlg.Entity.Natural type ('S n) + (m :: N') = 'S (n + m)

toN' :: N -> N' Source #

mapping a natural number in N to N'.

type family (n :: N') + (m :: k) :: N' infixr 6 Source #

addition of natural numbers.

Instances

Instances details

type N0 + (n :: N') Source #
Instance details Defined in OAlg.Entity.Natural type N0 + (n :: N') = n
type n + 0 Source #
Instance details Defined in OAlg.Entity.Natural type n + 0 = n
type n + 1 Source #
Instance details Defined in OAlg.Entity.Natural type n + 1 = 'S n
type n + 2 Source #
Instance details Defined in OAlg.Entity.Natural type n + 2 = 'S ('S n)
type n + 3 Source #
Instance details Defined in OAlg.Entity.Natural type n + 3 = 'S ('S ('S n))
type ('S n) + (m :: N') Source #
Instance details Defined in OAlg.Entity.Natural type ('S n) + (m :: N') = 'S (n + m)

type family (n :: k) * (m :: N') :: N' infixr 7 Source #

multiplication of natural numbers.

Instances

Instances details

type N0 * m Source #
Instance details Defined in OAlg.Entity.Natural type N0 * m = N0
type 0 * m Source #
Instance details Defined in OAlg.Entity.Natural type 0 * m = N0
type 1 * m Source #
Instance details Defined in OAlg.Entity.Natural type 1 * m = m
type 2 * m Source #
Instance details Defined in OAlg.Entity.Natural type 2 * m = m + m
type ('S n :: N') * m Source #
Instance details Defined in OAlg.Entity.Natural type ('S n :: N') * m = m + (n * m)

Attest

class Typeable n => Attestable n where Source #

attest for any natural number.

Methods

attest :: W n Source #

Instances

Instances details

Attestable N0 Source #
Instance details Defined in OAlg.Entity.Natural Methods attest :: W N0 Source #
Attestable n => Attestable ('S n) Source #
Instance details Defined in OAlg.Entity.Natural Methods attest :: W ('S n) Source #

data Ats n where Source #

witness of being attestable.

Constructors

Ats :: Attestable n => Ats n

nValue :: Attestable n => p n -> N Source #

the corresponding natural number in N of a type parameterized by n.

data W n where Source #

witness for a natural number and serves for inductively definable elements (see induction).

Constructors

W0 :: W N0
SW :: W n -> W (n + 1)

Instances

Instances details

Show (W n) Source #
Instance details Defined in OAlg.Entity.Natural Methods showsPrec :: Int -> W n -> ShowS # show :: W n -> String # showList :: [W n] -> ShowS #
Eq (W n) Source #
Instance details Defined in OAlg.Entity.Natural Methods (==) :: W n -> W n -> Bool # (/=) :: W n -> W n -> Bool #
LengthN (W n) Source #
Instance details Defined in OAlg.Entity.Natural Methods lengthN :: W n -> N Source #
Validable (W n) Source #
Instance details Defined in OAlg.Entity.Natural Methods valid :: W n -> Statement Source #

cmpW :: W n -> W m -> Ordering Source #

comparing of two witnesses.

(++) :: W n -> W m -> W (n + m) infixr 6 Source #

addition of witnesses.

(**) :: W n -> W m -> W (n * m) infixr 7 Source #

multiplication of witnesses.

data W' Source #

union of all witnesses, which is isomorphic to N and N'.

Constructors

forall n. W' (W n)

Instances

Instances details

Enum W' Source #
Instance details Defined in OAlg.Entity.Natural Methods succ :: W' -> W' # pred :: W' -> W' # toEnum :: Int -> W' # fromEnum :: W' -> Int # enumFrom :: W' -> [W'] # enumFromThen :: W' -> W' -> [W'] # enumFromTo :: W' -> W' -> [W'] # enumFromThenTo :: W' -> W' -> W' -> [W'] #
Show W' Source #
Instance details Defined in OAlg.Entity.Natural Methods showsPrec :: Int -> W' -> ShowS # show :: W' -> String # showList :: [W'] -> ShowS #
Eq W' Source #
Instance details Defined in OAlg.Entity.Natural Methods (==) :: W' -> W' -> Bool # (/=) :: W' -> W' -> Bool #
Ord W' Source #
Instance details Defined in OAlg.Entity.Natural Methods compare :: W' -> W' -> Ordering # (<) :: W' -> W' -> Bool # (<=) :: W' -> W' -> Bool # (>) :: W' -> W' -> Bool # (>=) :: W' -> W' -> Bool # max :: W' -> W' -> W' # min :: W' -> W' -> W' #
LengthN W' Source #
Instance details Defined in OAlg.Entity.Natural Methods lengthN :: W' -> N Source #
Validable W' Source #
Instance details Defined in OAlg.Entity.Natural Methods valid :: W' -> Statement Source #
Entity W' Source #
Instance details Defined in OAlg.Entity.Natural
Additive W' Source #
Instance details Defined in OAlg.Entity.Natural Methods zero :: Root W' -> W' Source # (+) :: W' -> W' -> W' Source # ntimes :: N -> W' -> W' Source #
Distributive W' Source #
Instance details Defined in OAlg.Entity.Natural
Fibred W' Source #
Instance details Defined in OAlg.Entity.Natural Associated Types type Root W' Source # Methods root :: W' -> Root W' Source #
FibredOriented W' Source #
Instance details Defined in OAlg.Entity.Natural
Commutative W' Source #
Instance details Defined in OAlg.Entity.Natural
Multiplicative W' Source #
Instance details Defined in OAlg.Entity.Natural Methods one :: Point W' -> W' Source # (*) :: W' -> W' -> W' Source # npower :: W' -> N -> W' Source #
Oriented W' Source #
Instance details Defined in OAlg.Entity.Natural Associated Types type Point W' Source # Methods orientation :: W' -> Orientation (Point W') Source # start :: W' -> Point W' Source # end :: W' -> Point W' Source #
Total W' Source #
Instance details Defined in OAlg.Entity.Natural
type Root W' Source #
Instance details Defined in OAlg.Entity.Natural type Root W' = Orientation ()
type Point W' Source #
Instance details Defined in OAlg.Entity.Natural type Point W' = ()

toW' :: N -> W' Source #

mapping a natural value in N to W'.

data SomeNatural where Source #

witnesse of some natural.

Constructors

SomeNatural :: Attestable n => W n -> SomeNatural

Instances

Instances details

Show SomeNatural Source #
Instance details Defined in OAlg.Entity.Natural Methods showsPrec :: Int -> SomeNatural -> ShowS # show :: SomeNatural -> String # showList :: [SomeNatural] -> ShowS #
Eq SomeNatural Source #
Instance details Defined in OAlg.Entity.Natural Methods (==) :: SomeNatural -> SomeNatural -> Bool # (/=) :: SomeNatural -> SomeNatural -> Bool #
Validable SomeNatural Source #
Instance details Defined in OAlg.Entity.Natural Methods valid :: SomeNatural -> Statement Source #

succSomeNatural :: SomeNatural -> SomeNatural Source #

successor of some natural number.

someNatural :: N -> SomeNatural Source #

mapping N to SomeNatural.

Note The implementation of this mapping is quite inefficent for high values of N.

naturals :: [SomeNatural] Source #

the infinite list of some naturals.

Induction

induction :: Any n -> f N0 -> (forall i. f i -> f (i + 1)) -> f n Source #

induction for general type functions.

Propositions

The following propositions are based - for the most part - on induction. To ensure that the proofs yield a terminal value, i.e. Refl, we used in the proof of the induction hypothesis only propositions which are proofed before. So: if these propositions terminate, then also the hypothesis will terminate.

type Any = W Source #

predicate for any natural number.

type Some = W' Source #

some witness.

Some basic Lemmas

refl :: Any x -> x :~: x Source #

reflexivity.

lemma1 :: (x :~: y) -> f x :~: f y Source #

well definition of parameterized types.

sbstAdd :: (a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b') Source #

substitution rule for addition.

Some abbreviations