{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Predicate.Logic (
Evident,
Impossible,
type Not,
decideNot,
type (&&&),
decideAnd,
type (|||),
decideOr,
type (^||),
type (||^),
type (^^^),
decideXor,
type (==>),
proveImplies,
Implies,
type (<==>),
Equiv,
compImpl,
explosion,
atom,
complementation,
doubleNegation,
tripleNegation,
negateTwice,
contrapositive,
contrapositive',
projAndFst,
projAndSnd,
injOrLeft,
injOrRight,
) where
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Predicate
import Data.Void
data (&&&) :: Predicate k -> Predicate k -> Predicate k
type instance Apply (p &&& q) a = (p @@ a, q @@ a)
infixr 3 &&&
instance (Decidable p, Decidable q) => Decidable (p &&& q) where
decide :: Decide (p &&& q)
decide (Sing a
x :: Sing a) = forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
forall (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
decideAnd @p @q @a (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x) (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @q Sing a
x)
instance (Provable p, Provable q) => Provable (p &&& q) where
prove :: Prove (p &&& q)
prove Sing a
x = (forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k1 ~> *). Provable p => Prove p
prove @p Sing a
x, forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k1 ~> *). Provable p => Prove p
prove @q Sing a
x)
decideAnd ::
forall p q a.
() =>
Decision (p @@ a) ->
Decision (q @@ a) ->
Decision ((p &&& q) @@ a)
decideAnd :: forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
decideAnd = \case
Proved p @@ a
p -> ((q @@ a) -> (p @@ a, q @@ a))
-> ((p @@ a, q @@ a) -> q @@ a)
-> Decision (q @@ a)
-> Decision (p @@ a, q @@ a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (p @@ a
p,) (p @@ a, q @@ a) -> q @@ a
forall a b. (a, b) -> b
snd
Disproved Refuted (p @@ a)
v -> \Decision (q @@ a)
_ -> Refuted ((p &&& q) @@ a) -> Decision ((p &&& q) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted ((p &&& q) @@ a) -> Decision ((p &&& q) @@ a))
-> Refuted ((p &&& q) @@ a) -> Decision ((p &&& q) @@ a)
forall a b. (a -> b) -> a -> b
$ \(p @@ a
p, q @@ a
_) -> Refuted (p @@ a)
v p @@ a
p
data (|||) :: Predicate k -> Predicate k -> Predicate k
type instance Apply (p ||| q) a = Either (p @@ a) (q @@ a)
infixr 2 |||
instance (Decidable p, Decidable q) => Decidable (p ||| q) where
decide :: Decide (p ||| q)
decide (Sing a
x :: Sing a) = forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
forall (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
decideOr @p @q @a (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x) (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @q Sing a
x)
decideOr ::
forall p q a.
() =>
Decision (p @@ a) ->
Decision (q @@ a) ->
Decision ((p ||| q) @@ a)
decideOr :: forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
decideOr = \case
Proved p @@ a
p -> \Decision (q @@ a)
_ -> ((p ||| q) @@ a) -> Decision ((p ||| q) @@ a)
forall a. a -> Decision a
Proved (((p ||| q) @@ a) -> Decision ((p ||| q) @@ a))
-> ((p ||| q) @@ a) -> Decision ((p ||| q) @@ a)
forall a b. (a -> b) -> a -> b
$ (p @@ a) -> Either (p @@ a) (q @@ a)
forall a b. a -> Either a b
Left p @@ a
p
Disproved Refuted (p @@ a)
v -> ((q @@ a) -> Either (p @@ a) (q @@ a))
-> (Either (p @@ a) (q @@ a) -> q @@ a)
-> Decision (q @@ a)
-> Decision (Either (p @@ a) (q @@ a))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (q @@ a) -> Either (p @@ a) (q @@ a)
forall a b. b -> Either a b
Right (((p @@ a) -> q @@ a)
-> ((q @@ a) -> q @@ a) -> Either (p @@ a) (q @@ a) -> q @@ a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> q @@ a
forall a. Void -> a
absurd (Void -> q @@ a) -> Refuted (p @@ a) -> (p @@ a) -> q @@ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refuted (p @@ a)
v) (q @@ a) -> q @@ a
forall a. a -> a
id)
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)
decideXor :: forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
decideXor Decision (p @@ a)
p Decision (q @@ a)
q =
forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
forall (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
decideOr @(p &&& Not q) @(Not p &&& q) @a
(forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
forall (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
decideAnd @p @(Not q) @a Decision (p @@ a)
p (forall {k1} (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
forall (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @q @a Decision (q @@ a)
q))
(forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
forall (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
decideAnd @(Not p) @q @a (forall {k1} (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
forall (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @p @a Decision (p @@ a)
p) Decision (q @@ a)
q)
data (==>) :: Predicate k -> Predicate k -> Predicate k
type instance Apply (p ==> q) a = p @@ a -> q @@ a
infixr 1 ==>
instance Decidable (Impossible ==> p)
instance Provable (Impossible ==> p) where
prove :: Prove (Impossible ==> p)
prove = forall {k1} (p :: k1 ~> *) (a :: k1).
Sing a -> (Impossible @@ a) -> p @@ a
forall (p :: Predicate k1) (a :: k1).
Sing a -> (Impossible @@ a) -> p @@ a
explosion @p
instance (Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p) where
decide :: Decide (Not q ==> Not p)
decide Sing a
x = case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: Predicate k1). Decidable p => Decide p
decide @(p ==> q) Sing a
x of
Proved (p ==> q) @@ a
pq -> ((Not q ==> Not p) @@ a) -> Decision ((Not q ==> Not p) @@ a)
forall a. a -> Decision a
Proved (((Not q ==> Not p) @@ a) -> Decision ((Not q ==> Not p) @@ a))
-> ((Not q ==> Not p) @@ a) -> Decision ((Not q ==> Not p) @@ a)
forall a b. (a -> b) -> a -> b
$ \Apply q a -> Void
vq Apply p a
p -> Apply q a -> Void
vq ((p ==> q) @@ a
Apply p a -> Apply q a
pq Apply p a
p)
Disproved Refuted ((p ==> q) @@ a)
vpq -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: Predicate k1). Decidable p => Decide p
decide @q Sing a
x of
Proved Apply q a
q -> Refuted ((Not q ==> Not p) @@ a)
-> Decision ((Not q ==> Not p) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted ((Not q ==> Not p) @@ a)
-> Decision ((Not q ==> Not p) @@ a))
-> Refuted ((Not q ==> Not p) @@ a)
-> Decision ((Not q ==> Not p) @@ a)
forall a b. (a -> b) -> a -> b
$ \(Not q ==> Not p) @@ a
_ -> Refuted ((p ==> q) @@ a)
vpq (Apply q a -> Apply p a -> Apply q a
forall a b. a -> b -> a
const Apply q a
q)
Disproved Apply q a -> Void
vq -> Refuted ((Not q ==> Not p) @@ a)
-> Decision ((Not q ==> Not p) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted ((Not q ==> Not p) @@ a)
-> Decision ((Not q ==> Not p) @@ a))
-> Refuted ((Not q ==> Not p) @@ a)
-> Decision ((Not q ==> Not p) @@ a)
forall a b. (a -> b) -> a -> b
$ \(Not q ==> Not p) @@ a
vnpnq -> Refuted ((p ==> q) @@ a)
vpq (Void -> Apply q a
forall a. Void -> a
absurd (Void -> Apply q a)
-> (Apply p a -> Void) -> Apply p a -> Apply q a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Not q ==> Not p) @@ a
(Apply q a -> Void) -> Apply p a -> Void
vnpnq Apply q a -> Void
vq)
instance Provable (p ==> q) => Provable (Not q ==> Not p) where
prove :: Prove (Not q ==> Not p)
prove = forall {k} (p :: k ~> *) (q :: k ~> *).
(p --> q) -> Not q --> Not p
forall (p :: Predicate k1) (q :: Predicate k1).
(p --> q) -> Not q --> Not p
contrapositive @p @q (forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: Predicate k1). Provable p => Prove p
prove @(p ==> q))
instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p)
instance {-# OVERLAPPING #-} Provable (p &&& q ==> p) where
prove :: Prove ((p &&& q) ==> p)
prove = forall {k1} (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> p @@ a
forall (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> p @@ a
projAndFst @p @q
instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q)
instance {-# OVERLAPPING #-} Provable (p &&& q ==> q) where
prove :: Prove ((p &&& q) ==> q)
prove = forall {k1} (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> q @@ a
forall (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> q @@ a
projAndSnd @p @q
instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p)
instance {-# OVERLAPPING #-} Provable (p &&& p ==> p) where
prove :: Prove ((p &&& p) ==> p)
prove = forall {k1} (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> p @@ a
forall (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> p @@ a
projAndFst @p @p
instance {-# OVERLAPPING #-} Decidable (p ==> p ||| q)
instance {-# OVERLAPPING #-} Provable (p ==> p ||| q) where
prove :: Prove (p ==> (p ||| q))
prove = forall {k} (p :: k ~> *) (q :: k ~> *) (a :: k).
Sing a -> (p @@ a) -> (p ||| q) @@ a
forall (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> (p @@ a) -> (p ||| q) @@ a
injOrLeft @p @q
instance {-# OVERLAPPING #-} Decidable (q ==> p ||| q)
instance {-# OVERLAPPING #-} Provable (q ==> p ||| q) where
prove :: Prove (q ==> (p ||| q))
prove = forall {k} (p :: Predicate k) (q :: Predicate k) (a :: k).
Sing a -> (q @@ a) -> (p ||| q) @@ a
forall (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> (q @@ a) -> (p ||| q) @@ a
injOrRight @p @q
instance {-# OVERLAPPING #-} Decidable (p ==> p ||| p)
instance {-# OVERLAPPING #-} Provable (p ==> p ||| p) where
prove :: Prove (p ==> (p ||| p))
prove = forall {k} (p :: k ~> *) (q :: k ~> *) (a :: k).
Sing a -> (p @@ a) -> (p ||| q) @@ a
forall (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> (p @@ a) -> (p ||| q) @@ a
injOrLeft @p @p
type Implies p q = Provable (p ==> q)
type Equiv p q = Provable (p <==> q)
proveImplies :: Prove q -> Prove (p ==> q)
proveImplies :: forall {k1} (q :: k1 ~> *) (p :: k1 ~> *).
Prove q -> Prove (p ==> q)
proveImplies Prove q
q Sing a
x Apply p a
_ = Sing a -> q @@ a
Prove q
q Sing a
x
type p <==> q = p ==> q &&& q ==> p
infixr 1 <==>
explosion :: Impossible --> p
explosion :: forall {k1} (p :: k1 ~> *) (a :: k1).
Sing a -> (Impossible @@ a) -> p @@ a
explosion Sing a
x Impossible @@ a
v = Void -> p @@ a
forall a. Void -> a
absurd (Void -> p @@ a) -> Void -> p @@ a
forall a b. (a -> b) -> a -> b
$ Impossible @@ a
Sing a -> Void
v Sing a
x
atom :: p --> Evident
atom :: forall {k1} (p :: k1 ~> *) (a :: k1).
Sing a -> (p @@ a) -> Evident @@ a
atom = Sing a -> Apply p a -> Sing a
Sing a -> Apply p a -> Apply Evident a
forall a b. a -> b -> a
const
complementation :: forall p. (p &&& Not p) --> Impossible
complementation :: forall {k1} (p :: Predicate k1) (a :: k1).
Sing a -> ((p &&& Not p) @@ a) -> Impossible @@ a
complementation Sing a
_ (Apply p a
p, Apply p a -> Void
notP) Sing a
_ = Apply p a -> Void
notP Apply p a
p
instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where
prove :: Prove ((p &&& Not p) ==> Impossible)
prove = forall {k1} (p :: Predicate k1) (a :: k1).
Sing a -> ((p &&& Not p) @@ a) -> Impossible @@ a
forall (p :: Predicate k1) (a :: k1).
Sing a -> ((p &&& Not p) @@ a) -> Impossible @@ a
complementation @p
contrapositive ::
(p --> q) ->
(Not q --> Not p)
contrapositive :: forall {k} (p :: k ~> *) (q :: k ~> *).
(p --> q) -> Not q --> Not p
contrapositive p --> q
f Sing a
x Not q @@ a
vQ Apply p a
p = Not q @@ a
Refuted (q @@ a)
vQ (Sing a -> Apply p a -> q @@ a
p --> q
f Sing a
x Apply p a
p)
contrapositive' ::
forall p q.
Decidable q =>
(Not q --> Not p) ->
(p --> q)
contrapositive' :: forall {k1} (p :: Predicate k1) (q :: Predicate k1).
Decidable q =>
(Not q --> Not p) -> p --> q
contrapositive' Not q --> Not p
f Sing a
x p @@ a
p = Decision (q @@ a) -> Refuted (Refuted (q @@ a)) -> q @@ a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @q Sing a
x) (Refuted (Refuted (q @@ a)) -> q @@ a)
-> Refuted (Refuted (q @@ a)) -> q @@ a
forall a b. (a -> b) -> a -> b
$ \Refuted (q @@ a)
vQ ->
Sing a -> (Not q @@ a) -> Not p @@ a
Not q --> Not p
f Sing a
x Not q @@ a
Refuted (q @@ a)
vQ p @@ a
p
doubleNegation :: forall p. Decidable p => Not (Not p) --> p
doubleNegation :: forall {k1} (p :: k1 ~> *). Decidable p => Not (Not p) --> p
doubleNegation Sing a
x Not (Not p) @@ a
vvP = Decision (p @@ a) -> Refuted (Refuted (p @@ a)) -> p @@ a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x) (Refuted (Refuted (p @@ a)) -> p @@ a)
-> Refuted (Refuted (p @@ a)) -> p @@ a
forall a b. (a -> b) -> a -> b
$ \Refuted (p @@ a)
vP ->
Not (Not p) @@ a
Refuted (Refuted (p @@ a))
vvP Refuted (p @@ a)
vP
tripleNegation :: forall p. Not (Not (Not p)) --> Not p
tripleNegation :: forall {k} (p :: Predicate k) (a :: k).
Sing a -> (Not (Not (Not p)) @@ a) -> Not p @@ a
tripleNegation Sing a
_ Not (Not (Not p)) @@ a
vvvP Apply p a
p = Not (Not (Not p)) @@ a
(Refuted (Apply p a) -> Void) -> Void
vvvP ((Refuted (Apply p a) -> Void) -> Void)
-> (Refuted (Apply p a) -> Void) -> Void
forall a b. (a -> b) -> a -> b
$ \Refuted (Apply p a)
vP -> Refuted (Apply p a)
vP Apply p a
p
negateTwice :: p --> Not (Not p)
negateTwice :: forall {k} (p :: k ~> *) (a :: k).
Sing a -> (p @@ a) -> Not (Not p) @@ a
negateTwice Sing a
_ p @@ a
p (p @@ a) -> Void
vP = (p @@ a) -> Void
vP p @@ a
p
projAndFst :: (p &&& q) --> p
projAndFst :: forall {k1} (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> p @@ a
projAndFst Sing a
_ = (Apply p a, Apply q a) -> Apply p a
Apply (p &&& q) a -> Apply p a
forall a b. (a, b) -> a
fst
projAndSnd :: (p &&& q) --> q
projAndSnd :: forall {k1} (p :: Predicate k1) (q :: Predicate k1) (a :: k1).
Sing a -> ((p &&& q) @@ a) -> q @@ a
projAndSnd Sing a
_ = (Apply p a, Apply q a) -> Apply q a
Apply (p &&& q) a -> Apply q a
forall a b. (a, b) -> b
snd
injOrLeft :: forall p q. p --> (p ||| q)
injOrLeft :: forall {k} (p :: k ~> *) (q :: k ~> *) (a :: k).
Sing a -> (p @@ a) -> (p ||| q) @@ a
injOrLeft Sing a
_ = Apply p a -> Either (Apply p a) (Apply q a)
Apply p a -> Apply (p ||| q) a
forall a b. a -> Either a b
Left
injOrRight :: forall p q. q --> (p ||| q)
injOrRight :: forall {k} (p :: Predicate k) (q :: Predicate k) (a :: k).
Sing a -> (q @@ a) -> (p ||| q) @@ a
injOrRight Sing a
_ = Apply q a -> Either (Apply p a) (Apply q a)
Apply q a -> Apply (p ||| q) a
forall a b. b -> Either a b
Right