{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Provides type synonyms for logical connectives.
module Proof.Propositional
  ( type (/\),
    type (\/),
    Not,
    exfalso,
    orIntroL,
    orIntroR,
    orElim,
    andIntro,
    andElimL,
    andElimR,
    orAssocL,
    orAssocR,
    andAssocL,
    andAssocR,
    IsTrue (..),
    withWitness,
    Empty (..),
    withEmpty,
    withEmpty',
    refute,
    Inhabited (..),
    withInhabited,
    prove,
  )
where

import Data.Data (Data)
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Typeable (Typeable)
import Data.Void
import Proof.Propositional.Empty
import Proof.Propositional.Inhabited
import Proof.Propositional.TH
import Unsafe.Coerce

type a /\ b = (a, b)

type a \/ b = Either a b

type Not a = a -> Void

infixr 2 \/

infixr 3 /\

exfalso :: a -> Not a -> b
exfalso :: forall a b. a -> Not a -> b
exfalso a
a Not a
neg = forall a. Void -> a
absurd (Not a
neg a
a)

orIntroL :: a -> a \/ b
orIntroL :: forall a b. a -> a \/ b
orIntroL = forall a b. a -> a \/ b
Left

orIntroR :: b -> a \/ b
orIntroR :: forall b a. b -> a \/ b
orIntroR = forall a b. b -> Either a b
Right

orElim :: a \/ b -> (a -> c) -> (b -> c) -> c
orElim :: forall a b c. (a \/ b) -> (a -> c) -> (b -> c) -> c
orElim a \/ b
aORb a -> c
aTOc b -> c
bTOc = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> c
aTOc b -> c
bTOc a \/ b
aORb

andIntro :: a -> b -> a /\ b
andIntro :: forall a b. a -> b -> a /\ b
andIntro = (,)

andElimL :: a /\ b -> a
andElimL :: forall a b. (a /\ b) -> a
andElimL = forall a b. (a /\ b) -> a
fst

andElimR :: a /\ b -> b
andElimR :: forall a b. (a /\ b) -> b
andElimR = forall a b. (a /\ b) -> b
snd

andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c
andAssocL :: forall a b c. (a /\ (b /\ c)) -> (a /\ b) /\ c
andAssocL (a
a, (b
b, c
c)) = ((a
a, b
b), c
c)

andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)
andAssocR :: forall a b c. ((a /\ b) /\ c) -> a /\ (b /\ c)
andAssocR ((a
a, b
b), c
c) = (a
a, (b
b, c
c))

orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c
orAssocL :: forall a b c. (a \/ (b \/ c)) -> (a \/ b) \/ c
orAssocL (Left a
a) = forall a b. a -> a \/ b
Left (forall a b. a -> a \/ b
Left a
a)
orAssocL (Right (Left b
b)) = forall a b. a -> a \/ b
Left (forall a b. b -> Either a b
Right b
b)
orAssocL (Right (Right c
c)) = forall a b. b -> Either a b
Right c
c

orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
orAssocR :: forall a b c. ((a \/ b) \/ c) -> a \/ (b \/ c)
orAssocR (Left (Left a
a)) = forall a b. a -> a \/ b
Left a
a
orAssocR (Left (Right b
b)) = forall a b. b -> Either a b
Right (forall a b. a -> a \/ b
Left b
b)
orAssocR (Right c
c) = forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right c
c)

{- | Utility type to convert type-level (@'Bool'@-valued) predicate function
   into concrete witness data-type.
-}
data IsTrue (b :: Bool) where
  Witness :: IsTrue 'True

withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r
withWitness :: forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness IsTrue b
_ = forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (forall a b. a -> b
unsafeCoerce (forall {k} (a :: k). a :~: a
Refl :: () :~: ()) :: b :~: 'True)
{-# NOINLINE withWitness #-}

deriving instance Show (IsTrue b)

deriving instance Eq (IsTrue b)

deriving instance Ord (IsTrue b)

deriving instance Read (IsTrue 'True)

deriving instance Typeable IsTrue

deriving instance Data (IsTrue 'True)

instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where
  eliminate :: forall x. (a -> b) -> x
eliminate a -> b
f = forall a x. Empty a => a -> x
eliminate (a -> b
f forall a. Inhabited a => a
trivial)

refute [t|0 :~: 1|]
refute [t|() :~: Int|]
refute [t| 'True :~: 'False|]
refute [t| 'False :~: 'True|]
refute [t| 'LT :~: 'GT|]
refute [t| 'LT :~: 'EQ|]
refute [t| 'EQ :~: 'LT|]
refute [t| 'EQ :~: 'GT|]
refute [t| 'GT :~: 'LT|]
refute [t| 'GT :~: 'EQ|]

prove [t|Bool|]
prove [t|Int|]
prove [t|Integer|]
prove [t|Word|]
prove [t|Double|]
prove [t|Float|]
prove [t|Char|]
prove [t|Ordering|]
prove [t|forall a. [a]|]
prove [t|Rational|]
prove [t|forall a. Maybe a|]
prove [t|forall n. n :~: n|]
prove [t|IsTrue 'True|]

instance Empty (IsTrue 'False) where
  eliminate :: forall x. IsTrue 'False -> x
eliminate = IsTrue 'False -> x
\case