Logic.NegClasses

Algebraic properties

class Irreflexive r where

A binary relation R is irreflexive if, for all x, R(x, x) is false. The Irreflexive r typeclass provides a single method, irrefl :: Proof (Not (r x x)), proving the negation of R(x, x) for an arbitrary x.

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

-- Define an irreflexive binary relation
newtype DifferentColor p q = DifferentColor Defn
instance Irreflexive DifferentColor

Methods

irrefl :: Proof (Not (r x x))

irrefl :: Defining (r x x) => Proof (Not (r x x))

class Antisymmetric c where

A binary relation R is antisymmetric if, for all x and y, when R(x, y) is true, then R(y, x) is false. The Antisymmetric typeclass provides a single method, antisymmetric :: r x y -> Proof (Not (r y x)), proving the implication "R(x, y) implies the negation of R(y, x)".

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

-- Define an antisymmetric binary relation
newtype AncestorOf p q = AncestorOf Defn
instance Antisymmetric AncestorOf

Methods

antisymmetric :: c p q -> Proof (Not (c q p))

antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p))