Copyright	(c) L. S. Leary 2025
Safe Haskell	None
Language	Haskell2010

Data.Type.Ord.Lemmata

Contents

Equivalence
Ordering

Description

Lemmata for easier use of Data.Type.Ord.

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

Synopsis

symEq :: forall e (a :: e) (b :: e). (Equivalence 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)
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)
leqToGeq :: forall o (a :: o) (b :: o). (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)
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)
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)
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)
minDefl1 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Proof (Min a b <= a)
minDefl2 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Proof (Min a b <= b)
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)
minSym :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Min a b :~: Min b a
maxInfl1 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Proof (a <= Max a b)
maxInfl2 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Proof (b <= Max a b)
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)
maxSym :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Max a b :~: Max b a

Equivalence

symEq Source #

Arguments

:: forall e (a :: e) (b :: e). (Equivalence e, a == b)
=> Sing e a
-> Sing e b
-> Proof (b == a)

Symmetry of equivalence.

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

symNeq Source #

Arguments

:: forall e (a :: e) (b :: e). (TotalOrder e, a /= b)
=> Sing e a
-> Sing e b
-> Proof (b /= a)

Symmetry of inequivalence.

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

transEq Source #

Arguments

:: 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)

Transitivity of equivalence.

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

Ordering

Reflection

leqToGeq :: forall o (a :: o) (b :: o). (TotalOrder o, a <= b) => Sing o a -> Sing o b -> Proof (b >= a) Source #

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

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

geqToLeq :: forall o (a :: o) (b :: o). (TotalOrder o, a >= b) => Sing o a -> Sing o b -> Proof (b <= a) Source #

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

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

Transitivity

transLt Source #

Arguments

:: 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)

Transitivity of \( \lt \).

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

transGt Source #

Arguments

:: 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)

Transitivity of \( \gt \).

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

transGeq Source #

Arguments

:: 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)

Transitivity of \( \geq \).

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

Properties of Min

minDefl1 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Proof (Min a b <= a)

Min is deflationary in its first argument.

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

minDefl2 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Proof (Min a b <= b)

Min is deflationary in its second argument.

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

minMono Source #

Arguments

:: 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)

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 \]

minSym Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Min a b :~: Min b a

Min is symmetric.

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

Properties of Max

maxInfl1 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Proof (a <= Max a b)

Max is inflationary in its first argument.

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

maxInfl2 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Proof (b <= Max a b)

Max is inflationary in its second argument.

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

maxMono Source #

Arguments

:: 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)

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 \]

maxSym Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Max a b :~: Max b a

Max is symmetric.

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