{-# Language AllowAmbiguousTypes #-}
module Data.Semilattice.Property (
monotone_join
, idempotent_join
, idempotent_join_on
, associative_join
, associative_join_on
, commutative_join
, commutative_join_on
, neutral_join
, neutral_join_on
, distributive_join
, monotone_meet
, idempotent_meet
, idempotent_meet_on
, associative_meet
, associative_meet_on
, commutative_meet
, commutative_meet_on
, neutral_meet
, neutral_meet_on
, distributive_meet
, absorbative
, absorbative'
, annihilative_join
, annihilative_meet
, distributive
, codistributive
, majority_glb
, commutative_glb
, commutative_glb'
, associative_glb
, morphism_join
, morphism_join_on
, morphism_join'
, morphism_join_on'
, morphism_meet
, morphism_meet_on
, morphism_meet'
, morphism_meet_on'
, morphism_distributive
) where
import Data.Prd hiding ((~~))
import Data.Semigroup
import Data.Semigroup.Join
import Data.Semigroup.Meet
import Data.Semilattice
import Test.Function as Prop
import Test.Logic (Rel, (==>))
import qualified Test.Operation as Prop
import Prelude hiding (Ord(..), Num(..), sum)
monotone_join :: JoinSemilattice r => r -> r -> r -> Bool
monotone_join x = Prop.monotone_on (<=) (<=) (∨ x)
idempotent_join :: JoinSemilattice r => r -> Bool
idempotent_join = idempotent_join_on (=~)
idempotent_join_on :: (Join-Semigroup) r => Rel r b -> r -> b
idempotent_join_on (~~) r = (∨) r r ~~ r
associative_join :: JoinSemilattice r => r -> r -> r -> Bool
associative_join = Prop.associative_on (=~) (∨)
associative_join_on :: (Join-Semigroup) r => Rel r b -> r -> r -> r -> b
associative_join_on (~~) = Prop.associative_on (~~) (∨)
commutative_join :: JoinSemilattice r => r -> r -> Bool
commutative_join = commutative_join_on (=~)
commutative_join_on :: (Join-Semigroup) r => Rel r b -> r -> r -> b
commutative_join_on (~~) = Prop.commutative_on (~~) (∨)
neutral_join :: BoundedJoinSemilattice r => r -> Bool
neutral_join = neutral_join_on (=~)
neutral_join_on :: (Join-Monoid) r => Rel r b -> r -> b
neutral_join_on (~~) = Prop.neutral_on (~~) (∨) bottom
distributive_join :: JoinSemilattice r => r -> r -> r -> r -> r -> Bool
distributive_join c a b a' b' = c <= a ∨ b ==> a' <= a && b' <= b && c <= a' ∨ b'
monotone_meet :: MeetSemilattice r => r -> r -> r -> Bool
monotone_meet x = Prop.monotone_on (<=) (<=) (∧ x)
associative_meet :: MeetSemilattice r => r -> r -> r -> Bool
associative_meet = associative_meet_on (=~)
associative_meet_on :: (Meet-Semigroup) r => Rel r b -> r -> r -> r -> b
associative_meet_on (~~) = Prop.associative_on (~~) (∧)
commutative_meet :: MeetSemilattice r => r -> r -> Bool
commutative_meet = commutative_meet_on (=~)
commutative_meet_on :: (Meet-Semigroup) r => Rel r b -> r -> r -> b
commutative_meet_on (~~) = Prop.commutative_on (~~) (∧)
idempotent_meet :: MeetSemilattice r => r -> Bool
idempotent_meet = idempotent_meet_on (=~)
idempotent_meet_on :: (Meet-Semigroup) r => Rel r b -> r -> b
idempotent_meet_on (~~) r = (∧) r r ~~ r
neutral_meet :: BoundedMeetSemilattice r => r -> Bool
neutral_meet = neutral_meet_on (=~)
neutral_meet_on :: (Meet-Monoid) r => Rel r b -> r -> b
neutral_meet_on (~~) = Prop.neutral_on (~~) (∧) top
distributive_meet :: MeetSemilattice r => r -> r -> r -> r -> r -> Bool
distributive_meet c a b a' b' = c >= a ∧ b ==> a' >= a && b' >= b && c >= a' ∧ b'
absorbative :: Lattice r => r -> r -> Bool
absorbative x y = (x ∧ y ∨ y) =~ y
absorbative' :: Lattice r => r -> r -> Bool
absorbative' x y = (x ∨ y ∧ y) =~ y
annihilative_join :: UpperBoundedLattice r => r -> Bool
annihilative_join r = Prop.annihilative_on (=~) (∨) top r
annihilative_meet :: LowerBoundedLattice r => r -> Bool
annihilative_meet r = Prop.annihilative_on (=~) (∧) bottom r
distributive :: Lattice r => r -> r -> r -> Bool
distributive = Prop.distributive_on (=~) (∧) (∨)
codistributive :: Lattice r => r -> r -> r -> Bool
codistributive = Prop.distributive_on' (=~) (∧) (∨)
majority_glb :: Lattice r => r -> r -> Bool
majority_glb x y = glb x y y =~ y
commutative_glb :: Lattice r => r -> r -> r -> Bool
commutative_glb x y z = 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 x z y
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)
morphism_join :: JoinSemilattice r => JoinSemilattice s => (r -> s) -> r -> r -> Bool
morphism_join = morphism_join_on (=~)
morphism_join_on :: (Join-Semigroup) r => (Join-Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b
morphism_join_on (~~) f x y = (f $ x ∨ y) ~~ (f x ∨ f y)
morphism_join' :: BoundedJoinSemilattice r => BoundedJoinSemilattice s => (r -> s) -> Bool
morphism_join' = morphism_join_on' (=~)
morphism_join_on' :: (Join-Monoid) r => (Join-Monoid) s => Rel s b -> (r -> s) -> b
morphism_join_on' (~~) f = (f bottom) ~~ bottom
morphism_meet :: MeetSemilattice r => MeetSemilattice s => (r -> s) -> r -> r -> Bool
morphism_meet = morphism_meet_on (=~)
morphism_meet_on :: (Meet-Semigroup) r => (Meet-Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b
morphism_meet_on (~~) f x y = (f $ x ∧ y) ~~ (f x ∧ f y)
morphism_meet' :: BoundedMeetSemilattice r => BoundedMeetSemilattice s => (r -> s) -> Bool
morphism_meet' = morphism_meet_on' (=~)
morphism_meet_on' :: (Meet-Monoid) r => (Meet-Monoid) s => Rel s b -> (r -> s) -> b
morphism_meet_on' (~~) f = (f top) ~~ top
morphism_distributive :: Prd r => Prd s => Lattice r => Lattice s => (r -> s) -> r -> r -> r -> Bool
morphism_distributive f x y z = f (glb x y z) =~ glb (f x) (f y) (f z)