Test.Property.Relation.Connex

See https://en.wikipedia.org/wiki/Connex_relation.

Documentation

connex :: (r -> r -> Bool) -> r -> r -> Bool

\( \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.

semiconnex :: Eq r => (r -> r -> Bool) -> r -> r -> Bool

\( \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_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool

\( \forall a, b: \neg (a \doteq b) \Rightarrow ((a \# b) \vee (b \# a)) \)

trichotomous :: Eq r => (r -> r -> Bool) -> r -> r -> Bool

\( \forall a, b, c: ((a \# b) \vee (a \equiv b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \equiv b) \wedge (b \# a)) \)

Note that trichotomous (>) should hold for any Ord instance.

trichotomous_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool

\( \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.