Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Logical and algebraic connectives for predicates, as well as common logical combinators.
Synopsis
- type Evident = (TyPred Sing :: Predicate k)
- type Impossible = (Not Evident :: Predicate k)
- data Not :: Predicate k -> Predicate k
- decideNot :: forall p a. Decision (p @@ a) -> Decision (Not p @@ a)
- data (&&&) :: Predicate k -> Predicate k -> Predicate k
- decideAnd :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
- data (|||) :: Predicate k -> Predicate k -> Predicate k
- decideOr :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
- type (^||) p q = p ||| (Not p &&& q)
- type (||^) p q = (p &&& Not q) ||| q
- type (^^^) p q = (p &&& Not q) ||| (Not p &&& q)
- decideXor :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
- data (==>) :: Predicate k -> Predicate k -> Predicate k
- proveImplies :: Prove q -> Prove (p ==> q)
- type Implies p q = Provable (p ==> q)
- type (<==>) p q = p ==> ((q &&& q) ==> p)
- type Equiv p q = Provable (p <==> q)
- compImpl :: forall p q r. (p --> q) -> (q --> r) -> p --> r
- explosion :: Impossible --> p
- atom :: p --> Evident
- excludedMiddle :: (p &&& Not p) --> Impossible
- doubleNegation :: forall p. Decidable p => Not (Not p) --> p
- contrapositive :: (p --> q) -> Not q --> Not p
- contrapositive' :: forall p q. Decidable q => (Not q --> Not p) -> p --> q
- projAndFst :: (p &&& q) --> p
- projAndSnd :: (p &&& q) --> q
- injOrLeft :: forall p q. p --> (p ||| q)
- injOrRight :: forall p q. q --> (p ||| q)
Top and bottom
Logical connectives
data Not :: Predicate k -> Predicate k Source #
is the predicate that Not
pp
is not true.
Instances
Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate | |
Decidable p => Decidable (Not p :: TyFun k1 Type -> *) Source # | |
SingI a => Auto (Not (Impossible :: Predicate k) :: TyFun k Type -> *) (a :: k) Source # | Since: decidable-0.1.2.0 |
Defined in Data.Type.Predicate.Auto | |
AutoNot p (f @@ a) => Auto (Not (PMap f p) :: TyFun k Type -> *) (a :: k) Source # | Since: decidable-0.1.2.0 |
Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *) Source # | |
Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate.Logic | |
(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *) Source # | |
Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate.Logic | |
Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k) Source # | Since: decidable-0.1.2.0 |
(SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p)) :: TyFun (f k) Type -> *) (as :: f k) Source # | Since: decidable-0.1.2.0 |
(SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p) :: TyFun (f k) Type -> *) (as :: f k) Source # | Since: decidable-0.1.2.0 |
type Apply (Not p :: TyFun k1 Type -> *) (a :: k1) Source # | |
decideNot :: forall p a. Decision (p @@ a) -> Decision (Not p @@ a) Source #
Decide Not p
based on decisions of p
.
data (&&&) :: Predicate k -> Predicate k -> Predicate k infixr 3 Source #
p
is a predicate that both &&&
qp
and q
are true.
Instances
(Provable p, Provable q) => Provable (p &&& q :: TyFun k1 Type -> *) Source # | |
Provable ((p &&& p) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable ((p &&& q) ==> q :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable ((p &&& q) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
(Decidable p, Decidable q) => Decidable (p &&& q :: TyFun k1 Type -> *) Source # | |
Decidable ((p &&& p) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable ((p &&& q) ==> q :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable ((p &&& q) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
(Auto p a, Auto q a) => Auto (p &&& q :: TyFun k Type -> *) (a :: k) Source # | |
type Apply (p &&& q :: TyFun k1 Type -> *) (a :: k1) Source # | |
decideAnd :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a) Source #
Decide p
based on decisions of &&&
qp
and q
.
data (|||) :: Predicate k -> Predicate k -> Predicate k infixr 2 Source #
p
is a predicate that either |||
qp
and q
are true.
Instances
Provable (p ==> (p ||| p) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable (q ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable (p ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
(Decidable p, Decidable q) => Decidable (p ||| q :: TyFun k1 Type -> *) Source # | |
Decidable (p ==> (p ||| p) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable (q ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable (p ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
type Apply (p ||| q :: TyFun k1 Type -> *) (a :: k1) Source # | |
decideOr :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a) Source #
Decide p
based on decisions of |||
qp
and q
.
type (^||) p q = p ||| (Not p &&& q) Source #
Left-biased "or". In proofs, prioritize a proof of the left side over a proof of the right side.
type (||^) p q = (p &&& Not q) ||| q Source #
Right-biased "or". In proofs, prioritize a proof of the right side over a proof of the left side.
type (^^^) p q = (p &&& Not q) ||| (Not p &&& q) Source #
p
is a predicate that either ^^^
qp
and q
are true, but not
both.
decideXor :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a) Source #
Decide p
based on decisions of ^^^
qp
and q
.
data (==>) :: Predicate k -> Predicate k -> Predicate k infixr 1 Source #
p ==> q
is true if q
is provably true under the condition that p
is true.
Instances
Provable (p ==> (p ||| p) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable (q ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable (p ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable ((p &&& p) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable ((p &&& q) ==> q :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable ((p &&& q) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *) Source # | |
Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate.Logic | |
Decidable (p ==> (p ||| p) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable (q ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable (p ==> (p ||| q) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable ((p &&& p) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable ((p &&& q) ==> q :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
Decidable ((p &&& q) ==> p :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.1.0 |
(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *) Source # | |
Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate.Logic | |
Auto q a => Auto (p ==> q :: TyFun k Type -> *) (a :: k) Source # | |
Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # | |
Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # | |
Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # | |
(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # | |
Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # | |
Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # | |
type Apply (p ==> q :: TyFun k1 Type -> *) (a :: k1) Source # | |
type (<==>) p q = p ==> ((q &&& q) ==> p) infixr 1 Source #
Two-way implication, or logical equivalence
Logical deductions
explosion :: Impossible --> p Source #
From Impossible
a
, you can prove anything. Essentially
a lifted version of absurd
.
excludedMiddle :: (p &&& Not p) --> Impossible Source #
We cannot have both p
and
.Not
p
doubleNegation :: forall p. Decidable p => Not (Not p) --> p Source #
Logical double negation. Only possible if p
is Decidable
.
contrapositive :: (p --> q) -> Not q --> Not p Source #
If only this worked, but darn overlapping instances. Same for p ==> p ||| q and p &&& q ==> p :( q) ==> instance Provable (p &&& Not p ==> Impossible) where prove = excludedMiddle @p
If p implies q, then not q implies not p.
contrapositive' :: forall p q. Decidable q => (Not q --> Not p) -> p --> q Source #
Reverse direction of contrapositive
. Only possible if q
is
Decidable
on its own, without the help of p
, which makes this much
less useful.