{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Data.Lattice.Property where

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

coheyting0 :: Coheyting a => a -> a -> a -> Bool
coheyting0 x y z = x \\ y <= z <=> x <= y \/ z

coheyting1 :: Coheyting a => a -> a -> a -> Bool
coheyting1 x y z = x \\ y >= (x /\ z) \\ y

coheyting2 :: Coheyting a => a -> a -> a -> Bool
coheyting2 x y z = x \\ (y /\ z) >= x \\ y

coheyting3 :: Coheyting a => a -> a -> a -> Bool
coheyting3 x y z = x >= y ==> x \\ z >= y \\ z

coheyting4 :: Coheyting a => a -> a -> a -> Bool
coheyting4 x y z = z \\ (x \/ y) == z \\ x \\ y

coheyting5 :: Coheyting a => a -> a -> a -> Bool
coheyting5 x y z = (y \/ z) \\ x == y \\ x \/ z \\ x

coheyting6 :: Coheyting a => a -> a -> Bool
coheyting6 x y = x >= x \\ y

coheyting7 :: Coheyting a => a -> a -> Bool
coheyting7 x y = x \/ y \\ x == x \/ y

coheyting8 :: forall a. Coheyting a => a -> Bool
coheyting8 _ = non bottom == top @a && non top == bottom @a

-- Double co-negation is a co-monad.
coheyting9 :: Coheyting a => a -> a -> Bool
coheyting9 x y = x /\ non y >= x \\ y

coheyting10 :: Coheyting a => a -> a -> Bool
coheyting10 x y = x >= y <=> y \\ x == bottom

coheyting11 :: Coheyting a => a -> a -> Bool
coheyting11 x y = non (x /\ y) >= non x

coheyting12 :: Coheyting a => a -> a -> Bool
coheyting12 x y = non (y \\ x) == non (non x) \/ non y

coheyting13 :: Coheyting a => a -> a -> Bool
coheyting13 x y = non (x /\ y) == non x \/ non y

coheyting14 :: Coheyting a => a -> Bool
coheyting14 x = x \/ non x == top

coheyting15 :: Coheyting a => a -> Bool
coheyting15 x = non (non (non x)) == non x

coheyting16 :: Coheyting a => a -> Bool
coheyting16 x = non (non (x /\ non x)) == bottom

coheyting17 :: Coheyting a => a -> Bool
coheyting17 x = x >= non (non x)

coheyting18 :: Coheyting c => c -> Bool
coheyting18 x = x == boundary x \/ (non . non) x

coheyting19 :: Coheyting a => a -> a -> Bool
coheyting19 x y = boundary (x /\ y) == (boundary x /\ y) \/ (x /\ boundary y) -- (Leibniz rule)

coheyting20 :: Coheyting a => a -> a -> Bool
coheyting20 x y = boundary (x \/ y) \/ boundary (x /\ y) == boundary x \/ boundary y

heyting0 :: Heyting a => a -> a -> a -> Bool
heyting0 x y z = x /\ y <= z <=> x <= y // z

heyting1 :: Heyting a => a -> a -> a -> Bool
heyting1 x y z = x // y <= x // (y \/ z)

heyting2 :: Heyting a => a -> a -> a -> Bool
heyting2 x y z = (x \/ z) // y <= x // y

heyting3 :: Heyting a => a -> a -> a -> Bool
heyting3 x y z = x <= y ==> z // x <= z // y

heyting4 :: Heyting a => a -> a -> a -> Bool
heyting4 x y z = (x /\ y) // z == x // y // z

heyting5 :: Heyting a => a -> a -> a -> Bool
heyting5 x y z = x // (y /\ z) == x // y /\ x // z

heyting6 :: Heyting a => a -> a -> Bool
heyting6 x y = y <= x // (x /\ y)

heyting7 :: Heyting a => a -> a -> Bool
heyting7 x y = x /\ x // y == x /\ y

heyting8 :: forall a. Heyting a => a -> Bool
heyting8 _ = neg bottom == top @a && neg top == bottom @a

-- Double negation is a monad.
heyting9 :: Heyting a => a -> a -> Bool
heyting9 x y = neg x \/ y <= x // y

heyting10 :: Heyting a => a -> a -> Bool
heyting10 x y = x <= y <=> x // y == top

heyting11 :: Heyting a => a -> a -> Bool
heyting11 x y = neg (x \/ y) <= neg x

heyting12 :: Heyting a => a -> a -> Bool
heyting12 x y = neg (x // y) == neg (neg x) /\ neg y

heyting13 :: Heyting a => a -> a -> Bool
heyting13 x y = neg (x \/ y) == neg x /\ neg y

heyting14 :: Heyting a => a -> Bool
heyting14 x = x /\ neg x == bottom

heyting15 :: Heyting a => a -> Bool
heyting15 x = neg (neg (neg x)) == neg x

heyting16 :: Heyting a => a -> Bool
heyting16 x = neg (neg (x \/ neg x)) == top

heyting17 :: Heyting a => a -> Bool
heyting17 x = x <= neg (neg x)

--
-- x '\\' x           = 'top'
-- x '/\' (x '\\' y)  = x '/\' y
-- y '/\' (x '\\' y)  = y
-- x '\\' (y '\\' z) = (x '/\' y) '\\' z
-- x '\\' (y '/\' z)  = (x '\\' y) '/\' (x '\\' z)
-- 'neg' (x '/\' y)    = 'neg' (x '\/' y)
-- 'neg' (x '\/' y)    = 'neg' x '/\' 'neg' y
-- (x '\\' y) '\/' x '<=' y
-- y '<=' (x '\\' x '/\' y)
-- x '<=' y => (z '\\' x) '<=' (z '\\' y)
-- x '<=' y => (x '\\' z) '<=' (y '\\' z)
-- x '<=' y <=> x '\\' y '==' 'top'
-- x '/\' y '<=' z <=> x '<=' (y '\\' z) <=> y '<=' (x '\\' z)
--
--

-- adjointL $ ConnL (\x -> y \\ not x) (\z -> not z // not y)
symmetric1 :: Biheyting a => a -> Bool
symmetric1 x = neg x <= non x

symmetric2 :: Symmetric a => a -> Bool
symmetric2 x = (neg . neg) x == (converseR . converseL) x

symmetric3 :: Symmetric a => a -> Bool
symmetric3 x = (non . non) x == (converseL . converseR) x

symmetric4 :: Symmetric a => a -> Bool
symmetric4 x = non x == (converseL . not) x && neg x == (not . converseL) x

symmetric5 :: Symmetric a => a -> Bool
symmetric5 x = non x == (not . converseR) x && neg x == (converseR . not) x

symmetric6 :: Heyting a => a -> Bool
symmetric6 x = neg x \/ neg (neg x) == top

symmetric7 :: Symmetric a => a -> a -> Bool
symmetric7 x y = not (x /\ y) == not x \/ not y

symmetric8 :: Symmetric a => a -> a -> Bool
symmetric8 x y = (not . not) (x \/ y) == not (not x) \/ not (not y)

symmetric9 :: Symmetric a => a -> a -> Bool
symmetric9 x y = not (x \/ y) == not x /\ not y

symmetric10 :: Symmetric a => a -> a -> Bool
symmetric10 x y = converseL (x \/ y) == converseL x \/ converseL y

symmetric11 :: Symmetric a => a -> a -> Bool
symmetric11 x y = converseR (x /\ y) == converseR x /\ converseR y

symmetric12 :: Symmetric a => a -> a -> Bool
symmetric12 x y = converseL (x /\ y) == (non . non) (converseL x /\ converseL y)

symmetric13 :: Symmetric a => a -> a -> Bool
symmetric13 x y = converseR (x \/ y) == (neg . neg) (converseR x \/ converseR y)

boolean0 :: Biheyting a => a -> Bool
boolean0 x = neg x == non x

boolean1 :: Heyting a => a -> Bool
boolean1 x = neg (neg x) == x

boolean2 :: Heyting a => a -> Bool
boolean2 x = x \/ neg x == top

boolean3 :: Coheyting a => a -> Bool
boolean3 x = x /\ non x == bottom

boolean4 :: Heyting a => a -> a -> Bool
boolean4 x y = (x <= y) // (neg y <= neg x)

boolean5 :: Biheyting a => a -> a -> Bool
boolean5 x y = x \\ y == neg (neg y // neg x)

boolean6 :: Biheyting a => a -> a -> Bool
boolean6 x y = x // y == non (non y \\ non x)

{-
infix 4 `joinLe`
-- | The partial ordering induced by the join-semilattice structure.
--
--
-- Normally when /a/ implements 'Ord' we should have:
-- @ 'joinLe' x y = x '<=' y @
--
joinLe :: Lattice a => a -> a -> Bool
joinLe x y = y == x \/ y

infix 4 `joinGe`
-- | The partial ordering induced by the join-semilattice structure.
--
-- Normally when /a/ implements 'Ord' we should have:
-- @ 'joinGe' x y = x '>=' y @
--
joinGe :: Lattice a => a -> a -> Bool
joinGe x y = x == x \/ y

-- | Partial version of 'Data.Ord.compare'.
--
-- Normally when /a/ implements 'Preorder' we should have:
-- @ 'pcompareJoin' x y = 'pcompare' x y @
--
pcompareJoin :: Lattice a => a -> a -> Maybe Ordering
pcompareJoin x y
  | x == y = Just EQ
  | joinLe x y && x /= y = Just LT
  | joinGe x y && x /= y = Just GT
  | otherwise = Nothing

infix 4 `meetLe`
-- | The partial ordering induced by the meet-semilattice structure.
--
-- Normally when /a/ implements 'Preorder' we should have:
-- @ 'meetLe' x y = x '<~' y @
--
meetLe :: Lattice a => a -> a -> Bool
meetLe x y = x == x /\ y

infix 4 `meetGe`
-- | The partial ordering induced by the meet-semilattice structure.
--
-- Normally when /a/ implements 'Preorder' we should have:
-- @ 'meetGe' x y = x '>~' y @
--
meetGe :: Lattice a => a -> a -> Bool
meetGe x y = y == x /\ y

-- | Partial version of 'Data.Ord.compare'.
--
-- Normally when /a/ implements 'Preorder' we should have:
-- @ 'pcompareJoin' x y = 'pcompare' x y @
--
pcompareMeet :: Lattice a => a -> a -> Maybe Ordering
pcompareMeet x y
  | x == y = Just EQ
  | meetLe x y && x /= y = Just LT
  | meetGe x y && x /= y = Just GT
  | otherwise = Nothing

-- | \( \forall a \in R: a \/ a = a \)
--
-- @ 'idempotent_join' = 'absorbative' 'top' @
--
-- See < https:\\en.wikipedia.org/wiki/Band_(mathematics) >.
--
-- This is a required property.
--
idempotent_join :: Lattice r => r -> Bool
idempotent_join = idempotent_join_on (~~)

idempotent_join_on :: Semilattice 'L r => Rel r b -> r -> b
idempotent_join_on (~~) r = (\/) r r ~~ r

-- | \( \forall a, b, c \in R: (a \/ b) \/ c = a \/ (b \/ c) \)
--
-- This is a required property.
--
associative_join :: Lattice r => r -> r -> r -> Bool
associative_join = associative_on (~~) (\/)

associative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> r -> b
associative_join_on (=~) = associative_on (=~) (\/)

-- | \( \forall a, b, c: (a \# b) \# c \doteq a \# (b \# c) \)
--
associative_on :: Rel r b -> (r -> r -> r) -> (r -> r -> r -> b)
associative_on (~~) (#) a b c = ((a # b) # c) ~~ (a # (b # c))

-- | \( \forall a, b \in R: a \/ b = b \/ a \)
--
-- This is a required property.
--
commutative_join :: Lattice r => r -> r -> Bool
commutative_join = commutative_join_on (~~)

commutative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> b
commutative_join_on (=~) = commutative_on (=~) (\/)

-- | \( \forall a, b: a \# b \doteq b \# a \)
--
commutative_on :: Rel r b -> (r -> r -> r) -> r -> r -> b
commutative_on (=~) (#) a b = (a # b) =~ (b # a)

-- | \( \forall a, b \in R: a /\ b \/ b = b \)
--
-- Absorbativity is a generalized form of idempotency:
--
-- @
-- 'absorbative' 'top' a = a \/ a = a
-- @
--
-- This is a required property.
--
absorbative_on :: Lattice r => Rel r Bool -> r -> r -> Bool
absorbative_on (=~) x y = (x /\ y \/ y) =~ y

-- | \( \forall a, b \in R: a \/ b /\ b = b \)
--
-- Absorbativity is a generalized form of idempotency:
--
-- @
-- 'absorbative'' 'bottom' a = a \/ a = a
-- @
--
-- This is a required property.
--
absorbative_on' :: Lattice r => Rel r Bool -> r -> r -> Bool
absorbative_on' (=~) x y = ((x \/ y) /\ y) =~ y

distributive :: Lattice r => r -> r -> r -> Bool
distributive = distributive_on (~~) (/\) (\/)

codistributive :: Lattice r => r -> r -> r -> Bool
codistributive = distributive_on (~~) (\/) (/\)

distributive_on :: Rel r b -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> b)
distributive_on (=~) (#) (%) a b c = ((a # b) % c) =~ ((a % c) # (b % c))

distributive_on' :: Rel r b -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> b)
distributive_on' (=~) (#) (%) a b c = (c % (a # b)) =~ ((c % a) # (c % b))

-- | @ 'glb' x x y = x @
--
-- See < https:\\en.wikipedia.org/wiki/Median_algebra >.
majority_glb :: Lattice r => r -> r -> Bool
majority_glb x y = glb x y y ~~ y

-- | @ 'glb' x y z = 'glb' z x y @
--
commutative_glb :: Lattice r => r -> r -> r -> Bool
commutative_glb x y z = glb x y z ~~ glb z x y

-- | @ 'glb' x y z = 'glb' x z y @
--
commutative_glb' :: Lattice r => r -> r -> r -> Bool
commutative_glb' x y z = glb x y z ~~ glb x z y

-- | @ 'glb' ('glb' x w y) w z = 'glb' x w ('glb' y w z) @
--
associative_glb :: Lattice r => r -> r -> r -> r -> Bool
associative_glb x y z w = glb (glb x w y) w z ~~ glb x w (glb y w z)

distributive_glb :: (Bounded r, Lattice r) => r -> r -> r -> Bool
distributive_glb x y z = glb x y z ~~ lub x y z

interval_glb :: Lattice r => r -> r -> r -> Bool
interval_glb x y z = glb x y z ~~ y ==> (x <~ y && y <~ z) || (z <~ y && y <~ x)

-- |  \( \forall a, b, c: a \leq b \Rightarrow a \/ (c /\ b) \eq (a \/ c) /\ b \)
--
-- See < https:\\en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices >
--
modular :: Lattice r => r -> r -> r -> Bool
modular a b c = a \/ (c /\ b) ~~ (a \/ c) /\ b

-}