{- HLINT ignore "Use camelCase" -}
{- HLINT ignore "Redundant bracket" -}
{- HLINT ignore "Use &&" -}

-- |
-- Copyright: © 2022–2024 Jonathan Knowles
-- License: Apache-2.0
--
-- This module provides 'Laws' definitions for classes exported by
-- "Data.Monoid.LCM".
--
module Test.QuickCheck.Classes.Monoid.LCM
    ( lcmMonoidLaws
    , distributiveLCMMonoidLaws
    )
    where

import Prelude hiding
    ( gcd, lcm )

import Data.Function
    ( (&) )
import Data.Maybe
    ( isJust )
import Data.Monoid.GCD
    ( GCDMonoid (..) )
import Data.Monoid.LCM
    ( DistributiveLCMMonoid, LCMMonoid (..) )
import Data.Proxy
    ( Proxy (..) )
import Data.Semigroup.Cancellative
    ( Reductive (..) )
import Internal
    ( cover, makeLaw1, makeLaw2, makeLaw3, makeProperty, report, (==>) )
import Test.QuickCheck
    ( Arbitrary (..), Property )
import Test.QuickCheck.Classes
    ( Laws (..) )

--------------------------------------------------------------------------------
-- LCMMonoid
--------------------------------------------------------------------------------

-- | 'Laws' for instances of 'LCMMonoid'.
--
-- Includes the following laws:
--
-- __/Reductivity/__
--
-- @
-- 'isJust' ('lcm' a b '</>' a)
-- @
-- @
-- 'isJust' ('lcm' a b '</>' b)
-- @
--
-- __/Uniqueness/__
--
-- @
-- 'all' 'isJust'
--     [ \   \   c '</>' a
--     , \   \   c '</>' b
--     , 'lcm' a b '</>' c
--     ]
-- ==>
--     ('lcm' a b '==' c)
-- @
--
-- __/Idempotence/__
--
-- @
-- 'lcm' a a '==' a
-- @
--
-- __/Identity/__
--
-- @
-- 'lcm' 'mempty' a '==' a
-- @
-- @
-- 'lcm' a 'mempty' '==' a
-- @
--
-- __/Commutativity/__
--
-- @
-- 'lcm' a b '==' 'lcm' b a
-- @
--
-- __/Associativity/__
--
-- @
-- 'lcm' ('lcm' a b) c '==' 'lcm' a ('lcm' b c)
-- @
--
-- __/Absorption/__
--
-- @
-- 'lcm' a ('gcd' a b) '==' a
-- @
-- @
-- 'gcd' a ('lcm' a b) '==' a
-- @
--
-- Note that the following superclass laws are __not__ included:
--
-- * 'Test.QuickCheck.Classes.Monoid.GCD.gcdMonoidLaws'
--
lcmMonoidLaws
    :: forall a. (Arbitrary a, Show a, Eq a, LCMMonoid a)
    => Proxy a
    -> Laws
lcmMonoidLaws :: forall a.
(Arbitrary a, Show a, Eq a, LCMMonoid a) =>
Proxy a -> Laws
lcmMonoidLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"LCMMonoid"
    [ forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"lcmMonoidLaw_reductivity_left"
        (a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_reductivity_left)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"lcmMonoidLaw_reductivity_right"
        (a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_reductivity_right)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> a -> t) -> (String, Property)
makeLaw3 @a
        String
"lcmMonoidLaw_uniqueness"
        (a -> a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> a -> Property
lcmMonoidLaw_uniqueness)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"lcmMonoidLaw_idempotence"
        (a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_idempotence)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"lcmMonoidLaw_identity_left"
        (a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_identity_left)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"lcmMonoidLaw_identity_right"
        (a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_identity_right)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"lcmMonoidLaw_commutativity"
        (a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_commutativity)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> a -> t) -> (String, Property)
makeLaw3 @a
        String
"lcmMonoidLaw_associativity"
        (a -> a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> a -> Property
lcmMonoidLaw_associativity)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"lcmMonoidLaw_absorption_gcd_lcm"
        (a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_absorption_gcd_lcm)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"lcmMonoidLaw_absorption_lcm_gcd"
        (a -> a -> Property
forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_absorption_lcm_gcd)
    ]

lcmMonoidLaw_reductivity_left
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_reductivity_left :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_reductivity_left a
a a
b =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"isJust (lcm a b </> a)"
        (Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"lcm a b /= mempty"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"(lcm a b </> a) /= Just mempty"
        ((a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a) Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
/= a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b </> a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a)

lcmMonoidLaw_reductivity_right
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_reductivity_right :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_reductivity_right a
a a
b =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"isJust (lcm a b </> b)"
        (Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"lcm a b /= mempty"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"(lcm a b </> b) /= Just mempty"
        ((a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b) Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
/= a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b </> b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b)

lcmMonoidLaw_uniqueness
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> a -> Property
lcmMonoidLaw_uniqueness :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> a -> Property
lcmMonoidLaw_uniqueness a
a a
b a
c =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"all isJust [c </> a, c </> b, lcm a b </> c] ==> (lcm a b == c)"
        ((Maybe a -> Bool) -> [Maybe a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe a -> Bool
forall a. Maybe a -> Bool
isJust [a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a, a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b, a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
c] Bool -> Bool -> Bool
==> (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"all isJust [c </> a, c </> b, lcm a b </> c]"
        ((Maybe a -> Bool) -> [Maybe a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe a -> Bool
forall a. Maybe a -> Bool
isJust [a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a, a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b, a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
c])
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"not (all isJust [c </> a, c </> b, lcm a b </> c])"
        (Bool -> Bool
not ((Maybe a -> Bool) -> [Maybe a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe a -> Bool
forall a. Maybe a -> Bool
isJust [a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a, a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b, a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
c]))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"c == lcm a b"
        (a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"c /= lcm a b"
        (a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b </> c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"c </> a"
        (a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"c </> b"
        (a
c a -> a -> Maybe a
forall m. Reductive m => m -> m -> Maybe m
</> a
b)

lcmMonoidLaw_idempotence
    :: (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_idempotence :: forall a. (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_idempotence a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm a a == a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
a)

lcmMonoidLaw_identity_left
    :: (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_identity_left :: forall a. (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_identity_left a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm mempty a == a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
forall a. Monoid a => a
mempty a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"a /= mempty"
        (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm mempty a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
forall a. Monoid a => a
mempty a
a)

lcmMonoidLaw_identity_right
    :: (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_identity_right :: forall a. (Eq a, Show a, LCMMonoid a) => a -> Property
lcmMonoidLaw_identity_right a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm a mempty == a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
forall a. Monoid a => a
mempty a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"a /= mempty"
        (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a mempty"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
forall a. Monoid a => a
mempty)

lcmMonoidLaw_commutativity
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_commutativity :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_commutativity a
a a
b =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm a b == lcm b a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"lcm a b /= mempty"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm b a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
a)

lcmMonoidLaw_associativity
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> a -> Property
lcmMonoidLaw_associativity :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> a -> Property
lcmMonoidLaw_associativity a
a a
b a
c =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm (lcm a b) c == lcm a (lcm b c)"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b) a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"lcm a b /= mempty"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"lcm b c /= mempty"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm (lcm a b) c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b) a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm b c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a (lcm b c)"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c))

lcmMonoidLaw_absorption_gcd_lcm
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_absorption_gcd_lcm :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_absorption_gcd_lcm a
a a
b =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm a (gcd a b) == a"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"gcd a b == mempty"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"gcd a b /= mempty"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"gcd a b"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a (gcd a b)"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b))

lcmMonoidLaw_absorption_lcm_gcd
    :: (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_absorption_lcm_gcd :: forall a. (Eq a, Show a, LCMMonoid a) => a -> a -> Property
lcmMonoidLaw_absorption_lcm_gcd a
a a
b =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"gcd a (lcm a b) == a"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"gcd a b == mempty"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"gcd a b /= mempty"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. Monoid a => a
mempty)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"gcd a (lcm a b)"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b))

--------------------------------------------------------------------------------
-- DistributiveLCMMonoid
--------------------------------------------------------------------------------

-- | 'Laws' for instances of 'DistributiveLCMMonoid'.
--
-- Includes the following laws:
--
-- __/Left-distributivity/__
--
-- @
-- 'lcm' (a '<>' b) (a '<>' c) '==' a '<>' 'lcm' b c
-- @
--
-- __/Right-distributivity/__
--
-- @
-- 'lcm' (a '<>' c) (b '<>' c) '==' 'lcm' a b '<>' c
-- @
--
-- __/Lattice distributivity/__
--
-- @
-- 'lcm' a ('gcd' b c) '==' 'gcd' ('lcm' a b) ('lcm' a c)
-- @
--
-- @
-- 'gcd' a ('lcm' b c) '==' 'lcm' ('gcd' a b) ('gcd' a c)
-- @
--
-- Note that the following superclass laws are __not__ included:
--
-- * 'Test.QuickCheck.Classes.Monoid.GCD.distributiveGCDMonoidLaws'
-- * 'lcmMonoidLaws'
--
distributiveLCMMonoidLaws
    :: forall a. (Arbitrary a, Show a, Eq a, DistributiveLCMMonoid a)
    => Proxy a
    -> Laws
distributiveLCMMonoidLaws :: forall a.
(Arbitrary a, Show a, Eq a, DistributiveLCMMonoid a) =>
Proxy a -> Laws
distributiveLCMMonoidLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"DistributiveLCMMonoid"
    [ forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> a -> t) -> (String, Property)
makeLaw3 @a
        String
"distributiveLCMMonoidLaw_distributivity_left"
        (a -> a -> a -> Property
forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_left)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> a -> t) -> (String, Property)
makeLaw3 @a
        String
"distributiveLCMMonoidLaw_distributivity_right"
        (a -> a -> a -> Property
forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_right)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> a -> t) -> (String, Property)
makeLaw3 @a
        String
"distributiveLCMMonoidLaw_distributivity_gcd_lcm"
        (a -> a -> a -> Property
forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_gcd_lcm)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> a -> t) -> (String, Property)
makeLaw3 @a
        String
"distributiveLCMMonoidLaw_distributivity_lcm_gcd"
        (a -> a -> a -> Property
forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_lcm_gcd)
    ]

distributiveLCMMonoidLaw_distributivity_left
    :: (Eq a, Show a, DistributiveLCMMonoid a) => a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_left :: forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_left a
a a
b a
c =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm (a <> b) (a <> c) == a <> lcm b c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b) (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> b"
        (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> c"
        (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm (a <> b) (a <> c)"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b) (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm b c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> lcm b c"
        (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c)

distributiveLCMMonoidLaw_distributivity_right
    :: (Eq a, Show a, DistributiveLCMMonoid a) => a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_right :: forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_right a
a a
b a
c =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm (a <> c) (b <> c) == lcm a b <> c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c) (a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> c"
        (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"b <> c"
        (a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm (a <> c) (b <> c)"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c) (a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"lcm a b <> c"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c)

distributiveLCMMonoidLaw_distributivity_gcd_lcm
    :: (Eq a, Show a, DistributiveLCMMonoid a) => a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_gcd_lcm :: forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_gcd_lcm a
a a
b a
c =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"lcm a (gcd b c) == gcd (lcm a b) (lcm a c)"
        (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
b a
c) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
b) (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
a a
c))

distributiveLCMMonoidLaw_distributivity_lcm_gcd
    :: (Eq a, Show a, DistributiveLCMMonoid a) => a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_lcm_gcd :: forall a.
(Eq a, Show a, DistributiveLCMMonoid a) =>
a -> a -> a -> Property
distributiveLCMMonoidLaw_distributivity_lcm_gcd a
a a
b a
c =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"gcd a (lcm b c) == lcm (gcd a b) (gcd a c)"
        (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a (a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm a
b a
c) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a
forall m. LCMMonoid m => m -> m -> m
lcm (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
b) (a -> a -> a
forall m. GCDMonoid m => m -> m -> m
gcd a
a a
c))