{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}

-- |
-- Module      : OAlg.Data.Boolean.Proposition
-- Description : propositions on boolean structures.
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- propositions on boolean structures which must always be true, i.e. tautologies. They
-- serve also to describe the semantic of the boolean operators.
module OAlg.Data.Boolean.Proposition
  ( prpBool, prpBoolTautologies
  
    -- * Tautologies
  , prpTautologies
    
    -- ** Not
  , prpNotNot

    -- ** And
  , prpAndAssoc, prpAndOr, prpAndTrue, prpAnd0, prpAnds

    -- ** Or
  , prpOrAssoc, prpOrAnd, prpOr0, prpOrs

    -- * Impl
  , prpImplRefl, prpImplFalseEverything, prpImplCurry, prpImplTransitive

    -- * Eqvl
  , prpEqvlAnd

    -- * Lazy
  , prpLazy, prpLazyAnd, prpLazyOr, prpLazyImpl
  )
  where

import Prelude(IO,undefined)

import Control.Monad

import Data.List(take,repeat)

import OAlg.Category.Definition

import OAlg.Data.Canonical
import OAlg.Data.Number
import OAlg.Data.Boolean.Definition
import OAlg.Data.Statement.Definition
import OAlg.Data.X

--------------------------------------------------------------------------------
-- not -
-- | for all @p@ holds: @'not' ('not' p) '<~>' p@.
prpNotNot :: Boolean b => b -> b
prpNotNot :: forall b. Boolean b => b -> b
prpNotNot b
p = forall b. Boolean b => b -> b
not (forall b. Boolean b => b -> b
not b
p) forall b. Boolean b => b -> b -> b
<~> b
p

--------------------------------------------------------------------------------
-- and -

-- | for all @a@, @b@ and @c@ holds: @(a '&&' b) '&&' c '<~>' a '&&' (b '&&' c)@.
prpAndAssoc :: Boolean b => b -> b -> b -> b
prpAndAssoc :: forall b. Boolean b => b -> b -> b -> b
prpAndAssoc b
a b
b b
c = (b
a forall b. Boolean b => b -> b -> b
&& b
b) forall b. Boolean b => b -> b -> b
&& b
c forall b. Boolean b => b -> b -> b
<~> b
a forall b. Boolean b => b -> b -> b
&& (b
b forall b. Boolean b => b -> b -> b
&& b
c)

-- | for all @a@, @b@ and @c@ holds: @(a '&&' b) '||' c '<~>' (a '||' c) '&&' (b '||' c)@.
prpAndOr :: Boolean b => b -> b -> b -> b
prpAndOr :: forall b. Boolean b => b -> b -> b -> b
prpAndOr b
a b
b b
c = (b
a forall b. Boolean b => b -> b -> b
&& b
b) forall b. Boolean b => b -> b -> b
|| b
c forall b. Boolean b => b -> b -> b
<~> (b
a forall b. Boolean b => b -> b -> b
|| b
c) forall b. Boolean b => b -> b -> b
&& (b
b forall b. Boolean b => b -> b -> b
|| b
c)

-- | for all @p@ holds: @'true' '&&' p '<~>' p@.
prpAndTrue :: Boolean b => b -> b
prpAndTrue :: forall b. Boolean b => b -> b
prpAndTrue b
p = forall b. Boolean b => b
true forall b. Boolean b => b -> b -> b
&& b
p forall b. Boolean b => b -> b -> b
<~> b
p

-- | @'and' [] '<~>' 'true'@.
prpAnd0 :: Boolean b => b
prpAnd0 :: forall b. Boolean b => b
prpAnd0 = forall b. Boolean b => [b] -> b
and [] forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
true

-- | for all @a@ and @as@ holds: @'and' (a':'as) '<~>' a '&&' 'and' as@.
prpAnds :: Boolean b => b -> [b] -> b
prpAnds :: forall b. Boolean b => b -> [b] -> b
prpAnds b
a [b]
as = forall b. Boolean b => [b] -> b
and (b
aforall a. a -> [a] -> [a]
:[b]
as) forall b. Boolean b => b -> b -> b
<~> b
a forall b. Boolean b => b -> b -> b
&& forall b. Boolean b => [b] -> b
and [b]
as

-- | substituting equivalent boolenas in '&&' yiels equivalent booleans, i.e.
--   @for all @(a,a')@ and @(b,b')@ holds:
--   (a '<~>' a') '&&' (b '<~>' b') '~>' ((a '&&' b) '<~>' (a' '&&' b'))@.
prpAndSubs :: Boolean b => (b,b) -> (b,b) -> b
prpAndSubs :: forall b. Boolean b => (b, b) -> (b, b) -> b
prpAndSubs (b
a,b
a') (b
b,b
b') = (b
a forall b. Boolean b => b -> b -> b
<~> b
a') forall b. Boolean b => b -> b -> b
&& (b
b forall b. Boolean b => b -> b -> b
<~> b
b') forall b. Boolean b => b -> b -> b
~> ((b
a forall b. Boolean b => b -> b -> b
&& b
b) forall b. Boolean b => b -> b -> b
<~> (b
a' forall b. Boolean b => b -> b -> b
&& b
b'))

--------------------------------------------------------------------------------
-- Or -

-- | for all @a@, @b@ and @c@ holds: @(a '||' b) '||' c '<~>' a '||' (b '||' c)@.
prpOrAssoc :: Boolean  b => b -> b -> b -> b
prpOrAssoc :: forall b. Boolean b => b -> b -> b -> b
prpOrAssoc b
a b
b b
c = (b
a forall b. Boolean b => b -> b -> b
|| b
b) forall b. Boolean b => b -> b -> b
|| b
c forall b. Boolean b => b -> b -> b
<~> b
a forall b. Boolean b => b -> b -> b
|| (b
b forall b. Boolean b => b -> b -> b
|| b
c)

-- | for all @a@, @b@ and @c@ holds: @(a '||' b) '&&' c '<~>' (a '&&' c) '||' (b '&&' c)@.
prpOrAnd ::  Boolean b => b -> b -> b -> b
prpOrAnd :: forall b. Boolean b => b -> b -> b -> b
prpOrAnd b
a b
b b
c = (b
a forall b. Boolean b => b -> b -> b
|| b
b) forall b. Boolean b => b -> b -> b
&& b
c forall b. Boolean b => b -> b -> b
<~> (b
a forall b. Boolean b => b -> b -> b
&& b
c) forall b. Boolean b => b -> b -> b
|| (b
b forall b. Boolean b => b -> b -> b
&& b
c)

-- | for all @p@ holds:  @'false' '||' p '<~>' p@.
prpOrFalse :: Boolean b => b -> b
prpOrFalse :: forall b. Boolean b => b -> b
prpOrFalse b
p = forall b. Boolean b => b
false forall b. Boolean b => b -> b -> b
|| b
p forall b. Boolean b => b -> b -> b
<~> b
p

-- | @'or' [] '<~>' 'false'@.
prpOr0 :: Boolean b => b
prpOr0 :: forall b. Boolean b => b
prpOr0 = forall b. Boolean b => [b] -> b
or [] forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
false

-- | @for all @a@ and @as@ holds: 'or' (a':'as) '<~>' a '||' 'or' as@.
prpOrs :: Boolean b => b -> [b] -> b
prpOrs :: forall b. Boolean b => b -> [b] -> b
prpOrs b
a [b]
as = forall b. Boolean b => [b] -> b
or (b
aforall a. a -> [a] -> [a]
:[b]
as) forall b. Boolean b => b -> b -> b
<~> b
a forall b. Boolean b => b -> b -> b
|| forall b. Boolean b => [b] -> b
or [b]
as

--------------------------------------------------------------------------------
-- Impl -

-- | @for all @p@ holds: p '~>' p@.
prpImplRefl :: Boolean b => b -> b
prpImplRefl :: forall b. Boolean b => b -> b
prpImplRefl b
p = b
p forall b. Boolean b => b -> b -> b
~> b
p

-- | for all @p@ holds: @'false' '~>' (p '<~>' 'true')@.
--
--   i.e. a false premisis implies everithing.
prpImplFalseEverything :: Boolean b => b -> b
prpImplFalseEverything :: forall b. Boolean b => b -> b
prpImplFalseEverything b
p = forall b. Boolean b => b
false forall b. Boolean b => b -> b -> b
~> (b
p forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
true)

-- | for all @a@, @b@ and @c@ holds: @((a '&&' b) '~>' c) '<~>' (a '~>' b '~>' c)@.
prpImplCurry :: Boolean b => b -> b -> b -> b
prpImplCurry :: forall b. Boolean b => b -> b -> b -> b
prpImplCurry b
a b
b b
c = ((b
a forall b. Boolean b => b -> b -> b
&& b
b) forall b. Boolean b => b -> b -> b
~> b
c) forall b. Boolean b => b -> b -> b
<~> (b
a forall b. Boolean b => b -> b -> b
~> b
b forall b. Boolean b => b -> b -> b
~> b
c)

-- | for all @a@, @b@ and @c@ holds: @(a '~>' b) '&&' (b '~>' c) '~>' (a '~>' c)@. 
prpImplTransitive :: Boolean b => b -> b -> b -> b
prpImplTransitive :: forall b. Boolean b => b -> b -> b -> b
prpImplTransitive b
a b
b b
c = (b
a forall b. Boolean b => b -> b -> b
~> b
b) forall b. Boolean b => b -> b -> b
&& (b
b forall b. Boolean b => b -> b -> b
~> b
c) forall b. Boolean b => b -> b -> b
~> (b
a forall b. Boolean b => b -> b -> b
~> b
c)

--------------------------------------------------------------------------------
-- Eqvl -

-- | for all @a@ and @b@ holds: @(a '<~>' b) '<~>' ((a '~>' b) && (b '~>' a))@.
prpEqvlAnd :: Boolean b => b -> b -> b
prpEqvlAnd :: forall b. Boolean b => b -> b -> b
prpEqvlAnd b
a b
b = (b
a forall b. Boolean b => b -> b -> b
<~> b
b) forall b. Boolean b => b -> b -> b
<~> ((b
a forall b. Boolean b => b -> b -> b
~> b
b) forall b. Boolean b => b -> b -> b
&& (b
b forall b. Boolean b => b -> b -> b
~> b
a))

--------------------------------------------------------------------------------
-- lazy -

-- | lazy evaluation of '&&', i.e. @'false' '&&' 'undefined' '<~>' 'false'@.
--
--  __Note__ @('undefined' '&&' 'false')@ evaluates to an exception!
prpLazyAnd :: Boolean b => b
prpLazyAnd :: forall b. Boolean b => b
prpLazyAnd = forall b. Boolean b => b
false forall b. Boolean b => b -> b -> b
&& forall a. HasCallStack => a
undefined forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
false

-- | lazy evaluationof '||', i.e. @'true' '||' 'undefined'@.
prpLazyOr :: Boolean b => b
prpLazyOr :: forall b. Boolean b => b
prpLazyOr = forall b. Boolean b => b
true forall b. Boolean b => b -> b -> b
|| forall a. HasCallStack => a
undefined

-- | lazy evaluation of '~>', i.e. @'false' ':=>' 'undefined'@.
prpLazyImpl :: Boolean b => b
prpLazyImpl :: forall b. Boolean b => b
prpLazyImpl = forall b. Boolean b => b
false forall b. Boolean b => b -> b -> b
~> forall a. HasCallStack => a
undefined

--------------------------------------------------------------------------------
-- prpTautologies -

-- | tautologies on boolean structures.
prpTautologies :: Boolean b => (b -> Statement) -> X b -> X [b] -> Statement
prpTautologies :: forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies b -> Statement
prp X b
xb X [b]
xbs = String -> Label
Prp String
"Tautologies"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ -- Not
              String -> Label
Prp String
"NotNot" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall b. Boolean b => b -> b
prpNotNot)

              -- And
            , String -> Label
Prp String
"AndAssoc" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall b. Boolean b => b -> b -> b -> b
prpAndAssoc))
            , String -> Label
Prp String
"AndOr" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall b. Boolean b => b -> b -> b -> b
prpAndOr))
            , String -> Label
Prp String
"AndTrue" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall b. Boolean b => b -> b
prpAndTrue)
            , String -> Label
Prp String
"And0" Label -> Statement -> Statement
:<=>: b -> Statement
prp forall b. Boolean b => b
prpAnd0
            , String -> Label
Prp String
"Ands" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, [b])
xbbs (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b. Boolean b => b -> [b] -> b
prpAnds))

              -- Or
            , String -> Label
Prp String
"OrAssoc" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall b. Boolean b => b -> b -> b -> b
prpOrAssoc))
            , String -> Label
Prp String
"OrAnd" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall b. Boolean b => b -> b -> b -> b
prpOrAnd))
            , String -> Label
Prp String
"OrFalse" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall b. Boolean b => b -> b
prpOrFalse)
            , String -> Label
Prp String
"Or0" Label -> Statement -> Statement
:<=>: b -> Statement
prp forall b. Boolean b => b
prpOr0
            , String -> Label
Prp String
"Ors" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, [b])
xbbs (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b. Boolean b => b -> [b] -> b
prpOrs))

              -- Impl
            , String -> Label
Prp String
"ImplRefl" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall b. Boolean b => b -> b
prpImplRefl)
            , String -> Label
Prp String
"ImplFalseEverything" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall b. Boolean b => b -> b
prpImplFalseEverything)
            , String -> Label
Prp String
"ImplCurry" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall b. Boolean b => b -> b -> b -> b
prpImplCurry))
            , String -> Label
Prp String
"ImplTransitive" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall b. Boolean b => b -> b -> b -> b
prpImplTransitive))

              -- Eqvl
            , String -> Label
Prp String
"EqvlAnd" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b)
xab (b -> Statement
prp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b. Boolean b => b -> b -> b
prpEqvlAnd))
            ]
  where xab :: X (b, b)
xab  = forall a b. X a -> X b -> X (a, b)
xTupple2 X b
xb X b
xb
        xabc :: X (b, b, b)
xabc = forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X b
xb X b
xb X b
xb
        xbbs :: X (b, [b])
xbbs = forall a b. X a -> X b -> X (a, b)
xTupple2 X b
xb X [b]
xbs

--------------------------------------------------------------------------------
-- prpBoolTautologies -

-- | tautologies for 'Bool'.
prpBoolTautologies :: Statement
prpBoolTautologies :: Statement
prpBoolTautologies = String -> Label
Prp String
"BoolTautologies"
  Label -> Statement -> Statement
:<=>: forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies forall a b. Embeddable a b => a -> b
inj X Bool
xBool (forall x. N -> N -> X x -> X [x]
xTakeB N
0 N
10 X Bool
xBool)
  
--------------------------------------------------------------------------------
-- prpLazy -

-- | laziness of 'and', 'or' and @('~>')@.
prpLazy :: Boolean b => (b -> Statement) -> Statement
prpLazy :: forall b. Boolean b => (b -> Statement) -> Statement
prpLazy b -> Statement
prp = String -> Label
Prp String
"Lazy"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ String -> Label
Prp String
"LazyAnd" Label -> Statement -> Statement
:<=>: b -> Statement
prp forall b. Boolean b => b
prpLazyAnd
            , String -> Label
Prp String
"LazyOr" Label -> Statement -> Statement
:<=>: b -> Statement
prp forall b. Boolean b => b
prpLazyOr
            , String -> Label
Prp String
"LazyImpl" Label -> Statement -> Statement
:<=>: b -> Statement
prp forall b. Boolean b => b
prpLazyImpl
            ]
  
xbDst :: Int -> X Bool -> IO ()
xbDst :: Int -> X Bool -> IO ()
xbDst Int
n X Bool
xb = IO Omega
getOmega forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X Bool
xb

xabDst :: Int -> X Bool -> IO ()
xabDst :: Int -> X Bool -> IO ()
xabDst Int
n X Bool
xb = IO Omega
getOmega forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Bool, Bool)
xab where
  xab :: X (Bool, Bool)
xab = forall a b. X a -> X b -> X (a, b)
xTupple2 X Bool
xb X Bool
xb

xabcDst :: Int -> X Bool -> IO ()
xabcDst :: Int -> X Bool -> IO ()
xabcDst Int
n X Bool
xb = IO Omega
getOmega forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Bool, Bool, Bool)
xabc where
  xabc :: X (Bool, Bool, Bool)
xabc = forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X Bool
xb X Bool
xb X Bool
xb

xbbsDst :: Int -> Int -> X Bool -> IO ()
xbbsDst :: Int -> Int -> X Bool -> IO ()
xbbsDst Int
n Int
m X Bool
xb = IO Omega
getOmega forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Bool, [Bool])
xbbs where
  xbs :: X [Bool]
xbs  = Int -> Int -> X Int
xIntB Int
0 Int
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
n' -> forall x. [X x] -> X [x]
xList forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
n' forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a]
repeat X Bool
xb
  xbbs :: X (Bool, [Bool])
xbbs = forall a b. X a -> X b -> X (a, b)
xTupple2 X Bool
xb X [Bool]
xbs

--------------------------------------------------------------------------------
-- prpBool -

-- | validity of the 'Boolean' structure of 'Bool'.
prpBool :: Statement
prpBool :: Statement
prpBool = String -> Label
Prp String
"Bool"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpBoolTautologies
            , forall b. Boolean b => (b -> Statement) -> Statement
prpLazy (forall a b. Embeddable a b => a -> b
inj :: Bool -> Statement)
            ]