{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module      : Data.Type.Predicate.Quantification
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Higher-level predicates for quantifying predicates over universes and
-- sets.
module Data.Type.Predicate.Quantification (
  -- * Any
  Any,
  WitAny (..),
  None,
  anyImpossible,

  -- ** Decision
  decideAny,
  idecideAny,
  decideNone,
  idecideNone,

  -- ** Entailment
  entailAny,
  ientailAny,
  entailAnyF,
  ientailAnyF,

  -- * All
  All,
  WitAll (..),
  NotAll,

  -- ** Decision
  decideAll,
  idecideAll,

  -- ** Entailment
  entailAll,
  ientailAll,
  entailAllF,
  ientailAllF,
  decideEntailAll,
  idecideEntailAll,

  -- * Logical interplay
  allToAny,
  allNotNone,
  noneAllNot,
  anyNotNotAll,
  notAllAnyNot,
) where

import Data.Kind
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Universe

-- | 'decideNone', but providing an 'Elem'.
idecideNone ::
  forall f k (p :: k ~> Type) (as :: f k).
  Universe f =>
  -- | predicate on value
  (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
  -- | predicate on collection
  (Sing as -> Decision (None f p @@ as))
idecideNone :: forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (None f p @@ as)
idecideNone forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f Sing as
xs = forall {k1} (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
forall (p :: f k ~> *) (a :: f k).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @(Any f p) (Decision (Any f p @@ as) -> Decision (Apply (Not (Any f p)) as))
-> Decision (Any f p @@ as) -> Decision (Apply (Not (Any f p)) as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny Elem f as a -> Sing a -> Decision (p @@ a)
forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f Sing as
xs

-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
-- a collection @as@ that is true if and only if /no/ item in @as@
-- satisfies the original predicate.
--
-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
-- of kind @f k ~> Type@.
decideNone ::
  forall f k (p :: k ~> Type).
  Universe f =>
  -- | predicate on value
  Decide p ->
  -- | predicate on collection
  Decide (None f p)
decideNone :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (None f p)
decideNone Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Not (Any f p)) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (None f p @@ as)
idecideNone ((Sing a -> Decision (Apply p a))
-> Elem f a a -> Sing a -> Decision (Apply p a)
forall a b. a -> b -> a
const Sing a -> Decision (Apply p a)
Decide p
f)

-- | 'entailAny', but providing an 'Elem'.
ientailAny ::
  forall f p q as.
  (Universe f, SingI as) =>
  -- | implication
  (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) ->
  Any f p @@ as ->
  Any f q @@ as
ientailAny :: forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k).
(Universe f, SingI as) =>
(forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a)
-> (Any f p @@ as) -> Any f q @@ as
ientailAny forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f (WitAny Elem f as a1
i p @@ a1
x) = Elem f as a1 -> (q @@ a1) -> WitAny f q as
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f as a1
i (Elem f as a1 -> Sing a1 -> (p @@ a1) -> q @@ a1
forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f Elem f as a1
i (Elem f as a1 -> Sing as -> Sing a1
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a1
i Sing as
forall {k} (a :: k). SingI a => Sing a
sing) p @@ a1
x)

-- | If there exists an @a@ s.t. @p a@, and if @p@ implies @q@, then there
-- must exist an @a@ s.t. @q a@.
entailAny ::
  forall f p q.
  Universe f =>
  (p --> q) ->
  (Any f p --> Any f q)
entailAny :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *).
Universe f =>
(p --> q) -> Any f p --> Any f q
entailAny = forall {k1} {k2} (f :: (k1 ~> *) -> k2 ~> *) (p :: k1 ~> *)
       (q :: k1 ~> *).
TFunctor f =>
(p --> q) -> f p --> f q
forall (f :: (k ~> *) -> f k ~> *) (p :: k ~> *) (q :: k ~> *).
TFunctor f =>
(p --> q) -> f p --> f q
tmap @(Any f)

-- | 'entailAll', but providing an 'Elem'.
ientailAll ::
  forall f p q as.
  (Universe f, SingI as) =>
  -- | implication
  (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) ->
  All f p @@ as ->
  All f q @@ as
ientailAll :: forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k).
(Universe f, SingI as) =>
(forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a)
-> (All f p @@ as) -> All f q @@ as
ientailAll forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f All f p @@ as
a = (forall (a :: k). Elem f as a -> q @@ a) -> WitAll f q as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem f as a -> q @@ a) -> WitAll f q as)
-> (forall (a :: k). Elem f as a -> q @@ a) -> WitAll f q as
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i -> Elem f as a -> Sing a -> (p @@ a) -> q @@ a
forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f Elem f as a
i (Elem f as a -> Sing as -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i Sing as
forall {k} (a :: k). SingI a => Sing a
sing) (WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ as
WitAll f p as
a Elem f as a
i)

-- | If for all @a@ we have @p a@, and if @p@ implies @q@, then for all @a@
-- we must also have @p a@.
entailAll ::
  forall f p q.
  Universe f =>
  (p --> q) ->
  (All f p --> All f q)
entailAll :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *).
Universe f =>
(p --> q) -> All f p --> All f q
entailAll = forall {k1} {k2} (f :: (k1 ~> *) -> k2 ~> *) (p :: k1 ~> *)
       (q :: k1 ~> *).
TFunctor f =>
(p --> q) -> f p --> f q
forall (f :: (k ~> *) -> f k ~> *) (p :: k ~> *) (q :: k ~> *).
TFunctor f =>
(p --> q) -> f p --> f q
tmap @(All f)

-- | 'entailAnyF', but providing an 'Elem'.
ientailAnyF ::
  forall f p q as h.
  Functor h =>
  -- | implication in context
  (forall a. Elem f as a -> p @@ a -> h (q @@ a)) ->
  Any f p @@ as ->
  h (Any f q @@ as)
ientailAnyF :: forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k) (h :: * -> *).
Functor h =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (Any f p @@ as) -> h (Any f q @@ as)
ientailAnyF forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f = \case WitAny Elem f as a1
i p @@ a1
x -> Elem f as a1 -> Apply q a1 -> WitAny f q as
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f as a1
i (Apply q a1 -> WitAny f q as)
-> h (Apply q a1) -> h (WitAny f q as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem f as a1 -> (p @@ a1) -> h (Apply q a1)
forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f Elem f as a1
i p @@ a1
x

-- | If @p@ implies @q@ under some context @h@, and if there exists some
-- @a@ such that @p a@, then there must exist some @a@ such that @p q@
-- under that context @h@.
--
-- @h@ might be something like, say, 'Maybe', to give predicate that is
-- either provably true or unprovably false.
--
-- Note that it is not possible to do this with @p a -> 'Decision' (q a)@.
-- This is if the @p a -> 'Decision' (q a)@ implication is false, there
-- it doesn't mean that there is /no/ @a@ such that @q a@, necessarily.
-- There could have been an @a@ where @p@ does not hold, but @q@ does.
entailAnyF ::
  forall f p q h.
  (Universe f, Functor h) =>
  -- | implication in context
  (p --># q) h ->
  (Any f p --># Any f q) h
entailAnyF :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *) (h :: * -> *).
(Universe f, Functor h) =>
(-->#) p q h -> (-->#) (Any f p) (Any f q) h
entailAnyF (-->#) p q h
f Sing a
x Any f p @@ a
a =
  Sing a -> (SingI a => h (Any f q @@ a)) -> h (Any f q @@ a)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
x ((SingI a => h (Any f q @@ a)) -> h (Any f q @@ a))
-> (SingI a => h (Any f q @@ a)) -> h (Any f q @@ a)
forall a b. (a -> b) -> a -> b
$
    forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k) (h :: * -> *).
Functor h =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (Any f p @@ as) -> h (Any f q @@ as)
forall (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k) (h :: * -> *).
Functor h =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (Any f p @@ as) -> h (Any f q @@ as)
ientailAnyF @f @p @q (\Elem f a a
i -> Sing a -> (p @@ a) -> h (q @@ a)
(-->#) p q h
f (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
x)) Any f p @@ a
a

-- | 'entailAllF', but providing an 'Elem'.
ientailAllF ::
  forall f p q as h.
  (Universe f, Applicative h, SingI as) =>
  -- | implication in context
  (forall a. Elem f as a -> p @@ a -> h (q @@ a)) ->
  All f p @@ as ->
  h (All f q @@ as)
ientailAllF :: forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k) (h :: * -> *).
(Universe f, Applicative h, SingI as) =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (All f p @@ as) -> h (All f q @@ as)
ientailAllF forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f All f p @@ as
a =
  (Prod f (Wit q) as -> WitAll f q as)
-> h (Prod f (Wit q) as) -> h (WitAll f q as)
forall a b. (a -> b) -> h a -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (a :: k). Wit q a -> q @@ a)
-> Prod f (Wit q) as -> Apply (All f q) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *)
       (as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll Wit q a -> q @@ a
forall (a :: k). Wit q a -> q @@ a
forall {k1} (p :: k1 ~> *) (a :: k1). Wit p a -> p @@ a
getWit)
    (h (Prod f (Wit q) as) -> h (Apply (All f q) as))
-> (Prod f Sing as -> h (Prod f (Wit q) as))
-> Prod f Sing as
-> h (Apply (All f q) as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Elem f as a -> Sing a -> h (Wit q a))
-> Prod f Sing as -> h (Prod f (Wit q) as)
forall {k} (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
       (h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd (\Elem f as a
i Sing a
_ -> forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
forall (p :: k ~> *) (a :: k). (p @@ a) -> Wit p a
Wit @q ((q @@ a) -> Wit q a) -> h (q @@ a) -> h (Wit q a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem f as a -> (p @@ a) -> h (q @@ a)
forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f Elem f as a
i (WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ as
WitAll f p as
a Elem f as a
i))
    (Prod f Sing as -> h (Apply (All f q) as))
-> Prod f Sing as -> h (Apply (All f q) as)
forall a b. (a -> b) -> a -> b
$ Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd (forall (a :: f k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as)

-- | If @p@ implies @q@ under some context @h@, and if we have @p a@ for
-- all @a@, then we must have @q a@ for all @a@ under context @h@.
entailAllF ::
  forall f p q h.
  (Universe f, Applicative h) =>
  -- | implication in context
  (p --># q) h ->
  (All f p --># All f q) h
entailAllF :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *) (h :: * -> *).
(Universe f, Applicative h) =>
(-->#) p q h -> (-->#) (All f p) (All f q) h
entailAllF (-->#) p q h
f Sing a
x All f p @@ a
a =
  Sing a -> (SingI a => h (All f q @@ a)) -> h (All f q @@ a)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
x ((SingI a => h (All f q @@ a)) -> h (All f q @@ a))
-> (SingI a => h (All f q @@ a)) -> h (All f q @@ a)
forall a b. (a -> b) -> a -> b
$
    forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k) (h :: * -> *).
(Universe f, Applicative h, SingI as) =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (All f p @@ as) -> h (All f q @@ as)
forall (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k) (h :: * -> *).
(Universe f, Applicative h, SingI as) =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (All f p @@ as) -> h (All f q @@ as)
ientailAllF @f @p @q (\Elem f a a
i -> Sing a -> (p @@ a) -> h (q @@ a)
(-->#) p q h
f (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
x)) All f p @@ a
a

-- | 'entailAllF', but providing an 'Elem'.
idecideEntailAll ::
  forall f p q as.
  (Universe f, SingI as) =>
  -- | decidable implication
  (forall a. Elem f as a -> p @@ a -> Decision (q @@ a)) ->
  All f p @@ as ->
  Decision (All f q @@ as)
idecideEntailAll :: forall {k} (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
       (as :: f k).
(Universe f, SingI as) =>
(forall (a :: k). Elem f as a -> (p @@ a) -> Decision (q @@ a))
-> (All f p @@ as) -> Decision (All f q @@ as)
idecideEntailAll forall (a :: k). Elem f as a -> (p @@ a) -> Decision (q @@ a)
f All f p @@ as
a = (forall (a :: k). Elem f as a -> Sing a -> Decision (q @@ a))
-> Sing as -> Decision (Apply (All f q) as)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll (\Elem f as a
i Sing a
_ -> Elem f as a -> (p @@ a) -> Decision (q @@ a)
forall (a :: k). Elem f as a -> (p @@ a) -> Decision (q @@ a)
f Elem f as a
i (WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ as
WitAll f p as
a Elem f as a
i)) Sing as
forall {k} (a :: k). SingI a => Sing a
sing

-- | If we have @p a@ for all @a@, and @p a@ can be used to test for @q a@,
-- then we can test all @a@s for @q a@.
decideEntailAll ::
  forall f p q.
  Universe f =>
  p -?> q ->
  All f p -?> All f q
decideEntailAll :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *).
Universe f =>
(p -?> q) -> All f p -?> All f q
decideEntailAll = forall {k1} {k2} (f :: (k1 ~> *) -> k2 ~> *) (p :: k1 ~> *)
       (q :: k1 ~> *).
DFunctor f =>
(p -?> q) -> f p -?> f q
forall (f :: (k ~> *) -> f k ~> *) (p :: k ~> *) (q :: k ~> *).
DFunctor f =>
(p -?> q) -> f p -?> f q
dmap @(All f)

-- | It is impossible for any value in a collection to be 'Impossible'.
--
-- @since 0.1.2.0
anyImpossible :: Universe f => Any f Impossible --> Impossible
anyImpossible :: forall {k} (f :: * -> *).
Universe f =>
Any f Impossible --> Impossible
anyImpossible Sing a
_ (WitAny Elem f a a1
i Impossible @@ a1
p) = Impossible @@ a1
Sing a1 -> Void
p (Sing a1 -> Void) -> (Sing a -> Sing a1) -> Sing a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f a a1 -> Sing a -> Sing a1
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a1
i

-- | If any @a@ in @as@ does not satisfy @p@, then not all @a@ in @as@
-- satisfy @p@.
--
-- @since 0.1.2.0
anyNotNotAll :: Any f (Not p) --> NotAll f p
anyNotNotAll :: forall {k} (f :: * -> *) (p :: Predicate k) (a :: f k).
Sing a -> (Any f (Not p) @@ a) -> NotAll f p @@ a
anyNotNotAll Sing a
_ (WitAny Elem f a a1
i Not p @@ a1
v) WitAll f p a
a = Not p @@ a1
Refuted (p @@ a1)
v Refuted (p @@ a1) -> Refuted (p @@ a1)
forall a b. (a -> b) -> a -> b
$ WitAll f p a -> forall (a :: k). Elem f a a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll f p a
a Elem f a a1
i

-- | If not all @a@ in @as@ satisfy @p@, then there must be at least one
-- @a@ in @as@ that does not satisfy @p@.  Requires @'Decidable' p@ in
-- order to locate that specific @a@.
--
-- @since 0.1.2.0
notAllAnyNot ::
  forall f p.
  (Universe f, Decidable p) =>
  NotAll f p --> Any f (Not p)
notAllAnyNot :: forall {k} (f :: * -> *) (p :: k ~> *).
(Universe f, Decidable p) =>
NotAll f p --> Any f (Not p)
notAllAnyNot Sing a
xs NotAll f p @@ a
vAll = Decision (Any f (Not p) @@ a)
-> Refuted (Refuted (Any f (Not p) @@ a)) -> Any f (Not p) @@ a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: f k ~> *). Decidable p => Decide p
decide @(Any f (Not p)) Sing a
xs) (Refuted (Refuted (Any f (Not p) @@ a)) -> Any f (Not p) @@ a)
-> Refuted (Refuted (Any f (Not p) @@ a)) -> Any f (Not p) @@ a
forall a b. (a -> b) -> a -> b
$ \Refuted (Any f (Not p) @@ a)
vAny ->
  NotAll f p @@ a
WitAll f p a -> Void
vAll (WitAll f p a -> Void) -> WitAll f p a -> Void
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem f a a -> p @@ a) -> WitAll f p a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem f a a -> p @@ a) -> WitAll f p a)
-> (forall (a :: k). Elem f a a -> p @@ a) -> WitAll f p a
forall a b. (a -> b) -> a -> b
$ \Elem f a a
i ->
    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 :: k ~> *). Decidable p => Decide p
decide @p (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs)) (Refuted (Refuted (p @@ a)) -> p @@ a)
-> Refuted (Refuted (p @@ a)) -> p @@ a
forall a b. (a -> b) -> a -> b
$ \Refuted (p @@ a)
vP ->
      Refuted (Any f (Not p) @@ a)
vAny Refuted (Any f (Not p) @@ a) -> Refuted (Any f (Not p) @@ a)
forall a b. (a -> b) -> a -> b
$ Elem f a a -> (Not p @@ a) -> WitAny f (Not p) a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a a
i Not p @@ a
Refuted (p @@ a)
vP

-- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies
-- @p@.
--
-- @since 0.1.2.0
allNotNone :: All f (Not p) --> None f p
allNotNone :: forall {k} (f :: * -> *) (p :: Predicate k) (a :: f k).
Sing a -> (All f (Not p) @@ a) -> None f p @@ a
allNotNone Sing a
_ All f (Not p) @@ a
a (WitAny Elem f a a1
i p @@ a1
v) = WitAll f (Not p) a -> forall (a :: k). Elem f a a -> Not p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f (Not p) @@ a
WitAll f (Not p) a
a Elem f a a1
i p @@ a1
v

-- | If no @a@ in @as@ satisfies @p@, then @p@ is false for all @a@ in
-- @as@.  Requires @'Decidable' p@ to interrogate the input disproof.
--
-- @since 0.1.2.0
noneAllNot ::
  forall f p.
  (Universe f, Decidable p) =>
  None f p --> All f (Not p)
noneAllNot :: forall {k} (f :: * -> *) (p :: k ~> *).
(Universe f, Decidable p) =>
None f p --> All f (Not p)
noneAllNot Sing a
xs None f p @@ a
vAny = Decision (All f (Not p) @@ a)
-> Refuted (Refuted (All f (Not p) @@ a)) -> All f (Not p) @@ a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: f k ~> *). Decidable p => Decide p
decide @(All f (Not p)) Sing a
xs) (Refuted (Refuted (All f (Not p) @@ a)) -> All f (Not p) @@ a)
-> Refuted (Refuted (All f (Not p) @@ a)) -> All f (Not p) @@ a
forall a b. (a -> b) -> a -> b
$ \Refuted (All f (Not p) @@ a)
vAll ->
  Refuted (All f (Not p) @@ a)
vAll Refuted (All f (Not p) @@ a) -> Refuted (All f (Not p) @@ a)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem f a a -> Not p @@ a) -> WitAll f (Not p) a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem f a a -> Not p @@ a) -> WitAll f (Not p) a)
-> (forall (a :: k). Elem f a a -> Not p @@ a)
-> WitAll f (Not p) a
forall a b. (a -> b) -> a -> b
$ \Elem f a a
i Apply p a
p -> None f p @@ a
WitAny f p a -> Void
vAny (WitAny f p a -> Void) -> WitAny f p a -> Void
forall a b. (a -> b) -> a -> b
$ Elem f a a -> Apply p a -> WitAny f p a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a a
i Apply p a
p

-- | If something is true for all xs, then it must be true for at least one
-- x in xs, provided that xs is not empty.
--
-- @since 0.1.5.0
allToAny :: (All f p &&& NotNull f) --> Any f p
allToAny :: forall {k} (f :: * -> *) (p :: Predicate k) (a :: f k).
Sing a -> ((All f p &&& NotNull f) @@ a) -> Any f p @@ a
allToAny Sing a
_ (WitAll f p a
a, WitAny Elem f a a1
i Evident @@ a1
_) = Elem f a a1 -> (p @@ a1) -> WitAny f p a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a a1
i ((p @@ a1) -> WitAny f p a) -> (p @@ a1) -> WitAny f p a
forall a b. (a -> b) -> a -> b
$ WitAll f p a -> forall (a :: k). Elem f a a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll f p a
a Elem f a a1
i