{-# LANGUAGE TupleSections #-} -- | -- Properties of Heyting algebras; useful for testing lawfulness of instances. -- module Algebra.Heyting.Properties where import Prelude hiding (not) import Data.List (intersperse) import Data.Semigroup ((<>)) 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 (Eq, Ord) instance Show a => Show (BoundedMeetSemiLatticeLawViolation a) where show (BMSLVNonAssociative a b c) = withArgs "a ∧ (b ∧ c) ≠ (a ∧ b) ∧ c" [a, b, c] show (BMSLVNonCommutative a b) = withArgs "a ∧ b ٍ≠ b ∧ a" [a, b] show (BMSLVNonIdempotent a) = withArgs "a ∧ a ≠ a" [a] show (BMSLVNonUnital a) = withArgs "a ∧ top ≠ a" [a] show (BMSLVMeetOrderViolation a b) = withArgs "a ∧ b > a" [a, b] withArgs :: Show a => String -> [a] -> String withArgs s bs = s ++ "\n\t" ++ foldr (<>) mempty (intersperse "\n\t" (map show 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 b c = annotate (BMSLVNonAssociative a b c) ((a /\ (b /\ c)) === ((a /\ b) /\ c)) /\ annotate (BMSLVNonCommutative a b) ((a /\ b) === (b /\ a)) /\ annotate (BMSLVNonIdempotent a) ((a /\ a) === a) /\ annotate (BMSLVNonUnital a) ((top /\ a) === a) /\ annotate (BMSLVMeetOrderViolation a b) ((Meet (a /\ b) `leq` Meet a) === True) data BoundedJoinSemiLatticeLawViolation a = BJSLVNonAssociative a a a | BJSLVNonCommutative a a | BJSLVNonIdempotent a | BJSLVNonUnital a | BJSLVJoinOrderViolation a a deriving (Eq, Ord) instance Show a => Show (BoundedJoinSemiLatticeLawViolation a) where show (BJSLVNonAssociative a b c) = withArgs "a ∨ (b ∨ c) ≠ (a ∨ b) ∨ c" [a, b, c] show (BJSLVNonCommutative a b) = withArgs "a ∨ b ٍ≠ b ∨ a" [a, b] show (BJSLVNonIdempotent a) = withArgs "a ∨ a ≠ a" [a] show (BJSLVNonUnital a) = withArgs "a ∨ top ≠ a" [a] show (BJSLVJoinOrderViolation a b) = withArgs "a ∨ b > 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 b c = annotate (BJSLVNonAssociative a b c) ((a \/ (b \/ c)) === ((a \/ b) \/ c)) /\ annotate (BJSLVNonCommutative a b) ((a \/ b) === (b \/ a)) /\ annotate (BJSLVNonIdempotent a) ((a \/ a) === a) /\ annotate (BJSLVNonUnital a) ((bottom \/ a) === a) /\ fromBool (BJSLVJoinOrderViolation a b) (Join a `leq` Join (a \/ b)) data DistributiveLatticeLawViolation a = DLLVJoinOverMeetViolation a a a | DLLVMeetOverJoinViolation a a a deriving (Eq, Ord) instance Show a => Show (DistributiveLatticeLawViolation a) where show (DLLVJoinOverMeetViolation a b c) = withArgs "a ∧ (b ∨ c) ≠ a ∧ b ∨ a ∧ c" [a, b, c] show (DLLVMeetOverJoinViolation a b c) = withArgs "a ∨ (b ∧ c) ≠ (a ∨ b) ∧ (a ∨ c)" [a, b, 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 b c = annotate (DLLVJoinOverMeetViolation a b c) ((a /\ (b \/ c)) === ((a /\ b) \/ (a /\ c))) /\ annotate (DLLVMeetOverJoinViolation a b c) ((a \/ (b /\ c)) === ((a \/ b) /\ (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 (Eq, Ord) instance Show a => Show (HeytingAlgebraLawViolation a) where show (HAVImplication1 x a b)= withArgs "x ≤ (a ⇒ b) then x ∧ a ≤ b" [x, a, b] show (HAVImplication2 x a b) = withArgs "x ∧ a ≤ b then x ≤ (a ⇒ b)" [x, a, b] show (HAVNot a b) = withArgs "a ≤ b ⇏ not a" [a, b] show (HAVNotAndMeet a b) = withArgs "not (a ∧ b) ≠ not a ∨ not b" [a, b] show (HAVNotAndJoin a b) = withArgs "not (a ∨ b) ≠ not a ∧ not b" [a, b] show (HAVImplicationAndOrd a b) = withArgs "(a ⇒ b) ∧ a ≰ b" [a, b] show (HAVDistributiveLatticeLawViolation e) = show e show (HAVBoundedJoinSemilatticeLawViolation e) = show e show (HAVBoundedMeetSemilatticeLawViolation e) = show 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 :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) prop_implies x a b = fromBool (HAVImplication1 x a b) (Meet x `leq` Meet (a ==> b) ==> (Meet (x /\ a) `leq` Meet b)) /\ fromBool (HAVImplication2 x a b) (Meet (x /\ a) `leq` Meet b ==> (Meet x `leq` Meet (a ==> b))) /\ fromBool (HAVNot a b) (Meet a `leq` Meet b ==> (Meet (not b) `leq` Meet (not a))) /\ annotate (HAVNotAndMeet a b) (not (a /\ b) === (not a \/ not b)) /\ annotate (HAVNotAndJoin a b) (not (a \/ b) === (not a /\ not b)) /\ fromBool (HAVImplicationAndOrd a a) (Meet ((a ==> b) /\ a) `leq` Meet b) -- | -- Useful for testing valid instances of @'HeytingAlgebra'@ type class. It -- validates: -- -- * bounded lattice laws -- * @'prop_implies'@ prop_HeytingAlgebra :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) prop_HeytingAlgebra a b c = fmapCounterExample HAVBoundedJoinSemilatticeLawViolation (prop_BoundedJoinSemiLattice a b c) /\ fmapCounterExample HAVBoundedMeetSemilatticeLawViolation (prop_BoundedMeetSemiLattice a b c) /\ fmapCounterExample HAVDistributiveLatticeLawViolation (prop_DistributiveLattice a b c) /\ prop_implies a b c