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
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 (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 {}