Proof.Propositional

Provides type synonyms for logical connectives.

Documentation

type (/\) a b = (a, b) infixr 3

type (\/) a b = Either a b infixr 2

type Not a = a -> Void

exfalso :: a -> Not a -> b

orIntroL :: a -> a \/ b

orIntroR :: b -> a \/ b

orElim :: (a \/ b) -> (a -> c) -> (b -> c) -> c

andIntro :: a -> b -> a /\ b

andElimL :: (a /\ b) -> a

andElimR :: (a /\ b) -> b

orAssocL :: (a \/ (b \/ c)) -> (a \/ b) \/ c

orAssocR :: ((a \/ b) \/ c) -> a \/ (b \/ c)

andAssocL :: (a /\ (b /\ c)) -> (a /\ b) /\ c

andAssocR :: ((a /\ b) /\ c) -> a /\ (b /\ c)

data IsTrue (b :: Bool) where

Utility type to convert type-level (Bool-valued) predicate function into concrete witness data-type.

Constructors

Witness :: IsTrue 'True

Instances

Data (IsTrue 'True)

Defined in Proof.Propositional

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsTrue 'True -> c (IsTrue 'True)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (IsTrue 'True)

toConstr :: IsTrue 'True -> Constr

dataTypeOf :: IsTrue 'True -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (IsTrue 'True))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (IsTrue 'True))

gmapT :: (forall b. Data b => b -> b) -> IsTrue 'True -> IsTrue 'True

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsTrue 'True -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsTrue 'True -> r

gmapQ :: (forall d. Data d => d -> u) -> IsTrue 'True -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsTrue 'True -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True)

Read (IsTrue 'True)

Defined in Proof.Propositional

Methods

readsPrec :: Int -> ReadS (IsTrue 'True)

readList :: ReadS [IsTrue 'True]

readPrec :: ReadPrec (IsTrue 'True)

readListPrec :: ReadPrec [IsTrue 'True]

Show (IsTrue b)

Defined in Proof.Propositional

Methods

showsPrec :: Int -> IsTrue b -> ShowS

show :: IsTrue b -> String

showList :: [IsTrue b] -> ShowS

Empty (IsTrue 'False)

Defined in Proof.Propositional

Methods

eliminate :: IsTrue 'False -> x

Inhabited (IsTrue 'True)

Defined in Proof.Propositional

Methods

trivial :: IsTrue 'True

Eq (IsTrue b)

Defined in Proof.Propositional

Methods

(==) :: IsTrue b -> IsTrue b -> Bool

(/=) :: IsTrue b -> IsTrue b -> Bool

Ord (IsTrue b)

Defined in Proof.Propositional

Methods

compare :: IsTrue b -> IsTrue b -> Ordering

(<) :: IsTrue b -> IsTrue b -> Bool

(<=) :: IsTrue b -> IsTrue b -> Bool

(>) :: IsTrue b -> IsTrue b -> Bool

(>=) :: IsTrue b -> IsTrue b -> Bool

max :: IsTrue b -> IsTrue b -> IsTrue b

min :: IsTrue b -> IsTrue b -> IsTrue b

withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r

class Empty a where

Type-class for types without inhabitants, dual to Inhabited. Current GHC doesn't provide selective-instance, hence we don't Empty provide instances for product types in a generic deriving (DeriveAnyClass).

To derive an instance for each concrete types, use refute.

Since 0.4.0.0.

Minimal complete definition

Nothing

Methods

eliminate :: a -> x

default eliminate :: (Generic a, GEmpty (Rep a)) => a -> x

Instances

Empty Void

Defined in Proof.Propositional.Empty

Methods

eliminate :: Void -> x

Empty (IsTrue 'False)

Defined in Proof.Propositional

Methods

eliminate :: IsTrue 'False -> x

(Empty a, Empty b) => Empty (Either a b)

Defined in Proof.Propositional.Empty

Methods

eliminate :: Either a b -> x

(Inhabited a, Empty b) => Empty (a -> b)

Defined in Proof.Propositional

Methods

eliminate :: (a -> b) -> x

Empty ('EQ :~: 'GT)

Defined in Proof.Propositional

Methods

eliminate :: ('EQ :~: 'GT) -> x

Empty ('EQ :~: 'LT)

Defined in Proof.Propositional

Methods

eliminate :: ('EQ :~: 'LT) -> x

Empty ('GT :~: 'EQ)

Defined in Proof.Propositional

Methods

eliminate :: ('GT :~: 'EQ) -> x

Empty ('GT :~: 'LT)

Defined in Proof.Propositional

Methods

eliminate :: ('GT :~: 'LT) -> x

Empty ('LT :~: 'EQ)

Defined in Proof.Propositional

Methods

eliminate :: ('LT :~: 'EQ) -> x

Empty ('LT :~: 'GT)

Defined in Proof.Propositional

Methods

eliminate :: ('LT :~: 'GT) -> x

Empty (0 :~: 1)

Defined in Proof.Propositional

Methods

eliminate :: (0 :~: 1) -> x

Empty ('False :~: 'True)

Defined in Proof.Propositional

Methods

eliminate :: ('False :~: 'True) -> x

Empty ('True :~: 'False)

Defined in Proof.Propositional

Methods

eliminate :: ('True :~: 'False) -> x

Empty (() :~: Int)

Defined in Proof.Propositional

Methods

eliminate :: (() :~: Int) -> x

withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b

Giving falsity witness by proving Void from a. See also withEmpty'.

Since 0.4.0.0

withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b

Giving falsity witness by showing a entails everything. See also withEmpty.

Since 0.4.0.0

refute :: TypeQ -> DecsQ

Macro to automatically derive Empty instance for concrete (variable-free) types which may contain products.

class Inhabited a where

Types with at least one inhabitant, dual to Empty. Currently, GHC doesn't provide a selective-instance, hence we can't generically derive Inhabited instances for sum types (i.e. by DeriveAnyClass).

To derive an instance for each concrete types, use prove.

Since 0.4.0.0.

Minimal complete definition

Nothing

Methods

trivial :: a

A generic inhabitant of type a, which means that one cannot assume anything about the value of trivial except that it

• is of type a, and
• doesn't contain any partial values.

default trivial :: (Generic a, GInhabited (Rep a)) => a

Instances

Inhabited Ordering

Defined in Proof.Propositional

Methods

trivial :: Ordering

Inhabited Integer

Defined in Proof.Propositional

Methods

trivial :: Integer

Inhabited ()

Defined in Proof.Propositional.Inhabited

Methods

trivial :: ()

Inhabited Bool

Defined in Proof.Propositional

Methods

trivial :: Bool

Inhabited Char

Defined in Proof.Propositional

Methods

trivial :: Char

Inhabited Double

Defined in Proof.Propositional

Methods

trivial :: Double

Inhabited Float

Defined in Proof.Propositional

Methods

trivial :: Float

Inhabited Int

Defined in Proof.Propositional

Methods

trivial :: Int

Inhabited Word

Defined in Proof.Propositional

Methods

trivial :: Word

Inhabited (Ratio Integer)

Defined in Proof.Propositional

Methods

trivial :: Ratio Integer

Inhabited (IsTrue 'True)

Defined in Proof.Propositional

Methods

trivial :: IsTrue 'True

Inhabited (Maybe a)

Defined in Proof.Propositional

Methods

trivial :: Maybe a

Inhabited [a]

Defined in Proof.Propositional

Methods

trivial :: [a]

(Inhabited a, Inhabited b) => Inhabited (a, b)

Defined in Proof.Propositional.Inhabited

Methods

trivial :: (a, b)

Inhabited b => Inhabited (a -> b)

Defined in Proof.Propositional.Inhabited

Methods

trivial :: a -> b

Inhabited (n :~: n)

Defined in Proof.Propositional

Methods

trivial :: n :~: n

(Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c)

Defined in Proof.Propositional.Inhabited

Methods

trivial :: (a, b, c)

(Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d)

Defined in Proof.Propositional.Inhabited

Methods

trivial :: (a, b, c, d)

withInhabited :: forall a b. a -> (Inhabited a => b) -> b

prove :: TypeQ -> DecsQ

Macro to automatically derive Inhabited instance for concrete (variable-free) types which may contain sums.

Orphan instances

Inhabited Ordering

Methods

trivial :: Ordering

Inhabited Integer

Methods

trivial :: Integer

Inhabited Bool

Methods

trivial :: Bool

Inhabited Char

Methods

trivial :: Char

Inhabited Double

Methods

trivial :: Double

Inhabited Float

Methods

trivial :: Float

Inhabited Int

Methods

trivial :: Int

Inhabited Word

Methods

trivial :: Word

Inhabited (Ratio Integer)

Methods

trivial :: Ratio Integer

Inhabited (Maybe a)

Methods

trivial :: Maybe a

Inhabited [a]

Methods

trivial :: [a]

(Inhabited a, Empty b) => Empty (a -> b)

Methods

eliminate :: (a -> b) -> x

Empty ('EQ :~: 'GT)

Methods

eliminate :: ('EQ :~: 'GT) -> x

Empty ('EQ :~: 'LT)

Methods

eliminate :: ('EQ :~: 'LT) -> x

Empty ('GT :~: 'EQ)

Methods

eliminate :: ('GT :~: 'EQ) -> x

Empty ('GT :~: 'LT)

Methods

eliminate :: ('GT :~: 'LT) -> x

Empty ('LT :~: 'EQ)

Methods

eliminate :: ('LT :~: 'EQ) -> x

Empty ('LT :~: 'GT)

Methods

eliminate :: ('LT :~: 'GT) -> x

Empty (0 :~: 1)

Methods

eliminate :: (0 :~: 1) -> x

Empty ('False :~: 'True)

Methods

eliminate :: ('False :~: 'True) -> x

Empty ('True :~: 'False)

Methods

eliminate :: ('True :~: 'False) -> x

Empty (() :~: Int)

Methods

eliminate :: (() :~: Int) -> x

Inhabited (n :~: n)

Methods

trivial :: n :~: n