{-# LANGUAGE DataKinds #-}
module Data.Order.Property (
Rel,
(==>),
(<=>),
xor,
xor3,
preorder,
order,
antisymmetric_le,
reflexive_le,
transitive_le,
connex_le,
asymmetric_lt,
transitive_lt,
irreflexive_lt,
semiconnex_lt,
trichotomous_lt,
chain_22,
chain_31,
symmetric_eq,
reflexive_eq,
transitive_eq,
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 (..))
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)
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
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
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
(<~)
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
(<~)
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
(<~)
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
(<~)
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
(<)
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
(<)
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
(<)
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
(<)
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
(<)
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
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)
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
(~~)
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
(~~)
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
(~~)
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
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
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)
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)
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
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
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
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)
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
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)
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)
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)
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)