module Algebra.Boolean.Properties where

import           Prelude hiding (not)

import           Algebra.Lattice (bottom, top, (/\), (\/))
import           Algebra.Boolean
import           Algebra.Heyting
import           Algebra.Heyting.CounterExample ( CounterExample
                                                , annotate
                                                , fmapCounterExample
                                                , (===)
                                                )
import           Algebra.Heyting.Properties

-- |
-- Test that @'not'@ satisfies Boolean algebra axioms.
prop_neg :: (Heyting a, Ord a, Eq a, Ord e) => a -> CounterExample e
prop_neg :: a -> CounterExample e
prop_neg a
a =
     (a -> a
forall a. Heyting a => a -> a
neg (a -> a
forall a. Heyting a => a -> a
neg a
a) a -> a -> CounterExample e
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
a)
  CounterExample e -> CounterExample e -> CounterExample e
forall a. Lattice a => a -> a -> a
/\ (a -> a
forall a. Heyting a => a -> a
neg a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
a a -> a -> CounterExample e
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
forall a. BoundedJoinSemiLattice a => a
bottom)
  CounterExample e -> CounterExample e -> CounterExample e
forall a. Lattice a => a -> a -> a
/\ (a -> a
forall a. Heyting a => a -> a
neg a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
a a -> a -> CounterExample e
forall e a. (Ord e, Eq a) => a -> a -> CounterExample e
=== a
forall a. BoundedMeetSemiLattice a => a
top)

prop_not :: (Heyting a, Ord a, Eq a, Ord e) => a -> CounterExample e
prop_not :: a -> CounterExample e
prop_not = a -> CounterExample e
forall a e.
(Heyting a, Ord a, Eq a, Ord e) =>
a -> CounterExample e
prop_neg

{-# DEPRECATED prop_not "Use prop_neg" #-}

data BooleanAlgebraLawViolation a
  = BALVHeytingAlgebraLawViolation (HeytingAlgebraLawViolation a)
  | BALVNotLawViolation a
  deriving (BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
(BooleanAlgebraLawViolation a
 -> BooleanAlgebraLawViolation a -> Bool)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> Bool)
-> Eq (BooleanAlgebraLawViolation a)
forall a.
Eq a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
$c/= :: forall a.
Eq a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
== :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
$c== :: forall a.
Eq a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
Eq, Eq (BooleanAlgebraLawViolation a)
Eq (BooleanAlgebraLawViolation a)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> Ordering)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> Bool)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> Bool)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> Bool)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> Bool)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a)
-> (BooleanAlgebraLawViolation a
    -> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a)
-> Ord (BooleanAlgebraLawViolation a)
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Ordering
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation 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 (BooleanAlgebraLawViolation a)
forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Ordering
forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a
min :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a
$cmin :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a
max :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a
$cmax :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> BooleanAlgebraLawViolation a
>= :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
$c>= :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
> :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
$c> :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
<= :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
$c<= :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
< :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
$c< :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Bool
compare :: BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Ordering
$ccompare :: forall a.
Ord a =>
BooleanAlgebraLawViolation a
-> BooleanAlgebraLawViolation a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (BooleanAlgebraLawViolation a)
Ord, Int -> BooleanAlgebraLawViolation a -> ShowS
[BooleanAlgebraLawViolation a] -> ShowS
BooleanAlgebraLawViolation a -> String
(Int -> BooleanAlgebraLawViolation a -> ShowS)
-> (BooleanAlgebraLawViolation a -> String)
-> ([BooleanAlgebraLawViolation a] -> ShowS)
-> Show (BooleanAlgebraLawViolation a)
forall a. Show a => Int -> BooleanAlgebraLawViolation a -> ShowS
forall a. Show a => [BooleanAlgebraLawViolation a] -> ShowS
forall a. Show a => BooleanAlgebraLawViolation a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BooleanAlgebraLawViolation a] -> ShowS
$cshowList :: forall a. Show a => [BooleanAlgebraLawViolation a] -> ShowS
show :: BooleanAlgebraLawViolation a -> String
$cshow :: forall a. Show a => BooleanAlgebraLawViolation a -> String
showsPrec :: Int -> BooleanAlgebraLawViolation a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> BooleanAlgebraLawViolation a -> ShowS
Show)

-- |
-- Test that @a@ is satisfy both @'Algebra.Heyting.prop_HeytingAlgebra'@ and
-- @'prop_not'@.
prop_BooleanAlgebra
  :: (Boolean a, Ord a, Eq a, Show a)
  => a -> a -> a -> CounterExample (BooleanAlgebraLawViolation a)
prop_BooleanAlgebra :: a -> a -> a -> CounterExample (BooleanAlgebraLawViolation a)
prop_BooleanAlgebra a
a a
b a
c =
     ((HeytingAlgebraLawViolation a -> BooleanAlgebraLawViolation a)
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (BooleanAlgebraLawViolation a)
forall a b.
(Ord a, Ord b) =>
(a -> b) -> CounterExample a -> CounterExample b
fmapCounterExample HeytingAlgebraLawViolation a -> BooleanAlgebraLawViolation a
forall a.
HeytingAlgebraLawViolation a -> BooleanAlgebraLawViolation a
BALVHeytingAlgebraLawViolation (CounterExample (HeytingAlgebraLawViolation a)
 -> CounterExample (BooleanAlgebraLawViolation a))
-> CounterExample (HeytingAlgebraLawViolation a)
-> CounterExample (BooleanAlgebraLawViolation a)
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
forall a.
(Heyting a, Ord a, Eq a, Show a) =>
a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_HeytingAlgebra a
a a
b a
c)
  CounterExample (BooleanAlgebraLawViolation a)
-> CounterExample (BooleanAlgebraLawViolation a)
-> CounterExample (BooleanAlgebraLawViolation a)
forall a. Lattice a => a -> a -> a
/\ BooleanAlgebraLawViolation a
-> CounterExample (BooleanAlgebraLawViolation a)
-> CounterExample (BooleanAlgebraLawViolation a)
forall e. Ord e => e -> CounterExample e -> CounterExample e
annotate (a -> BooleanAlgebraLawViolation a
forall a. a -> BooleanAlgebraLawViolation a
BALVNotLawViolation a
a) (a -> CounterExample (BooleanAlgebraLawViolation a)
forall a e.
(Heyting a, Ord a, Eq a, Ord e) =>
a -> CounterExample e
prop_not a
a)