{-# 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 :: a -> a -> a -> Bool
coheyting0 a
x a
y a
z = a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
z Bool -> Bool -> Bool
<=> a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
y a -> a -> a
forall a. Join a => a -> a -> a
\/ a
z

coheyting1 :: Coheyting a => a -> a -> a -> Bool
coheyting1 :: a -> a -> a -> Bool
coheyting1 a
x a
y a
z = a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
z) a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y

coheyting2 :: Coheyting a => a -> a -> a -> Bool
coheyting2 :: a -> a -> a -> Bool
coheyting2 a
x a
y a
z = a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ (a
y a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
z) a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y

coheyting3 :: Coheyting a => a -> a -> a -> Bool
coheyting3 :: a -> a -> a -> Bool
coheyting3 a
x a
y a
z = a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a
y Bool -> Bool -> Bool
==> a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
z a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
z

coheyting4 :: Coheyting a => a -> a -> a -> Bool
coheyting4 :: a -> a -> a -> Bool
coheyting4 a
x a
y a
z = a
z a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
z a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y

coheyting5 :: Coheyting a => a -> a -> a -> Bool
coheyting5 :: a -> a -> a -> Bool
coheyting5 a
x a
y a
z = (a
y a -> a -> a
forall a. Join a => a -> a -> a
\/ a
z) a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
z a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x

coheyting6 :: Coheyting a => a -> a -> Bool
coheyting6 :: a -> a -> Bool
coheyting6 a
x a
y = a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y

coheyting7 :: Coheyting a => a -> a -> Bool
coheyting7 :: a -> a -> Bool
coheyting7 a
x a
y = a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y

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

-- Double co-negation is a co-monad.
coheyting9 :: Coheyting a => a -> a -> Bool
coheyting9 :: a -> a -> Bool
coheyting9 a
x a
y = a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Coheyting a => a -> a
non a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y

coheyting10 :: Coheyting a => a -> a -> Bool
coheyting10 :: a -> a -> Bool
coheyting10 a
x a
y = a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a
y Bool -> Bool -> Bool
<=> a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Join a => a
bottom

coheyting11 :: Coheyting a => a -> a -> Bool
coheyting11 :: a -> a -> Bool
coheyting11 a
x a
y = a -> a
forall a. Coheyting a => a -> a
non (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Order a => a -> a -> Bool
>= a -> a
forall a. Coheyting a => a -> a
non a
x

coheyting12 :: Coheyting a => a -> a -> Bool
coheyting12 :: a -> a -> Bool
coheyting12 a
x a
y = a -> a
forall a. Coheyting a => a -> a
non (a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Coheyting a => a -> a
non (a -> a
forall a. Coheyting a => a -> a
non a
x) a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Coheyting a => a -> a
non a
y

coheyting13 :: Coheyting a => a -> a -> Bool
coheyting13 :: a -> a -> Bool
coheyting13 a
x a
y = a -> a
forall a. Coheyting a => a -> a
non (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Coheyting a => a -> a
non a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Coheyting a => a -> a
non a
y

coheyting14 :: Coheyting a => a -> Bool
coheyting14 :: a -> Bool
coheyting14 a
x = a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Coheyting a => a -> a
non a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Meet a => a
top

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

coheyting16 :: Coheyting a => a -> Bool
coheyting16 :: a -> Bool
coheyting16 a
x = a -> a
forall a. Coheyting a => a -> a
non (a -> a
forall a. Coheyting a => a -> a
non (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Coheyting a => a -> a
non a
x)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Join a => a
bottom

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

coheyting18 :: Coheyting c => c -> Bool
coheyting18 :: c -> Bool
coheyting18 c
x = c
x c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c -> c
forall a. Coheyting a => a -> a
boundary c
x c -> c -> c
forall a. Join a => a -> a -> a
\/ (c -> c
forall a. Coheyting a => a -> a
non (c -> c) -> (c -> c) -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> c
forall a. Coheyting a => a -> a
non) c
x

coheyting19 :: Coheyting a => a -> a -> Bool
coheyting19 :: a -> a -> Bool
coheyting19 a
x a
y = a -> a
forall a. Coheyting a => a -> a
boundary (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Coheyting a => a -> a
boundary a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> a
forall a. Join a => a -> a -> a
\/ (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Coheyting a => a -> a
boundary a
y) -- (Leibniz rule)

coheyting20 :: Coheyting a => a -> a -> Bool
coheyting20 :: a -> a -> Bool
coheyting20 a
x a
y = a -> a
forall a. Coheyting a => a -> a
boundary (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Coheyting a => a -> a
boundary (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Coheyting a => a -> a
boundary a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Coheyting a => a -> a
boundary a
y

heyting0 :: Heyting a => a -> a -> a -> Bool
heyting0 :: a -> a -> a -> Bool
heyting0 a
x a
y a
z = a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
z Bool -> Bool -> Bool
<=> a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
y a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
z

heyting1 :: Heyting a => a -> a -> a -> Bool
heyting1 :: a -> a -> a -> Bool
heyting1 a
x a
y a
z = a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// (a
y a -> a -> a
forall a. Join a => a -> a -> a
\/ a
z)

heyting2 :: Heyting a => a -> a -> a -> Bool
heyting2 :: a -> a -> a -> Bool
heyting2 a
x a
y a
z = (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
z) a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y

heyting3 :: Heyting a => a -> a -> a -> Bool
heyting3 :: a -> a -> a -> Bool
heyting3 a
x a
y a
z = a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
y Bool -> Bool -> Bool
==> a
z a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
z a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y

heyting4 :: Heyting a => a -> a -> a -> Bool
heyting4 :: a -> a -> a -> Bool
heyting4 a
x a
y a
z = (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
z a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
z

heyting5 :: Heyting a => a -> a -> a -> Bool
heyting5 :: a -> a -> a -> Bool
heyting5 a
x a
y a
z = a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// (a
y a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
z) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
z

heyting6 :: Heyting a => a -> a -> Bool
heyting6 :: a -> a -> Bool
heyting6 a
x a
y = a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y)

heyting7 :: Heyting a => a -> a -> Bool
heyting7 :: a -> a -> Bool
heyting7 a
x a
y = a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y

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

-- Double negation is a monad.
heyting9 :: Heyting a => a -> a -> Bool
heyting9 :: a -> a -> Bool
heyting9 a
x a
y = a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y

heyting10 :: Heyting a => a -> a -> Bool
heyting10 :: a -> a -> Bool
heyting10 a
x a
y = a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
y Bool -> Bool -> Bool
<=> a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Meet a => a
top

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

heyting12 :: Heyting a => a -> a -> Bool
heyting12 :: a -> a -> Bool
heyting12 a
x a
y = a -> a
forall a. Heyting a => a -> a
neg (a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Heyting a => a -> a
neg (a -> a
forall a. Heyting a => a -> a
neg a
x) a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Heyting a => a -> a
neg a
y

heyting13 :: Heyting a => a -> a -> Bool
heyting13 :: a -> a -> Bool
heyting13 a
x a
y = a -> a
forall a. Heyting a => a -> a
neg (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Heyting a => a -> a
neg a
y

heyting14 :: Heyting a => a -> Bool
heyting14 :: a -> Bool
heyting14 a
x = a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Join a => a
bottom

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

heyting16 :: Heyting a => a -> Bool
heyting16 :: a -> Bool
heyting16 a
x = a -> a
forall a. Heyting a => a -> a
neg (a -> a
forall a. Heyting a => a -> a
neg (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Heyting a => a -> a
neg a
x)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Meet a => a
top

heyting17 :: Heyting a => a -> Bool
heyting17 :: a -> Bool
heyting17 a
x = a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a -> a
forall a. Heyting a => a -> a
neg (a -> a
forall a. Heyting a => a -> a
neg a
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 :: a -> Bool
symmetric1 a
x = a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a -> a
forall a. Coheyting a => a -> a
non a
x

symmetric2 :: Symmetric a => a -> Bool
symmetric2 :: a -> Bool
symmetric2 a
x = (a -> a
forall a. Heyting a => a -> a
neg (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Heyting a => a -> a
neg) a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Symmetric a => a -> a
converseR (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
converseL) a
x

symmetric3 :: Symmetric a => a -> Bool
symmetric3 :: a -> Bool
symmetric3 a
x = (a -> a
forall a. Coheyting a => a -> a
non (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Coheyting a => a -> a
non) a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Symmetric a => a -> a
converseL (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
converseR) a
x

symmetric4 :: Symmetric a => a -> Bool
symmetric4 :: a -> Bool
symmetric4 a
x = a -> a
forall a. Coheyting a => a -> a
non a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Symmetric a => a -> a
converseL (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
not) a
x Bool -> Bool -> Bool
&& a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Symmetric a => a -> a
not (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
converseL) a
x

symmetric5 :: Symmetric a => a -> Bool
symmetric5 :: a -> Bool
symmetric5 a
x = a -> a
forall a. Coheyting a => a -> a
non a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Symmetric a => a -> a
not (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
converseR) a
x Bool -> Bool -> Bool
&& a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Symmetric a => a -> a
converseR (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
not) a
x

symmetric6 :: Heyting a => a -> Bool
symmetric6 :: a -> Bool
symmetric6 a
x = a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Heyting a => a -> a
neg (a -> a
forall a. Heyting a => a -> a
neg a
x) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Meet a => a
top

symmetric7 :: Symmetric a => a -> a -> Bool
symmetric7 :: a -> a -> Bool
symmetric7 a
x a
y = a -> a
forall a. Symmetric a => a -> a
not (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Symmetric a => a -> a
not a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Symmetric a => a -> a
not a
y

symmetric8 :: Symmetric a => a -> a -> Bool
symmetric8 :: a -> a -> Bool
symmetric8 a
x a
y = (a -> a
forall a. Symmetric a => a -> a
not (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
not) (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Symmetric a => a -> a
not (a -> a
forall a. Symmetric a => a -> a
not a
x) a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Symmetric a => a -> a
not (a -> a
forall a. Symmetric a => a -> a
not a
y)

symmetric9 :: Symmetric a => a -> a -> Bool
symmetric9 :: a -> a -> Bool
symmetric9 a
x a
y = a -> a
forall a. Symmetric a => a -> a
not (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Symmetric a => a -> a
not a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Symmetric a => a -> a
not a
y

symmetric10 :: Symmetric a => a -> a -> Bool
symmetric10 :: a -> a -> Bool
symmetric10 a
x a
y = a -> a
forall a. Symmetric a => a -> a
converseL (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Symmetric a => a -> a
converseL a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Symmetric a => a -> a
converseL a
y

symmetric11 :: Symmetric a => a -> a -> Bool
symmetric11 :: a -> a -> Bool
symmetric11 a
x a
y = a -> a
forall a. Symmetric a => a -> a
converseR (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Symmetric a => a -> a
converseR a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Symmetric a => a -> a
converseR a
y

symmetric12 :: Symmetric a => a -> a -> Bool
symmetric12 :: a -> a -> Bool
symmetric12 a
x a
y = a -> a
forall a. Symmetric a => a -> a
converseL (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Coheyting a => a -> a
non (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Coheyting a => a -> a
non) (a -> a
forall a. Symmetric a => a -> a
converseL a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Symmetric a => a -> a
converseL a
y)

symmetric13 :: Symmetric a => a -> a -> Bool
symmetric13 :: a -> a -> Bool
symmetric13 a
x a
y = a -> a
forall a. Symmetric a => a -> a
converseR (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a. Heyting a => a -> a
neg (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Heyting a => a -> a
neg) (a -> a
forall a. Symmetric a => a -> a
converseR a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Symmetric a => a -> a
converseR a
y)

boolean0 :: Biheyting a => a -> Bool
boolean0 :: a -> Bool
boolean0 a
x = a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Coheyting a => a -> a
non a
x

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

boolean2 :: Heyting a => a -> Bool
boolean2 :: a -> Bool
boolean2 a
x = a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Heyting a => a -> a
neg a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Meet a => a
top

boolean3 :: Coheyting a => a -> Bool
boolean3 :: a -> Bool
boolean3 a
x = a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Coheyting a => a -> a
non a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Join a => a
bottom

boolean4 :: Heyting a => a -> a -> Bool
boolean4 :: a -> a -> Bool
boolean4 a
x a
y = (a
x a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a
y) Bool -> Bool -> Bool
forall a. Algebra 'R a => a -> a -> a
// (a -> a
forall a. Heyting a => a -> a
neg a
y a -> a -> Bool
forall a. Order a => a -> a -> Bool
<= a -> a
forall a. Heyting a => a -> a
neg a
x)

boolean5 :: Biheyting a => a -> a -> Bool
boolean5 :: a -> a -> Bool
boolean5 a
x a
y = a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Heyting a => a -> a
neg (a -> a
forall a. Heyting a => a -> a
neg a
y a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a -> a
forall a. Heyting a => a -> a
neg a
x)

boolean6 :: Biheyting a => a -> a -> Bool
boolean6 :: a -> a -> Bool
boolean6 a
x a
y = a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Coheyting a => a -> a
non (a -> a
forall a. Coheyting a => a -> a
non a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a -> a
forall a. Coheyting a => a -> a
non a
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

-}