src/Logic/Theory/Eq.hs

   1 -- For `(==)`
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE Safe #-}
   4
   5 module Logic.Theory.Eq (
   6   type (==) (),
   7   type (/=) (),
   8   (==),
   9   (/=),
  10 ) where
  11
  12 import Data.Bool (Bool)
  13 import Data.Bool qualified as Bool
  14 import Data.Either (Either (..))
  15 import Data.Eq qualified as Eq
  16 import Logic.Kernel
  17
  18 data (==) x y = EqualAxiom
  19 data (/=) x y = NotEqualAxiom
  20
  21 type role (==) nominal nominal
  22 type role (/=) nominal nominal
  23
  24 instance Axiom (Associative (==) x y z)
  25 instance Axiom (Associative (/=) x y z)
  26 instance Axiom (Commutative (==) x y)
  27 instance Axiom (Commutative (/=) x y)
  28
  29 (==) :: Eq.Eq a => x ::: a -> y ::: a -> (x == y) ::: Bool
  30 (==) (Named x) (Named y) = EqualAxiom ... x Eq.== y
  31 {-# INLINE (==) #-}
  32
  33 (/=) :: Eq.Eq a => x ::: a -> y ::: a -> (x /= y) ::: Bool
  34 (/=) (Named x) (Named y) = NotEqualAxiom ... x Eq./= y
  35 {-# INLINE (/=) #-}
  36
  37 infix 4 ==
  38 infix 4 /=
  39
  40 instance Provable ((x == y) ::: Bool) where
  41   type ProofOf ((x == y) ::: Bool) = Either (Proof (x /= y)) (Proof (x == y))
  42   prove (Named b) = case b of
  43     Bool.False -> Left (proven NotEqualAxiom)
  44     Bool.True -> Right (proven EqualAxiom)
  45
  46 instance Provable ((x /= y) ::: Bool) where
  47   type ProofOf ((x /= y) ::: Bool) = Either (Proof (x == y)) (Proof (x /= y))
  48   prove (Named b) = case b of
  49     Bool.False -> Left (proven EqualAxiom)
  50     Bool.True -> Right (proven NotEqualAxiom)