NegClasses.hs

{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts      #-}

{-|
  Module      :  Logic.NegClasses
  Copyright   :  (c) Matt Noonan 2018
  License     :  BSD-style
  Maintainer  :  matt.noonan@gmail.com
  Portability :  portable
-}

module Logic.NegClasses
  ( -- * Algebraic properties
    Irreflexive(..)
  , Antisymmetric(..)
  ) where

import Logic.Proof
import Logic.Propositional (Not)
import Theory.Equality
import Theory.Named

{--------------------------------------------------------
  Special properties of predicates and functions
--------------------------------------------------------}

{-| 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
@
-}
class Irreflexive r where
  irrefl :: Proof (Not (r x x))
  default irrefl :: (Defining (r x x)) => Proof (Not (r x x))
  irrefl = axiom


{-| 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
@
-}   
class Antisymmetric c where
  antisymmetric :: c p q -> Proof (Not (c q p))
  default antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p))
  antisymmetric _ = axiom