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

{-# LANGUAGE GADTs #-}


{- |

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

Lemmata for easier use of "Data.Type.Ord".

\(\newcommand{\ldot}{.\,\,}\)

-}

-- }}}

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

module Data.Type.Ord.Lemmata (

  -- * Equivalence
  symEq,
  symNeq,
  transEq,

  -- * Ordering

  -- ** Reflection
  leqToGeq,
  geqToLeq,

  -- ** Transitivity
  transLt,
  transGt,
  transGeq,

  -- ** Properties of Min
  minDefl1,
  minDefl2,
  minMono,
  minSym,

  -- ** Properties of Max
  maxInfl1,
  maxInfl2,
  maxMono,
  maxSym,

) where

-- }}}

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

-- base
import Data.Type.Equality ((:~:)(..))
import Data.Type.Ord (OrderingI(..), Min, Max)

-- ord-axiomata
import Data.Type.Ord.Axiomata

-- }}}

-- --< Equivalence >-- {{{

{- |

Symmetry of equivalence.

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

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

{- |

Symmetry of inequivalence.

\[
  \forall a, b \ldot
    a \neq b \iff b \neq a
\]

-}
symNeq
  :: (TotalOrder e, a /= b)
  => Sing e a -> Sing e b {- ^ -}
  -> Proof (b /= a)
symNeq :: forall e (a :: e) (b :: e).
(TotalOrder e, a /= b) =>
Sing e a -> Sing e b -> Proof (b /= a)
symNeq Sing e a
a Sing e b
b = case Sing e b -> Sing e a -> Compare b a :~: Reflect (Compare a b)
forall (a :: e) (b :: e).
Sing e a -> Sing e 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 e b
b Sing e a
a of
  Compare b a :~: Reflect (Compare a b)
Refl -> case Sing e a
a Sing e a -> Sing e b -> OrderingI a b
forall (a :: e) (b :: e). Sing e a -> Sing e b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing e b
b of
    OrderingI a b
LTI -> 'True :~: 'True
Proof (b /= a)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
GTI -> 'True :~: 'True
Proof (b /= a)
forall {k} (a :: k). a :~: a
Refl

{- |

Transitivity of equivalence.

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

-}
transEq
  :: (Equivalence e, a == b, b == c)
  => Sing e a -> Sing e b -> Sing e c {- ^ -}
  -> Proof (a == c)
transEq :: forall e (a :: e) (b :: e) (c :: e).
(Equivalence e, a == b, b == c) =>
Sing e a -> Sing e b -> Sing e c -> Proof (a == c)
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).
(a == b) =>
Sing e a -> Sing e b -> a :~: b
forall e (a :: e) (b :: e).
(Equivalence e, a == b) =>
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).
(a == b) =>
Sing e a -> Sing e b -> a :~: b
forall e (a :: e) (b :: e).
(Equivalence e, a == b) =>
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
Proof (a == c)
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Ordering: Reflection >-- {{{

{- |

Anti-symmetry of \( \leq \) and \( \geq \).

\[
  \forall a, b \ldot
    a \leq b \implies b \geq a
\]

-}
leqToGeq
  :: (TotalOrder o, a <= b)
  => Sing o a -> Sing o b
  -> Proof (b >= a)
leqToGeq :: forall o (a :: o) (b :: o).
(TotalOrder o, a <= b) =>
Sing o a -> Sing o b -> Proof (b >= a)
leqToGeq Sing o a
a Sing o b
b = 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 -> 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
Proof (b >= a)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> 'True :~: 'True
Proof (b >= a)
forall {k} (a :: k). a :~: a
Refl

{- |

Anti-symmetry of \( \geq \) and \( \leq \).

\[
  \forall a, b \ldot
    a \geq b \implies b \leq a
\]

-}
geqToLeq
  :: (TotalOrder o, a >= b)
  => Sing o a -> Sing o b
  -> Proof (b <= a)
geqToLeq :: forall o (a :: o) (b :: o).
(TotalOrder o, a >= b) =>
Sing o a -> Sing o b -> Proof (b <= a)
geqToLeq Sing o a
a Sing o b
b = 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 -> 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
EQI -> 'True :~: 'True
Proof (b <= a)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
GTI -> 'True :~: 'True
Proof (b <= a)
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Ordering: Transitivity >-- {{{

{- |

Transitivity of \( \lt \).

\[
  \forall a, b, c \ldot
    a \lt b \land b \lt c \implies a \lt c
\]

-}
transLt
  :: (TotalOrder o, a < b, b < c)
  => Sing o a -> Sing o b -> Sing o c {- ^ -}
  -> Proof (a < c)
transLt :: forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a < b, b < c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a < c)
transLt Sing o a
a Sing o b
b Sing o c
c = case Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq Sing o a
a Sing o b
b Sing o c
c of
  OrdCond (Compare a c) 'True 'True 'False :~: 'True
Proof (a <= c)
Refl -> case Sing o a
a Sing o a -> Sing o c -> OrderingI a c
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 c
c of
    OrderingI a c
LTI -> 'LT :~: 'LT
Proof (a < c)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a c
EQI -> case Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
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 a
a Sing o b
b of

{- |

Transitivity of \( \gt \).

\[
  \forall a, b, c \ldot
    a \gt b \land b \gt c \implies a \gt c
\]

-}
transGt
  :: (TotalOrder o, a > b, b > c)
  => Sing o a -> Sing o b -> Sing o c {- ^ -}
  -> Proof (a > c)
transGt :: forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a > b, b > c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a > c)
transGt Sing o a
a Sing o b
b Sing o c
c = case Sing o c -> Sing o b -> Compare c b :~: Reflect (Compare b c)
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 c
c Sing o b
b of
  Compare c b :~: Reflect (Compare b c)
Refl -> 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 -> case Sing o c -> Sing o b -> Sing o a -> Proof (c < a)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a < b, b < c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a < c)
transLt Sing o c
c Sing o b
b Sing o a
a of
      Compare c a :~: 'LT
Proof (c < a)
Refl -> case Sing o a -> Sing o c -> Compare a c :~: Reflect (Compare c a)
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 a
a Sing o c
c of
        Compare a c :~: Reflect (Compare c a)
Refl -> 'GT :~: 'GT
Proof (a > c)
forall {k} (a :: k). a :~: a
Refl

{- |

Transitivity of \( \geq \).

\[
  \forall a, b, c \ldot
    a \geq b \land b \geq c \implies a \geq c
\]

-}
transGeq
  :: (TotalOrder o, a >= b, b >= c)
  => Sing o a -> Sing o b -> Sing o c {- ^ -}
  -> Proof (a >= c)
transGeq :: forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a >= b, b >= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a >= c)
transGeq Sing o a
a Sing o b
b Sing o c
c = case Sing o b -> Sing o c -> Proof (c <= b)
forall o (a :: o) (b :: o).
(TotalOrder o, a >= b) =>
Sing o a -> Sing o b -> Proof (b <= a)
geqToLeq Sing o b
b Sing o c
c of
  OrdCond (Compare c b) 'True 'True 'False :~: 'True
Proof (c <= b)
Refl -> case Sing o a -> Sing o b -> Proof (b <= a)
forall o (a :: o) (b :: o).
(TotalOrder o, a >= b) =>
Sing o a -> Sing o b -> Proof (b <= a)
geqToLeq Sing o a
a Sing o b
b of
    OrdCond (Compare b a) 'True 'True 'False :~: 'True
Proof (b <= a)
Refl -> case Sing o c -> Sing o b -> Sing o a -> Proof (c <= a)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq Sing o c
c Sing o b
b Sing o a
a of
      OrdCond (Compare c a) 'True 'True 'False :~: 'True
Proof (c <= a)
Refl -> case Sing o c -> Sing o a -> Proof (a >= c)
forall o (a :: o) (b :: o).
(TotalOrder o, a <= b) =>
Sing o a -> Sing o b -> Proof (b >= a)
leqToGeq Sing o c
c Sing o a
a of
        OrdCond (Compare a c) 'False 'True 'True :~: 'True
Proof (a >= c)
Refl -> 'True :~: 'True
Proof (a >= c)
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Ordering: Properties of Min >-- {{{

{- |

'Min' is deflationary in its first argument.

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

-}
minDefl1
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> Proof (Min a b <= a)
minDefl1 :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (Min a b <= a)
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 -> Proof (a == a)
forall (a :: o). Sing o a -> Proof (a == a)
forall e (a :: e). Equivalence e => Sing e a -> Proof (a == a)
refl Sing o a
a of
    Compare a a :~: 'EQ
Proof (a == a)
Refl -> 'True :~: 'True
Proof (Min a b <= a)
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
EQI -> 'True :~: 'True
Proof (Min a b <= a)
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
Proof (Min a b <= a)
forall {k} (a :: k). a :~: a
Refl

{- |

'Min' is deflationary in its second argument.

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

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

{- |

'Min' is monotonic in both arguments.

\[
  \forall a, b, c, d \ldot
    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 {- ^ -}
  -> Proof (Min a b <= Min c d)
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 -> Proof (Min a b <= Min c d)
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 -> Proof (Min a b <= a)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (Min a b <= a)
minDefl1 Sing o a
a Sing o b
b of
    OrdCond (Compare (Min a b) a) 'True 'True 'False :~: 'True
Proof (Min a b <= a)
Refl -> Sing o (Min a b) -> Sing o a -> Sing o c -> Proof (Min a b <= c)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq (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 -> Proof (Min a b <= a)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (Min a b <= a)
minDefl1 Sing o a
a Sing o b
b of
    OrdCond (Compare (Min a b) a) 'True 'True 'False :~: 'True
Proof (Min a b <= a)
Refl -> Sing o (Min a b) -> Sing o a -> Sing o c -> Proof (Min a b <= c)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq (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 -> Proof (Min a b <= b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (Min a b <= b)
minDefl2 Sing o a
a Sing o b
b of
    OrdCond (Compare (Min a b) b) 'True 'True 'False :~: 'True
Proof (Min a b <= b)
Refl -> Sing o (Min a b) -> Sing o b -> Sing o d -> Proof (Min a b <= d)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq (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

{- |

'Min' is symmetric.

\[
  \forall a, b \ldot
    \mathrm{min} \, a \, b \sim \mathrm{min} \, b \, a
\]

-}
minSym
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> Min a b :~: Min b a
minSym :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Min a b :~: Min b a
minSym Sing o a
a Sing o b
b = 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 -> 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 -> a :~: a
Min a b :~: Min b a
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> a :~: a
Min a b :~: Min b a
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
GTI -> b :~: b
Min a b :~: Min b a
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Ordering: Properties of Max >-- {{{

{- |

'Max' is inflationary in its first argument.

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

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

{- |

'Max' is inflationary in its second argument.

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

-}
maxInfl2
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> Proof (b <= Max a b)
maxInfl2 :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (b <= Max a b)
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 -> Proof (b == b)
forall (a :: o). Sing o a -> Proof (a == a)
forall e (a :: e). Equivalence e => Sing e a -> Proof (a == a)
refl Sing o b
b of
    Compare b b :~: 'EQ
Proof (b == b)
Refl -> 'True :~: 'True
Proof (b <= Max a b)
forall {k} (a :: k). a :~: a
Refl
  OrderingI a b
EQI -> 'True :~: 'True
Proof (b <= Max a b)
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
Proof (b <= Max a b)
forall {k} (a :: k). a :~: a
Refl

{- |

'Max' is monotonic in both arguments.

\[
  \forall a, b, c, d \ldot
    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 {- ^ -}
  -> Proof (Max a b <= Max c d)
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 -> Proof (Max a b <= Max c d)
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 -> Proof (d <= Max c d)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (b <= Max a b)
maxInfl2 Sing o c
c Sing o d
d of
    OrdCond (Compare d (Max c d)) 'True 'True 'False :~: 'True
Proof (d <= Max c d)
Refl -> Sing o b -> Sing o d -> Sing o (Max c d) -> Proof (b <= Max c d)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq 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 -> Proof (d <= Max c d)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (b <= Max a b)
maxInfl2 Sing o c
c Sing o d
d of
    OrdCond (Compare d (Max c d)) 'True 'True 'False :~: 'True
Proof (d <= Max c d)
Refl -> Sing o a -> Sing o d -> Sing o (Max c d) -> Proof (a <= Max c d)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq 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 -> Proof (c <= Max c d)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (a <= Max a b)
maxInfl1 Sing o c
c Sing o d
d of
    OrdCond (Compare c (Max c d)) 'True 'True 'False :~: 'True
Proof (c <= Max c d)
Refl -> Sing o a -> Sing o c -> Sing o (Max c d) -> Proof (a <= Max c d)
forall (a :: o) (b :: o) (c :: o).
(a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
transLeq 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)

{- |

'Max' is symmetric.

\[
  \forall a, b \ldot
    \mathrm{max} \, a \, b \sim \mathrm{max} \, b \, a
\]

-}
maxSym
  :: TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> Max a b :~: Max b a
maxSym :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Max a b :~: Max b a
maxSym Sing o a
a Sing o b
b = 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 -> 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 -> b :~: b
Max a b :~: Max b a
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> a :~: a
Max a b :~: Max b a
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
GTI -> a :~: a
Max a b :~: Max b a
forall {k} (a :: k). a :~: a
Refl

-- }}}