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

Eq (IsTrue b)

Methods

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

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

Data (IsTrue True)

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 :: (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)

Ord (IsTrue b)

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

Read (IsTrue True)

Methods

readsPrec :: Int -> ReadS (IsTrue True)

readList :: ReadS [IsTrue True]

readPrec :: ReadPrec (IsTrue True)

readListPrec :: ReadPrec [IsTrue True]

Show (IsTrue b)

Methods

showsPrec :: Int -> IsTrue b -> ShowS

show :: IsTrue b -> String

showList :: [IsTrue b] -> ShowS

Empty (IsTrue False)

Methods

eliminate :: IsTrue False -> x

Inhabited (IsTrue True)

Methods

trivial :: IsTrue True

withWitness :: 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.

Methods

eliminate :: a -> x

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

Instances

Empty Void

Methods

eliminate :: Void -> x

Empty (IsTrue False)

Methods

eliminate :: IsTrue False -> x

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

Methods

eliminate :: Either a b -> 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.

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.

trivial :: (Generic a, GInhabited (Rep a)) => 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.

Instances

Inhabited ()

Methods

trivial :: ()

Inhabited (IsTrue True)

Methods

trivial :: IsTrue True

Inhabited b => Inhabited (a -> b)

Methods

trivial :: a -> b

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

Methods

trivial :: (a, b)

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

Methods

trivial :: (a, b, c)

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

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 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 Integer

Methods

trivial :: Integer

Inhabited Ordering

Methods

trivial :: Ordering

Inhabited Word

Methods

trivial :: Word

Inhabited [a]

Methods

trivial :: [a]

Inhabited (Maybe a)

Methods

trivial :: Maybe a

Inhabited (Ratio Integer)

Methods

trivial :: Ratio Integer

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

Methods

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

Empty ((:~:) Bool False True)

Methods

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

Empty ((:~:) Bool True False)

Methods

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

Empty ((:~:) Ordering LT EQ)

Methods

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

Empty ((:~:) Ordering LT GT)

Methods

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

Empty ((:~:) Ordering EQ LT)

Methods

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

Empty ((:~:) Ordering EQ GT)

Methods

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

Empty ((:~:) Ordering GT LT)

Methods

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

Empty ((:~:) Ordering GT EQ)

Methods

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

Empty ((:~:) * () Int)

Methods

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

Empty ((:~:) Nat 0 1)

Methods

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

Inhabited ((:~:) k n n)

Methods

trivial :: (k :~: n) n