# *ord-axiomata*

When using `Data.Type.Ord`, there are many facts one intuitively expects to hold that GHC is not clever enough to infer.

We rectify this situation with `TotalOrder` and related typeclasses that not only enable comparison of singletons, but also provide axiomata allowing one to safely prove such facts to GHC.

## Axiomata

Due to the expression of equivalence and ordering in terms of `Compare`, the phrasing of the axiomata is a little different than normal—some are reduced to consistency conditions for the following definitions.

$$
\begin{alignat*}{3}
  &a  <   b &&\iff &&\mathrm{Compare} \kern3pt a \kern3pt b \sim \mathrm{LT} \\
  &a  =   b &&\iff &&\mathrm{Compare} \kern3pt a \kern3pt b \sim \mathrm{EQ} \\
  &a  >   b &&\iff &&\mathrm{Compare} \kern3pt a \kern3pt b \sim \mathrm{GT} \\
  &a \leq b &&\iff &&a < b \lor a = b                                        \\
  &a \geq b &&\iff &&a > b \lor a = b
\end{alignat*}
$$

### Equivalence

$$
\begin{alignat*}{3}
&\text{decidability}     \quad\quad\quad && \forall a, b \kern-2pt :
  \kern6pt && a = b \lor a \neq b     \\
&\text{reflexivity}      \quad\quad\quad && \forall a, b \kern-2pt :
  \kern6pt && a \sim b \implies a = b \\
&\text{substitutability} \quad\quad\quad && \forall a, b \kern-2pt :
  \kern6pt && a = b \implies a \sim b \\
\end{alignat*}
$$

### Total Ordering

$$
\begin{alignat*}{3}
&\text{connectivity}  \quad\quad\quad && \forall a, b    \kern-2pt :
  \kern6pt && a \lt b \lor a = b \lor a \gt b           \\
&\text{anti-symmetry} \quad\quad\quad && \forall a, b    \kern-2pt :
  \kern6pt && a \le b \implies b \ge a                  \\
&\text{transitivity}  \quad\quad\quad && \forall a, b, c \kern-2pt :
  \kern6pt && a \leq b \land b \leq c \implies a \leq c \\
\end{alignat*}
$$

### Bounding

$$
\begin{alignat*}{3}
&\text{bounded below} \quad\quad\quad && \exists b_l \forall a \kern-2pt :
  \kern6pt && b_l \leq a \\
&\text{bounded above} \quad\quad\quad && \exists b_u \forall a \kern-2pt :
  \kern6pt && a \leq b_u \\
\end{alignat*}
$$

## Lemmata

With the above at our disposal, we can prove general, reusable facts.

### Equivalence

$$
\begin{alignat*}{3}
&\text{symmetry}     \quad\quad\quad && \forall a, b    \kern-2pt :
  \kern6pt && a = b \iff b = a                 \\
&\text{transitivity} \quad\quad\quad && \forall a, b, c \kern-2pt :
  \kern6pt && a = b \land b = c \implies a = c \\
\end{alignat*}
$$

### Minimum

$$
\begin{alignat*}{3}
&\text{deflationary} \quad\quad\quad && \forall a, b \kern-2pt :
  \kern6pt && \mathrm{min} \kern3pt a \kern3pt b \leq a, b \\
&\text{monotonicity} \quad\quad\quad && \forall a, b, c, d \kern-2pt :
  \kern6pt && a \leq c \land b \leq d
    \implies \mathrm{min} \kern3pt a \kern3pt b
        \leq \mathrm{min} \kern3pt c \kern3pt d            \\
\end{alignat*}
$$

### Maximum

$$
\begin{alignat*}{3}
&\text{inflationary} \quad\quad\quad && \forall a, b \kern-2pt :
  \kern6pt && a, b \leq \mathrm{max} \kern3pt a \kern3pt b \\
&\text{monotonicity} \quad\quad\quad && \forall a, b, c, d \kern-2pt :
  \kern6pt && a \leq c \land b \leq d
    \implies \mathrm{max} \kern3pt a \kern3pt b
        \leq \mathrm{max} \kern3pt c \kern3pt d            \\
\end{alignat*}
$$