Property.hs

-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.
module Data.Prd.Property (
  -- * Equivalence relations
    symmetric
  , coreflexive
  , reflexive_eq
  , transitive_eq

  -- * Partial orders
  -- ** Non-strict partial orders
  , antisymmetric
  , reflexive_le
  , transitive_le
  -- ** Connex non-strict partial orders
  , connex
  -- ** Strict partial orders
  , asymmetric
  , transitive_lt
  , irreflexive_lt
  -- ** Semiconnex strict partial orders
  , semiconnex
  , trichotomous
  -- ** Semiorders
  , chain_22
  , chain_31
) where

import Data.Prd
import Data.Prd.Lattice
import Test.Property.Util
import Prelude hiding (Ord(..))

import qualified Prelude as P
import qualified Test.Property.Relation as R

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

-- | \( \forall x, y: x \eq y \Leftrightarrow x == y \)
--
-- '=~' is a coreflexive relation.
--
-- See <https://en.wikipedia.org/wiki/Reflexive_relation#Related_terms>.
--
-- This is a required property.
--
coreflexive :: (Eq r, Prd r) => r -> r -> Bool
coreflexive x y = x =~ y ==> x == y

-- | \( \forall a: (a \eq a) \)
--
-- '=~' is a reflexive relation.
--
-- This is a required property.
--
reflexive_eq :: Prd r => r ->  Bool
reflexive_eq = R.reflexive (=~) 

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

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

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

-- | \( \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 :: Prd r => r -> r -> r -> Bool
transitive_le = R.transitive (<~)

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

-- | \( \forall a, b: (a \lt b) \Rightarrow \neg (b \lt a) \)
--
-- 'lt' is an asymmetric relation.
--
-- This is a required property.
--
asymmetric :: Eq r => Prd r => r -> r -> Bool
asymmetric = R.asymmetric lt

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

-- | \( \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 :: Eq r => Prd r => r -> r -> r -> Bool
transitive_lt = R.transitive lt

-- | \( \forall a, b: \neg (a \eq b) \Rightarrow ((a \lt b) \vee (b \lt a)) \)
--
-- 'lt' is a semiconnex relation.
--
semiconnex :: Eq r => Prd r => r -> r -> Bool
semiconnex = R.semiconnex_on (=~) lt

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

-- | \( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \) 
--
-- A semiorder does not allow 2-2 chains.
--
chain_22 :: Eq r => Prd r => r -> r -> r -> r -> Bool
chain_22 x y z w = x `lt` y && y ~~ z && z `lt` w ==> x `lt` 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 semiorder does not allow 3-1 chains.
--
chain_31 :: Eq r => Prd r => r -> r -> r -> r -> Bool
chain_31 x y z w = x `lt` y && y `lt` z && y ~~ w ==> not (x ~~ w && z ~~ w)