{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell, TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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 Proof.Propositional.Empty
import Proof.Propositional.Inhabited
import Proof.Propositional.TH
import Data.Data (Data)
import Data.Type.Equality ((:~:))
import Data.Typeable (Typeable)
import Data.Void
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 a neg = absurd (neg a)
orIntroL :: a -> a \/ b
orIntroL = Left
orIntroR :: b -> a \/ b
orIntroR = Right
orElim :: a \/ b -> (a -> c) -> (b -> c) -> c
orElim aORb aTOc bTOc = either aTOc bTOc aORb
andIntro :: a -> b -> a /\ b
andIntro = (,)
andElimL :: a /\ b -> a
andElimL = fst
andElimR :: a /\ b -> b
andElimR = snd
andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c
andAssocL (a,(b,c)) = ((a,b), c)
andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)
andAssocR ((a,b),c) = (a,(b,c))
orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c
orAssocL (Left a) = Left (Left a)
orAssocL (Right (Left b)) = Left (Right b)
orAssocL (Right (Right c)) = Right c
orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
orAssocR (Left (Left a)) = Left a
orAssocR (Left (Right b)) = Right (Left b)
orAssocR (Right c) = Right (Right c)
data IsTrue (b :: Bool) where
Witness :: IsTrue 'True
withWitness :: IsTrue b -> (b ~ 'True => r) -> r
withWitness Witness r = r
{-# NOINLINE withWitness #-}
{-# RULES
"withWitness/coercion" [~1] forall x.
withWitness x = unsafeCoerce
#-}
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 f = eliminate (f 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 = \ case {}