Data.Type.Natural.Builtin

Coercion between Peano Numerals Nat and builtin naturals Nat

Sysnonym to avoid confusion

type Peano = Nat

Type synonym for Nat to avoid confusion with built-in Nat.

Coercion between builtin type-level natural and peano numerals

type family FromPeano (n :: Nat) :: Nat where ...

Equations

FromPeano Z = 0

FromPeano (S n) = Succ (FromPeano n)

type family ToPeano (n :: Nat) :: Nat where ...

Equations

ToPeano 0 = Z

ToPeano n = S (ToPeano (Pred n))

sFromPeano :: Sing n -> Sing (FromPeano n)

sToPeano :: Sing n -> Sing (ToPeano n)

Properties of FromPeano and ToPeano.

fromPeanoInjective :: forall n m. (SingI n, SingI m) => (FromPeano n :=: FromPeano m) -> n :=: m

toPeanoInjective :: (ToPeano n :=: ToPeano m) -> n :=: m

Bijection

fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n

toFromPeano :: Sing n -> ToPeano (FromPeano n) :=: n

Algebraic isomorphisms

fromPeanoZeroCong :: FromPeano Z :=: 0

toPeanoZeroCong :: ToPeano 0 :=: Z

fromPeanoOneCong :: FromPeano One :=: 1

toPeanoOneCong :: ToPeano 1 :=: One

fromPeanoSuccCong :: Sing n -> FromPeano (S n) :=: Succ (FromPeano n)

toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :=: S (ToPeano n)

fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n :+ m) :=: (FromPeano n + FromPeano m)

toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :=: (ToPeano n :+ ToPeano m)

fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n :* m) :=: (FromPeano n * FromPeano m)

toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n :* m) :=: (ToPeano n :* ToPeano m)

fromPeanoMonotone :: (n :<<= m) ~ True => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :=: True

toPeanoMonotone :: n <= m => Sing n -> Sing m -> (ToPeano n :<<= ToPeano m) :~: True

Peano and commutative ring axioms for built-in Nat

plusZR :: Sing n -> (n + 0) :~: n

plusZL :: Sing n -> (0 + n) :~: n

plusSuccR :: Sing n -> Sing m -> (n + Succ m) :~: Succ (n + m)

plusSuccL :: Sing n -> Sing m -> (Succ n + m) :~: Succ (n + m)

multZR :: Sing n -> (n * 0) :~: 0

multZL :: Sing n -> (0 * n) :~: 0

multSuccR :: Sing n -> Sing m -> (n * Succ m) :~: ((n * m) + n)

multSuccL :: Sing n -> Sing m -> (Succ n * m) :~: ((n * m) + m)

inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n

Induction scheme for built-in Nat.

plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n)

multComm :: Sing n -> Sing m -> (n * m) :~: (m * n)

plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusMultDistr :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistr :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))