{-# LANGUAGE TupleSections #-}
-- |
-- Properties of Heyting algebras; useful for testing lawfulness of instances.
--
module Algebra.Heyting.Properties where

import           Prelude

import           Data.List (intersperse)

import           Algebra.Lattice ( Lattice
                                 , BoundedJoinSemiLattice
                                 , BoundedMeetSemiLattice
                                 , Meet (..)
                                 , Join (..)
                                 , top
                                 , bottom
                                 , (/\)
                                 , (\/)
                                 )
import           Algebra.PartialOrd (leq)
import           Algebra.Heyting
import           Algebra.Heyting.CounterExample

data BoundedMeetSemiLatticeLawViolation a
  = BMSLVNonAssociative a a a
  | BMSLVNonCommutative a a
  | BMSLVNonIdempotent a
  | BMSLVNonUnital a
  | BMSLVMeetOrderViolation a a
  deriving (BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
(BoundedMeetSemiLatticeLawViolation a
 -> BoundedMeetSemiLatticeLawViolation a -> Bool)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a -> Bool)
-> Eq (BoundedMeetSemiLatticeLawViolation a)
forall a.
Eq a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
$c/= :: forall a.
Eq a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
== :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
$c== :: forall a.
Eq a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
Eq, Eq (BoundedMeetSemiLatticeLawViolation a)
Eq (BoundedMeetSemiLatticeLawViolation a)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a -> Ordering)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a -> Bool)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a -> Bool)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a -> Bool)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a -> Bool)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a)
-> (BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a
    -> BoundedMeetSemiLatticeLawViolation a)
-> Ord (BoundedMeetSemiLatticeLawViolation a)
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Ordering
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (BoundedMeetSemiLatticeLawViolation a)
forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Ordering
forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
min :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
$cmin :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
max :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
$cmax :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a
>= :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
$c>= :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
> :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
$c> :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
<= :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
$c<= :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
< :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
$c< :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Bool
compare :: BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Ordering
$ccompare :: forall a.
Ord a =>
BoundedMeetSemiLatticeLawViolation a
-> BoundedMeetSemiLatticeLawViolation a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (BoundedMeetSemiLatticeLawViolation a)
Ord)

instance Show a => Show (BoundedMeetSemiLatticeLawViolation a) where
  show :: BoundedMeetSemiLatticeLawViolation a -> String
show (BMSLVNonAssociative a
a a
b a
c) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∧ (b ∧ c) ≠ (a ∧ b) ∧ c" [a
a, a
b, a
c]
  show (BMSLVNonCommutative a
a a
b) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∧ b ٍ≠ b ∧ a" [a
a, a
b]
  show (BMSLVNonIdempotent a
a) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∧ a ≠ a" [a
a]
  show (BMSLVNonUnital a
a) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∧ top ≠ a" [a
a]
  show (BMSLVMeetOrderViolation a
a a
b) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∧ b > a" [a
a, a
b]

withArgs :: Show a => String -> [a] -> String
withArgs :: String -> [a] -> String
withArgs String
s [a]
bs = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> ShowS) -> String -> [String] -> String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> ShowS
forall a. Semigroup a => a -> a -> a
(<>) String
forall a. Monoid a => a
mempty (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"\n\t" ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
bs))

-- |
-- Verifies bounded meet semilattice laws.
prop_BoundedMeetSemiLattice
  :: (BoundedMeetSemiLattice a, Ord a, Eq a, Show a)
  => a -> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
prop_BoundedMeetSemiLattice :: a
-> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
prop_BoundedMeetSemiLattice a
a a
b a
c =
  BoundedMeetSemiLatticeLawViolation a
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> a -> BoundedMeetSemiLatticeLawViolation a
forall a. a -> a -> a -> BoundedMeetSemiLatticeLawViolation a
BMSLVNonAssociative a
a a
b a
c) ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ (a
b a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
c)) a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b) a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
c))
  CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedMeetSemiLatticeLawViolation a
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> BoundedMeetSemiLatticeLawViolation a
forall a. a -> a -> BoundedMeetSemiLatticeLawViolation a
BMSLVNonCommutative a
a a
b) ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b) a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== (a
b a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a))
  CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedMeetSemiLatticeLawViolation a
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> BoundedMeetSemiLatticeLawViolation a
forall a. a -> BoundedMeetSemiLatticeLawViolation a
BMSLVNonIdempotent a
a) ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a) a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
a)
  CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedMeetSemiLatticeLawViolation a
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> BoundedMeetSemiLatticeLawViolation a
forall a. a -> BoundedMeetSemiLatticeLawViolation a
BMSLVNonUnital a
a) ((a
forall a. BoundedMeetSemiLattice a => a
top a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a) a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
a)
  CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedMeetSemiLatticeLawViolation a
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> BoundedMeetSemiLatticeLawViolation a
forall a. a -> a -> BoundedMeetSemiLatticeLawViolation a
BMSLVMeetOrderViolation a
a a
b) ((a -> Meet a
forall a. a -> Meet a
Meet (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b) Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet a
a) Bool
-> Bool -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== Bool
True)

data BoundedJoinSemiLatticeLawViolation a
  = BJSLVNonAssociative a a a
  | BJSLVNonCommutative a a
  | BJSLVNonIdempotent a
  | BJSLVNonUnital a
  | BJSLVJoinOrderViolation a a
  deriving (BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
(BoundedJoinSemiLatticeLawViolation a
 -> BoundedJoinSemiLatticeLawViolation a -> Bool)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a -> Bool)
-> Eq (BoundedJoinSemiLatticeLawViolation a)
forall a.
Eq a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
$c/= :: forall a.
Eq a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
== :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
$c== :: forall a.
Eq a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
Eq, Eq (BoundedJoinSemiLatticeLawViolation a)
Eq (BoundedJoinSemiLatticeLawViolation a)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a -> Ordering)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a -> Bool)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a -> Bool)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a -> Bool)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a -> Bool)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a)
-> (BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a
    -> BoundedJoinSemiLatticeLawViolation a)
-> Ord (BoundedJoinSemiLatticeLawViolation a)
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Ordering
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (BoundedJoinSemiLatticeLawViolation a)
forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Ordering
forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
min :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
$cmin :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
max :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
$cmax :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a
>= :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
$c>= :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
> :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
$c> :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
<= :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
$c<= :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
< :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
$c< :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Bool
compare :: BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Ordering
$ccompare :: forall a.
Ord a =>
BoundedJoinSemiLatticeLawViolation a
-> BoundedJoinSemiLatticeLawViolation a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (BoundedJoinSemiLatticeLawViolation a)
Ord)

instance Show a => Show (BoundedJoinSemiLatticeLawViolation a) where
  show :: BoundedJoinSemiLatticeLawViolation a -> String
show (BJSLVNonAssociative a
a a
b a
c) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∨ (b ∨ c) ≠ (a ∨ b) ∨ c" [a
a, a
b, a
c]
  show (BJSLVNonCommutative a
a a
b) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∨ b ٍ≠ b ∨ a" [a
a, a
b]
  show (BJSLVNonIdempotent a
a) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∨ a ≠ a" [a
a]
  show (BJSLVNonUnital a
a) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∨ top ≠ a" [a
a]
  show (BJSLVJoinOrderViolation a
a a
b) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∨ b > a" [a
a, a
b]

-- |
-- Verifies bounded join semilattice laws.
prop_BoundedJoinSemiLattice
  :: (BoundedJoinSemiLattice a, Ord a, Eq a, Show a)
  => a -> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
prop_BoundedJoinSemiLattice :: a
-> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
prop_BoundedJoinSemiLattice a
a a
b a
c =
     BoundedJoinSemiLatticeLawViolation a
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> a -> BoundedJoinSemiLatticeLawViolation a
forall a. a -> a -> a -> BoundedJoinSemiLatticeLawViolation a
BJSLVNonAssociative a
a a
b a
c)
        ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ (a
b a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
c)) a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b) a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
c))
  CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedJoinSemiLatticeLawViolation a
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> BoundedJoinSemiLatticeLawViolation a
forall a. a -> a -> BoundedJoinSemiLatticeLawViolation a
BJSLVNonCommutative a
a a
b)
        ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b) a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== (a
b a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
a))
  CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedJoinSemiLatticeLawViolation a
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> BoundedJoinSemiLatticeLawViolation a
forall a. a -> BoundedJoinSemiLatticeLawViolation a
BJSLVNonIdempotent a
a)
        ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
a) a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
a)
  CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedJoinSemiLatticeLawViolation a
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> BoundedJoinSemiLatticeLawViolation a
forall a. a -> BoundedJoinSemiLatticeLawViolation a
BJSLVNonUnital a
a)
        ((a
forall a. BoundedJoinSemiLattice a => a
bottom a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
a) a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
a)
  CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BoundedJoinSemiLatticeLawViolation a
-> Bool -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall e. Ord e => e -> Bool -> CounterExample e
fromBool (a -> a -> BoundedJoinSemiLatticeLawViolation a
forall a. a -> a -> BoundedJoinSemiLatticeLawViolation a
BJSLVJoinOrderViolation a
a a
b)
        (a -> Join a
forall a. a -> Join a
Join a
a Join a -> Join a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Join a
forall a. a -> Join a
Join (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b))

data DistributiveLatticeLawViolation a
  = DLLVJoinOverMeetViolation a a a
  | DLLVMeetOverJoinViolation a a a
  deriving (DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
(DistributiveLatticeLawViolation a
 -> DistributiveLatticeLawViolation a -> Bool)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a -> Bool)
-> Eq (DistributiveLatticeLawViolation a)
forall a.
Eq a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
$c/= :: forall a.
Eq a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
== :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
$c== :: forall a.
Eq a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
Eq, Eq (DistributiveLatticeLawViolation a)
Eq (DistributiveLatticeLawViolation a)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a -> Ordering)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a -> Bool)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a -> Bool)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a -> Bool)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a -> Bool)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a)
-> (DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a
    -> DistributiveLatticeLawViolation a)
-> Ord (DistributiveLatticeLawViolation a)
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Ordering
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (DistributiveLatticeLawViolation a)
forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Ordering
forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
min :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
$cmin :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
max :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
$cmax :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a
>= :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
$c>= :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
> :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
$c> :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
<= :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
$c<= :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
< :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
$c< :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Bool
compare :: DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Ordering
$ccompare :: forall a.
Ord a =>
DistributiveLatticeLawViolation a
-> DistributiveLatticeLawViolation a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (DistributiveLatticeLawViolation a)
Ord)

instance Show a => Show (DistributiveLatticeLawViolation a) where
  show :: DistributiveLatticeLawViolation a -> String
show (DLLVJoinOverMeetViolation a
a a
b a
c) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∧ (b ∨ c) ≠ a ∧ b ∨ a ∧ c" [a
a, a
b, a
c]
  show (DLLVMeetOverJoinViolation a
a a
b a
c) = String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ∨ (b ∧ c) ≠ (a ∨ b) ∧ (a ∨ c)" [a
a, a
b, a
c]

-- |
-- Distributivity laws for a lattice.
prop_DistributiveLattice
  :: (Lattice a, Ord a, Eq a, Show a)
  => a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a)
prop_DistributiveLattice :: a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a)
prop_DistributiveLattice a
a a
b a
c =
     DistributiveLatticeLawViolation a
-> CounterExample (DistributiveLatticeLawViolation a)
-> CounterExample (DistributiveLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> a -> DistributiveLatticeLawViolation a
forall a. a -> a -> a -> DistributiveLatticeLawViolation a
DLLVJoinOverMeetViolation a
a a
b a
c)
      ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ (a
b a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
c)) a -> a -> CounterExample (DistributiveLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b) a -> a -> a
forall a. Lattice a => a -> a -> a
\/ (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
c)))
  CounterExample (DistributiveLatticeLawViolation a)
-> CounterExample (DistributiveLatticeLawViolation a)
-> CounterExample (DistributiveLatticeLawViolation a)
forall a. Lattice a => a -> a -> a
/\ DistributiveLatticeLawViolation a
-> CounterExample (DistributiveLatticeLawViolation a)
-> CounterExample (DistributiveLatticeLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> a -> a -> DistributiveLatticeLawViolation a
forall a. a -> a -> a -> DistributiveLatticeLawViolation a
DLLVMeetOverJoinViolation a
a a
b a
c)
      ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ (a
b a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
c)) a -> a -> CounterExample (DistributiveLatticeLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== ((a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b) a -> a -> a
forall a. Lattice a => a -> a -> a
/\ (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
c)))

data HeytingAlgebraLawViolation a
  = HAVImplication1 a a a
  | HAVImplication2 a a a
  | HAVNot a a
  | HAVNotAndMeet a a
  | HAVNotAndJoin a a
  | HAVImplicationAndOrd a a
  | HAVDistributiveLatticeLawViolation (DistributiveLatticeLawViolation a)
  | HAVBoundedJoinSemilatticeLawViolation (BoundedJoinSemiLatticeLawViolation a)
  | HAVBoundedMeetSemilatticeLawViolation (BoundedMeetSemiLatticeLawViolation a)
  deriving (HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
(HeytingAlgebraLawViolation a
 -> HeytingAlgebraLawViolation a -> Bool)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> Bool)
-> Eq (HeytingAlgebraLawViolation a)
forall a.
Eq a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
$c/= :: forall a.
Eq a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
== :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
$c== :: forall a.
Eq a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
Eq, Eq (HeytingAlgebraLawViolation a)
Eq (HeytingAlgebraLawViolation a)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> Ordering)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> Bool)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> Bool)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> Bool)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> Bool)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a)
-> (HeytingAlgebraLawViolation a
    -> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a)
-> Ord (HeytingAlgebraLawViolation a)
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Ordering
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (HeytingAlgebraLawViolation a)
forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Ordering
forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a
min :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a
$cmin :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a
max :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a
$cmax :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a
>= :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
$c>= :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
> :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
$c> :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
<= :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
$c<= :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
< :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
$c< :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Bool
compare :: HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Ordering
$ccompare :: forall a.
Ord a =>
HeytingAlgebraLawViolation a
-> HeytingAlgebraLawViolation a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (HeytingAlgebraLawViolation a)
Ord)

instance Show a => Show (HeytingAlgebraLawViolation a) where
  show :: HeytingAlgebraLawViolation a -> String
show (HAVImplication1 a
x a
a a
b)=
    String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"x ≤ (a ⇒ b) then x ∧ a ≤ b" [a
x, a
a, a
b]

  show (HAVImplication2 a
x a
a a
b) =
      String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"x ∧ a ≤ b then x ≤ (a ⇒ b)" [a
x, a
a, a
b]

  show (HAVNot a
a a
b) =
    String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"a ≤ b ⇏ neg a" [a
a, a
b]

  show (HAVNotAndMeet a
a a
b) =
    String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"neg (a ∧ b) ≠ neg a ∨ neg b" [a
a, a
b]

  show (HAVNotAndJoin a
a a
b) =
    String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"neg (a ∨ b) ≠ neg a ∧ neg b" [a
a, a
b]

  show (HAVImplicationAndOrd a
a a
b) =
    String -> [a] -> String
forall a. Show a => String -> [a] -> String
withArgs String
"(a ⇒ b) ∧ a ≰ b" [a
a, a
b]

  show (HAVDistributiveLatticeLawViolation DistributiveLatticeLawViolation a
e)    = DistributiveLatticeLawViolation a -> String
forall a. Show a => a -> String
show DistributiveLatticeLawViolation a
e
  show (HAVBoundedJoinSemilatticeLawViolation BoundedJoinSemiLatticeLawViolation a
e) = BoundedJoinSemiLatticeLawViolation a -> String
forall a. Show a => a -> String
show BoundedJoinSemiLatticeLawViolation a
e
  show (HAVBoundedMeetSemilatticeLawViolation BoundedMeetSemiLatticeLawViolation a
e) = BoundedMeetSemiLatticeLawViolation a -> String
forall a. Show a => a -> String
show BoundedMeetSemiLatticeLawViolation a
e

-- |
-- Verifies the Heyting algebra law for @==>@:
-- for all @a@: @_ /\ a@ is left adjoint to  @a ==>@
-- and some other properties that are a consequence of that.
prop_implies :: (Heyting a, Ord a, Eq a, Show a)
             => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_implies :: a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_implies a
x a
a a
b =
    HeytingAlgebraLawViolation a
-> Bool -> CounterExample (HeytingAlgebraLawViolation a)
forall e. Ord e => e -> Bool -> CounterExample e
fromBool
      (a -> a -> a -> HeytingAlgebraLawViolation a
forall a. a -> a -> a -> HeytingAlgebraLawViolation a
HAVImplication1 a
x a
a a
b)
      (a -> Meet a
forall a. a -> Meet a
Meet a
x Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b) Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
==> (a -> Meet a
forall a. a -> Meet a
Meet (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a) Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet a
b))
  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ HeytingAlgebraLawViolation a
-> Bool -> CounterExample (HeytingAlgebraLawViolation a)
forall e. Ord e => e -> Bool -> CounterExample e
fromBool
      (a -> a -> a -> HeytingAlgebraLawViolation a
forall a. a -> a -> a -> HeytingAlgebraLawViolation a
HAVImplication2 a
x a
a a
b)
      (a -> Meet a
forall a. a -> Meet a
Meet (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a) Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet a
b Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
==> (a -> Meet a
forall a. a -> Meet a
Meet a
x Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)))
  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ HeytingAlgebraLawViolation a
-> Bool -> CounterExample (HeytingAlgebraLawViolation a)
forall e. Ord e => e -> Bool -> CounterExample e
fromBool
      (a -> a -> HeytingAlgebraLawViolation a
forall a. a -> a -> HeytingAlgebraLawViolation a
HAVNot a
a a
b)
      (a -> Meet a
forall a. a -> Meet a
Meet a
a Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet a
b Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
==> (a -> Meet a
forall a. a -> Meet a
Meet (a -> a
forall a. Heyting a => a -> a
neg a
b) Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet (a -> a
forall a. Heyting a => a -> a
neg a
a)))
  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ HeytingAlgebraLawViolation a
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate
      (a -> a -> HeytingAlgebraLawViolation a
forall a. a -> a -> HeytingAlgebraLawViolation a
HAVNotAndMeet a
a a
b)
      (a -> a
forall a. Heyting a => a -> a
neg (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b) a -> a -> CounterExample (HeytingAlgebraLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== (a -> a
forall a. Heyting a => a -> a
neg a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a -> a
forall a. Heyting a => a -> a
neg a
b))
  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ HeytingAlgebraLawViolation a
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate
      (a -> a -> HeytingAlgebraLawViolation a
forall a. a -> a -> HeytingAlgebraLawViolation a
HAVNotAndJoin a
a a
b)
      (a -> a
forall a. Heyting a => a -> a
neg (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b) a -> a -> CounterExample (HeytingAlgebraLawViolation a)
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== (a -> a
forall a. Heyting a => a -> a
neg a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a -> a
forall a. Heyting a => a -> a
neg a
b))
  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ HeytingAlgebraLawViolation a
-> Bool -> CounterExample (HeytingAlgebraLawViolation a)
forall e. Ord e => e -> Bool -> CounterExample e
fromBool
      (a -> a -> HeytingAlgebraLawViolation a
forall a. a -> a -> HeytingAlgebraLawViolation a
HAVImplicationAndOrd a
a a
a)
      (a -> Meet a
forall a. a -> Meet a
Meet ((a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b) a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a) Meet a -> Meet a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a -> Meet a
forall a. a -> Meet a
Meet a
b)

-- |
-- Useful for testing valid instances of @'Heyting'@ type class. It
-- validates:
--
-- * bounded lattice laws
-- * @'prop_implies'@
prop_HeytingAlgebra
  :: (Heyting a, Ord a, Eq a, Show a)
  => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_HeytingAlgebra :: a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_HeytingAlgebra a
a a
b a
c =

     (BoundedJoinSemiLatticeLawViolation a
 -> HeytingAlgebraLawViolation a)
-> CounterExample (BoundedJoinSemiLatticeLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a b.
(Ord a, Ord b) =>
(a -> b) -> CounterExample a -> CounterExample b
fmapCounterExample BoundedJoinSemiLatticeLawViolation a
-> HeytingAlgebraLawViolation a
forall a.
BoundedJoinSemiLatticeLawViolation a
-> HeytingAlgebraLawViolation a
HAVBoundedJoinSemilatticeLawViolation
        (a
-> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
forall a.
(BoundedJoinSemiLattice a, Ord a, Eq a, Show a) =>
a
-> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
prop_BoundedJoinSemiLattice a
a a
b a
c)

  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ (BoundedMeetSemiLatticeLawViolation a
 -> HeytingAlgebraLawViolation a)
-> CounterExample (BoundedMeetSemiLatticeLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a b.
(Ord a, Ord b) =>
(a -> b) -> CounterExample a -> CounterExample b
fmapCounterExample BoundedMeetSemiLatticeLawViolation a
-> HeytingAlgebraLawViolation a
forall a.
BoundedMeetSemiLatticeLawViolation a
-> HeytingAlgebraLawViolation a
HAVBoundedMeetSemilatticeLawViolation
        (a
-> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
forall a.
(BoundedMeetSemiLattice a, Ord a, Eq a, Show a) =>
a
-> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
prop_BoundedMeetSemiLattice a
a a
b a
c)

  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ (DistributiveLatticeLawViolation a -> HeytingAlgebraLawViolation a)
-> CounterExample (DistributiveLatticeLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a b.
(Ord a, Ord b) =>
(a -> b) -> CounterExample a -> CounterExample b
fmapCounterExample DistributiveLatticeLawViolation a -> HeytingAlgebraLawViolation a
forall a.
DistributiveLatticeLawViolation a -> HeytingAlgebraLawViolation a
HAVDistributiveLatticeLawViolation
        (a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a)
forall a.
(Lattice a, Ord a, Eq a, Show a) =>
a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a)
prop_DistributiveLattice a
a a
b a
c)

  CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
forall a.
(Heyting a, Ord a, Eq a, Show a) =>
a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_implies a
a a
b a
c