{-# LANGUAGE DataKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}

module Data.Type.Natural.Lemma.Order
  ( DiffNat (..),
    LeqView (..),
    type (<),
    type (<?),
    (%<?),
    type (>),
    type (>?),
    (%>?),
    type (>=),
    type (>=?),
    (%>=?),
    FlipOrdering,
    Min,
    sMin,
    Max,
    sMax,

    -- * Lemmas
    sFlipOrdering,
    coerceLeqL,
    coerceLeqR,
    sLeqCongL,
    sLeqCongR,
    sLeqCong,
    succDiffNat,
    compareCongR,
    leqToCmp,
    eqlCmpEQ,
    eqToRefl,
    flipCmpNat,
    ltToNeq,
    leqNeqToLT,
    succLeqToLT,
    ltToLeq,
    gtToLeq,
    congFlipOrdering,
    ltToSuccLeq,
    cmpZero,
    leqToGT,
    cmpZero',
    zeroNoLT,
    ltRightPredSucc,
    cmpSucc,
    ltSucc,
    cmpSuccStepR,
    ltSuccLToLT,
    leqToLT,
    leqZero,
    leqSucc,
    fromLeqView,
    leqViewRefl,
    viewLeq,
    leqWitness,
    leqStep,
    leqNeqToSuccLeq,
    leqRefl,
    leqSuccStepR,
    leqSuccStepL,
    leqReflexive,
    leqTrans,
    leqAntisymm,
    plusMonotone,
    leqZeroElim,
    plusMonotoneL,
    plusMonotoneR,
    plusLeqL,
    plusLeqR,
    plusCancelLeqR,
    plusCancelLeqL,
    succLeqZeroAbsurd,
    succLeqZeroAbsurd',
    succLeqAbsurd,
    succLeqAbsurd',
    notLeqToLeq,
    leqSucc',
    leqToMin,
    geqToMin,
    minComm,
    minLeqL,
    minLeqR,
    minLargest,
    leqToMax,
    geqToMax,
    maxComm,
    maxLeqR,
    maxLeqL,
    maxLeast,
    lneqSuccLeq,
    lneqReversed,
    lneqToLT,
    ltToLneq,
    lneqZero,
    lneqSucc,
    succLneqSucc,
    lneqRightPredSucc,
    lneqSuccStepL,
    lneqSuccStepR,
    plusStrictMonotone,
    maxZeroL,
    maxZeroR,
    minZeroL,
    minZeroR,
    minusSucc,
    lneqZeroAbsurd,
    minusPlus,
    minPlusTruncMinus,
    truncMinusLeq,
    type (-.),
    (%-.),

    -- * Various witnesses for orderings
    LeqWitness,
    (:<:),
    Leq (..),
    leqRhs,
    leqLhs,

    -- ** conversions between lax orders
    propToBoolLeq,
    boolToPropLeq,

    -- ** conversions between strict orders
    propToBoolLt,
    boolToPropLt,
  )
where

import Data.Coerce (coerce)
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural.Core
import Data.Type.Natural.Lemma.Arithmetic
import Data.Void (Void, absurd)
import Numeric.Natural (Natural)
import Proof.Equational
  ( because,
    start,
    sym,
    trans,
    (===),
    (=~=),
  )
import Proof.Propositional (IsTrue (..), eliminate, withWitness)

--------------------------------------------------

-- ** Type-level predicate & judgements.

--------------------------------------------------

-- | Comparison via GADTs.
data Leq n m where
  ZeroLeq :: SNat m -> Leq 0 m
  SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)

type LeqWitness n m = IsTrue (n <=? m)

data a :<: b where
  ZeroLtSucc :: 0 :<: (m + 1)
  SuccLtSucc :: n :<: m -> (n + 1) :<: (m + 1)

deriving instance Show (a :<: b)

--------------------------------------------------

-- * Total orderings on natural numbers.

--------------------------------------------------
propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m
propToBoolLeq (ZeroLeq _) = Witness
propToBoolLeq (SuccLeqSucc leq) = withWitness (propToBoolLeq leq) Witness
{-# INLINE propToBoolLeq #-}

boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m
boolToPropLeq Zero m = ZeroLeq m
boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m
boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness

leqRhs :: Leq n m -> SNat m
leqRhs (ZeroLeq m) = m
leqRhs (SuccLeqSucc leq) = sSucc $ leqRhs leq

leqLhs :: Leq n m -> SNat n
leqLhs (ZeroLeq _) = Zero
leqLhs (SuccLeqSucc leq) = sSucc $ leqLhs leq

propToBoolLt :: n :<: m -> IsTrue (n <? m)
propToBoolLt ZeroLtSucc = Witness
propToBoolLt (SuccLtSucc lt) =
  withWitness (propToBoolLt lt) Witness

boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m
boolToPropLt Zero (Succ _) = ZeroLtSucc
boolToPropLt (Succ _) Zero = eliminate (Refl :: 0 :~: 1)
boolToPropLt (Succ n) (Succ m) = SuccLtSucc (boolToPropLt n m)

type Min n m = MinAux (n <=? m) n m

sMin :: SNat n -> SNat m -> SNat (Min n m)
sMin = coerce $ min @Natural

sMax :: SNat n -> SNat m -> SNat (Max n m)
sMax = coerce $ max @Natural

type family MinAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
  MinAux 'True n _ = n
  MinAux 'False _ m = m

type Max n m = MaxAux (n >=? m) n m

type family MaxAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
  MaxAux 'True n _ = n
  MaxAux 'False _ m = m

infix 4 <?, <, >=?, >=, >, >?

type n <? m = n + 1 <=? m

(%<?) :: SNat n -> SNat m -> SBool (n <? m)
(%<?) = (%<=?) . sSucc

type n < m = (n <? m) ~ 'True

type n >=? m = m <=? n

(%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
(%>=?) = flip (%<=?)

type n >= m = (n >=? m) ~ 'True

type n >? m = m <? n

(%>?) :: SNat n -> SNat m -> SBool (n >? m)
(%>?) = flip (%<?)

type n > m = (n >? m) ~ 'True

infix 4 %>?, %<?, %>=?

data LeqView n m where
  LeqZero :: SNat n -> LeqView 0 n
  LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)

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

newtype LeqWitPf n = LeqWitPf {leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m}

succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat _ _ (DiffNat n m) = gcastWith (plusSuccL n m) $ DiffNat (sSucc n) m

-- | Since 1.0.0.0 (type changed)
coerceLeqL ::
  forall n m l.
  n :~: m ->
  SNat l ->
  IsTrue (n <=? l) ->
  IsTrue (m <=? l)
coerceLeqL Refl _ Witness = Witness

-- | Since 1.0.0.0 (type changed)
coerceLeqR ::
  forall n m l.
  SNat l ->
  n :~: m ->
  IsTrue (l <=? n) ->
  IsTrue (l <=? m)
coerceLeqR _ Refl Witness = Witness

compareCongR :: SNat a -> b :~: c -> CmpNat a b :~: CmpNat a c
compareCongR _ Refl = Refl

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

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

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

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

leqToCmp ::
  SNat a ->
  SNat b ->
  IsTrue (a <=? b) ->
  Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp n m Witness =
  case n %~ m of
    Equal -> Left Refl
    NonEqual -> Right Refl

eqlCmpEQ :: SNat a -> SNat b -> a :~: b -> CmpNat a b :~: 'EQ
eqlCmpEQ _ _ Refl = Refl

eqToRefl :: SNat a -> SNat b -> CmpNat a b :~: 'EQ -> a :~: b
eqToRefl _ _ Refl = Refl

flipCmpNat ::
  SNat a ->
  SNat b ->
  FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat n m = case sCmpNat n m of
  SGT -> Refl
  SLT -> Refl
  SEQ -> Refl

ltToNeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  a :~: b ->
  Void
ltToNeq a b aLTb aEQb =
  eliminate $
    start SLT
      === sCmpNat a b `because` sym aLTb
      === SEQ `because` eqlCmpEQ a b aEQb

leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> (a :~: b -> Void) -> CmpNat a b :~: 'LT
leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb

succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT _ _ Witness = Refl

ltToLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  IsTrue (a <=? b)
ltToLeq _ _ Refl = Witness

gtToLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'GT ->
  IsTrue (b <=? a)
gtToLeq _ _ Refl = Witness

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

ltToSuccLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  IsTrue (Succ a <=? b)
ltToSuccLeq _ _ Refl = Witness

cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero _ = Refl

leqToGT ::
  SNat a ->
  SNat b ->
  IsTrue (Succ b <=? a) ->
  CmpNat a b :~: 'GT
leqToGT _ _ Witness = Refl

cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' n =
  case zeroOrSucc n of
    IsZero -> Left $ eqlCmpEQ sZero n Refl
    IsSucc n' -> Right $ cmpZero n'

zeroNoLT :: SNat a -> CmpNat a 0 :~: 'LT -> Void
zeroNoLT n eql =
  case cmpZero' n of
    Left cmp0nEQ ->
      eliminate $
        start SGT
          =~= sFlipOrdering SLT
          === sFlipOrdering (sCmpNat n sZero) `because` congFlipOrdering (sym eql)
          === sCmpNat sZero n `because` flipCmpNat n sZero
          === SEQ `because` cmp0nEQ
    Right cmp0nLT ->
      eliminate $
        start SGT
          =~= sFlipOrdering SLT
          === sFlipOrdering (sCmpNat n sZero) `because` congFlipOrdering (sym eql)
          === sCmpNat sZero n `because` flipCmpNat n sZero
          === SLT `because` cmp0nLT

ltRightPredSucc :: SNat a -> SNat b -> CmpNat a b :~: 'LT -> b :~: Succ (Pred b)
ltRightPredSucc _ _ Refl = Refl

cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc _ _ = Refl

ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc _ = Refl

cmpSuccStepR ::
  forall n m.
  SNat n ->
  SNat m ->
  CmpNat n m :~: 'LT ->
  CmpNat n (Succ m) :~: 'LT
cmpSuccStepR _ _ Refl = Refl

ltSuccLToLT ::
  SNat n ->
  SNat m ->
  CmpNat (Succ n) m :~: 'LT ->
  CmpNat 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 (sCmpNat n (sSucc m'))
            === SLT `because` cmpSuccStepR n m' nLTm

leqToLT ::
  SNat a ->
  SNat b ->
  IsTrue (Succ a <=? b) ->
  CmpNat a b :~: 'LT
leqToLT _ _ Witness = Refl

leqZero :: SNat n -> IsTrue (0 <=? n)
leqZero _ = Witness

leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc _ _ Witness = Witness

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

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

viewLeq :: forall n m. SNat n -> SNat 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 gcastWith (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm'

leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness = \sn -> leqWitPf (induction base step sn) @m
  where
    base :: LeqWitPf 0
    base = LeqWitPf $ \sm _ -> gcastWith (plusZeroL sm) $ DiffNat sZero sm

    step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
    step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
      case viewLeq (sSucc n) m snLEQm of
#if !MIN_VERSION_ghc(9,2,0)
        LeqZero _ -> absurd $ succNonCyclic n Refl
#endif
        LeqSucc (_ :: SNat n') pm nLEQpm ->
          succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm

leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
leqStep _ _ _ Refl = Witness

leqNeqToSuccLeq :: SNat n -> SNat 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 :: SNat n -> IsTrue (n <=? n)
leqRefl _ = Witness

leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR _ _ Witness = Witness

leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL _ _ Witness = Witness

leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)
leqReflexive _ _ Refl = Witness

leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)
leqTrans _ _ _ Witness Witness = Witness

leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm _ _ Witness Witness = Refl

plusMonotone ::
  SNat n ->
  SNat m ->
  SNat l ->
  SNat k ->
  IsTrue (n <=? m) ->
  IsTrue (l <=? k) ->
  IsTrue ((n + l) <=? (m + k))
plusMonotone _ _ _ _ Witness Witness = Witness

leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim _ Witness = Refl

plusMonotoneL ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue (n <=? m) ->
  IsTrue ((n + l) <=? (m + l))
plusMonotoneL _ _ _ Witness = Witness

plusMonotoneR ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue (m <=? l) ->
  IsTrue ((n + m) <=? (n + l))
plusMonotoneR _ _ _ Witness = Witness

plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL _ _  = Witness

plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR _ _ = Witness

plusCancelLeqR ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue ((n + l) <=? (m + l)) ->
  IsTrue (n <=? m)
plusCancelLeqR _ _ _ Witness = Witness

plusCancelLeqL ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue ((n + m) <=? (n + l)) ->
  IsTrue (m <=? l)
plusCancelLeqL _ _ _ Witness = Witness

succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd n leq =
  succNonCyclic n (leqZeroElim (sSucc n) leq)

succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' _ = Refl

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

succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False
succLeqAbsurd' _ = Refl

notLeqToLeq :: forall n m. ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq _ _ = Witness

leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' _ _ = Refl

leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin _ _ Witness = Refl

geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin n m Witness =
  case n %<=? m of
    SFalse -> Refl
    STrue -> Refl

minComm :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: SNat n -> SNat 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 ::
  SNat l ->
  SNat n ->
  SNat m ->
  IsTrue (l <=? n) ->
  IsTrue (l <=? m) ->
  IsTrue (l <=? Min n m)
minLargest l n m lLEQn lLEQm =
  withKnownNat l $
    withKnownNat n $
      withKnownNat m $
        withKnownNat (sMin n m) $
          case n %<=? m of
            STrue -> lLEQn
            SFalse -> lLEQm

leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax n m Witness =
  case n %>=? m of
    STrue -> Refl
    SFalse -> Refl

geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax n m Witness =
  case n %>=? m of
    STrue -> Refl

maxComm :: SNat n -> SNat 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 :: SNat n -> SNat 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 :: SNat n -> SNat 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 ::
  SNat l ->
  SNat n ->
  SNat m ->
  IsTrue (n <=? l) ->
  IsTrue (m <=? l) ->
  IsTrue (Max n m <=? l)
maxLeast l n m lLEQn lLEQm =
  withKnownNat l $
    withKnownNat n $
      withKnownNat m $
        withKnownNat (sMax n m) $
          case n %>=? m of
            STrue -> lLEQn
            SFalse -> lLEQm

lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)
lneqSuccLeq _ _ = Refl

lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)
lneqReversed _ _ = Refl

lneqToLT ::
  SNat n ->
  SNat m ->
  IsTrue (n <? m) ->
  CmpNat n m :~: 'LT
lneqToLT n m nLNEm =
  succLeqToLT n m $ gcastWith (lneqSuccLeq n m) nLNEm

ltToLneq ::
  SNat n ->
  SNat m ->
  CmpNat n m :~: 'LT ->
  IsTrue (n <? m)
ltToLneq n m nLTm =
  gcastWith (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm

lneqZero :: SNat a -> IsTrue (0 <? Succ a)
lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n

lneqSucc :: SNat n -> IsTrue (n <? Succ n)
lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n

succLneqSucc ::
  SNat n ->
  SNat m ->
  (n <? m) :~: (Succ n <? Succ m)
succLneqSucc _ _ = Refl

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

lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepL n m snLNEQm =
  gcastWith (sym $ lneqSuccLeq n m) $
    leqSuccStepL (sSucc n) m $
      gcastWith (lneqSuccLeq (sSucc n) m) snLNEQm

lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
lneqSuccStepR n m nLNEQm =
  gcastWith (sym $ lneqSuccLeq n (sSucc m)) $
    leqSuccStepR (sSucc n) m $
      gcastWith (lneqSuccLeq n m) nLNEQm

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

maxZeroL :: SNat n -> Max 0 n :~: n
maxZeroL n = leqToMax sZero n (leqZero n)

maxZeroR :: SNat n -> Max n 0 :~: n
maxZeroR n = geqToMax n sZero (leqZero n)

minZeroL :: SNat n -> Min 0 n :~: 0
minZeroL n = leqToMin sZero n (leqZero n)

minZeroR :: SNat n -> Min n 0 :~: 0
minZeroR n = geqToMin n sZero (leqZero n)

minusSucc :: SNat n -> SNat 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 :: SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd n leq =
  succLeqZeroAbsurd n (gcastWith (lneqSuccLeq n sZero) leq)

minusPlus ::
  forall n m.
  SNat n ->
  SNat 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 m (b :: Bool) where
  Subt n m 'True = n - m
  Subt n m 'False = 0

infixl 6 -.

(%-.) :: SNat n -> SNat m -> SNat (n -. m)
n %-. m =
  case m %<=? n of
    STrue -> n %- m
    SFalse -> sZero

minPlusTruncMinus ::
  SNat n ->
  SNat m ->
  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 :: SNat n -> SNat 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