乘法交换律与结合律

{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

module Kata.AdditionCommutes
  (  ) where

import Kata.AdditionCommutes.Definitions
  ( Z, S
  , Natural(..), Equal(..)
  , (:+:))


reflexive :: Natural n -> Equal n n
reflexive NumZ = EqlZ
reflexive (NumS n) = EqlS $ reflexive n

-- | if a = b, then b = a.
symmetric :: Equal a b -> Equal b a
symmetric EqlZ = EqlZ
symmetric (EqlS a) = EqlS $ symmetric a

plus :: Natural a -> Natural b -> Natural (a :+: b)
plus NumZ x = x
plus (NumS x) a = NumS (plus x a)

-- | if a = b and b = c, then a = c.
transitive :: Equal a b -> Equal b c -> Equal a c
transitive EqlZ EqlZ = EqlZ
transitive (EqlS a) (EqlS b) = EqlS $ transitive a b

nPlusZero :: Equal n n -> Equal n (n :+: Z)
nPlusZero EqlZ = EqlZ
nPlusZero (EqlS n) = EqlS $ nPlusZero n

nPlusSm :: Natural n -> Natural m -> Equal (n :+: S m) (S (n :+: m))
nPlusSm NumZ m = EqlS $ reflexive m
nPlusSm (NumS n) m = EqlS $ nPlusSm n m

-- This is the proof that the kata requires.
-- | a + b = b + a
 :: Natural a -> Natural b -> Equal (a :+: b) (b :+: a)
 n NumZ = symmetric $ nPlusZero $ reflexive n
 n (NumS m) = transitive (nPlusSm n m) (symmetric (EqlS $ plusCommutes m n))

-- For reference, here are the definitions, if you
-- want to copy them into an IDE:
{-

-- | The natural numbers, encoded in types.
data Z
data S n

-- | Predicate describing natural numbers.
-- | This allows us to reason with Nats.
data Natural :: * -> * where
    NumZ :: Natural Z
    NumS :: Natural n -> Natural (S n)

-- | Predicate describing equality of natural numbers.
data Equal :: * -> * -> * where
    EqlZ :: Equal Z Z
    EqlS :: Equal n m -> Equal (S n) (S m)

-- | Peano definition of addition.
type family (:+:) (n :: *) (m :: *) :: *
type instance Z :+: m = m
type instance S n :+: m = S (n :+: m)

-}

{-# LANGUAGE TypeOperators, TypeFamilies, GADTs #-}

module Kata.AdditionAssoc where

import Kata.AdditionAssoc.Definitions

{- Preloaded code, might be helpful for
   doing this Kata locally

-- | The natural numbers, encoded in types.
data Z
data S n

-- | Predicate describing natural numbers.
-- | This allows us to reason with Nats.
data Natural :: * -> * where
  NumZ :: Natural Z
  NumS :: Natural n -> Natural (S n)

-- | Predicate describing equality of natural numbers.
data Equal :: * -> * -> * where
  EqlZ :: Equal Z Z
  EqlS :: Equal n m -> Equal (S n) (S m)

-- | Peano definition of addition.
type family (:+:) (n :: *) (m :: *) :: *
type instance Z :+: m = m
type instance S n :+: m = S (n :+: m)

-}


reflexive :: Natural n -> Equal n n
reflexive NumZ = EqlZ
reflexive (NumS n) = EqlS $ reflexive n

-- | if a = b, then b = a.
symmetric :: Equal a b -> Equal b a
symmetric EqlZ = EqlZ
symmetric (EqlS a) = EqlS $ symmetric a

plus :: Natural a -> Natural b -> Natural (a :+: b)
plus NumZ x = x
plus (NumS x) a = NumS (plus x a)

-- This is the proof that the kata requires.
-- | a + (b + c) = (a + b) + c
plusAssoc :: Natural a -> Natural b -> Natural c -> Equal (a :+: (b :+: c)) ((a :+: b) :+: c)
plusAssoc NumZ p q = reflexive (plus p q)
plusAssoc (NumS n) m p = EqlS $ plusAssoc n m p