-- --< Header >-- {{{

{-#
LANGUAGE
  TypeFamilyDependencies, DataKinds, PatternSynonyms, RankNTypes,
  TypeOperators, PolyKinds, TypeApplications, ScopedTypeVariables,
  TypeSynonymInstances, BangPatterns, BlockArguments, LambdaCase, EmptyCase
#-}


{- |

Description : Axiomata & lemmata for easier use of "Data.Type.Ord"
Copyright   : (c) L. S. Leary, 2025

Axiomata & lemmata for easier use of "Data.Type.Ord".

\[
  \newcommand{\colon}{ \! : }
\]

-}

-- }}}

-- --< Exports >-- {{{

module Data.Type.Ord.Axiomata (

  -- * Sing
  Sing,

  -- * Axiomata
  -- $axiomata

  -- ** Equivalence
  Equivalence(..),

  -- ** Total Order
  TotalOrder(..),
  Reflect,
  minTO, maxTO,
  defaultDecideEq,

  -- ** Bounding
  BoundedBelow(..),
  BoundedAbove(..),

  -- * Lemmata

  -- ** Equivalence
  sym,
  transEq,

  -- ** Min
  minDefl1,
  minDefl2,
  minMono,

  -- ** Max
  maxInfl1,
  maxInfl2,
  maxMono,

) where

-- }}}

-- --< Imports >-- {{{

-- GHC/base
import GHC.TypeNats
  ( Nat   , SNat   , pattern SNat   , natSing   , cmpNat
  )
import GHC.TypeLits
  (         SChar  , pattern SChar  , charSing  , cmpChar
  , Symbol, SSymbol, pattern SSymbol, symbolSing, cmpSymbol
  )

-- base
import Unsafe.Coerce (unsafeCoerce)
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import Data.Type.Ord (OrderingI(..), Compare, Min, Max, type (<=?), type (<=))
import Data.Void (Void)

-- }}}

-- --< Sing >-- {{{

-- | Maps kinds to their corresponding singleton type constructors.
type family   Sing k      = (s :: k -> Type) | s -> k
type instance Sing Nat    = SNat
type instance Sing Char   = SChar
type instance Sing Symbol = SSymbol

-- }}}

-- --< Axiomata >-- {{{

{- $axiomata

@'Compare' \@O@ should give rise to an equivalence relation and a total ordering on @O@.
In particular, we can define:

\[
\begin{align}
  a  <   b &\iff \mathtt{Compare} \, a \, b \sim \mathtt{LT} \\
  a  =   b &\iff \mathtt{Compare} \, a \, b \sim \mathtt{EQ} \\
  a  >   b &\iff \mathtt{Compare} \, a \, b \sim \mathtt{GT} \\
  a \leq b &\iff a < b \lor a = b                            \\
  a \geq b &\iff a > b \lor a = b
\end{align}
\]

These aren't consistent by construction, however—we need more axiomata.

-}

-- }}}

-- --< Axiomata: Equivalence >-- {{{

-- | 'Eq' for @'Sing' e@ with @'Compare' \@e@.
--   Due to the inclusion of 'sub', 'sym' and 'transEq' are demoted to lemmata.
class Equivalence e where

  {- |

  Decidability of equivalence.

  \[
    \forall a, b \colon a = b \lor a \neq b
  \]

  Since 'refl' and 'sub' make them interchangeable, however, we actually use regular type equality for better ergonomics:

  \[
    \forall a, b \colon a \sim b \lor a \not\sim b
  \]

  -}
  (=?)
    :: Sing e a -> Sing e b {- ^ -}
    -> Either (a :~: b -> Void) (a :~: b)

  {- |

  Reflexivity of equivalence.

  \[
    \forall a \colon a = a
  \]

  Can also be read as:

  \[
    \forall a, b \colon a \sim b \implies a = b
  \]

  The other direction of 'sub'.

  -}
  refl
    :: Sing e a {- ^ -}
    -> Compare a a :~: EQ

  {- |

  Substitutability: if two types are equivalent, one can be substituted for the other.

  \[
    \forall a, b \colon a = b \implies a \sim b
  \]

  The other direction of 'refl'.

  -}
  sub
    :: Compare a b ~ EQ
    => Sing e a {- ^ -}
    -> Sing e b
    -> a :~: b

instance Equivalence Nat where
  =? :: forall (a :: Nat) (b :: Nat).
Sing Nat a -> Sing Nat b -> Either ((a :~: b) -> Void) (a :~: b)
(=?) = Sing Nat a -> Sing Nat b -> Either ((a :~: b) -> Void) (a :~: b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq
  refl :: forall (a :: Nat). Sing Nat a -> Compare a a :~: 'EQ
refl Sing Nat a
_  = 'EQ :~: 'EQ
Compare a a :~: 'EQ
forall {k} (a :: k). a :~: a
Refl
  sub :: forall (a :: Nat) (b :: Nat).
(Compare a b ~ 'EQ) =>
Sing Nat a -> Sing Nat b -> a :~: b
sub m :: Sing Nat a
m@SNat a
Sing Nat a
SNat n :: Sing Nat b
n@SNat b
Sing Nat b
SNat = case SNat a -> SNat b -> OrderingI a b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat a
m SNat b
Sing Nat b
n of
    OrderingI a b
EQI -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance Equivalence Char where
  =? :: forall (a :: Char) (b :: Char).
Sing Char a -> Sing Char b -> Either ((a :~: b) -> Void) (a :~: b)
(=?) = Sing Char a -> Sing Char b -> Either ((a :~: b) -> Void) (a :~: b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq
  refl :: forall (a :: Char). Sing Char a -> Compare a a :~: 'EQ
refl Sing Char a
_  = 'EQ :~: 'EQ
Compare a a :~: 'EQ
forall {k} (a :: k). a :~: a
Refl
  sub :: forall (a :: Char) (b :: Char).
(Compare a b ~ 'EQ) =>
Sing Char a -> Sing Char b -> a :~: b
sub m :: Sing Char a
m@SChar a
Sing Char a
SChar n :: Sing Char b
n@SChar b
Sing Char b
SChar = case SChar a -> SChar b -> OrderingI a b
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char a
m SChar b
Sing Char b
n of
    OrderingI a b
EQI -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance Equivalence Symbol where
  =? :: forall (a :: Symbol) (b :: Symbol).
Sing Symbol a
-> Sing Symbol b -> Either ((a :~: b) -> Void) (a :~: b)
(=?) = Sing Symbol a
-> Sing Symbol b -> Either ((a :~: b) -> Void) (a :~: b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq
  refl :: forall (a :: Symbol). Sing Symbol a -> Compare a a :~: 'EQ
refl Sing Symbol a
_  = 'EQ :~: 'EQ
Compare a a :~: 'EQ
forall {k} (a :: k). a :~: a
Refl
  sub :: forall (a :: Symbol) (b :: Symbol).
(Compare a b ~ 'EQ) =>
Sing Symbol a -> Sing Symbol b -> a :~: b
sub m :: Sing Symbol a
m@SSymbol a
Sing Symbol a
SSymbol n :: Sing Symbol b
n@SSymbol b
Sing Symbol b
SSymbol = case SSymbol a -> SSymbol b -> OrderingI a b
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol a
m SSymbol b
Sing Symbol b
n of
    OrderingI a b
EQI -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Axiomata: Total Order >-- {{{

-- | 'Ord' for @'Sing' e@ with @'Compare' \@e@.
class Equivalence o => TotalOrder o where

  {- |

  Decidable connectivity of ordering.

  \[
    \forall a, b \colon a \lt b \lor a = b \lor a \gt b
  \]

  -}
  (<|=|>)
    :: Sing o a -> Sing o b {- ^ -}
    -> OrderingI a b

  {- |

  Anti-symmetry of ordering.

  \[
    \forall a, b \colon a \leq b \iff b \geq a
  \]

  -}
  antiSym
    :: Sing o a -> Sing o b {- ^ -}
    -> Compare a b :~: Reflect (Compare b a)

  {- |

  Transitivity of ordering.

  \[
    \forall a, b, c \colon a \leq b \land b \leq c \implies a \leq c
  \]

  -}
  transTO
    :: (a <= b, b <= c)
    => Sing o a -> Sing o b -> Sing o c {- ^ -}
    -> (a <=? c) :~: True

-- | @Reflect@ an 'Ordering' (to express anti-symmetry).
type family Reflect (o :: Ordering) = (p :: Ordering) | p -> o where
  Reflect LT = GT
  Reflect EQ = EQ
  Reflect GT = LT

instance TotalOrder Nat where
  m :: Sing Nat a
m@SNat a
Sing Nat a
SNat <|=|> :: forall (a :: Nat) (b :: Nat).
Sing Nat a -> Sing Nat b -> OrderingI a b
<|=|> n :: Sing Nat b
n@SNat b
Sing Nat b
SNat = SNat a -> SNat b -> OrderingI a b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat a
m SNat b
Sing Nat b
n
  antiSym :: forall (a :: Nat) (b :: Nat).
Sing Nat a -> Sing Nat b -> Compare a b :~: Reflect (Compare b a)
antiSym = SNat a -> SNat b -> Compare a b :~: Reflect (Compare b a)
Sing Nat a -> Sing Nat b -> Compare a b :~: Reflect (Compare b a)
forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym
  transTO :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(a <= b, b <= c) =>
Sing Nat a -> Sing Nat b -> Sing Nat c -> (a <=? c) :~: 'True
transTO l :: Sing Nat a
l@SNat a
Sing Nat a
SNat m :: Sing Nat b
m@SNat b
Sing Nat b
SNat n :: Sing Nat c
n@SNat c
Sing Nat c
SNat = case SNat a -> SNat b -> OrderingI a b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat a
l SNat b
Sing Nat b
m of
    OrderingI a b
LTI -> case SNat b -> SNat c -> OrderingI b c
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat b
Sing Nat b
m SNat c
Sing Nat c
n of
      OrderingI b c
LTI -> case SNat a -> SNat b -> SNat c -> Compare a c :~: 'LT
forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(Compare a b ~ 'LT, Compare b c ~ 'LT) =>
sing a -> sing b -> sing c -> Compare a c :~: 'LT
unsafeLtTrans SNat a
Sing Nat a
l SNat b
Sing Nat b
m SNat c
Sing Nat c
n of
        Compare a c :~: 'LT
Refl -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
      OrderingI b c
EQI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> case SNat a -> SNat c -> OrderingI a c
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat b
m SNat c
Sing Nat c
n of
      OrderingI a c
LTI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
      OrderingI a c
EQI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance TotalOrder Char where
  m :: Sing Char a
m@SChar a
Sing Char a
SChar <|=|> :: forall (a :: Char) (b :: Char).
Sing Char a -> Sing Char b -> OrderingI a b
<|=|> n :: Sing Char b
n@SChar b
Sing Char b
SChar = SChar a -> SChar b -> OrderingI a b
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char a
m SChar b
Sing Char b
n
  antiSym :: forall (a :: Char) (b :: Char).
Sing Char a -> Sing Char b -> Compare a b :~: Reflect (Compare b a)
antiSym = SChar a -> SChar b -> Compare a b :~: Reflect (Compare b a)
Sing Char a -> Sing Char b -> Compare a b :~: Reflect (Compare b a)
forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym
  transTO :: forall (a :: Char) (b :: Char) (c :: Char).
(a <= b, b <= c) =>
Sing Char a -> Sing Char b -> Sing Char c -> (a <=? c) :~: 'True
transTO l :: Sing Char a
l@SChar a
Sing Char a
SChar m :: Sing Char b
m@SChar b
Sing Char b
SChar n :: Sing Char c
n@SChar c
Sing Char c
SChar = case SChar a -> SChar b -> OrderingI a b
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char a
l SChar b
Sing Char b
m of
    OrderingI a b
LTI -> case SChar b -> SChar c -> OrderingI b c
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar b
Sing Char b
m SChar c
Sing Char c
n of
      OrderingI b c
LTI -> case SChar a -> SChar b -> SChar c -> Compare a c :~: 'LT
forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(Compare a b ~ 'LT, Compare b c ~ 'LT) =>
sing a -> sing b -> sing c -> Compare a c :~: 'LT
unsafeLtTrans SChar a
Sing Char a
l SChar b
Sing Char b
m SChar c
Sing Char c
n of
        Compare a c :~: 'LT
Refl -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
      OrderingI b c
EQI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> case SChar a -> SChar c -> OrderingI a c
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char b
m SChar c
Sing Char c
n of
      OrderingI a c
LTI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
      OrderingI a c
EQI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance TotalOrder Symbol where
  m :: Sing Symbol a
m@SSymbol a
Sing Symbol a
SSymbol <|=|> :: forall (a :: Symbol) (b :: Symbol).
Sing Symbol a -> Sing Symbol b -> OrderingI a b
<|=|> n :: Sing Symbol b
n@SSymbol b
Sing Symbol b
SSymbol = SSymbol a -> SSymbol b -> OrderingI a b
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol a
m SSymbol b
Sing Symbol b
n
  antiSym :: forall (a :: Symbol) (b :: Symbol).
Sing Symbol a
-> Sing Symbol b -> Compare a b :~: Reflect (Compare b a)
antiSym = SSymbol a -> SSymbol b -> Compare a b :~: Reflect (Compare b a)
Sing Symbol a
-> Sing Symbol b -> Compare a b :~: Reflect (Compare b a)
forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym
  transTO :: forall (a :: Symbol) (b :: Symbol) (c :: Symbol).
(a <= b, b <= c) =>
Sing Symbol a
-> Sing Symbol b -> Sing Symbol c -> (a <=? c) :~: 'True
transTO l :: Sing Symbol a
l@SSymbol a
Sing Symbol a
SSymbol m :: Sing Symbol b
m@SSymbol b
Sing Symbol b
SSymbol n :: Sing Symbol c
n@SSymbol c
Sing Symbol c
SSymbol = case SSymbol a -> SSymbol b -> OrderingI a b
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol a
l SSymbol b
Sing Symbol b
m of
    OrderingI a b
LTI -> case SSymbol b -> SSymbol c -> OrderingI b c
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol b
Sing Symbol b
m SSymbol c
Sing Symbol c
n of
      OrderingI b c
LTI -> case SSymbol a -> SSymbol b -> SSymbol c -> Compare a c :~: 'LT
forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(Compare a b ~ 'LT, Compare b c ~ 'LT) =>
sing a -> sing b -> sing c -> Compare a c :~: 'LT
unsafeLtTrans SSymbol a
Sing Symbol a
l SSymbol b
Sing Symbol b
m SSymbol c
Sing Symbol c
n of
        Compare a c :~: 'LT
Refl -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
      OrderingI b c
EQI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> case SSymbol a -> SSymbol c -> OrderingI a c
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol b
m SSymbol c
Sing Symbol c
n of
      OrderingI a c
LTI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl
      OrderingI a c
EQI -> 'True :~: 'True
(a <=? c) :~: 'True
forall {k} (a :: k). a :~: a
Refl

unsafeAntiSym
  :: forall o (sing :: o -> Type) (a :: o) (b :: o)
  .  sing a -> sing b
  -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym :: forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym !sing a
_ !sing b
_ = (Compare a b :~: Compare a b)
-> Compare a b :~: Reflect (Compare b a)
forall a b. a -> b
unsafeCoerce (forall (a :: Ordering). a :~: a
forall {k} (a :: k). a :~: a
Refl @(Compare a b))

unsafeLtTrans
  :: (Compare a b ~ LT, Compare b c ~ LT)
  => sing a -> sing b -> sing c -> Compare a c :~: LT
unsafeLtTrans :: forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(Compare a b ~ 'LT, Compare b c ~ 'LT) =>
sing a -> sing b -> sing c -> Compare a c :~: 'LT
unsafeLtTrans !sing a
_ !sing b
_ !sing c
_ = ('LT :~: 'LT) -> Compare a c :~: 'LT
forall a b. a -> b
unsafeCoerce (forall (a :: Ordering). a :~: a
forall {k} (a :: k). a :~: a
Refl @LT)

-- | The minimum of two totally-ordered singletons.
minTO :: TotalOrder o => Sing o a -> Sing o b -> Sing o (Min a b)
minTO :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Min a b)
minTO Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> Sing o a
Sing o (Min a b)
a
  OrderingI a b
EQI -> Sing o a
Sing o (Min a b)
a
  OrderingI a b
GTI -> Sing o b
Sing o (Min a b)
b

-- | The maximum of two totally-ordered singletons.
maxTO :: TotalOrder o => Sing o a -> Sing o b -> Sing o (Max a b)
maxTO :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Max a b)
maxTO Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> Sing o b
Sing o (Max a b)
b
  OrderingI a b
EQI -> Sing o b
Sing o (Max a b)
b
  OrderingI a b
GTI -> Sing o a
Sing o (Max a b)
a

-- | A default implementation of '=?' in terms of '<|=|>'.
defaultDecideEq
  :: forall o a b. TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> Either (a :~: b -> Void) (a :~: b)
defaultDecideEq :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq Sing o a
m Sing o b
n = case Sing o a -> Compare a a :~: 'EQ
forall (a :: o). Sing o a -> Compare a a :~: 'EQ
forall e (a :: e). Equivalence e => Sing e a -> Compare a a :~: 'EQ
refl Sing o a
m of
  Compare a a :~: 'EQ
Refl -> case Sing o a
m Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
n of
    OrderingI a b
LTI -> ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left \case{}
    OrderingI a b
EQI -> (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
GTI -> ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left \case{}

-- }}}

-- --< Axiomata: Bounding >-- {{{

-- | 'TotalOrder's with 'LowerBound's.
class TotalOrder o => BoundedBelow o where

  type LowerBound o = (l :: o) | l -> o

  -- | Existence of a lower bound \( b_l \).
  lowerBound :: Sing o (LowerBound o)

  {- |

  \( b_l \) is the @least@ element of @o@.

  \[
    \forall a \colon b_l \leq a
  \]

  -}
  least :: Sing o a -> (LowerBound o <=? a) :~: True

instance BoundedBelow Nat where
  type LowerBound Nat = 0
  lowerBound :: Sing Nat (LowerBound Nat)
lowerBound = SNat 0
Sing Nat (LowerBound Nat)
forall (n :: Nat). KnownNat n => SNat n
natSing
  least :: forall (a :: Nat). Sing Nat a -> (LowerBound Nat <=? a) :~: 'True
least = Sing Nat a -> (LowerBound Nat <=? a) :~: 'True
forall o (a :: o). Sing o a -> (LowerBound o <=? a) :~: 'True
unsafeLeast

instance BoundedBelow Char where
  type LowerBound Char = '\NUL'
  lowerBound :: Sing Char (LowerBound Char)
lowerBound = SChar '\NUL'
Sing Char (LowerBound Char)
forall (n :: Char). KnownChar n => SChar n
charSing
  least :: forall (a :: Char).
Sing Char a -> (LowerBound Char <=? a) :~: 'True
least = Sing Char a -> (LowerBound Char <=? a) :~: 'True
forall o (a :: o). Sing o a -> (LowerBound o <=? a) :~: 'True
unsafeLeast

instance BoundedBelow Symbol where
  type LowerBound Symbol = ""
  lowerBound :: Sing Symbol (LowerBound Symbol)
lowerBound = SSymbol ""
Sing Symbol (LowerBound Symbol)
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing
  least :: forall (a :: Symbol).
Sing Symbol a -> (LowerBound Symbol <=? a) :~: 'True
least = Sing Symbol a -> (LowerBound Symbol <=? a) :~: 'True
forall o (a :: o). Sing o a -> (LowerBound o <=? a) :~: 'True
unsafeLeast

unsafeLeast :: Sing o a -> (LowerBound o <=? a) :~: True
unsafeLeast :: forall o (a :: o). Sing o a -> (LowerBound o <=? a) :~: 'True
unsafeLeast !Sing o a
_ = ('True :~: 'True)
-> OrdCond (Compare (LowerBound o) a) 'True 'True 'False :~: 'True
forall a b. a -> b
unsafeCoerce (forall (a :: Bool). a :~: a
forall {k} (a :: k). a :~: a
Refl @True)


-- | 'TotalOrder's with 'UpperBound's.
class TotalOrder o => BoundedAbove o where

  type UpperBound o = (u :: o) | u -> o

  -- | Existence of an upper bound \( b_u \).
  upperBound :: Sing o (UpperBound o)

  {- |

  \( b_u \) is the @greatest@ element of @o@.

  \[
    \forall a \colon a \leq b_u
  \]

  -}
  greatest :: Sing o a -> (a <=? UpperBound o) :~: True

-- }}}

-- --< Lemmata: Equivalence >-- {{{

{- |

Symmetry of equivalence.

\[
  \forall a, b \colon a = b \iff b = a
\]

-}
sym
  :: (Equivalence e, Compare a b ~ EQ)
  => Sing e a -> Sing e b {- ^ -}
  -> Compare b a :~: EQ
sym :: forall e (a :: e) (b :: e).
(Equivalence e, Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> Compare b a :~: 'EQ
sym Sing e a
a Sing e b
b = case Sing e a -> Sing e b -> a :~: b
forall (a :: e) (b :: e).
(Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> a :~: b
forall e (a :: e) (b :: e).
(Equivalence e, Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> a :~: b
sub Sing e a
a Sing e b
b of
  a :~: b
Refl -> 'EQ :~: 'EQ
Compare b a :~: 'EQ
forall {k} (a :: k). a :~: a
Refl

{- |

Transitivity of equivalence.

\[
  \forall a, b, c \colon a = b \land b = c \implies a = c
\]

-}
transEq
  :: (Equivalence e, Compare a b ~ EQ, Compare b c ~ EQ)
  => Sing e a -> Sing e b -> Sing e c {- ^ -}
  -> Compare a c :~: EQ
transEq :: forall e (a :: e) (b :: e) (c :: e).
(Equivalence e, Compare a b ~ 'EQ, Compare b c ~ 'EQ) =>
Sing e a -> Sing e b -> Sing e c -> Compare a c :~: 'EQ
transEq Sing e a
a Sing e b
b Sing e c
c = case Sing e a -> Sing e b -> a :~: b
forall (a :: e) (b :: e).
(Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> a :~: b
forall e (a :: e) (b :: e).
(Equivalence e, Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> a :~: b
sub Sing e a
a Sing e b
b of
  a :~: b
Refl -> case Sing e a -> Sing e c -> a :~: c
forall (a :: e) (b :: e).
(Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> a :~: b
forall e (a :: e) (b :: e).
(Equivalence e, Compare a b ~ 'EQ) =>
Sing e a -> Sing e b -> a :~: b
sub Sing e a
Sing e b
b Sing e c
c of
    a :~: c
Refl -> 'EQ :~: 'EQ
Compare a c :~: 'EQ
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Lemmata: Min >-- {{{

{- |

'Min' is deflationary in its first argument.

\[
  \mathrm{min} \, a \, b \leq a
\]

-}
minDefl1
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> (Min a b <=? a) :~: True
minDefl1 :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (Min a b <=? a) :~: 'True
minDefl1 Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> case Sing o a -> Compare a a :~: 'EQ
forall (a :: o). Sing o a -> Compare a a :~: 'EQ
forall e (a :: e). Equivalence e => Sing e a -> Compare a a :~: 'EQ
refl Sing o a
a of
    Compare a a :~: 'EQ
Refl -> 'True :~: 'True
(Min a b <=? a) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
EQI -> 'True :~: 'True
(Min a b <=? a) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
GTI -> case Sing o b -> Sing o a -> Compare b a :~: Reflect (Compare a b)
forall (a :: o) (b :: o).
Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
antiSym Sing o b
b Sing o a
a of
    Compare b a :~: Reflect (Compare a b)
Refl -> 'True :~: 'True
(Min a b <=? a) :~: 'True
forall {k} (a :: k). a :~: a
Refl

{- |

'Min' is deflationary in its second argument.

\[
  \mathrm{min} \, a \, b \leq b
\]

-}
minDefl2
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> (Min a b <=? b) :~: True
minDefl2 :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (Min a b <=? b) :~: 'True
minDefl2 Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> case Sing o b -> Compare b b :~: 'EQ
forall (a :: o). Sing o a -> Compare a a :~: 'EQ
forall e (a :: e). Equivalence e => Sing e a -> Compare a a :~: 'EQ
refl Sing o b
b of
    Compare b b :~: 'EQ
Refl -> 'True :~: 'True
(Min a b <=? b) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
EQI -> 'True :~: 'True
(Min a b <=? b) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
GTI -> case Sing o b -> Compare b b :~: 'EQ
forall (a :: o). Sing o a -> Compare a a :~: 'EQ
forall e (a :: e). Equivalence e => Sing e a -> Compare a a :~: 'EQ
refl Sing o b
b of
    Compare b b :~: 'EQ
Refl -> 'True :~: 'True
(Min a b <=? b) :~: 'True
forall {k} (a :: k). a :~: a
Refl

{- |

'Min' is monotonic in both arguments.

\[
  a \leq c \land b \leq d
    \implies \mathrm{min} \, a \, b \leq \mathrm{min} \, c \, d
\]

-}
minMono
  :: (TotalOrder o, a <= c, b <= d)
  => Sing o a -> Sing o b -> Sing o c -> Sing o d {- ^ -}
  -> (Min a b <=? Min c d) :~: True
minMono :: forall o (a :: o) (c :: o) (b :: o) (d :: o).
(TotalOrder o, a <= c, b <= d) =>
Sing o a
-> Sing o b
-> Sing o c
-> Sing o d
-> (Min a b <=? Min c d) :~: 'True
minMono Sing o a
a Sing o b
b Sing o c
c Sing o d
d = case Sing o c
c Sing o c -> Sing o d -> OrderingI c d
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o d
d of
  OrderingI c d
LTI -> case Sing o a -> Sing o b -> (Min a b <=? a) :~: 'True
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (Min a b <=? a) :~: 'True
minDefl1 Sing o a
a Sing o b
b of
    (Min a b <=? a) :~: 'True
Refl -> Sing o (Min a b)
-> Sing o a -> Sing o c -> (Min a b <=? c) :~: 'True
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
transTO (Sing o a -> Sing o b -> Sing o (Min a b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Min a b)
minTO Sing o a
a Sing o b
b) Sing o a
a Sing o c
c
  OrderingI c d
EQI -> case Sing o a -> Sing o b -> (Min a b <=? a) :~: 'True
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (Min a b <=? a) :~: 'True
minDefl1 Sing o a
a Sing o b
b of
    (Min a b <=? a) :~: 'True
Refl -> Sing o (Min a b)
-> Sing o a -> Sing o c -> (Min a b <=? c) :~: 'True
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
transTO (Sing o a -> Sing o b -> Sing o (Min a b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Min a b)
minTO Sing o a
a Sing o b
b) Sing o a
a Sing o c
c
  OrderingI c d
GTI -> case Sing o a -> Sing o b -> (Min a b <=? b) :~: 'True
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (Min a b <=? b) :~: 'True
minDefl2 Sing o a
a Sing o b
b of
    (Min a b <=? b) :~: 'True
Refl -> Sing o (Min a b)
-> Sing o b -> Sing o d -> (Min a b <=? d) :~: 'True
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
transTO (Sing o a -> Sing o b -> Sing o (Min a b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Min a b)
minTO Sing o a
a Sing o b
b) Sing o b
b Sing o d
d

-- }}}

-- --< Lemmata: Max >-- {{{

{- |

'Max' is inflationary in its first argument.

\[
  a \leq \mathrm{max} \, a \, b
\]

-}
maxInfl1
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> (a <=? Max a b) :~: True
maxInfl1 :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (a <=? Max a b) :~: 'True
maxInfl1 Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> 'True :~: 'True
(a <=? Max a b) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
EQI -> 'True :~: 'True
(a <=? Max a b) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
GTI -> case Sing o a -> Compare a a :~: 'EQ
forall (a :: o). Sing o a -> Compare a a :~: 'EQ
forall e (a :: e). Equivalence e => Sing e a -> Compare a a :~: 'EQ
refl Sing o a
a of
    Compare a a :~: 'EQ
Refl -> 'True :~: 'True
(a <=? Max a b) :~: 'True
forall {k} (a :: k). a :~: a
Refl

{- |

'Max' is inflationary in its second argument.

\[
  b \leq \mathrm{max} \, a \, b
\]

-}
maxInfl2
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> (b <=? Max a b) :~: True
maxInfl2 :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (b <=? Max a b) :~: 'True
maxInfl2 Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> case Sing o b -> Compare b b :~: 'EQ
forall (a :: o). Sing o a -> Compare a a :~: 'EQ
forall e (a :: e). Equivalence e => Sing e a -> Compare a a :~: 'EQ
refl Sing o b
b of
    Compare b b :~: 'EQ
Refl -> 'True :~: 'True
(b <=? Max a b) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
EQI -> 'True :~: 'True
(b <=? Max a b) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
GTI -> case Sing o b -> Sing o a -> Compare b a :~: Reflect (Compare a b)
forall (a :: o) (b :: o).
Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
antiSym Sing o b
b Sing o a
a of
    Compare b a :~: Reflect (Compare a b)
Refl -> 'True :~: 'True
(b <=? Max a b) :~: 'True
forall {k} (a :: k). a :~: a
Refl

{- |

'Max' is monotonic in both arguments.

\[
  a \leq c \land b \leq d
    \implies \mathrm{max} \, a \, b \leq \mathrm{max} \, c \, d
\]

-}
maxMono
  :: (TotalOrder o, a <= c, b <= d)
  => Sing o a -> Sing o b -> Sing o c -> Sing o d {- ^ -}
  -> (Max a b <=? Max c d) :~: True
maxMono :: forall o (a :: o) (c :: o) (b :: o) (d :: o).
(TotalOrder o, a <= c, b <= d) =>
Sing o a
-> Sing o b
-> Sing o c
-> Sing o d
-> (Max a b <=? Max c d) :~: 'True
maxMono Sing o a
a Sing o b
b Sing o c
c Sing o d
d = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> case Sing o c -> Sing o d -> (d <=? Max c d) :~: 'True
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (b <=? Max a b) :~: 'True
maxInfl2 Sing o c
c Sing o d
d of
    (d <=? Max c d) :~: 'True
Refl -> Sing o b
-> Sing o d -> Sing o (Max c d) -> (b <=? Max c d) :~: 'True
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
transTO Sing o b
b Sing o d
d (Sing o c -> Sing o d -> Sing o (Max c d)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Max a b)
maxTO Sing o c
c Sing o d
d)
  OrderingI a b
EQI -> case Sing o c -> Sing o d -> (d <=? Max c d) :~: 'True
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (b <=? Max a b) :~: 'True
maxInfl2 Sing o c
c Sing o d
d of
    (d <=? Max c d) :~: 'True
Refl -> Sing o a
-> Sing o d -> Sing o (Max c d) -> (a <=? Max c d) :~: 'True
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
transTO Sing o a
Sing o b
b Sing o d
d (Sing o c -> Sing o d -> Sing o (Max c d)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Max a b)
maxTO Sing o c
c Sing o d
d)
  OrderingI a b
GTI -> case Sing o c -> Sing o d -> (c <=? Max c d) :~: 'True
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> (a <=? Max a b) :~: 'True
maxInfl1 Sing o c
c Sing o d
d of
    (c <=? Max c d) :~: 'True
Refl -> Sing o a
-> Sing o c -> Sing o (Max c d) -> (a <=? Max c d) :~: 'True
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
transTO Sing o a
a Sing o c
c (Sing o c -> Sing o d -> Sing o (Max c d)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Max a b)
maxTO Sing o c
c Sing o d
d)

-- }}}