Logic.Classes

Algebraic properties

class Reflexive r where

A binary relation R is reflexive if, for all x, R(x, x) is true. The Reflexive r typeclass provides a single method, refl :: Proof (r x x), proving R(x, x) for an arbitrary x.

Within the module where the relation R is defined, you can declare R to be reflexive with an empty instance:

-- Define a reflexive binary relation
newtype SameColor p q = SameColor Defn
instance Reflexive SameColor

Methods

refl :: Proof (r x x)

refl :: Defining (r x x) => Proof (r x x)

Instances

Reflexive Equals

Methods

refl :: Proof (Equals x x)

class Symmetric c where

A binary relation R is symmetric if, for all x and y, R(x, y) is true if and only if R(y, x) is true. The Symmetric typeclass provides a single method, symmetric :: r x y -> Proof (r y x), proving the implication "R(x, y) implies R(y, x)".

Within the module where R is defined, you can declare R to be symmetric with an empty instance:

-- Define a symmetric binary relation
newtype NextTo p q = NextTo Defn
instance Symmetric NextTo

Methods

symmetric :: c p q -> Proof (c q p)

symmetric :: Defining (c p q) => c p q -> Proof (c q p)

Instances

Symmetric Equals

Methods

symmetric :: Equals p q -> Proof (Equals q p)

Symmetric Or

Methods

symmetric :: Or p q -> Proof (Or q p)

Symmetric And

Methods

symmetric :: And p q -> Proof (And q p)

class Transitive c where

A binary relation R is transitive if, for all x, y, z, if R(x, y) is true and R(y, z) is true, then R(x, z) is true. The Transitive r typeclass provides a single method, transitive :: r x y -> r y z -> Proof (r x z), proving R(x, z) from R(x, y) and R(y, z).

Within the module where R is defined, you can declare R to be transitive with an empty instance:

-- Define a transitive binary relation
newtype CanReach p q = CanReach Defn
instance Transitive CanReach

Methods

transitive :: c p q -> c q r -> Proof (c p r)

transitive :: Defining (c p q) => c p q -> c q r -> Proof (c p r)

Instances

Transitive Equals

Methods

transitive :: Equals p q -> Equals q r -> Proof (Equals p r)

transitive' :: Transitive c => c q r -> c p q -> Proof (c p r)

transitive, with the arguments flipped.

class Idempotent c where

A binary operation # is idempotent if x # x == x for all x. The Idempotent c typeclass provides a single method, idempotent :: Proof (c p p == p).

Within the module where F is defined, you can declare F to be idempotent with an empty instance:

-- Define an idempotent binary operation
newtype Union x y = Union Defn
instance Idempotent Union

Methods

idempotent :: Proof (c p p == p)

idempotent :: Defining (c p p) => Proof (c p p == p)

class Commutative c where

A binary operation # is commutative if x x for all x and y. The Commutative c typeclass provides a single method, commutative :: Proof (c x y == c y x).

Within the module where F is defined, you can declare F to be commutative with an empty instance:

-- Define a commutative binary operation
newtype Union x y = Union Defn
instance Commutative Union

Methods

commutative :: Proof (c p q == c q p)

commutative :: Defining (c p q) => Proof (c p q == c q p)

class Associative c where

A binary operation # is associative if x z) == (x z for all x, y, and z. The Associative c typeclass provides a single method, associative :: Proof (c x (c y z) == c (c x y) z).

Within the module where F is defined, you can declare F to be associative with an empty instance:

-- Define an associative binary operation
newtype Union x y = Union Defn
instance Associative Union

Methods

associative :: Proof (c p (c q r) == c (c p q) r)

associative :: Defining (c p q) => Proof (c p (c q r) == c (c p q) r)

Instances

Associative Or

Methods

associative :: Proof (Or p (Or q r) == Or (Or p q) r)

Associative And

Methods

associative :: Proof (And p (And q r) == And (And p q) r)

class DistributiveL c c' where

A binary operation # distributes over % on the left if x y) % (x # z) for all x, y, and z. The DistributiveL c c' typeclass provides a single method, distributiveL :: Proof (c x (c' y z) == c' (c x y) (c x z)).

Within the module where F and G are defined, you can declare F to distribute over G on the left with an empty instance:

-- x Union (y Intersect z) == (x Union y) Intersect (x Union z)
newtype Union     x y = Union     Defn
newtype Intersect x y = Intersect Defn
instance DistributiveL Union Intersect

Methods

distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))

distributiveL :: (Defining (c p q), Defining (c' p q)) => Proof (c p (c' q r) == c' (c p q) (c p r))

Instances

DistributiveL Or Or

Methods

distributiveL :: Proof (Or p (Or q r) == Or (Or p q) (Or p r))

DistributiveL Or And

Methods

distributiveL :: Proof (Or p (And q r) == And (Or p q) (Or p r))

DistributiveL And Or

Methods

distributiveL :: Proof (And p (Or q r) == Or (And p q) (And p r))

DistributiveL And And

Methods

distributiveL :: Proof (And p (And q r) == And (And p q) (And p r))

class DistributiveR c c' where

A binary operation # distributes over % on the right if (x % y) z) % (y # z) for all x, y, and z. The DistributiveR c c' typeclass provides a single method, distributiveR :: Proof (c (c' x y) z == c' (c x z) (c y z)).

Within the module where F and G are defined, you can declare F to distribute over G on the left with an empty instance:

-- (x Intersect y) Union z == (x Union z) Intersect (y Union z)
newtype Union     x y = Union     Defn
newtype Intersect x y = Intersect Defn
instance DistributiveR Union Intersect

Methods

distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))

distributiveR :: (Defining (c p q), Defining (c' p q)) => Proof (c (c' p q) r == c' (c p r) (c q r))

Instances

DistributiveR Or Or

Methods

distributiveR :: Proof (Or (Or p q) r == Or (Or p r) (Or q r))

DistributiveR Or And

Methods

distributiveR :: Proof (Or (And p q) r == And (Or p r) (Or q r))

DistributiveR And Or

Methods

distributiveR :: Proof (And (Or p q) r == Or (And p r) (And q r))

DistributiveR And And

Methods

distributiveR :: Proof (And (And p q) r == And (And p r) (And q r))

class Injective f where

A function f is injective if f x == f y implies x == y. The Injective f typeclass provides a single method, elim_inj :: (f x == f y) -> Proof (x == y).

Within the module where F is defined, you can declare F to be injective with an empty instance:

-- {x} == {y} implies x == y.
newtype Singleton x = Singleton Defn
instance Injective Singleton

Methods

elim_inj :: (f x == f y) -> Proof (x == y)

elim_inj :: (Defining (f x), Defining (f y)) => (f x == f y) -> Proof (x == y)