{-# LANGUAGE DataKinds #-}

-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.
module Data.Order.Property (
    Rel,
    (==>),
    (<=>),
    xor,
    xor3,

    -- * Orders
    preorder,
    order,

    -- ** Non-strict preorders
    antisymmetric_le,
    reflexive_le,
    transitive_le,
    connex_le,

    -- ** Strict preorders
    asymmetric_lt,
    transitive_lt,
    irreflexive_lt,
    semiconnex_lt,
    trichotomous_lt,

    -- ** Semiorders
    chain_22,
    chain_31,

    -- * Equivalence relations
    symmetric_eq,
    reflexive_eq,
    transitive_eq,

    -- * Properties of generic relations
    reflexive,
    irreflexive,
    coreflexive,
    quasireflexive,
    transitive,
    euclideanL,
    euclideanR,
    connex,
    semiconnex,
    trichotomous,
    symmetric,
    asymmetric,
    antisymmetric,
) where

import Data.Lattice hiding (not)
import Data.Order
import Data.Order.Syntax
import Prelude hiding (Eq (..), Ord (..))

-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.
--
-- Note that these properties do not exhaust all of the possibilities.
--
-- As an example over the natural numbers, the relation \(a \# b \) defined by
-- \( a > 2 \) is neither symmetric nor antisymmetric, let alone asymmetric.
type Rel r b = r -> r -> b

infix 1 ==>

(==>) :: Bool -> Bool -> Bool
==> :: Bool -> Bool -> Bool
(==>) Bool
x Bool
y = Bool -> Bool
not Bool
x Bool -> Bool -> Bool
|| Bool
y

infix 0 <=>

(<=>) :: Bool -> Bool -> Bool
<=> :: Bool -> Bool -> Bool
(<=>) Bool
x Bool
y = (Bool
x Bool -> Bool -> Bool
==> Bool
y) Bool -> Bool -> Bool
&& (Bool
y Bool -> Bool -> Bool
==> Bool
x)

xor3 :: Bool -> Bool -> Bool -> Bool
xor3 :: Bool -> Bool -> Bool -> Bool
xor3 Bool
a Bool
b Bool
c = (Bool
a Bool -> Bool -> Bool
forall a. Symmetric a => a -> a -> a
`xor` (Bool
b Bool -> Bool -> Bool
forall a. Symmetric a => a -> a -> a
`xor` Bool
c)) Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c)

-- | Check a 'Preorder' is internally consistent.
--
-- This is a required property.
preorder :: Preorder r => r -> r -> Bool
preorder :: r -> r -> Bool
preorder r
x r
y =
    ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
<~ r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
le r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
>~ r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
ge r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
?~ r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
cp r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
~~ r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
eq r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
/~ r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
ne r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
< r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
lt r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
> r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
gt r
x r
y)
        Bool -> Bool -> Bool
&& (r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
similar r
x r
y Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
sm r
x r
y)
        Bool -> Bool -> Bool
&& (r -> r -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare r
x r
y Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcmp r
x r
y)
  where
    le :: a -> a -> Bool
le a
x1 a
y1 = a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
< a
y1 Bool -> Bool -> Bool
|| a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
~~ a
y1

    ge :: r -> r -> Bool
ge = (r -> r -> Bool) -> r -> r -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
le

    cp :: a -> a -> Bool
cp a
x1 a
y1 = a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
y1 Bool -> Bool -> Bool
|| a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
>~ a
y1

    eq :: a -> a -> Bool
eq a
x1 a
y1 = a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
y1 Bool -> Bool -> Bool
&& a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
>~ a
y1

    ne :: a -> a -> Bool
ne a
x1 a
y1 = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
eq a
x1 a
y1

    lt :: a -> a -> Bool
lt a
x1 a
y1 = a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
y1 Bool -> Bool -> Bool
&& a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
/~ a
y1

    gt :: r -> r -> Bool
gt = (r -> r -> Bool) -> r -> r -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
lt

    sm :: a -> a -> Bool
sm a
x1 a
y1 = Bool -> Bool
not (a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
< a
y1) Bool -> Bool -> Bool
&& Bool -> Bool
not (a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
> a
y1)

    pcmp :: a -> a -> Maybe Ordering
pcmp a
x1 a
y1
        | a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
y1 = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ if a
y1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
x1 then Ordering
EQ else Ordering
LT
        | a
y1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
x1 = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
        | Bool
otherwise = Maybe Ordering
forall a. Maybe a
Nothing

-- | Check that an 'Order' is internally consistent.
--
-- This is a required property.
order :: Order r => r -> r -> Bool
order :: r -> r -> Bool
order r
x r
y =
    ((r
x r -> r -> Bool
forall a. Order a => a -> a -> Bool
<= r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
le r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Order a => a -> a -> Bool
>= r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
ge r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
eq r
x r
y)
        Bool -> Bool -> Bool
&& ((r
x r -> r -> Bool
forall a. Eq a => a -> a -> Bool
/= r
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
ne r
x r
y)
  where
    le :: a -> a -> Bool
le a
x1 a
y1 = Bool -> (Ordering -> Bool) -> Maybe Ordering -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Ordering -> Ordering -> Bool
forall a. Preorder a => a -> a -> Bool
<~ Ordering
EQ) (Maybe Ordering -> Bool) -> Maybe Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare a
x1 a
y1

    ge :: a -> a -> Bool
ge a
x1 a
y1 = Bool -> (Ordering -> Bool) -> Maybe Ordering -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Ordering -> Ordering -> Bool
forall a. Preorder a => a -> a -> Bool
>~ Ordering
EQ) (Maybe Ordering -> Bool) -> Maybe Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare a
x1 a
y1

    eq :: a -> a -> Bool
eq a
x1 a
y1 = Bool -> (Ordering -> Bool) -> Maybe Ordering -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Ordering -> Ordering -> Bool
forall a. Preorder a => a -> a -> Bool
~~ Ordering
EQ) (Maybe Ordering -> Bool) -> Maybe Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare a
x1 a
y1

    ne :: a -> a -> Bool
ne a
x1 a
y1 = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
~~ a
y1

---------------------------------------------------------------------
-- Non-strict preorders
---------------------------------------------------------------------

-- | \( \forall a, b: (a \leq b) \wedge (b \leq a) \Rightarrow a = b \)
--
-- '<~' is an antisymmetric relation.
--
-- This is a required property.
antisymmetric_le :: Preorder r => r -> r -> Bool
antisymmetric_le :: r -> r -> Bool
antisymmetric_le = (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool
forall r. Rel r Bool -> Rel r Bool -> Rel r Bool
antisymmetric r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(~~) r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<~)

-- | \( \forall a: (a \leq a) \)
--
-- '<~' is a reflexive relation.
--
-- This is a required property.
reflexive_le :: Preorder r => r -> Bool
reflexive_le :: r -> Bool
reflexive_le = Rel r Bool -> r -> Bool
forall r b. Rel r b -> r -> b
reflexive Rel r Bool
forall a. Preorder a => a -> a -> Bool
(<~)

-- | \( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \)
--
-- '<~' is an transitive relation.
--
-- This is a required property.
transitive_le :: Preorder r => r -> r -> r -> Bool
transitive_le :: r -> r -> r -> Bool
transitive_le = (r -> r -> Bool) -> r -> r -> r -> Bool
forall r. Rel r Bool -> r -> Rel r Bool
transitive r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<~)

-- | \( \forall a, b: ((a \leq b) \vee (b \leq a)) \)
--
-- '<~' is a connex relation.
connex_le :: Preorder r => r -> r -> Bool
connex_le :: r -> r -> Bool
connex_le = (r -> r -> Bool) -> r -> r -> Bool
forall r. Rel r Bool -> Rel r Bool
connex r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<~)

---------------------------------------------------------------------
-- Strict preorders
---------------------------------------------------------------------

-- | \( \forall a, b: (a \lt b) \Rightarrow \neg (b \lt a) \)
--
-- 'lt' is an asymmetric relation.
--
-- This is a required property.
asymmetric_lt :: Preorder r => r -> r -> Bool
asymmetric_lt :: r -> r -> Bool
asymmetric_lt = (r -> r -> Bool) -> r -> r -> Bool
forall r. Rel r Bool -> Rel r Bool
asymmetric r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<)

-- | \( \forall a: \neg (a \lt a) \)
--
-- 'lt' is an irreflexive relation.
--
-- This is a required property.
irreflexive_lt :: Preorder r => r -> Bool
irreflexive_lt :: r -> Bool
irreflexive_lt = Rel r Bool -> r -> Bool
forall r. Rel r Bool -> r -> Bool
irreflexive Rel r Bool
forall a. Preorder a => a -> a -> Bool
(<)

-- | \( \forall a, b, c: ((a \lt b) \wedge (b \lt c)) \Rightarrow (a \lt c) \)
--
-- 'lt' is a transitive relation.
--
-- This is a required property.
transitive_lt :: Preorder r => r -> r -> r -> Bool
transitive_lt :: r -> r -> r -> Bool
transitive_lt = (r -> r -> Bool) -> r -> r -> r -> Bool
forall r. Rel r Bool -> r -> Rel r Bool
transitive r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<)

-- | \( \forall a, b: \neg (a = b) \Rightarrow ((a \lt b) \vee (b \lt a)) \)
--
-- 'lt' is a semiconnex relation.
semiconnex_lt :: Preorder r => r -> r -> Bool
semiconnex_lt :: r -> r -> Bool
semiconnex_lt = (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool
forall r. Rel r Bool -> Rel r Bool -> Rel r Bool
semiconnex r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(~~) r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<)

-- | \( \forall a, b, c: ((a \lt b) \vee (a = b) \vee (b \lt a)) \wedge \neg ((a \lt b) \wedge (a = b) \wedge (b \lt a)) \)
--
-- In other words, exactly one of \(a \lt b\), \(a = b\), or \(b \lt a\) holds.
--
-- If 'lt' is a trichotomous relation then the set is totally ordered.
trichotomous_lt :: Preorder r => r -> r -> Bool
trichotomous_lt :: r -> r -> Bool
trichotomous_lt = (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool
forall r. Rel r Bool -> Rel r Bool -> Rel r Bool
trichotomous r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(~~) r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(<)

---------------------------------------------------------------------
-- Semiorders
---------------------------------------------------------------------

-- | \( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \)
--
-- A < https://en.wikipedia.org/wiki/Semiorder semiorder > does not allow 2-2 chains.
chain_22 :: Preorder r => r -> r -> r -> r -> Bool
chain_22 :: r -> r -> r -> r -> Bool
chain_22 r
x r
y r
z r
w = r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
< r
y Bool -> Bool -> Bool
&& r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
similar r
y r
z Bool -> Bool -> Bool
&& r
z r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
< r
w Bool -> Bool -> Bool
==> r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
< r
w

-- \( \forall x, y, z, w: x \lt y \wedge y \lt z \wedge y \sim w \Rightarrow \neg (x \sim w \wedge z \sim w) \) (3-1 chain)
--
-- A < https://en.wikipedia.org/wiki/Semiorder semiorder > does not allow 3-1 chains.
--
-- /Note/: This library models floats, doubles, rationals etc
-- as < https://en.wikipedia.org/wiki/Modular_lattice#Examples N5 > lattices,
-- which do not possess the 3-1 chain property and are not semiorders.
--
chain_31 :: Preorder r => r -> r -> r -> r -> Bool
chain_31 :: r -> r -> r -> r -> Bool
chain_31 r
x r
y r
z r
w = r
x r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
< r
y Bool -> Bool -> Bool
&& r
y r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
< r
z Bool -> Bool -> Bool
&& r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
similar r
y r
w Bool -> Bool -> Bool
==> Bool -> Bool
not (r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
similar r
x r
w Bool -> Bool -> Bool
&& r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
similar r
z r
w)

---------------------------------------------------------------------
-- Equivalence relations
---------------------------------------------------------------------

-- | \( \forall a, b: (a = b) \Leftrightarrow (b = a) \)
--
-- '~~' is a symmetric relation.
--
-- This is a required property.
symmetric_eq :: Preorder r => r -> r -> Bool
symmetric_eq :: r -> r -> Bool
symmetric_eq = (r -> r -> Bool) -> r -> r -> Bool
forall r. Rel r Bool -> Rel r Bool
symmetric r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(~~)

-- | \( \forall a: (a = a) \)
--
-- '~~' is a reflexive relation.
--
-- This is a required property
reflexive_eq :: Preorder r => r -> Bool
reflexive_eq :: r -> Bool
reflexive_eq = Rel r Bool -> r -> Bool
forall r b. Rel r b -> r -> b
reflexive Rel r Bool
forall a. Preorder a => a -> a -> Bool
(~~)

-- | \( \forall a, b, c: ((a = b) \wedge (b = c)) \Rightarrow (a = c) \)
--
-- '~~' is a transitive relation.
--
-- This is a required property.
transitive_eq :: Preorder r => r -> r -> r -> Bool
transitive_eq :: r -> r -> r -> Bool
transitive_eq = (r -> r -> Bool) -> r -> r -> r -> Bool
forall r. Rel r Bool -> r -> Rel r Bool
transitive r -> r -> Bool
forall a. Preorder a => a -> a -> Bool
(~~)

---------------------------------------------------------------------
-- Properties of general relations
---------------------------------------------------------------------

-- | \( \forall a: (a \# a) \)
--
-- For example, ≥ is a reflexive relation but > is not.
reflexive :: Rel r b -> r -> b
reflexive :: Rel r b -> r -> b
reflexive Rel r b
(#) r
a = r
a Rel r b
# r
a

-- | \( \forall a: \neg (a \# a) \)
--
-- For example, > is an irreflexive relation, but ≥ is not.
irreflexive :: Rel r Bool -> r -> Bool
irreflexive :: Rel r Bool -> r -> Bool
irreflexive Rel r Bool
(#) r
a = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ r
a Rel r Bool
# r
a

-- | \( \forall a, b: ((a \# b) \wedge (b \# a)) \Rightarrow (a \equiv b) \)
--
-- For example, the relation over the integers in which each odd number is
-- related to itself is a coreflexive relation. The equality relation is the
-- only example of a relation that is both reflexive and coreflexive, and any
-- coreflexive relation is a subset of the equality relation.
coreflexive :: Rel r Bool -> Rel r Bool -> r -> r -> Bool
coreflexive :: Rel r Bool -> Rel r Bool -> Rel r Bool
coreflexive Rel r Bool
(%) Rel r Bool
(#) r
a r
b = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
&& (r
b Rel r Bool
# r
a) Bool -> Bool -> Bool
==> (r
a Rel r Bool
% r
b)

-- | \( \forall a, b: (a \# b) \Rightarrow ((a \# a) \wedge (b \# b)) \)
quasireflexive :: Rel r Bool -> r -> r -> Bool
quasireflexive :: Rel r Bool -> Rel r Bool
quasireflexive Rel r Bool
(#) r
a r
b = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
==> (r
a Rel r Bool
# r
a) Bool -> Bool -> Bool
&& (r
b Rel r Bool
# r
b)

-- | \( \forall a, b, c: ((a \# b) \wedge (a \# c)) \Rightarrow (b \# c) \)
--
-- For example, /=/ is a right Euclidean relation because if /x = y/ and /x = z/ then /y = z/.
euclideanR :: Rel r Bool -> r -> r -> r -> Bool
euclideanR :: Rel r Bool -> r -> Rel r Bool
euclideanR Rel r Bool
(#) r
a r
b r
c = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
&& (r
a Rel r Bool
# r
c) Bool -> Bool -> Bool
==> r
b Rel r Bool
# r
c

-- |  \( \forall a, b, c: ((b \# a) \wedge (c \# a)) \Rightarrow (b \# c) \)
--
-- For example, /=/ is a left Euclidean relation because if /x = y/ and /x = z/ then /y = z/.
euclideanL :: Rel r Bool -> r -> Rel r Bool
euclideanL :: Rel r Bool -> r -> Rel r Bool
euclideanL Rel r Bool
(#) r
a r
b r
c = (r
b Rel r Bool
# r
a) Bool -> Bool -> Bool
&& (r
c Rel r Bool
# r
a) Bool -> Bool -> Bool
==> r
b Rel r Bool
# r
c

-- | \( \forall a, b, c: ((a \# b) \wedge (b \# c)) \Rightarrow (a \# c) \)
--
-- For example, "is ancestor of" is a transitive relation, while "is parent of" is not.
transitive :: Rel r Bool -> r -> r -> r -> Bool
transitive :: Rel r Bool -> r -> Rel r Bool
transitive Rel r Bool
(#) r
a r
b r
c = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
&& (r
b Rel r Bool
# r
c) Bool -> Bool -> Bool
==> r
a Rel r Bool
# r
c

-- | \( \forall a, b: ((a \# b) \vee (b \# a)) \)
--
-- For example, ≥ is a connex relation, while 'divides evenly' is not.
--
-- A connex relation cannot be symmetric, except for the universal relation.
connex :: Rel r Bool -> r -> r -> Bool
connex :: Rel r Bool -> Rel r Bool
connex Rel r Bool
(#) r
a r
b = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
|| (r
b Rel r Bool
# r
a)

-- | \( \forall a, b: \neg (a \equiv b) \Rightarrow ((a \# b) \vee (b \# a)) \)
--
-- A binary relation is semiconnex if it relates all pairs of _distinct_ elements in some way.
--
-- A relation is connex if and only if it is semiconnex and reflexive.
semiconnex :: Rel r Bool -> Rel r Bool -> r -> r -> Bool
semiconnex :: Rel r Bool -> Rel r Bool -> Rel r Bool
semiconnex Rel r Bool
(%) Rel r Bool
(#) r
a r
b = Bool -> Bool
not (r
a Rel r Bool
% r
b) Bool -> Bool -> Bool
==> Rel r Bool -> Rel r Bool
forall r. Rel r Bool -> Rel r Bool
connex Rel r Bool
(#) r
a r
b

-- | \( \forall a, b, c: ((a \# b) \vee (a \doteq b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \doteq b) \wedge (b \# a)) \)
--
-- In other words, exactly one of \(a \# b\), \(a \doteq b\), or \(b \# a\) holds.
--
-- For example, > is a trichotomous relation, while ≥ is not.
--
-- Note that @ trichotomous (>) @ should hold for any 'Ord' instance.
trichotomous :: Rel r Bool -> Rel r Bool -> r -> r -> Bool
trichotomous :: Rel r Bool -> Rel r Bool -> Rel r Bool
trichotomous Rel r Bool
(%) Rel r Bool
(#) r
a r
b = Bool -> Bool -> Bool -> Bool
xor3 (r
a Rel r Bool
# r
b) (r
a Rel r Bool
% r
b) (r
b Rel r Bool
# r
a)

-- | \( \forall a, b: (a \# b) \Leftrightarrow (b \# a) \)
--
-- For example, "is a blood relative of" is a symmetric relation, because
-- A is a blood relative of B if and only if B is a blood relative of A.
symmetric :: Rel r Bool -> r -> r -> Bool
symmetric :: Rel r Bool -> Rel r Bool
symmetric Rel r Bool
(#) r
a r
b = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
<=> (r
b Rel r Bool
# r
a)

-- | \( \forall a, b: (a \# b) \Rightarrow \neg (b \# a) \)
--
-- For example, > is an asymmetric relation, but ≥ is not.
--
-- A relation is asymmetric if and only if it is both antisymmetric and irreflexive.
asymmetric :: Rel r Bool -> r -> r -> Bool
asymmetric :: Rel r Bool -> Rel r Bool
asymmetric Rel r Bool
(#) r
a r
b = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
==> Bool -> Bool
not (r
b Rel r Bool
# r
a)

-- | \( \forall a, b: (a \# b) \wedge (b \# a) \Rightarrow a \equiv b \)
--
-- For example, ≥ is an antisymmetric relation; so is >, but vacuously
-- (the condition in the definition is always false).
antisymmetric :: Rel r Bool -> Rel r Bool -> r -> r -> Bool
antisymmetric :: Rel r Bool -> Rel r Bool -> Rel r Bool
antisymmetric Rel r Bool
(%) Rel r Bool
(#) r
a r
b = (r
a Rel r Bool
# r
b) Bool -> Bool -> Bool
&& (r
b Rel r Bool
# r
a) Bool -> Bool -> Bool
==> (r
a Rel r Bool
% r
b)