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
data SameColor p q
instance Reflexive SameColor

Minimal complete definition

Nothing

Methods

refl :: Proof (r x x)

Instances

Reflexive (Equals :: k -> k -> Type)

Defined in Logic.Classes

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
data NextTo p q
instance Symmetric NextTo

Minimal complete definition

Nothing

Methods

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

Instances

Symmetric (Equals :: k -> k -> Type)

Defined in Logic.Classes

Methods

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

Symmetric (And :: k -> k -> Type)

Defined in Logic.Propositional

Methods

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

Symmetric (Or :: k -> k -> Type)

Defined in Logic.Propositional

Methods

symmetric :: Proof (Or p q) -> Proof (Or 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
data CanReach p q
instance Transitive CanReach

Minimal complete definition

Nothing

Methods

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

Instances

Transitive (Equals :: k -> k -> Type)

Defined in Logic.Classes

Methods

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

transitive' :: Transitive c => Proof (c q r) -> Proof (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
data Union x y
instance Idempotent Union

Minimal complete definition

Nothing

Methods

idempotent :: 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
data Union x y
instance Commutative Union

Minimal complete definition

Nothing

Methods

commutative :: 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
data Union x y
instance Associative Union

Minimal complete definition

Nothing

Methods

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

Instances

Associative (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

Associative (And :: Type -> Type -> Type)

Defined in Logic.Propositional

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)
data Union     x y
data Intersect x y
instance DistributiveL Union Intersect

Minimal complete definition

Nothing

Methods

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

Instances

DistributiveL (And :: k -> Type -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

DistributiveL (Or :: k -> Type -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

DistributiveL (Or :: k -> Type -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

DistributiveL (And :: k -> Type -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (And p (Or q r) == Or (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)
data Union     x y
data Intersect x y
instance DistributiveR Union Intersect

Minimal complete definition

Nothing

Methods

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

Instances

DistributiveR (And :: Type -> k -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

DistributiveR (Or :: Type -> k -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

DistributiveR (Or :: Type -> k -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

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

DistributiveR (And :: Type -> k -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (And (Or p q) r == Or (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.
data Singleton x
instance Injective Singleton

Minimal complete definition

Nothing

Methods

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