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

Inhabited (IsTrue True)

Methods

trivial :: IsTrue True

Empty (IsTrue False)

Methods

eliminate :: IsTrue False -> x

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. | Current GHC doesn't provide selective-instance, hence we don't Empty provide instances for sum types in a generic deriving (DeriveAnyClass).

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

Since 0.4.0.0.

Methods

trivial :: a

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

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 [a0]

Methods

trivial :: [a0]

Inhabited (Maybe a0)

Methods

trivial :: Maybe a0

Inhabited (Ratio Integer)

Methods

trivial :: Ratio Integer

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

Methods

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

Inhabited ((:~:) k n0 n0)

Methods

trivial :: (k :~: n0) n0

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

Methods

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

Empty ((:~:) Nat 0 1)

Methods

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