{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces       #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures     #-}
{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes  #-}
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}
module Data.Type.Natural.Class.Order
       (PeanoOrder(..), DiffNat(..), LeqView(..),
        FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,
        sLeqCongL, sLeqCongR, sLeqCong,
        type (-.), (%-.), minPlusTruncMinus, truncMinusLeq,
        module Data.Type.Natural.Singleton.Compat
       ) where
import Data.Type.Natural.Class.Arithmetic
import Data.Type.Natural.Singleton.Compat (type (<), type (<=), type (<=@#@$),
                                           type (<=@#@$$), type (<=@#@$$$),
                                           type (<@#@$), type (<@#@$$),
                                           type (<@#@$$$), type (>), type (>=),
                                           type (>=@#@$), type (>=@#@$$),
                                           type (>=@#@$$$), type (>@#@$),
                                           type (>@#@$$), type (>@#@$$$),
                                           type Min, type Max, type Compare,
                                           type MinSym0, type MinSym1, type MinSym2,
                                           type MaxSym0, type MaxSym1, type MaxSym2,
                                           type CompareSym0, type CompareSym1, type CompareSym2,
                                           Sing (SLT, SEQ, SGT), SOrd(..), POrd(..),
                                           LTSym0, GTSym0, EQSym0,
                                           (%<), (%<=), (%>), (%>=))

import Data.Singletons.Prelude      (Sing (SFalse, STrue), sing, withSingI)
import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ)
import Data.Singletons.TH           (singletonsOnly)
import Data.Type.Equality           ((:~:) (..))
import Data.Void                    (Void, absurd)
import Proof.Equational             (because, coerce, start, sym, trans,
                                     withRefl, (===), (=~=))
import Proof.Propositional          (IsTrue (..), eliminate, withWitness)

data LeqView (n :: nat) (m :: nat) where
  LeqZero :: Sing n -> LeqView (Zero nat) n
  LeqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView (Succ n) (Succ m)

data DiffNat n m where
  DiffNat :: Sing n -> Sing m -> DiffNat n (n + m)

newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n <= m) -> DiffNat n m }
newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m) }

succDiffNat :: IsPeano nat
            => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m)
succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m

coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l
           -> IsTrue (n <= l) -> IsTrue (m <= l)
coerceLeqL Refl _ Witness = Witness

coerceLeqR :: forall (n :: nat) m l . IsPeano nat =>  Sing l -> n :~: m
           -> IsTrue (l <= n) -> IsTrue (l <= m)
coerceLeqR _ Refl Witness = Witness

singletonsOnly [d|
  flipOrdering :: Ordering -> Ordering
  flipOrdering EQ = EQ
  flipOrdering LT = GT
  flipOrdering GT = LT
 |]

congFlipOrdering :: a :~: b -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering Refl = Refl

compareCongR :: Sing (a :: k) -> b :~: c -> Compare a b :~: Compare a c
compareCongR _ Refl = Refl

sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d)
sLeqCong Refl Refl = Refl

sLeqCongL :: a :~: b -> Sing c -> (a <= c) :~: (b <= c)
sLeqCongL Refl _ = Refl

sLeqCongR :: Sing a -> b :~: c -> (a <= b) :~: (a <= c)
sLeqCongR _ Refl = Refl

newtype LTSucc n = LTSucc { proofLTSucc :: Compare n (Succ n) :~: 'LT }
newtype CmpSuccStepR (n :: nat) =
  CmpSuccStepR { proofCmpSuccStepR :: forall (m :: nat). Sing m
                                   -> Compare n m :~: 'LT
                                   -> Compare n (Succ m) :~: 'LT
                                   }

newtype LeqViewRefl n = LeqViewRefl { proofLeqViewRefl :: LeqView n n }

class (SOrd nat, IsPeano nat) => PeanoOrder nat where
  {-# MINIMAL ( succLeqToLT, cmpZero, leqRefl
              | leqZero, leqSucc , viewLeq
              | leqWitness, leqStep
              ),
              eqlCmpEQ, ltToLeq, eqToRefl,
              flipCompare, leqToCmp,
              leqReversed, lneqSuccLeq, lneqReversed,
              (leqToMin, geqToMin | minLeqL, minLeqR, minLargest),
              (leqToMax, geqToMax | maxLeqL, maxLeqR, maxLeast) #-}

  leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b)
           -> Either (a :~: b) (Compare a b :~: 'LT)
  eqlCmpEQ :: Sing (a :: nat) -> Sing b -> a :~: b -> Compare a b :~: 'EQ
  eqToRefl :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'EQ -> a :~: b

  flipCompare :: Sing (a :: nat) -> Sing b
              -> FlipOrdering (Compare a b) :~: Compare b a

  ltToNeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT
           -> a :~: b -> Void
  ltToNeq a b aLTb aEQb = eliminate $
    start SLT
      === sCompare a b `because` sym aLTb
      === SEQ          `because` eqlCmpEQ a b aEQb

  leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b) -> (a :~: b -> Void) -> Compare a b :~: 'LT
  leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb


  succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: 'LT
  succLeqToLT a b saLEQb =
    case leqWitness (sSucc a) b saLEQb of
      DiffNat _ k -> let aLEQb = leqStep a b (sSucc k) $
                                 start (a %+ sSucc k)
                                   === sSucc (a %+ k) `because` plusSuccR a k
                                   === sSucc a %+ k   `because` sym (plusSuccL a k)
                                   =~= b
                         aNEQb aeqb = succNonCyclic k $ plusEqCancelL a (sSucc k) sZero $
                                     start (a %+ sSucc k)
                                      === sSucc (a %+ k) `because` plusSuccR a k
                                      === sSucc a %+ k `because` sym (plusSuccL a k)
                                      =~= b
                                      === a               `because` sym aeqb
                                      === a %+ sZero     `because` sym (plusZeroR a)
                     in leqNeqToLT a b aLEQb aNEQb

  ltToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT
          -> IsTrue (a <= b)

  gtToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'GT
          -> IsTrue (b <= a)
  gtToLeq n m nGTm = ltToLeq m n $
    start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)
                         === sFlipOrdering SGT            `because` congFlipOrdering nGTm
                         =~= SLT

  ltToSuccLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT
              -> IsTrue (Succ a <= b)
  ltToSuccLeq n m nLTm =
     leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)

  cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: 'LT
  cmpZero sn = leqToLT sZero (sSucc sn) $ leqStep (sSucc sZero) (sSucc sn) sn $
               start (sSucc sZero %+ sn)
                 === sSucc (sZero %+ sn) `because` plusSuccL sZero sn
                 === sSucc sn             `because` succCong (plusZeroL sn)

  leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b <= a)
              -> Compare a b :~: 'GT
  leqToGT a b sbLEQa =
    start (sCompare a b)
      === sFlipOrdering (sCompare b a) `because` sym (flipCompare b a)
      === sFlipOrdering SLT            `because` congFlipOrdering (leqToLT b a sbLEQa)
      =~= SGT

  cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: 'EQ) (Compare (Zero nat) a :~: 'LT)
  cmpZero' n =
    case zeroOrSucc n of
      IsZero    -> Left $ eqlCmpEQ sZero n Refl
      IsSucc n' -> Right $ cmpZero n'

  zeroNoLT :: Sing a -> Compare a (Zero nat) :~: 'LT -> Void
  zeroNoLT n eql =
    case cmpZero' n of
      Left cmp0nEQ -> eliminate $
        start SGT
          =~= sFlipOrdering SLT
          === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql)
          === sCompare sZero n                 `because` flipCompare n sZero
          === SEQ                              `because` cmp0nEQ
      Right cmp0nLT -> eliminate $
        start SGT
          =~= sFlipOrdering SLT
          === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql)
          === sCompare sZero n                 `because` flipCompare n sZero
          === SLT                              `because` cmp0nLT

  ltRightPredSucc :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT -> b :~: Succ (Pred b)
  ltRightPredSucc a b aLTb =
    case zeroOrSucc b of
      IsZero -> absurd $ zeroNoLT a aLTb
      IsSucc b' -> sym $
        start (sSucc (sPred b))
          =~= sSucc (sPred (sSucc b'))
          === sSucc b' `because` succCong (predSucc b')
          =~= b

  cmpSucc :: Sing (n :: nat) -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)
  cmpSucc n m =
    case sCompare n m of
      SEQ -> let nEQm = eqToRefl n m Refl
             in sym $ eqlCmpEQ (sSucc n) (sSucc m) $ succCong nEQm
      SLT -> case leqWitness (sSucc n) m $ ltToSuccLeq n m Refl of
               DiffNat _ k ->
                 sym $ succLeqToLT (sSucc n) (sSucc m) $
                 leqStep (sSucc (sSucc n)) (sSucc m) k $
                 start (sSucc (sSucc n) %+ k)
                   === sSucc (sSucc n %+ k)    `because` plusSuccL (sSucc n) k
                   =~= sSucc m
      SGT -> case leqWitness (sSucc m) n $ ltToSuccLeq m n (sym $ flipCompare n m) of
               DiffNat _ k ->
                 let pf = (succLeqToLT (sSucc m) (sSucc n) $
                          leqStep (sSucc (sSucc m)) (sSucc n) k $
                          start (sSucc (sSucc m) %+ k)
                            === sSucc (sSucc m %+ k)    `because` plusSuccL (sSucc m) k
                            =~= sSucc n)
                 in start (sCompare n m)
                      =~= SGT
                      =~= sFlipOrdering SLT
                      === sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf)
                      === sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n)

  ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: 'LT
  ltSucc = proofLTSucc . induction base step
    where
      base :: LTSucc (Zero nat)
      base = LTSucc $ cmpZero (sZero :: Sing (Zero nat))

      step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n)
      step n (LTSucc ih) = LTSucc $
        start (sCompare (sSucc n) (sSucc (sSucc n)))
          === sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n))
          === SLT `because` ih

  cmpSuccStepR :: Sing (n :: nat) -> Sing m -> Compare n m :~: 'LT
               -> Compare n (Succ m) :~: 'LT
  cmpSuccStepR = proofCmpSuccStepR . induction base step
    where
      base :: CmpSuccStepR (Zero nat)
      base = CmpSuccStepR $ \m _ -> cmpZero m

      step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n)
      step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->
        case zeroOrSucc m of
          IsZero -> absurd $ zeroNoLT (sSucc n) snltm
          IsSucc m' ->
            let nLTm' = trans (cmpSucc n m') snltm
            in start (sCompare (sSucc n) (sSucc m))
                 =~= sCompare (sSucc n) (sSucc (sSucc m'))
                 === sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m'))
                 === SLT                   `because` ih m' nLTm'

  ltSuccLToLT :: Sing (n :: nat) -> Sing m -> Compare (Succ n) m :~: 'LT
           -> Compare n m :~: 'LT
  ltSuccLToLT n m snLTm =
    case zeroOrSucc m of
      IsZero -> absurd $ zeroNoLT (sSucc n) snLTm
      IsSucc m' ->
        let nLTm = cmpSucc n m' `trans` snLTm
        in start (sCompare n (sSucc m'))
             === SLT `because` cmpSuccStepR n m' nLTm

  leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a <= b)
           -> Compare a b :~: 'LT
  leqToLT n m snLEQm =
    case leqToCmp (sSucc n) m snLEQm of
      Left eql -> withRefl eql $
        start (sCompare n m)
          =~= sCompare n (sSucc n)
          === SLT `because` ltSucc n
      Right nLTm -> ltSuccLToLT n m nLTm

  leqZero :: Sing n -> IsTrue (Zero nat <= n)
  leqZero sn =
    case zeroOrSucc sn of
      IsZero    -> leqRefl sn
      IsSucc pn -> ltToLeq sZero sn $ cmpZero pn

  leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)
  leqSucc n m nLEQm =
    case leqToCmp n m nLEQm of
      Left  eql  -> withRefl eql $ leqRefl (sSucc n)
      Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm

  fromLeqView :: LeqView (n :: nat) m -> IsTrue (n <= m)
  fromLeqView (LeqZero n)         = leqZero n
  fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm

  leqViewRefl :: Sing (n :: nat) -> LeqView n n
  leqViewRefl = proofLeqViewRefl . induction base step
    where
      base :: LeqViewRefl (Zero nat)
      base = LeqViewRefl $ LeqZero sZero
      step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n)
      step n (LeqViewRefl nLEQn) =
        LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn)

  viewLeq :: forall n m . Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> LeqView n m
  viewLeq n m nLEQm =
    case (zeroOrSucc n, leqToCmp n m nLEQm) of
      (IsZero, _)    -> LeqZero m
      (_, Left Refl) -> leqViewRefl n
      (IsSucc n', Right nLTm) ->
         let sm'EQm = ltRightPredSucc n m nLTm
             m' = sPred m
             n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm
         in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm'

  leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> DiffNat n m
  leqWitness = leqWitPf . induction base step
    where
      base :: LeqWitPf (Zero nat)
      base = LeqWitPf $ \sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm

      step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n)
      step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
        case viewLeq (sSucc n) m snLEQm of
          LeqZero _ -> absurd $ succNonCyclic n Refl
          LeqSucc (_ :: Sing n') pm nLEQpm ->
            succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm

  leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m)
  leqStep = leqStepPf . induction base step
    where
      base :: LeqStepPf (Zero nat)
      base = LeqStepPf $ \k _ _ -> leqZero k

      step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n)
      step n (LeqStepPf ih) =
        LeqStepPf $ \k l snPlEqk ->
        let kEQspk = start k
                       === sSucc n %+ l   `because` sym snPlEqk
                       === sSucc (n %+ l) `because` plusSuccL n l
            pk = n %+ l
        in coerceLeqR (sSucc n) (sym kEQspk) $ leqSucc n pk $ ih pk l Refl

  leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> (n :~: m -> Void) -> IsTrue (Succ n <= m)
  leqNeqToSuccLeq n m nLEQm nNEQm =
    case leqWitness n m nLEQm of
      DiffNat _ k ->
        case zeroOrSucc k of
          IsZero -> absurd $ nNEQm $ sym $ plusZeroR n
          IsSucc k' -> leqStep (sSucc n) m k' $
            start (sSucc n %+ k')
              === sSucc (n %+ k') `because` plusSuccL n k'
              === n %+ sSucc k'   `because` sym (plusSuccR n k')
              =~= m

  leqRefl :: Sing (n :: nat) -> IsTrue (n <= n)
  leqRefl sn = leqStep sn sn sZero (plusZeroR sn)

  leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)
  leqSuccStepR n m nLEQm =
    case leqWitness n m nLEQm of
      DiffNat _ k -> leqStep n (sSucc m) (sSucc k) $
        start (n %+ sSucc k) === sSucc (n %+ k) `because` plusSuccR n k =~= sSucc m

  leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)
  leqSuccStepL n m snLEQm =
     leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm

  leqReflexive :: Sing (n :: nat) -> Sing m -> n :~: m -> IsTrue (n <= m)
  leqReflexive n _ Refl = leqRefl n

  leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)
  leqTrans n m k nLEm mLEk =
    case leqWitness n m nLEm of
      DiffNat _ mMn -> case leqWitness m k mLEk of
        DiffNat _ kMn -> leqStep n k (mMn %+ kMn) (sym $ plusAssoc n mMn kMn)

  leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m
  leqAntisymm n m nLEm mLEn =
    case (leqWitness n m nLEm, leqWitness m n mLEn) of
      (DiffNat _ mMn, DiffNat _ nMm) ->
        let pEQ0 = plusEqCancelL n (mMn %+ nMm) sZero $
                   start (n %+ (mMn %+ nMm))
                     === (n %+ mMn) %+ nMm
                         `because` sym (plusAssoc n mMn nMm)
                     =~= m %+ nMm
                     =~= n
                     === n %+ sZero
                         `because` sym (plusZeroR n)
            nMmEQ0 = plusEqZeroL mMn nMm pEQ0

        in sym $ start m
             =~= n %+ mMn
             === n %+ sZero  `because` plusCongR n nMmEQ0
             === n            `because` plusZeroR n

  plusMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k
               -> IsTrue (n <= m) -> IsTrue (l <= k)
               -> IsTrue ((n + l) <= (m + k))
  plusMonotone n m l k nLEm lLEk =
    case (leqWitness n m nLEm, leqWitness l k lLEk) of
      (DiffNat _ mMINn, DiffNat _ kMINl) ->
        let r = mMINn %+ kMINl
        in leqStep (n %+ l) (m %+ k) r $
           start (n %+ l %+ r)
             === n %+ (l %+ r)
                 `because` plusAssoc n l r
             =~= n %+ (l %+ (mMINn %+ kMINl))
             === n %+ (l %+ (kMINl %+ mMINn))
                 `because` plusCongR n (plusCongR l (plusComm mMINn kMINl))
             === n %+ ((l %+ kMINl) %+ mMINn)
                 `because` plusCongR n (sym $ plusAssoc l kMINl mMINn)
             =~= n %+ (k %+ mMINn)
             === n %+ (mMINn %+ k)
                 `because` plusCongR n (plusComm k mMINn)
             === n %+ mMINn %+ k
                 `because` sym (plusAssoc n mMINn k)
             =~= m %+ k

  leqZeroElim :: Sing n -> IsTrue (n <= Zero nat) -> n :~: Zero nat
  leqZeroElim n nLE0 =
    case viewLeq n sZero nLE0 of
      LeqZero _      -> Refl
      LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl

  plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n <= m)
           -> IsTrue ((n + l) <= (m + l))
  plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l)

  plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m <= l)
           -> IsTrue ((n + m) <= (n + l))
  plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq

  plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= (n + m))
  plusLeqL n m = leqStep n (n %+ m) m Refl

  plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= (n + m))
  plusLeqR n m = leqStep m (n %+ m) n $ plusComm m n

  plusCancelLeqR :: Sing (n :: nat) -> Sing m -> Sing l
                 -> IsTrue ((n + l) <= (m + l))
                 -> IsTrue (n <= m)
  plusCancelLeqR n m l nlLEQml =
    case leqWitness (n %+ l) (m %+ l) nlLEQml of
      DiffNat _ k ->
        let pf = plusEqCancelR (n %+ k) m l $
                 start ((n %+ k) %+ l)
                   === n %+ (k %+ l) `because` plusAssoc n k l
                   === n %+ (l %+ k) `because` plusCongR n (plusComm k l)
                   === n %+ l %+ k   `because` sym (plusAssoc n l k)
                   =~= m %+ l
        in leqStep n m k pf

  plusCancelLeqL :: Sing (n :: nat) -> Sing m -> Sing l
                 -> IsTrue ((n + m) <= (n + l))
                 -> IsTrue (m <= l)
  plusCancelLeqL n m l nmLEQnl =
    plusCancelLeqR m l n $
    coerceLeqL (plusComm n m) (l %+ n) $
    coerceLeqR (n %+ m) (plusComm n l) nmLEQnl

  succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero nat) -> Void
  succLeqZeroAbsurd n leq =
    succNonCyclic n (leqZeroElim (sSucc n) leq)

  succLeqZeroAbsurd' :: Sing n -> (S n <= Zero nat) :~: 'False
  succLeqZeroAbsurd' n =
    case sSucc n %<= sZero of
      STrue  -> absurd $ succLeqZeroAbsurd n Witness
      SFalse -> Refl

  succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n <= n) -> Void
  succLeqAbsurd n snLEQn =
    eliminate $
      start SLT
        === sCompare n n `because` sym (succLeqToLT n n snLEQn)
        === SEQ          `because` eqlCmpEQ n n Refl

  succLeqAbsurd' :: Sing (n :: nat) -> (S n <= n) :~: 'False
  succLeqAbsurd' n =
    case sSucc n %<= n of
      STrue  -> absurd $ succLeqAbsurd n Witness
      SFalse -> Refl

  notLeqToLeq :: ((n <= m) ~ 'False) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)
  notLeqToLeq n m =
    case sCompare n m of
      SLT -> eliminate $ ltToLeq n m Refl
      SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl
      SGT -> gtToLeq n m Refl

  leqSucc' :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (Succ n <= Succ m)
  leqSucc' n m =
    case n %<= m of
      STrue -> withWitness (leqSucc n m Witness) Refl
      SFalse ->
        case sSucc n %<= sSucc m of
          SFalse -> Refl
          STrue  ->
            case viewLeq (sSucc n) (sSucc m) Witness of
              LeqZero _ -> absurd $ succNonCyclic n Refl
              LeqSucc n' m' Witness ->
                eliminate $
                start STrue
                  =~= (n' %<= m')
                  === (n  %<= m)   `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl)
                  =~= SFalse

  leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Min n m :~: n
  leqToMin n m nLEQm =
     leqAntisymm (sMin n m) n (minLeqL n m)
                 (minLargest n n m (leqRefl n) nLEQm)

  geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Min n m :~: m
  geqToMin n m mLEQn =
     leqAntisymm (sMin n m) m (minLeqR n m)
                 (minLargest m n m mLEQn (leqRefl m))

  minComm :: Sing (n :: nat) -> Sing m -> Min n m :~: Min m n
  minComm n m =
    case n %<= m of
      STrue -> start (sMin n m) === n        `because` leqToMin n m Witness
                                === sMin m n `because` sym (geqToMin m n Witness)
      SFalse -> start (sMin n m) === m        `because` geqToMin n m (notLeqToLeq n m)
                                 === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m)

  minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= n)
  minLeqL n m =
    case n %<= m of
      STrue  -> leqReflexive (sMin n m) n $ leqToMin n m Witness
      SFalse -> let mLEQn = notLeqToLeq n m
                in leqTrans (sMin n m) m n
                     (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $
                     mLEQn

  minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= m)
  minLeqR n m = leqTrans (sMin n m) (sMin m n) m
                  (leqReflexive (sMin n m) (sMin m n) $ minComm n m)
                  (minLeqL m n)

  minLargest :: Sing (l :: nat) ->  Sing n -> Sing m
             -> IsTrue (l <= n) -> IsTrue (l <= m)
             -> IsTrue (l <= Min n m)
  minLargest l n m lLEQn lLEQm =
    withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $
    case n %<= m of
      STrue -> leqTrans l n (sMin n m) lLEQn $
               leqReflexive sing sing  $ sym $ leqToMin n m Witness
      SFalse ->
        let mLEQn = notLeqToLeq n m
        in leqTrans l m (sMin n m) lLEQm $
           leqReflexive sing sing  $ sym $ geqToMin n m mLEQn

  leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Max n m :~: m
  leqToMax n m nLEQm =
     leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m)

  geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Max n m :~: n
  geqToMax n m mLEQn =
     leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m)

  maxComm :: Sing (n :: nat) -> Sing m -> Max n m :~: Max m n
  maxComm n m =
    case n %<= m of
      STrue -> start (sMax n m) === m        `because` leqToMax n m Witness
                                === sMax m n `because` sym (geqToMax m n Witness)
      SFalse -> start (sMax n m) === n        `because` geqToMax n m (notLeqToLeq n m)
                                 === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m)

  maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= Max n m)
  maxLeqR n m =
    case n %<= m of
      STrue  -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness
      SFalse -> let mLEQn = notLeqToLeq n m
                in leqTrans m n (sMax n m) mLEQn
                     (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn))

  maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= Max n m)
  maxLeqL n m = leqTrans n (sMax m n) (sMax n m)
                  (maxLeqR m n)
                  (leqReflexive (sMax m n) (sMax n m) $ maxComm m n)

  maxLeast :: Sing (l :: nat) ->  Sing n -> Sing m
             -> IsTrue (n <= l) -> IsTrue (m <= l)
             -> IsTrue (Max n m <= l)
  maxLeast l n m lLEQn lLEQm =
    withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $
    case n %<= m of
      STrue -> leqTrans (sMax n m) m l
               (leqReflexive sing sing  $ leqToMax n m Witness)
               lLEQm
      SFalse ->
        let mLEQn = notLeqToLeq n m
        in leqTrans (sMax n m) n l
           (leqReflexive sing sing  $ geqToMax n m mLEQn)
           lLEQn

  leqReversed  :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (m >= n)
  lneqSuccLeq  :: Sing (n :: nat) -> Sing m -> (n < m)  :~: (Succ n <= m)
  lneqReversed :: Sing (n :: nat) -> Sing m -> (n < m)  :~: (m > n)

  lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m)
           -> Compare n m :~: 'LT
  lneqToLT n m nLNEm =
    succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm

  ltToLneq :: Sing (n :: nat) -> Sing (m :: nat) -> Compare n m :~: 'LT
           -> IsTrue (n < m)
  ltToLneq n m nLTm =
    coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm

  lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat < Succ a)
  lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n

  lneqSucc :: Sing (n :: nat) -> IsTrue (n < Succ n)
  lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n

  succLneqSucc :: Sing (n :: nat) -> Sing (m :: nat)
               -> (n < m) :~: (Succ n < Succ m)
  succLneqSucc n m =
    start (n %< m)
      === (sSucc n %<= m)               `because` lneqSuccLeq n m
      === (sSucc (sSucc n) %<= sSucc m) `because` leqSucc' (sSucc n) m
      === (sSucc n %< sSucc m)          `because` sym (lneqSuccLeq (sSucc n) (sSucc m))

  lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m)
                    -> m :~: Succ (Pred m)
  lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm

  lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)
  lneqSuccStepL n m snLNEQm =
    coerce (sym $ lneqSuccLeq n m) $
    leqSuccStepL (sSucc n) m $
    coerce (lneqSuccLeq (sSucc n) m) snLNEQm

  lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)
  lneqSuccStepR n m nLNEQm =
    coerce (sym $ lneqSuccLeq n (sSucc m)) $
    leqSuccStepR (sSucc n) m $
    coerce (lneqSuccLeq n m) nLNEQm

  plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k
                     -> IsTrue (n < m) -> IsTrue (l < k)
                     -> IsTrue ((n + l) < (m + k))
  plusStrictMonotone n m l k nLNm lLNk =
    coerce (sym $ lneqSuccLeq (n %+ l) (m %+ k)) $
      flip coerceLeqL (m %+ k) (plusSuccL n l) $
      plusMonotone (sSucc n) m l k
        (coerce (lneqSuccLeq n m) nLNm)
        (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $
           coerce (lneqSuccLeq l k) lLNk)

  maxZeroL :: Sing n -> Max (Zero nat) n :~: n
  maxZeroL n = leqToMax sZero n (leqZero n)

  maxZeroR  :: Sing n -> Max n (Zero nat) :~: n
  maxZeroR n = geqToMax n sZero (leqZero n)

  minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat
  minZeroL n = leqToMin sZero n (leqZero n)

  minZeroR  :: Sing n -> Min n (Zero nat) :~: Zero nat
  minZeroR n = geqToMin n sZero (leqZero n)

  minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Succ n - m :~: Succ (n - m)
  minusSucc n m mLEQn =
    case leqWitness m n mLEQn of
      DiffNat _ k ->
        start (sSucc n %- m)
          =~= sSucc (m %+ k) %- m
          === (m %+ sSucc k) %- m  `because` minusCongL (sym $ plusSuccR m k) m
          === (sSucc k %+ m) %- m  `because` minusCongL (plusComm m (sSucc k)) m
          === sSucc k                `because` plusMinus (sSucc k) m
          === sSucc (k %+ m %- m)  `because` succCong (sym $ plusMinus k m)
          === sSucc (m %+ k %- m)  `because` succCong (minusCongL (plusComm k m) m)
          =~= sSucc (n %- m)

  lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero nat) -> Void
  lneqZeroAbsurd n leq =
    succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq)

  minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)
            -> n - m + m :~: n
  minusPlus n m mLEQn =
    case leqWitness m n mLEQn of
      DiffNat _ k ->
        start (n %- m %+ m)
          =~= m %+ k %- m %+ m
          === k %+ m %- m %+ m  `because` plusCongL (minusCongL (plusComm m k) m) m
          === k %+ m              `because` plusCongL (plusMinus k m) m
          === m %+ k              `because` plusComm  k m
          =~= n

-- | Natural subtraction, truncated to zero if m > n.
type n -. m = Subt n m (m <= n)
type family Subt (n :: nat) (m :: nat) (b :: Bool) :: nat where
  Subt n          m 'True  = n - m
  Subt (n :: nat) m 'False = Zero nat
infixl 6 -.

(%-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n -. m)
n %-. m =
  case m %<= n of
    STrue  -> n %- m
    SFalse -> sZero

minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat)
                  -> Min n m + (n -. m) :~: n
minPlusTruncMinus n m =
  case m %<= n of
    STrue ->
      start (sMin n m %+ (n %-. m))
        === m %+ (n %-. m) `because` plusCongL (geqToMin n m Witness) (n %-. m)
        =~= m %+ (n %- m)
        === (n %- m) %+ m  `because` plusComm m (n %- m)
        === n                `because` minusPlus n m Witness
    SFalse ->
      start (sMin n m %+ (n %-. m))
        =~= sMin n m %+ sZero
        === sMin n m  `because` plusZeroR (sMin n m)
        === n         `because` leqToMin n m (notLeqToLeq m n)

truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue ((n -. m) <= n)
truncMinusLeq n m =
  case m %<= n of
    STrue  -> leqStep (n %-. m) n m $ minusPlus n m Witness
    SFalse -> leqZero n