equational-reasoning-0.7.0.3: Proof assistant for Haskell using DataKinds & PolyKinds
Safe HaskellSafe-Inferred
LanguageHaskell2010

Proof.Propositional

Description

Provides type synonyms for logical connectives.

Synopsis

Documentation

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

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

type Not a = a -> Void Source #

exfalso :: a -> Not a -> b Source #

orIntroL :: a -> a \/ b Source #

orIntroR :: b -> a \/ b Source #

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

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

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

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

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

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

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

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

data IsTrue (b :: Bool) where Source #

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

Constructors

Witness :: IsTrue 'True 

Instances

Instances details
Data (IsTrue 'True) Source # 
Instance details

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) Source # 
Instance details

Defined in Proof.Propositional

Show (IsTrue b) Source # 
Instance details

Defined in Proof.Propositional

Methods

showsPrec :: Int -> IsTrue b -> ShowS #

show :: IsTrue b -> String #

showList :: [IsTrue b] -> ShowS #

Empty (IsTrue 'False) Source # 
Instance details

Defined in Proof.Propositional

Methods

eliminate :: IsTrue 'False -> x Source #

Inhabited (IsTrue 'True) Source # 
Instance details

Defined in Proof.Propositional

Eq (IsTrue b) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

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

Ord (IsTrue b) Source # 
Instance details

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

class Empty a where Source #

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

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

Instances

Instances details
Empty Void Source # 
Instance details

Defined in Proof.Propositional.Empty

Methods

eliminate :: Void -> x Source #

Empty (IsTrue 'False) Source # 
Instance details

Defined in Proof.Propositional

Methods

eliminate :: IsTrue 'False -> x Source #

(Empty a, Empty b) => Empty (Either a b) Source # 
Instance details

Defined in Proof.Propositional.Empty

Methods

eliminate :: Either a b -> x Source #

(Inhabited a, Empty b) => Empty (a -> b) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('EQ :~: 'GT) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('EQ :~: 'LT) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('GT :~: 'EQ) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('GT :~: 'LT) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('LT :~: 'EQ) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('LT :~: 'GT) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty (0 :~: 1) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('False :~: 'True) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty ('True :~: 'False) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

Empty (() :~: Int) Source # 
Instance details

Defined in Proof.Propositional

Methods

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

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

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

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

Since 0.4.0.0

refute :: TypeQ -> DecsQ Source #

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

class Inhabited a where Source #

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

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

Instances

Instances details
Inhabited Ordering Source # 
Instance details

Defined in Proof.Propositional

Inhabited Integer Source # 
Instance details

Defined in Proof.Propositional

Inhabited () Source # 
Instance details

Defined in Proof.Propositional.Inhabited

Methods

trivial :: () Source #

Inhabited Bool Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: Bool Source #

Inhabited Char Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: Char Source #

Inhabited Double Source # 
Instance details

Defined in Proof.Propositional

Inhabited Float Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: Float Source #

Inhabited Int Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: Int Source #

Inhabited Word Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: Word Source #

Inhabited (Ratio Integer) Source # 
Instance details

Defined in Proof.Propositional

Inhabited (IsTrue 'True) Source # 
Instance details

Defined in Proof.Propositional

Inhabited (Maybe a) Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: Maybe a Source #

Inhabited [a] Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: [a] Source #

(Inhabited a, Inhabited b) => Inhabited (a, b) Source # 
Instance details

Defined in Proof.Propositional.Inhabited

Methods

trivial :: (a, b) Source #

Inhabited b => Inhabited (a -> b) Source # 
Instance details

Defined in Proof.Propositional.Inhabited

Methods

trivial :: a -> b Source #

Inhabited (n :~: n) Source # 
Instance details

Defined in Proof.Propositional

Methods

trivial :: n :~: n Source #

(Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c) Source # 
Instance details

Defined in Proof.Propositional.Inhabited

Methods

trivial :: (a, b, c) Source #

(Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d) Source # 
Instance details

Defined in Proof.Propositional.Inhabited

Methods

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

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

prove :: TypeQ -> DecsQ Source #

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

Orphan instances

Inhabited Ordering Source # 
Instance details

Inhabited Integer Source # 
Instance details

Inhabited Bool Source # 
Instance details

Methods

trivial :: Bool Source #

Inhabited Char Source # 
Instance details

Methods

trivial :: Char Source #

Inhabited Double Source # 
Instance details

Inhabited Float Source # 
Instance details

Methods

trivial :: Float Source #

Inhabited Int Source # 
Instance details

Methods

trivial :: Int Source #

Inhabited Word Source # 
Instance details

Methods

trivial :: Word Source #

Inhabited (Ratio Integer) Source # 
Instance details

Inhabited (Maybe a) Source # 
Instance details

Methods

trivial :: Maybe a Source #

Inhabited [a] Source # 
Instance details

Methods

trivial :: [a] Source #

(Inhabited a, Empty b) => Empty (a -> b) Source # 
Instance details

Methods

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

Empty ('EQ :~: 'GT) Source # 
Instance details

Methods

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

Empty ('EQ :~: 'LT) Source # 
Instance details

Methods

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

Empty ('GT :~: 'EQ) Source # 
Instance details

Methods

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

Empty ('GT :~: 'LT) Source # 
Instance details

Methods

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

Empty ('LT :~: 'EQ) Source # 
Instance details

Methods

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

Empty ('LT :~: 'GT) Source # 
Instance details

Methods

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

Empty (0 :~: 1) Source # 
Instance details

Methods

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

Empty ('False :~: 'True) Source # 
Instance details

Methods

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

Empty ('True :~: 'False) Source # 
Instance details

Methods

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

Empty (() :~: Int) Source # 
Instance details

Methods

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

Inhabited (n :~: n) Source # 
Instance details

Methods

trivial :: n :~: n Source #