自然数上の加法、乗法とその性質

code:NatProp.hs

module NatProp

where

import Data.Type.Equality

data Nat

= Zero

| Succ Nat

type family (m :: Nat) + (n :: Nat) :: Nat where

m + Zero = m

m + Succ n = Succ (m + n)

type family (m :: Nat) * (n :: Nat) :: Nat where

m * Zero = Zero

m * Succ n = (m * n) + m

data SNat (n :: Nat) where

SZero :: SNat Zero

SSucc :: SNat n -> SNat (Succ n)

(%+) :: SNat m -> SNat n -> SNat (m + n)

m %+ SZero = m

m %+ SSucc n = SSucc (m %+ n)

(%*) :: SNat m -> SNat n -> SNat (m * n)

m %* SZero = SZero

m %* SSucc n = (m %* n) %+ m

--

leftUnitAdd :: SNat n -> (Zero + n) :~: n

leftUnitAdd n = case n of

SZero -> Refl

SSucc n' -> case leftUnitAdd n' of

Refl -> Refl

rightUnitAdd :: SNat n -> (n + Zero) :~: n

rightUnitAdd n = Refl

unitAdd :: SNat n -> (n + Zero) :~: (Zero + n)

unitAdd n = case rightUnitAdd n of

Refl -> case leftUnitAdd n of

Refl -> Refl

leftSuccAdd :: SNat m -> SNat n -> (Succ m + n) :~: Succ (m + n)

leftSuccAdd m n = case n of

SZero -> Refl

SSucc n' -> case leftSuccAdd m n' of

Refl -> Refl

rightSuccAdd :: SNat m -> SNat n -> (m + Succ n) :~: Succ (m + n)

rightSuccAdd m n = Refl

succAdd :: SNat m -> SNat n -> (m + Succ n) :~: (Succ m + n)

succAdd m n = case rightSuccAdd m n of

Refl -> case leftSuccAdd m n of

Refl -> Refl

commutativeAdd :: SNat m -> SNat n -> (m + n) :~: (n + m)

commutativeAdd m n = case n of

SZero -> case unitAdd m of

Refl -> Refl

SSucc n' -> case succAdd m n' of

Refl -> case commutativeAdd m n' of

Refl -> case succAdd n' m of

Refl -> Refl

associativeAdd :: SNat k -> SNat m -> SNat n

-> ((k + m) + n) :~: (k + (m + n))

associativeAdd k m n = case n of

SZero -> Refl

SSucc n' -> case associativeAdd k m n' of

Refl -> Refl

--

leftZeroMul :: SNat n -> (Zero * n) :~: Zero

leftZeroMul n = case n of

SZero -> Refl

SSucc n' -> case leftZeroMul n' of

Refl -> Refl

rightZeroMul :: SNat n -> (n * Zero) :~: Zero

rightZeroMul n = Refl

zeroMul :: SNat n -> (n * Zero) :~: (Zero * n)

zeroMul n = case rightZeroMul n of

Refl -> case leftZeroMul n of

Refl -> Refl

leftUnitMul :: SNat n -> (Succ Zero * n) :~: n

leftUnitMul n = case n of

SZero -> Refl

SSucc n' -> case leftUnitMul n' of

Refl -> case succAdd n' SZero of

Refl -> Refl

rightUnitMul :: SNat n -> (n * Succ Zero) :~: n

rightUnitMul n = case rightZeroMul n of

Refl -> leftUnitAdd n

unitMul :: SNat n -> (n * Succ Zero) :~: (Succ Zero * n)

unitMul n = case rightUnitMul n of

Refl -> case leftUnitMul n of

Refl -> Refl

leftSuccMul :: SNat m -> SNat n -> (Succ m * n) :~: ((m * n) + n)

leftSuccMul m n = case n of

SZero -> Refl

SSucc n' -> case leftSuccMul m n' of

Refl -> case associativeAdd (m %* n') n' m of

Refl -> case commutativeAdd n' m of

Refl -> case associativeAdd (m %* n') m n' of

Refl -> Refl

rightSuccMul :: SNat m -> SNat n -> (m * Succ n) :~: ((m * n) + m)

rightSuccMul m n = Refl

--

commutativeMul :: SNat m -> SNat n -> (m * n) :~: (n * m)

commutativeMul m n = case m of

SZero -> case zeroMul n of

Refl -> Refl

SSucc m1 -> case leftSuccMul m1 n of

Refl -> case commutativeMul m1 n of

Refl -> Refl

distributiveMulAdd :: SNat k -> SNat m -> SNat n

-> (k * (m + n)) :~: ((k * m) + (k * n))

distributiveMulAdd k m n = case n of

SZero -> Refl

SSucc n' -> case distributiveMulAdd k m n' of

Refl -> case associativeAdd (k %* m) (k %* n') k of

Refl -> Refl

distributiveAddMul :: SNat k -> SNat m -> SNat n

-> ((k + m) * n) :~: ((k * n) + (m * n))

distributiveAddMul k m n

= case commutativeMul (k %+ m) n of

Refl -> case distributiveMulAdd n k m of

Refl -> case commutativeMul n k of

Refl -> case commutativeMul n m of

Refl -> Refl

associativityMul :: SNat k -> SNat m -> SNat n -> ((k * m) * n) :~: (k * (m * n))

associativityMul k m n = case n of

SZero -> Refl

SSucc n' -> case associativityMul k m n' of

Refl -> case distributiveMulAdd k (m %* n') m of

Refl -> Refl