{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE TypeOperators       #-}

-- |
-- Module      : Data.Type.Predicate.Logic
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Logical and algebraic connectives for predicates, as well as common
-- logical combinators.
module Data.Type.Predicate.Logic (
  -- * Top and bottom
    Evident, Impossible
  -- * Logical connectives
  , type Not, decideNot
  , type (&&&), decideAnd
  , type (|||), decideOr, type (^||), type (||^)
  , type (^^^), decideXor
  , type (==>), proveImplies, Implies
  , type (<==>), Equiv
  -- * Logical deductions
  , compImpl, explosion, atom
  , complementation, doubleNegation, tripleNegation, negateTwice
  , contrapositive, contrapositive'
  -- ** Lattice
  , projAndFst, projAndSnd, injOrLeft, injOrRight
  ) where

import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Type.Predicate
import           Data.Void

-- | @p '&&&' q@ is a predicate that both @p@ and @q@ are true.
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)
decideAnd @p @q @a (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x) (forall {k1} (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
prove @p Sing a
x, forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @q Sing a
x)

-- | Decide @p '&&&' q@ based on decisions of @p@ and @q@.
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    -> forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (p @@ a
p,) forall a b. (a, b) -> b
snd
    Disproved Refuted (p @@ a)
v -> \Decision (q @@ a)
_ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \(p @@ a
p, q @@ a
_) -> Refuted (p @@ a)
v p @@ a
p

-- | @p '|||' q@ is a predicate that either @p@ and @q@ are true.
data (|||) :: Predicate k -> Predicate k -> Predicate k
type instance Apply (p ||| q) a = Either (p @@ a) (q @@ a)
infixr 2 |||

-- | Prefers @p@ over @q@.
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)
decideOr @p @q @a (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x) (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @q Sing a
x)

-- | Decide @p '|||' q@ based on decisions of @p@ and @q@.
--
-- Prefers @p@ over @q@.
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)
_ -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left p @@ a
p
    Disproved Refuted (p @@ a)
v -> forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision forall a b. b -> Either a b
Right (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refuted (p @@ a)
v) forall a. a -> a
id)

-- | Left-biased "or".  In proofs, prioritize a proof of the left side over
-- a proof of the right side.
--
-- @since 0.1.2.0
type p ^|| q = p ||| Not p &&& q

-- | Right-biased "or".  In proofs, prioritize a proof of the right side over
-- a proof of the left side.
--
-- @since 0.1.2.0
type p ||^ q = p &&& Not q ||| q

-- | @p '^^^' q@ is a predicate that either @p@ and @q@ are true, but not
-- both.
type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)

-- | Decide @p '^^^' q@ based on decisions of @p@ and @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)
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)
decideAnd @p @(Not q) @a Decision (p @@ a)
p (forall {k1} (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)
decideAnd @(Not p) @q @a (forall {k1} (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @p @a Decision (p @@ a)
p) Decision (q @@ a)
q)

-- | @p ==> q@ is true if @q@ is provably true under the condition that @p@
-- is true.
data (==>) :: Predicate k -> Predicate k -> Predicate k
type instance Apply (p ==> q) a = p @@ a -> q @@ a

infixr 1 ==>

instance Decidable (Impossible ==> p) where
instance Provable (Impossible ==> p) where
    prove :: Prove (Impossible ==> p)
prove = forall {k1} (p :: k1 ~> *). Impossible --> p
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
decide @(p ==> q) Sing a
x of
      Proved (p ==> q) @@ a
pq     -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ \Apply q a -> Void
vq Apply p a
p -> Apply q a -> Void
vq ((p ==> q) @@ a
pq Apply p a
p)
      Disproved Refuted ((p ==> q) @@ a)
vpq -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @q Sing a
x of
        Proved    Apply q a
q  -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \(Not q ==> Not p) @@ a
_     -> Refuted ((p ==> q) @@ a)
vpq (forall a b. a -> b -> a
const Apply q a
q)
        Disproved Apply q a -> Void
vq -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \(Not q ==> Not p) @@ a
vnpnq -> Refuted ((p ==> q) @@ a)
vpq (forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Not q ==> Not p) @@ a
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
contrapositive @p @q (forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @(p ==> q))

-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p) where
-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Provable (p &&& q ==> p) where
    prove :: Prove ((p &&& q) ==> p)
prove = forall {k1} (p :: Predicate k1) (q :: Predicate k1).
(p &&& q) --> p
projAndFst @p @q

-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q) where
-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Provable (p &&& q ==> q) where
    prove :: Prove ((p &&& q) ==> q)
prove = forall {k1} (p :: Predicate k1) (q :: Predicate k1).
(p &&& q) --> q
projAndSnd @p @q

-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p) where
-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Provable (p &&& p ==> p) where
    prove :: Prove ((p &&& p) ==> p)
prove = forall {k1} (p :: Predicate k1) (q :: Predicate k1).
(p &&& q) --> p
projAndFst @p @p

-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Decidable (p ==> p ||| q)
-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Provable (p ==> p ||| q) where
    prove :: Prove (p ==> (p ||| q))
prove = forall {k} (p :: k ~> *) (q :: k ~> *). p --> (p ||| q)
injOrLeft @p @q

-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Decidable (q ==> p ||| q)
-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Provable (q ==> p ||| q) where
    prove :: Prove (q ==> (p ||| q))
prove = forall {k} (p :: Predicate k) (q :: Predicate k). q --> (p ||| q)
injOrRight @p @q

-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Decidable (p ==> p ||| p)
-- | @since 0.1.1.0
instance {-# OVERLAPPING #-} Provable (p ==> p ||| p) where
    prove :: Prove (p ==> (p ||| p))
prove = forall {k} (p :: k ~> *) (q :: k ~> *). p --> (p ||| q)
injOrLeft @p @p

-- | @'Implies' p q@ is a constraint that @p '==>' q@ is 'Provable'; that
-- is, you can prove that @p@ implies @q@.
type Implies  p q = Provable  (p ==> q)

-- | @'Equiv' p q@ is a constraint that @p '<==>' q@ is 'Provable'; that
-- is, you can prove that @p@ is logically equivalent to @q@.
type Equiv  p q = Provable  (p <==> q)

-- | If @q@ is provable, then so is @p '==>' q@.
--
-- This can be used as an easy plug-in 'Provable' instance for @p '==>' q@
-- if @q@ is 'Provable':
--
-- @
-- instance Provable (p ==> MyPred) where
--     prove = proveImplies @MyPred
-- @
--
-- This instance isn't provided polymorphically because of overlapping
-- instance issues.
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
_ = Prove q
q Sing a
x

-- | Two-way implication, or logical equivalence
type (p <==> q) = p ==> q &&& q ==> p
infixr 1 <==>

-- | From @'Impossible' @@ a@, you can prove anything.  Essentially
-- a lifted version of 'absurd'.
explosion :: Impossible --> p
explosion :: forall {k1} (p :: k1 ~> *). Impossible --> p
explosion Sing a
x Impossible @@ a
v = forall a. Void -> a
absurd forall a b. (a -> b) -> a -> b
$ Impossible @@ a
v Sing a
x

-- | 'Evident' can be proven from all predicates.
atom :: p --> Evident
atom :: forall {k1} (p :: k1 ~> *). p --> Evident
atom = forall a b. a -> b -> a
const

-- | We cannot have both @p@ and @'Not' p@.
--
-- (Renamed in v0.1.4.0; used to be @excludedMiddle@)
--
-- @since 0.1.4.0
complementation :: forall p. (p &&& Not p) --> Impossible
complementation :: forall {k1} (p :: Predicate k1). (p &&& Not p) --> Impossible
complementation Sing a
_ (Apply p a
p, Apply p a -> Void
notP) Sing a
_ = Apply p a -> Void
notP Apply p a
p

-- | @since 0.1.3.0
instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where
    prove :: Prove ((p &&& Not p) ==> Impossible)
prove = forall {k1} (p :: Predicate k1). (p &&& Not p) --> Impossible
complementation @p

-- | If p implies q, then not q implies not 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
vQ (p --> q
f Sing a
x Apply p a
p)

-- | Reverse direction of 'contrapositive'.  Only possible if @q@ is
-- 'Decidable' on its own, without the help of @p@, which makes this much
-- less useful.
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 = forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @q Sing a
x) forall a b. (a -> b) -> a -> b
$ \Refuted (q @@ a)
vQ ->
    Not q --> Not p
f Sing a
x Refuted (q @@ a)
vQ p @@ a
p

-- | Logical double negation.  Only possible if @p@ is 'Decidable'.
--
-- This is because in constructivist logic, not (not p) does not imply p.
-- However, p implies not (not p) (see 'negateTwice'), and not (not (not
-- p)) implies not p (see 'tripleNegation')
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 = forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x) forall a b. (a -> b) -> a -> b
$ \Refuted (p @@ a)
vP ->
    Not (Not p) @@ a
vvP Refuted (p @@ a)
vP

-- | In constructivist logic, not (not (not p)) implies not p.
--
-- @since 0.1.4.0
tripleNegation :: forall p. Not (Not (Not p)) --> Not p
tripleNegation :: forall {k} (p :: Predicate k). Not (Not (Not p)) --> Not p
tripleNegation Sing a
_ Not (Not (Not p)) @@ a
vvvP Apply p a
p = Not (Not (Not p)) @@ a
vvvP forall a b. (a -> b) -> a -> b
$ \Apply p a -> Void
vP -> Apply p a -> Void
vP Apply p a
p

-- | In constructivist logic, p implies not (not p).
--
-- @since 0.1.4.0
negateTwice :: p --> Not (Not p)
negateTwice :: forall {k} (p :: k ~> *). p --> Not (Not p)
negateTwice Sing a
_ p @@ a
p (p @@ a) -> Void
vP = (p @@ a) -> Void
vP p @@ a
p

-- | If @p '&&&' q@ is true, then so is @p@.
projAndFst :: (p &&& q) --> p
projAndFst :: forall {k1} (p :: Predicate k1) (q :: Predicate k1).
(p &&& q) --> p
projAndFst Sing a
_ = forall a b. (a, b) -> a
fst

-- | If @p '&&&' q@ is true, then so is @q@.
projAndSnd :: (p &&& q) --> q
projAndSnd :: forall {k1} (p :: Predicate k1) (q :: Predicate k1).
(p &&& q) --> q
projAndSnd Sing a
_ = forall a b. (a, b) -> b
snd

-- | If @p@ is true, then so is @p '|||' q@.
injOrLeft :: forall p q. p --> (p ||| q)
injOrLeft :: forall {k} (p :: k ~> *) (q :: k ~> *). p --> (p ||| q)
injOrLeft Sing a
_ = forall a b. a -> Either a b
Left

-- | If @q@ is true, then so is @p '|||' q@.
injOrRight :: forall p q. q --> (p ||| q)
injOrRight :: forall {k} (p :: Predicate k) (q :: Predicate k). q --> (p ||| q)
injOrRight Sing a
_ = forall a b. b -> Either a b
Right