{- HLINT ignore -}
{-|
Module      : Interval Algebra Axioms
Description : Properties of Intervals
Copyright   : (c) NoviSci, Inc 2020
License     : BSD3
Maintainer  : bsaul@novisci.com

This module exports a single typeclass @IntervalAxioms@ which contains
property-based tests for the axioms in section 1 of [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x).
The notation below is that of the original paper.

This module is useful if creating a new instance of interval types that you want to test.

-}

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}


module IntervalAlgebra.Axioms
  ( IntervalAxioms(..)
  , M1set(..)
  , M2set(..)
  , M5set(..)
  ) where

import           Data.Either               (isRight)
import           Data.Maybe                (fromJust, isJust, isNothing)
import           Data.Set                  (Set, disjointUnion, fromList,
                                            member)
import           Data.Time                 as DT (Day (..), DiffTime,
                                                  NominalDiffTime, UTCTime (..))
import           IntervalAlgebra.Arbitrary
import           IntervalAlgebra.Core
import           Test.QuickCheck           (Arbitrary (arbitrary), Property,
                                            (===), (==>))


xor :: Bool -> Bool -> Bool
xor :: Bool -> Bool -> Bool
xor Bool
a Bool
b = Bool
a forall a. Eq a => a -> a -> Bool
/= Bool
b

-- | Internal function for converting a number to a strictly positive value.
makePos :: (Ord b, Num b) => b -> b
makePos :: forall b. (Ord b, Num b) => b -> b
makePos b
x | b
x forall a. Eq a => a -> a -> Bool
== b
0    = b
x forall a. Num a => a -> a -> a
+ b
1
          | b
x forall a. Ord a => a -> a -> Bool
< b
0     = forall a. Num a => a -> a
negate b
x
          | Bool
otherwise = b
x

-- | A set used for testing M1 defined so that the M1 condition is true.
data M1set a = M1set
  { forall a. M1set a -> Interval a
m11 :: Interval a
  , forall a. M1set a -> Interval a
m12 :: Interval a
  , forall a. M1set a -> Interval a
m13 :: Interval a
  , forall a. M1set a -> Interval a
m14 :: Interval a
  }
  deriving Int -> M1set a -> ShowS
forall a. (Show a, Ord a) => Int -> M1set a -> ShowS
forall a. (Show a, Ord a) => [M1set a] -> ShowS
forall a. (Show a, Ord a) => M1set a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M1set a] -> ShowS
$cshowList :: forall a. (Show a, Ord a) => [M1set a] -> ShowS
show :: M1set a -> String
$cshow :: forall a. (Show a, Ord a) => M1set a -> String
showsPrec :: Int -> M1set a -> ShowS
$cshowsPrec :: forall a. (Show a, Ord a) => Int -> M1set a -> ShowS
Show

instance Arbitrary (M1set Int) where
  arbitrary :: Gen (M1set Int)
arbitrary = do
    Interval Int
x <- forall a. Arbitrary a => Gen a
arbitrary
    Int
a <- forall a. Arbitrary a => Gen a
arbitrary
    Int
b <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> b -> M1set a
m1set Interval Int
x Int
a Int
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M1set DT.Day) where
  arbitrary :: Gen (M1set Day)
arbitrary = do
    Interval Day
x <- forall a. Arbitrary a => Gen a
arbitrary
    Integer
a <- forall a. Arbitrary a => Gen a
arbitrary
    Integer
b <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> b -> M1set a
m1set Interval Day
x Integer
a Integer
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M1set DT.UTCTime) where
  arbitrary :: Gen (M1set UTCTime)
arbitrary = do
    Interval UTCTime
x <- forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
a <- forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
b <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> b -> M1set a
m1set Interval UTCTime
x NominalDiffTime
a NominalDiffTime
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary


-- | A set used for testing M2 defined so that the M2 condition is true.
data M2set a = M2set
  { forall a. M2set a -> Interval a
m21 :: Interval a
  , forall a. M2set a -> Interval a
m22 :: Interval a
  , forall a. M2set a -> Interval a
m23 :: Interval a
  , forall a. M2set a -> Interval a
m24 :: Interval a
  }
  deriving Int -> M2set a -> ShowS
forall a. (Show a, Ord a) => Int -> M2set a -> ShowS
forall a. (Show a, Ord a) => [M2set a] -> ShowS
forall a. (Show a, Ord a) => M2set a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M2set a] -> ShowS
$cshowList :: forall a. (Show a, Ord a) => [M2set a] -> ShowS
show :: M2set a -> String
$cshow :: forall a. (Show a, Ord a) => M2set a -> String
showsPrec :: Int -> M2set a -> ShowS
$cshowsPrec :: forall a. (Show a, Ord a) => Int -> M2set a -> ShowS
Show

instance Arbitrary (M2set Int) where
  arbitrary :: Gen (M2set Int)
arbitrary = do
    Interval Int
x <- forall a. Arbitrary a => Gen a
arbitrary
    Interval Int
a <- forall a. Arbitrary a => Gen a
arbitrary
    Int
b <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> Interval a -> b -> b -> M2set a
m2set Interval Int
x Interval Int
a Int
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M2set DT.Day) where
  arbitrary :: Gen (M2set Day)
arbitrary = do
    Interval Day
x <- forall a. Arbitrary a => Gen a
arbitrary
    Interval Day
a <- forall a. Arbitrary a => Gen a
arbitrary
    Integer
b <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> Interval a -> b -> b -> M2set a
m2set Interval Day
x Interval Day
a Integer
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M2set DT.UTCTime) where
  arbitrary :: Gen (M2set UTCTime)
arbitrary = do
    Interval UTCTime
x <- forall a. Arbitrary a => Gen a
arbitrary
    Interval UTCTime
a <- forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
b <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> Interval a -> b -> b -> M2set a
m2set Interval UTCTime
x Interval UTCTime
a NominalDiffTime
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

-- | A set used for testing M5.
data M5set a = M5set
  { forall a. M5set a -> Interval a
m51 :: Interval a
  , forall a. M5set a -> Interval a
m52 :: Interval a
  }
  deriving Int -> M5set a -> ShowS
forall a. (Show a, Ord a) => Int -> M5set a -> ShowS
forall a. (Show a, Ord a) => [M5set a] -> ShowS
forall a. (Show a, Ord a) => M5set a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M5set a] -> ShowS
$cshowList :: forall a. (Show a, Ord a) => [M5set a] -> ShowS
show :: M5set a -> String
$cshow :: forall a. (Show a, Ord a) => M5set a -> String
showsPrec :: Int -> M5set a -> ShowS
$cshowsPrec :: forall a. (Show a, Ord a) => Int -> M5set a -> ShowS
Show

instance Arbitrary (M5set Int) where
  arbitrary :: Gen (M5set Int)
arbitrary = do
    Interval Int
x <- forall a. Arbitrary a => Gen a
arbitrary
    Int
a <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> M5set a
m5set Interval Int
x Int
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M5set DT.Day) where
  arbitrary :: Gen (M5set Day)
arbitrary = do
    Interval Day
x <- forall a. Arbitrary a => Gen a
arbitrary
    Integer
a <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> M5set a
m5set Interval Day
x Integer
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M5set DT.UTCTime) where
  arbitrary :: Gen (M5set UTCTime)
arbitrary = do
    Interval UTCTime
x <- forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
a <- forall a. Arbitrary a => Gen a
arbitrary
    forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> M5set a
m5set Interval UTCTime
x NominalDiffTime
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

-- | = "An Axiomatization of Interval Time".
class ( IntervalSizeable a b ) => IntervalAxioms a b where

    -- | Smart constructor of 'M1set'.
    m1set :: (IntervalSizeable a b) => Interval a -> b -> b -> b -> M1set a
    m1set Interval a
x b
a b
b b
c = forall a.
Interval a -> Interval a -> Interval a -> Interval a -> M1set a
M1set Interval a
p1 Interval a
p2 Interval a
p3 Interval a
p4
      where p1 :: Interval a
p1 = Interval a
x                          -- interval i in prop_IAaxiomM1
            p2 :: Interval a
p2 = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
a (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
x)       -- interval j in prop_IAaxiomM1
            p3 :: Interval a
p3 = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
x)       -- interval k in prop_IAaxiomM1
            p4 :: Interval a
p4 = forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval (forall b. (Ord b, Num b) => b -> b
makePos b
c) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
p2)

    {- |

    == Axiom M1

    The first axiom of Allen and Hayes (1987) states that if "two periods both
    meet a third, thn any period met by one must also be met by the other."
    That is:

    \[
      \forall \text{ i,j,k,l } s.t. (i:j \text{ & } i:k \text{ & } l:j) \implies l:k
    \]
    -}
    prop_IAaxiomM1 :: (Ord a) => M1set a -> Property
    prop_IAaxiomM1 M1set a
x =
      (Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
l forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j) forall prop. Testable prop => Bool -> prop -> Property
==> (Interval a
l forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k)
      where i :: Interval a
i = forall a. M1set a -> Interval a
m11 M1set a
x
            j :: Interval a
j = forall a. M1set a -> Interval a
m12 M1set a
x
            k :: Interval a
k = forall a. M1set a -> Interval a
m13 M1set a
x
            l :: Interval a
l = forall a. M1set a -> Interval a
m14 M1set a
x

    -- | Smart constructor of 'M2set'.
    m2set :: (IntervalSizeable a b)=> Interval a -> Interval a -> b -> b -> M2set a
    m2set Interval a
x Interval a
y b
a b
b = forall a.
Interval a -> Interval a -> Interval a -> Interval a -> M2set a
M2set Interval a
p1 Interval a
p2 Interval a
p3 Interval a
p4
      where p1 :: Interval a
p1 = Interval a
x                          -- interval i in prop_IAaxiomM2
            p2 :: Interval a
p2 = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
a (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
x)       -- interval j in prop_IAaxiomM2
            p3 :: Interval a
p3 = Interval a
y                          -- interval k in prop_IAaxiomM2
            p4 :: Interval a
p4 = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
y)       -- interval l in prop_IAaxiomM2

    {- |

    == Axiom M2

    If period i meets period j and period k meets l,
    then exactly one of the following holds:

      1) i meets l;
      2) there is an m such that i meets m and m meets l;
      3) there is an n such that k meets n and n meets j.

    That is,

    \[
      \forall i,j,k,l s.t. (i:j \text { & } k:l) \implies
        i:l \oplus
        (\exists m s.t. i:m:l) \oplus
        (\exists m s.t. k:m:j)
    \]

    -}

    prop_IAaxiomM2 :: (IntervalSizeable a b, Show a) =>
        M2set a -> Property
    prop_IAaxiomM2 M2set a
x =
      (Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
k forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l) forall prop. Testable prop => Bool -> prop -> Property
==>
        (Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l)  Bool -> Bool -> Bool
`xor`
        forall a b. Either a b -> Bool
isRight Either ParseErrorInterval (Interval a)
m Bool -> Bool -> Bool
`xor`
        forall a b. Either a b -> Bool
isRight Either ParseErrorInterval (Interval a)
n
        where i :: Interval a
i = forall a. M2set a -> Interval a
m21 M2set a
x
              j :: Interval a
j = forall a. M2set a -> Interval a
m22 M2set a
x
              k :: Interval a
k = forall a. M2set a -> Interval a
m23 M2set a
x
              l :: Interval a
l = forall a. M2set a -> Interval a
m24 M2set a
x
              m :: Either ParseErrorInterval (Interval a)
m = forall a.
(Show a, Ord a) =>
a -> a -> Either ParseErrorInterval (Interval a)
parseInterval (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
l)
              n :: Either ParseErrorInterval (Interval a)
n = forall a.
(Show a, Ord a) =>
a -> a -> Either ParseErrorInterval (Interval a)
parseInterval (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
k) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)

    {- |

    == Axiom ML1

    An interval cannot meet itself.

    \[
      \forall i \lnot i:i
    \]
    -}

    prop_IAaxiomML1 :: (Ord a) => Interval a -> Property
    prop_IAaxiomML1 Interval a
x = Bool -> Bool
not (Interval a
x forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
x) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

    {- |

    == Axiom ML2

    If i meets j then j does not meet i.

    \[
    \forall i,j i:j \implies \lnot j:i
    \]
    -}

    prop_IAaxiomML2 :: (Ord a)=> M2set a -> Property
    prop_IAaxiomML2 M2set a
x =
      (Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j) forall prop. Testable prop => Bool -> prop -> Property
==> Bool -> Bool
not (Interval a
j forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i)
      where i :: Interval a
i = forall a. M2set a -> Interval a
m21 M2set a
x
            j :: Interval a
j = forall a. M2set a -> Interval a
m22 M2set a
x

    {- |

    == Axiom M3

    Time does not start or stop:

    \[
    \forall i \exists j,k s.t. j:i:k
    \]
    -}

    prop_IAaxiomM3 :: (IntervalSizeable a b)=>
          b -> Interval a -> Property
    prop_IAaxiomM3 b
b Interval a
i =
      (Interval a
j forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      where j :: Interval a
j = forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval   b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
            k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)

    {- |
      ML3 says that For all i, there does not exist m such that i meets m and
      m meet i. Not testing that this axiom holds, as I'm not sure how I would
      test the lack of existence easily.
    -}

    {- |

    == Axiom M4

    If two meets are separated by intervals, then this sequence is a longer interval.

    \[
    \forall i,j i:j \implies (\exists k,m,n s.t m:i:j:n \text { & } m:k:n)
    \]
    -}

    prop_IAaxiomM4 :: (IntervalSizeable a b)=>
        b -> M2set a -> Property
    prop_IAaxiomM4 b
b M2set a
x =
      ((Interval a
m forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n) Bool -> Bool -> Bool
&&
        (Interval a
m forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
k forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n)) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      where i :: Interval a
i = forall a. M2set a -> Interval a
m21 M2set a
x
            j :: Interval a
j = forall a. M2set a -> Interval a
m22 M2set a
x
            m :: Interval a
m = forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval   b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
            n :: Interval a
n = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j)
            k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
g (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
m)
            g :: b
g = forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
n) (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
m)


    -- | Smart constructor of 'M5set'.
    m5set :: (IntervalSizeable a b)=> Interval a -> b -> b -> M5set a
    m5set Interval a
x b
a b
b = forall a. Interval a -> Interval a -> M5set a
M5set Interval a
p1 Interval a
p2
      where p1 :: Interval a
p1 = Interval a
x                     -- interval i in prop_IAaxiomM5
            p2 :: Interval a
p2 = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
a a
ps       -- interval l in prop_IAaxiomM5
            ps :: a
ps = forall (i :: * -> *) a. Intervallic i => i a -> a
end (forall a b (i :: * -> *).
(IntervalSizeable a b, Intervallic i) =>
b -> i a -> i a
expandr (forall b. (Ord b, Num b) => b -> b
makePos b
b) Interval a
x) -- creating l by shifting and expanding i

    {- |

    == Axiom M5

    There is only one time period between any two meeting places.

    \[
    \forall i,j,k,l (i:j:l \text{ & } i:k:l) \equiv j = k
    \]
    -}
    prop_IAaxiomM5 :: (IntervalSizeable a b) =>
        M5set a -> Property
    prop_IAaxiomM5 M5set a
x =
      ((Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l) Bool -> Bool -> Bool
&&
       (Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
k forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l)) forall a. (Eq a, Show a) => a -> a -> Property
=== (Interval a
j forall a. Eq a => a -> a -> Bool
== Interval a
k)
      where i :: Interval a
i = forall a. M5set a -> Interval a
m51 M5set a
x
            j :: Interval a
j = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
g (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)
            k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
g (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)
            g :: b
g = forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
l) (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)
            l :: Interval a
l = forall a. M5set a -> Interval a
m52 M5set a
x

    {- |

    == Axiom M4.1

    Ordered unions:

    \[
    \forall i,j i:j \implies (\exists m,n s.t. m:i:j:n \text{ & } m:(i+j):n)
    \]
    -}
    prop_IAaxiomM4_1 :: (IntervalSizeable a b)=>
                    b -> M2set a -> Property
    prop_IAaxiomM4_1 b
b M2set a
x =
      ((Interval a
m forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n) Bool -> Bool -> Bool
&&
        (Interval a
m forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
ij Bool -> Bool -> Bool
&& Interval a
ij forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n)) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      where i :: Interval a
i = forall a. M2set a -> Interval a
m21 M2set a
x
            j :: Interval a
j = forall a. M2set a -> Interval a
m22 M2set a
x
            m :: Interval a
m = forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval   b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
            n :: Interval a
n = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j)
            ij :: Interval a
ij = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ Interval a
i forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
j

instance IntervalAxioms Int Int
instance IntervalAxioms Day Integer
instance IntervalAxioms UTCTime NominalDiffTime