{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces  #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures     #-}
{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes  #-}
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif

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,
#if MIN_VERSION_singletons(2,6,0)
                                           SOrdering (SLT, SEQ, SGT),
#else
                                           Sing (SLT, SEQ, SGT),
#endif

                                           SOrd(..), POrd(..),
                                           LTSym0, GTSym0, EQSym0,
                                           (%<), (%<=), (%>), (%>=))

import Data.Singletons.Prelude
  (Sing,
#if MIN_VERSION_singletons(2,6,0)
  SBool (SFalse, STrue),
#else
  Sing (SFalse, STrue),
#endif
  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

-- | Since 0.9.0.0 (type changed)
coerceLeqL
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810
  :: forall nat (n :: nat) m l.
#else
  :: forall (n :: nat) m l .
#endif
      IsPeano nat
  => n :~: m -> Sing l
  -> IsTrue (n <= l) -> IsTrue (m <= l)
coerceLeqL Refl _ Witness = Witness

-- | Since 0.9.0.0 (type changed)
coerceLeqR
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810
  :: forall nat (n :: nat) m l .
#else
  :: forall (n :: nat) m l .
#endif
      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