{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts   #-}
{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-}
{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies            #-}
{-# LANGUAGE TypeInType, ViewPatterns , ExplicitNamespaces                 #-}
module Data.Type.Natural.Class.Arithmetic
       (Zero, One, S, sZero, sOne, ZeroOrSucc(..),
        plusCong, plusCongR, plusCongL, succCong,
        multCong, multCongL, multCongR,
        minusCong, minusCongL, minusCongR,
        IsPeano(..), pattern Zero, pattern Succ,
        module Data.Type.Natural.Singleton.Compat
       ) where
import Data.Type.Natural.Singleton.Compat
  (type (/=), type (==), type (+), type (*), type (-)
  ,type (/=@#@$) ,type (/=@#@$$), type (/=@#@$$$)
  ,type (==@#@$) ,type (==@#@$$), type (==@#@$$$)
  ,type (+@#@$) ,type (+@#@$$), type (+@#@$$$)
  ,type (*@#@$) ,type (*@#@$$), type (*@#@$$$)
  ,type (-@#@$) ,type (-@#@$$), type (-@#@$$$)
  ,(%==), (%/=), (%+), (%*), (%-)
  , FromInteger, FromIntegerSym0, FromIntegerSym1
  ,SNum(..), PNum(..)
  )

import Data.Functor.Const           (Const (..))
import Data.Singletons.Decide       (SDecide (..))
import Data.Singletons.Prelude      (Apply, SingI (..), SingKind (..),
                                     SomeSing (..), Sing)
import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ, sPred, sSucc)
import Data.Type.Equality           ((:~:) (..))
import Data.Void                    (Void, absurd)
import Numeric.Natural              (Natural)
import Proof.Equational             (because, coerce, start, sym, trans, (===))

type family Zero nat :: nat where
  Zero nat = FromInteger 0

sZero :: (SNum nat) => Sing (Zero nat)
sZero = sFromInteger (sing :: Sing 0)

type family One nat :: nat where
  One nat = FromInteger 1

sOne :: SNum nat => Sing (One nat)
sOne = sFromInteger (sing :: Sing 1)

type S n = Succ n

sS :: SEnum nat => Sing (n :: nat) -> Sing (S n)
sS = sSucc

predCong :: n :~: m -> Pred n :~: Pred m
predCong Refl = Refl

plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m'
plusCong Refl Refl = Refl

plusCongL :: n :~: m -> Sing k -> n + k :~: m + k
plusCongL Refl _ = Refl

plusCongR :: Sing k -> n :~: m -> k + n :~: k + m
plusCongR _ Refl = Refl

succCong :: n :~: m -> S n :~: S m
succCong Refl = Refl

multCong :: n :~: m -> l :~: k -> n * l :~: m * k
multCong Refl Refl = Refl

multCongL :: n :~: m -> Sing k -> n * k :~: m * k
multCongL Refl _ = Refl

multCongR :: Sing k -> n :~: m -> k * n :~: k * m
multCongR _ Refl = Refl

minusCong :: n :~: m -> l :~: k -> n - l :~: m - k
minusCong Refl Refl = Refl

minusCongL :: n :~: m -> Sing k -> n - k :~: m - k
minusCongL Refl _ = Refl

minusCongR :: Sing k -> n :~: m -> k - n :~: k - m
minusCongR _ Refl = Refl

data ZeroOrSucc (n :: nat) where
  IsZero :: ZeroOrSucc (Zero nat)
  IsSucc :: Sing n -> ZeroOrSucc (Succ n)

newtype Assoc op n = Assoc { assocProof :: forall k l. Sing k -> Sing l ->
                             Apply (op (Apply (op n) k)) l :~:
                             Apply (op n) (Apply (op k) l)
                           }


newtype IdentityR op e (n :: nat) = IdentityR { idRProof :: Apply (op n) e :~: n }
newtype IdentityL op e (n :: nat) = IdentityL { idLProof :: Apply (op e) n :~: n }

type PlusZeroR (n :: nat) = IdentityR (+@#@$$) (Zero nat) n
newtype PlusSuccR (n :: nat) =
  PlusSuccR { plusSuccRProof :: forall m. Sing m -> n + S m :~: S (n + m) }

type PlusZeroL (n :: nat) = IdentityL (+@#@$$) (Zero nat) n
newtype PlusSuccL (m :: nat) =
  PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n + m :~: S (n + m) }

newtype Comm op n = Comm { commProof :: forall m. Sing m -> Apply (op n) m :~: Apply (op m) n }

type PlusComm = Comm (+@#@$$)

newtype MultZeroL (n :: nat) =  MultZeroL { multZeroLProof :: Zero nat * n :~: Zero nat }
newtype MultZeroR (n :: nat) =
  MultZeroR { multZeroRProof :: n * Zero nat :~: Zero nat }

newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n * m :~: n * m + m }
newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n * S m :~: n * m + n }

newtype PlusMultDistrib (n :: nat) =
  PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l
                                         -> (n + m) * l :~: (n * l) + (m * l)
                  }

newtype PlusEqCancelL (n :: nat) =
  PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l
                                                       -> n + m :~: n + l -> m :~: l }

newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat + n }
newtype MultEqCancelR n =
  MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l
                                        -> n * Succ l :~: m * Succ l
                                        -> n :~: m
                }

class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat)
    => IsPeano nat where
  {-# MINIMAL succOneCong, succNonCyclic, predSucc, plusMinus,
              succInj, ( (plusZeroL, plusSuccL) | (plusZeroR, plusZeroL))
                     , ( (multZeroL, multSuccL) | (multZeroR, multSuccR)),
              induction #-}

  succOneCong   :: Succ (Zero nat) :~: One nat
  succInj       :: Succ n :~: Succ (m :: nat) -> n :~: m
  succInj'      :: proxy n -> proxy' m -> Succ n :~: Succ (m :: nat) -> n :~: m
  succInj' _ _  = succInj
  succNonCyclic :: Sing n -> Succ n :~: Zero nat -> Void
  induction     :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k
  plusMinus :: Sing (n :: nat) -> Sing m -> n + m - m :~: n

  plusMinus' :: Sing (n :: nat) -> Sing m -> n + m - n :~: m
  plusMinus'  n m =
    start (n %+ m %- n)
      === m %+ n %- n   `because` minusCongL (plusComm n m) n
      === m               `because` plusMinus m n

  plusZeroL :: Sing n -> (Zero nat + n) :~: n
  plusZeroL sn = idLProof (induction base step sn)
    where
      base :: PlusZeroL (Zero nat)
      base = IdentityL (plusZeroR sZero)

      step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n)
      step sk (IdentityL ih) = IdentityL $
        start (sZero %+ sS sk)
          === sS (sZero %+ sk) `because` plusSuccR sZero sk
          === sS sk             `because` succCong ih

  plusSuccL :: Sing n -> Sing m -> S n + m :~: S (n + m :: nat)
  plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0
    where
      base :: PlusSuccL (Zero nat)
      base = PlusSuccL $ \sn ->
        start (sS sn %+ sZero)
          === sS sn             `because` plusZeroR (sS sn)
          === sS (sn %+ sZero) `because` succCong (sym $ plusZeroR sn)

      step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n)
      step sm (PlusSuccL ih) = PlusSuccL $ \sn ->
        start (sS sn %+ sS sm)
        === sS (sS sn %+ sm)   `because` plusSuccR (sS sn) sm
        === sS (sS (sn %+ sm)) `because` succCong (ih sn)
        === sS (sn %+ sS sm)   `because` succCong (sym $ plusSuccR sn sm)

  plusZeroR :: Sing n -> (n + Zero nat) :~: n
  plusZeroR sn = idRProof (induction base step sn)
    where
      base :: PlusZeroR (Zero nat)
      base = IdentityR (plusZeroL sZero)

      step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n)
      step sk (IdentityR ih) = IdentityR $
        start (sS sk %+ sZero)
          === sS (sk %+ sZero) `because` plusSuccL sk sZero
          === sS sk             `because` succCong ih

  plusSuccR :: Sing n -> Sing m -> n + S m :~: S (n + m :: nat)
  plusSuccR sn0 = plusSuccRProof (induction base step sn0)
    where
      base :: PlusSuccR (Zero nat)
      base = PlusSuccR $ \sk ->
        start (sZero %+ sS sk)
          === sS sk             `because` plusZeroL (sS sk)
          === sS (sZero %+ sk) `because` succCong (sym $ plusZeroL sk)

      step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n)
      step sn (PlusSuccR ih) = PlusSuccR $ \sk ->
        start (sS sn %+ sS sk)
        === sS (sn %+ sS sk)    `because` plusSuccL sn (sS sk)
        === sS (sS (sn %+ sk))  `because` succCong (ih sk)
        === sS (sS sn %+ sk)    `because` succCong (sym $ plusSuccL sn sk)

  plusComm  :: Sing n -> Sing m -> n + m :~: (m :: nat) + n
  plusComm sn0 = commProof (induction base step sn0)
    where
      base :: PlusComm (Zero nat)
      base = Comm $ \sk ->
        start (sZero %+ sk)
          === sk             `because` plusZeroL sk
          === (sk %+ sZero) `because` sym (plusZeroR sk)

      step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n)
      step sn (Comm ih) = Comm $ \sk ->
        start (sS sn %+ sk)
          === sS (sn %+ sk) `because` plusSuccL sn sk
          === sS (sk %+ sn) `because` succCong (ih sk)
          === sk %+ sS sn   `because` sym (plusSuccR sk sn)

  plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l
            -> (n + m) + l :~: n + (m + l)
  plusAssoc sn m l = assocProof (induction base step sn) m l
    where
      base :: Assoc (+@#@$$) (Zero nat)
      base = Assoc $ \ sk sl ->
        start ((sZero %+ sk) %+ sl)
          === sk %+ sl
              `because` plusCongL (plusZeroL sk) sl
          === (sZero %+ (sk %+ sl))
              `because` sym (plusZeroL (sk %+ sl))

      step :: forall k . Sing (k :: nat) -> Assoc (+@#@$$) k -> Assoc (+@#@$$) (S k)
      step sk (Assoc ih) = Assoc $ \ sl su ->
        start ((sS sk %+ sl) %+ su)
        ===   (sS (sk %+ sl) %+ su) `because` plusCongL (plusSuccL sk sl) su
        ===   sS (sk %+ sl %+ su)   `because` plusSuccL (sk %+ sl) su
        ===   sS (sk %+ (sl %+ su)) `because` succCong (ih sl su)
        ===   sS sk %+ (sl %+ su)   `because` sym (plusSuccL sk (sl %+ su))


  multZeroL :: Sing n -> Zero nat * n :~: Zero nat
  multZeroL sn0 = multZeroLProof $ induction base step sn0
    where
      base :: MultZeroL (Zero nat)
      base = MultZeroL (multZeroR sZero)

      step :: Sing (k :: nat) -> MultZeroL k ->  MultZeroL (S k)
      step sk (MultZeroL ih) = MultZeroL $
        start (sZero %* sS sk)
        === sZero %* sk %+ sZero  `because` multSuccR sZero sk
        === sZero %* sk            `because` plusZeroR (sZero %* sk)
        === sZero                   `because` ih

  multSuccL :: Sing (n :: nat) -> Sing m -> S n * m :~: n * m + m
  multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0
    where
      base :: MultSuccL (Zero nat)
      base = MultSuccL $ \sk ->
        start (sS sk %* sZero)
          === sZero                  `because` multZeroR (sS sk)
          === sk %* sZero           `because` sym (multZeroR sk)
          === sk %* sZero %+ sZero `because` sym (plusZeroR (sk %* sZero))

      step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m)
      step sm (MultSuccL ih) = MultSuccL $ \sk ->
        start (sS sk %* sS sm)
          === sS sk %* sm       %+ sS sk
              `because` multSuccR (sS sk) sm
          === (sk %* sm %+ sm) %+ sS sk
              `because` plusCongL (ih sk) (sS sk)
          === sS ((sk %* sm %+ sm) %+ sk)
              `because` plusSuccR (sk %* sm %+ sm) sk
          === sS (sk %* sm %+ (sm %+ sk))
              `because` succCong (plusAssoc (sk %* sm) sm sk)
          === sS (sk %* sm %+ (sk %+ sm))
              `because` succCong (plusCongR (sk %* sm) (plusComm sm sk))
          === sS ((sk %* sm %+ sk) %+ sm)
              `because` succCong (sym $ plusAssoc (sk %* sm) sk sm)
          === sS ((sk %* sS sm) %+ sm)
              `because` succCong (plusCongL (sym $ multSuccR sk sm) sm)
          === sk %* sS sm %+ sS sm `because` sym (plusSuccR (sk %* sS sm) sm)

  multZeroR :: Sing n -> n * Zero nat :~: Zero nat
  multZeroR sn0 = multZeroRProof $ induction base step sn0
    where
      base :: MultZeroR (Zero nat)
      base = MultZeroR (multZeroR sZero)

      step :: Sing (k :: nat) -> MultZeroR k ->  MultZeroR (S k)
      step sk (MultZeroR ih) = MultZeroR $
        start (sS sk %* sZero)
        === sk %* sZero %+ sZero  `because` multSuccL sk sZero
        === sk %* sZero            `because` plusZeroR (sk %* sZero)
        === sZero                   `because` ih

  multSuccR :: Sing n -> Sing m -> n * S m :~: n * m + (n :: nat)
  multSuccR sn0 = multSuccRProof $ induction base step sn0
    where
      base :: MultSuccR (Zero nat)
      base = MultSuccR $ \sk ->
        start (sZero %* sS sk)
          === sZero
              `because` multZeroL (sS sk)
          === sZero %* sk
              `because` sym (multZeroL sk)
          === sZero %* sk %+ sZero
              `because` sym (plusZeroR (sZero %* sk))


      step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n)
      step sn (MultSuccR ih) = MultSuccR $ \sk ->
        start (sS sn %* sS sk)
          === sn %* sS sk %+ sS sk
              `because` multSuccL sn (sS sk)
          === sS (sn %* sS sk %+ sk)
              `because` plusSuccR (sn %* sS sk) sk
          === sS (sn %* sk %+ sn %+ sk)
              `because` succCong (plusCongL (ih sk) sk)
          === sS (sn %* sk %+ (sn %+ sk))
              `because` succCong (plusAssoc (sn %* sk) sn sk)
          === sS (sn %* sk %+ (sk %+ sn))
              `because` succCong (plusCongR (sn %* sk) (plusComm sn sk))
          === sS (sn %* sk %+ sk %+ sn)
              `because` succCong (sym $ plusAssoc (sn %* sk) sk sn)
          === sS (sS sn %* sk %+ sn)
              `because` succCong (plusCongL (sym $ multSuccL sn sk) sn)
          === sS sn %* sk %+ sS sn
              `because` sym (plusSuccR (sS sn %* sk) sn)


  multComm  :: Sing (n :: nat) -> Sing m -> n * m :~: m * n
  multComm sn0 = commProof (induction base step sn0)
    where
      base :: Comm (*@#@$$) (Zero nat)
      base = Comm $ \sk ->
        start (sZero %* sk)
          === sZero           `because` multZeroL sk
          === sk %* sZero    `because` sym (multZeroR sk)

      step :: Sing (n :: nat) -> Comm (*@#@$$) n -> Comm (*@#@$$) (S n)
      step sn (Comm ih) = Comm $ \sk ->
        start (sS sn %* sk)
          === sn %* sk %+ sk `because` multSuccL sn sk
          === sk %* sn %+ sk `because` plusCongL (ih sk) sk
          === sk %* sS sn     `because` sym (multSuccR sk sn)

  multOneR :: Sing n -> n * One nat :~: n
  multOneR sn =
    start (sn %* sOne)
      === sn %* sS sZero      `because` multCongR sn (sym $ succOneCong)
      === sn %* sZero %+ sn  `because` multSuccR sn sZero
      === sZero %+ sn         `because` plusCongL (multZeroR sn) sn
      === sn                   `because` plusZeroL sn

  multOneL :: Sing n -> One nat * n :~: n
  multOneL sn =
    start (sOne %* sn)
      === sn %* sOne   `because` multComm sOne sn
      === sn            `because` multOneR sn

  plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l
                -> (n + m) * l :~: (n * l) + (m * l)
  plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0
    where
      base :: PlusMultDistrib (Zero nat)
      base = PlusMultDistrib $ \sk sl ->
        start ((sZero %+ sk) %* sl)
          === (sk %* sl)
              `because` multCongL (plusZeroL sk) sl
          === sZero %+ (sk %* sl)
              `because` sym (plusZeroL (sk %* sl))
          === sZero %* sl %+ sk %* sl
              `because` plusCongL (sym $ multZeroL sl) (sk %* sl)

      step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n)
      step sn (PlusMultDistrib ih) = PlusMultDistrib $ \sk sl ->
        start ((sS sn %+ sk) %* sl)
          === (sS (sn %+ sk) %* sl)           `because` multCongL (plusSuccL sn sk) sl
          === (sn %+ sk) %* sl %+ sl         `because` multSuccL (sn %+ sk) sl
          === ((sn %* sl) %+ (sk %* sl)) %+ sl  `because` plusCongL (ih sk sl) sl
          === sn %* sl %+ (sk %* sl %+ sl)  `because` plusAssoc (sn %* sl) (sk %* sl) sl
          === sn %* sl %+ (sl %+ (sk %* sl))  `because` plusCongR (sn %* sl) (plusComm (sk %* sl) sl)
          === (sn %* sl %+ sl) %+ (sk %* sl)  `because` sym (plusAssoc (sn %* sl) sl (sk %* sl))
          === (sS sn %* sl) %+ (sk %* sl)     `because` plusCongL (sym $ multSuccL sn sl) (sk %* sl)

  multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l
                -> n * (m + l) :~: (n * m) + (n * l)
  multPlusDistrib n m l =
    start (n %* (m %+ l))
      === (m %+ l) %* n     `because` multComm n (m %+ l)
      === m %* n %+ l %* n `because` plusMultDistrib m l n
      === n %* m %+ n %* l `because` plusCong (multComm m n) (multComm l n)

  minusNilpotent :: Sing n -> n - n :~: Zero nat
  minusNilpotent n =
    start (n %- n)
      === (sZero %+ n) %- n  `because` minusCongL (sym $ plusZeroL n) n
      === sZero                `because` plusMinus sZero n

  multAssoc :: Sing (n :: nat) -> Sing m -> Sing l
            -> (n * m) * l :~: n * (m * l)
  multAssoc sn0 = assocProof $ induction base step sn0
    where
      base :: Assoc (*@#@$$) (Zero nat)
      base = Assoc $ \ m l ->
        start (sZero %* m %* l)
          === sZero %* l  `because` multCongL (multZeroL m) l
          === sZero        `because` multZeroL l
          === sZero %*  (m %* l) `because` sym (multZeroL (m %* l))

      step :: Sing (n :: nat) -> Assoc (*@#@$$) n -> Assoc (*@#@$$) (S n)
      step n _ = Assoc $ \ m l ->
        start (sS n %* m %* l)
          === (n %* m %+ m) %* l        `because` multCongL (multSuccL n m) l
          === n %* m %* l %+ m %* l    `because` plusMultDistrib (n %* m) m l
          === n %* (m %* l) %+ m %* l  `because` plusCongL (multAssoc n m l) (m %* l)
          === sS n %* (m %* l)           `because` sym (multSuccL n (m %* l))

  plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n + m :~: n + l -> m :~: l
  plusEqCancelL = plusEqCancelLProof . induction base step
    where
      base :: PlusEqCancelL (Zero nat)
      base = PlusEqCancelL $ \l m nlnm ->
        start l === sZero %+ l `because` sym (plusZeroL l)
                === sZero %+ m `because` nlnm
                === m           `because` plusZeroL m

      step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n)
      step n (PlusEqCancelL ih) = PlusEqCancelL $ \l m snlsnm ->
        succInj $ ih (sS l) (sS m) $
          start (n %+ sS l)
            ===  sS (n %+ l)  `because` plusSuccR n l
            ===  sS n %+ l    `because` sym (plusSuccL n l)
            ===  sS n %+ m    `because` snlsnm
            ===  sS (n %+ m)  `because` plusSuccL n m
            ===  n %+ sS m    `because` sym (plusSuccR n m)

  plusEqCancelR :: forall n m l . Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m + l -> n :~: m
  plusEqCancelR n m l nlml = plusEqCancelL l n m $
    start (l %+ n)
      === (n %+ l) `because` plusComm l n
      === (m %+ l) `because` nlml
      === (l %+ m) `because` plusComm m l

  succAndPlusOneL :: Sing n -> Succ n :~: One nat + n
  succAndPlusOneL = proofSuccPlusL . induction base step
    where
      base :: SuccPlusL (Zero nat)
      base = SuccPlusL $
             start (sSucc sZero)
               === sOne           `because` succOneCong
               === sOne %+ sZero `because` sym (plusZeroR sOne)

      step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n)
      step sn (SuccPlusL ih) = SuccPlusL $
        start (sSucc (sSucc sn))
          === sSucc (sOne %+ sn) `because` succCong ih
          === sOne %+ sSucc sn   `because` sym (plusSuccR sOne sn)

  succAndPlusOneR :: Sing n -> Succ n :~: n + One nat
  succAndPlusOneR n =
    start (sSucc n)
      === sOne %+ n `because` succAndPlusOneL n
      === n %+ sOne `because` plusComm sOne n

  predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat)

  zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n
  zeroOrSucc = induction base step
    where
      base = IsZero
      step sn _ = IsSucc sn

  plusEqZeroL :: Sing n -> Sing m -> n + m :~: Zero nat -> n :~: Zero nat
  plusEqZeroL n m Refl =
    case zeroOrSucc n of
      IsZero    -> Refl
      IsSucc pn -> absurd $ succNonCyclic (pn %+ m) (sym $ plusSuccL pn m)

  plusEqZeroR :: Sing n -> Sing m -> n + m :~: Zero nat -> m :~: Zero nat
  plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n)

  predUnique :: Sing (n :: nat) -> Sing m -> Succ n :~: m -> n :~: Pred m
  predUnique n m snEm =
    start n === (sPred (sSucc n)) `because` sym (predSucc n)
            === sPred m           `because` predCong snEm

  multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> n :~: Succ (Pred n)
  multEqSuccElimL n m l nmEsl =
    case zeroOrSucc n of
      IsZero -> absurd $ succNonCyclic l $ sym $
                start sZero === sZero %* m `because` sym (multZeroL m)
                            === sSucc l     `because` nmEsl
      IsSucc pn -> succCong (predUnique pn n Refl)

  multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> m :~: Succ (Pred m)
  multEqSuccElimR n m l nmEsl =
    multEqSuccElimL m n l (multComm m n `trans` nmEsl)

  minusZero :: Sing n -> n - Zero nat :~: n
  minusZero n =
    start (n %- sZero)
      === (n %+ sZero) %- sZero
             `because` minusCongL (sym $ plusZeroR n) sZero
      === n  `because` plusMinus n sZero

  multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n * Succ l :~: m * Succ l -> n :~: m
  multEqCancelR = proofMultEqCancelR . induction base step
    where
      base :: MultEqCancelR (Zero nat)
      base = MultEqCancelR $ \m l zslmsl ->
        sym $ plusEqZeroR (m %* l) m $ sym $ start sZero
          === sZero %* l            `because` sym (multZeroL l)
          === sZero %* l %+ sZero  `because` sym (plusZeroR (sZero %* l))
          === sZero %* sSucc l      `because` sym (multSuccR sZero l)
          === m     %* sSucc l      `because` zslmsl
          === m %* l %+ m          `because` multSuccR m l

      step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n)
      step n (MultEqCancelR ih) = MultEqCancelR $ \m l snmssnl ->
        let m' = sPred m
            pf = start (m %* sSucc l)
                   === sSucc n %* sSucc l         `because` sym snmssnl
                   === n %* sSucc l %+ sSucc l   `because` multSuccL n (sSucc l)
                   === sSucc (n %* sSucc l %+ l) `because` plusSuccR (n %* sSucc l) l
            sm'Em = multEqSuccElimL m (sSucc l) (n %* sSucc l %+ l) pf
            pf' = ih m' l $ plusEqCancelR (n %* sSucc l) (m' %* sSucc l) (sSucc l) $
                  start (n %* sSucc l %+ sSucc l)
                    === sSucc (n %* sSucc l %+ l)  `because` plusSuccR (n %* sSucc l) l
                    === m %* sSucc l                `because` sym pf
                    === sSucc m' %* sSucc l         `because` multCongL sm'Em (sSucc l)
                    === (m' %* sSucc l %+ sSucc l) `because` multSuccL m' (sSucc l)
        in succCong pf' `trans` sym sm'Em

  succPred :: Sing n -> (n :~: Zero nat -> Void) -> Succ (Pred n) :~: n
  succPred n nonZero =
    case zeroOrSucc n of
      IsZero    -> absurd $ nonZero Refl
      IsSucc n' -> sym $ succCong $ predUnique n' n Refl

  multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> Succ n * m :~: Succ n * l -> m :~: l
  multEqCancelL n m l snmEsnl =
    multEqCancelR m l n $
    multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l

  sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)
  sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)

  toNatural :: Sing (n :: nat) -> Natural
  toNatural = getConst . induction (Const 0) (\_ (Const k) -> (Const k + 1))

  fromNatural :: Natural -> SomeSing nat
  fromNatural 0 = SomeSing sZero
  fromNatural n =
    case fromNatural (n - 1) of
      SomeSing sn -> SomeSing (Succ sn)

pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n
pattern Zero <- (zeroOrSucc -> IsZero) where
  Zero = sZero

pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n
pattern Succ n <- (zeroOrSucc -> IsSucc n) where
  Succ n = sSucc n