content: {-# LANGUAGE TypeOperators         #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PolyKinds             #-}
  
  {-|
    Module      :  Logic.Classes
    Copyright   :  (c) Matt Noonan 2018
    License     :  BSD-style
    Maintainer  :  matt.noonan@gmail.com
    Portability :  portable
  -}
  
  module Logic.Classes
    ( -- * Algebraic properties
      Reflexive(..)
    , Symmetric(..)
    , Transitive(..)
    , transitive'
  
    , Idempotent(..)
    , Commutative(..)
    , Associative(..)
    , DistributiveL(..)
    , DistributiveR(..)
  
    , Injective(..)
  
    ) where
  
  import Logic.Proof
  import Theory.Equality
  
  {--------------------------------------------------------
    Special properties of predicates and functions
  --------------------------------------------------------}
  
  {-| 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
  @
  -}
  class Reflexive r where
    refl :: Proof (r x x)
    refl = axiom
  
  {-| 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
  @
  -}
  class Symmetric c where
    symmetric :: Proof (c p q) -> Proof (c q p)
    symmetric _ = axiom
  
  {-| 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
  @
  -}
  class Transitive c where
    transitive :: Proof (c p q) -> Proof (c q r) -> Proof (c p r)
    transitive _ _ = axiom
  
  -- | @transitive@, with the arguments flipped.
  transitive' :: Transitive c => Proof (c q r) -> Proof (c p q) -> Proof (c p r)
  transitive' = flip transitive
  
  {-| 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
  @
  -}
  class Idempotent c where
    idempotent :: Proof (c p p == p)
    idempotent = axiom
  
  {-| A binary operation @#@ is commutative if @x # y == y # 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
  @
  -}
  class Commutative c where
    commutative :: Proof (c p q == c q p)
    commutative = axiom
  
  {-| A binary operation @#@ is associative if @x # (y # z) == (x # y) # 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
  @
  -}
  class Associative c where
    associative :: Proof (c p (c q r) == c (c p q) r)
    associative = axiom
  
  {-| A binary operation @#@ distributes over @%@ on the left if
      @x # (y % z) == (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
  @
  -}
  class DistributiveL c c' where
    distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))
    distributiveL = axiom
  
  {-| A binary operation @#@ distributes over @%@ on the right if
      @(x % y) # z == (x # 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
  @
  -}
  class DistributiveR c c' where
    distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))
    distributiveR = axiom
  
  {-| 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
  @
  -}
  class Injective f where
    elim_inj :: Proof (f x == f y) -> Proof (x == y)
    elim_inj _ = axiom
  
  
  {--------------------------------------------------------
    Properites of equality
  --------------------------------------------------------}
  
  instance Reflexive Equals where
    refl = axiom
  
  instance Symmetric Equals where
    symmetric _ = axiom
  
  instance Transitive Equals where
    transitive _ _ = axiom
  