Singletons + TypedHoles

NatProps.hs

{-# LANGUAGE
    DataKinds, PolyKinds, TypeFamilies, TemplateHaskell,
    ScopedTypeVariables, UndecidableInstances, GADTs, TypeOperators #-}

import Data.Singletons.TH

$(singletons [d|
    data Nat = Zero | Succ Nat

    (+) :: Nat -> Nat -> Nat
    Zero   + b = b
    Succ a + b = Succ (a + b)

    (*) :: Nat -> Nat -> Nat
    Zero   * b = Zero
    Succ a * b = b + (a * b)
    |])

sym :: a :~: b -> b :~: a
sym Refl = Refl

addAssoc :: SNat a -> SNat b -> SNat c -> (a :+ (b :+ c)) :~: ((a :+ b) :+ c)
addAssoc SZero b c = Refl
addAssoc (SSucc a) b c = case addAssoc a b c of Refl -> Refl

addComm :: SNat a -> SNat b -> (a :+ b) :~: (b :+ a)
addComm SZero SZero = Refl
addComm (SSucc a) SZero = case addComm a SZero of Refl -> Refl
addComm SZero (SSucc b) = case addComm SZero b of Refl -> Refl
addComm sa@(SSucc a) sb@(SSucc b) = case
    (addComm a sb,
     addComm b sa,
     addComm a b
    ) of (Refl, Refl, Refl) -> Refl

mulComm :: SNat a -> SNat b -> (a :* b) :~: (b :* a)
mulComm SZero     SZero = Refl
mulComm (SSucc a) SZero = case mulComm a SZero of Refl -> Refl
mulComm SZero (SSucc b) = case mulComm SZero b of Refl -> Refl
mulComm sa@(SSucc a) sb@(SSucc b) = case 
    (mulComm a sb, 
     mulComm b sa, 
     mulComm b a, 
     addAssoc b a (a %:* b), 
     addAssoc a b (a %:* b), 
     addComm b a
    ) of (Refl, Refl, Refl, Refl, Refl, Refl) -> Refl

mulDistL :: SNat a -> SNat b -> SNat c -> (a :* (b :+ c)) :~: ((a :* b) :+ (a :* c))
mulDistL SZero b c = Refl
mulDistL (SSucc a) b c = case
    (mulDistL a b c,
     sym $ addAssoc b (a %:* b) (c %:+ (a %:* c)),
     addAssoc (a %:* b) c (a %:* c),
     addComm (a %:* b) c,
     sym $ addAssoc c (a %:* b) (a %:* c),
     addAssoc b c ((a %:* b) %:+ (a %:* c))
    ) of (Refl, Refl, Refl, Refl, Refl, Refl) -> Refl

mulDistR :: SNat a -> SNat b -> SNat c -> ((a :+ b) :* c) :~: ((a :* c) :+ (b :* c))
mulDistR a b c = case 
    (mulComm (a %:+ b) c, 
     mulComm a c, 
     mulComm b c
    ) of (Refl, Refl, Refl) -> mulDistL c a b

mulAssoc :: SNat a -> SNat b -> SNat c -> (a :* (b :* c)) :~: ((a :* b) :* c)
mulAssoc SZero b c = Refl
mulAssoc (SSucc a) b c = case
    (mulDistR b (a %:* b) c,
     mulAssoc a b c
    ) of (Refl, Refl) -> Refl