{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 805
{-# LANGUAGE NoStarIsType #-}
#endif
module Data.Constraint.Nat
( Min, Max, Lcm, Gcd, Divides, Div, Mod
, plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat
, plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne
, plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates
, plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes
, plusDistributesOverTimes, timesDistributesOverPow, timesDistributesOverGcd, timesDistributesOverLcm
, minDistributesOverPlus, minDistributesOverTimes, minDistributesOverPow1, minDistributesOverPow2, minDistributesOverMax
, maxDistributesOverPlus, maxDistributesOverTimes, maxDistributesOverPow1, maxDistributesOverPow2, maxDistributesOverMin
, gcdDistributesOverLcm, lcmDistributesOverGcd
, minIsIdempotent, maxIsIdempotent, lcmIsIdempotent, gcdIsIdempotent
, plusIsCancellative, timesIsCancellative
, dividesPlus, dividesTimes, dividesMin, dividesMax, dividesPow, dividesGcd, dividesLcm
, plusMonotone1, plusMonotone2
, timesMonotone1, timesMonotone2
, powMonotone1, powMonotone2
, minMonotone1, minMonotone2
, maxMonotone1, maxMonotone2
, divMonotone1, divMonotone2
, euclideanNat
, plusMod, timesMod
, modBound
, dividesDef
, timesDiv
, eqLe, leEq, leId, leTrans
, leZero, zeroLe
, plusMinusInverse1, plusMinusInverse2, plusMinusInverse3
) where
import Data.Constraint
import Data.Proxy
import Data.Type.Bool
import GHC.TypeLits
import Unsafe.Coerce
type family Min (m::Nat) (n::Nat) :: Nat where
Min m n = If (n <=? m) n m
type family Max (m::Nat) (n::Nat) :: Nat where
Max m n = If (n <=? m) m n
#if !(MIN_VERSION_base(4,11,0))
type family Div (m::Nat) (n::Nat) :: Nat where
Div m 1 = m
type family Mod (m::Nat) (n::Nat) :: Nat where
Mod 0 m = 0
#endif
type family Gcd (m::Nat) (n::Nat) :: Nat where
Gcd m m = m
type family Lcm (m::Nat) (n::Nat) :: Nat where
Lcm m m = m
type Divides n m = n ~ Gcd n m
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
magic :: (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
f = ((KnownNat n, KnownNat m) => Dict (KnownNat o))
-> (KnownNat n, KnownNat m) :- KnownNat o
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownNat n, KnownNat m) => Dict (KnownNat o))
-> (KnownNat n, KnownNat m) :- KnownNat o)
-> ((KnownNat n, KnownNat m) => Dict (KnownNat o))
-> (KnownNat n, KnownNat m) :- KnownNat o
forall a b. (a -> b) -> a -> b
$ Magic Any -> Integer -> Dict (KnownNat o)
forall a b. a -> b
unsafeCoerce ((KnownNat Any => Dict (KnownNat Any)) -> Magic Any
forall (n :: Nat). (KnownNat n => Dict (KnownNat n)) -> Magic n
Magic KnownNat Any => Dict (KnownNat Any)
forall (a :: Constraint). a => Dict a
Dict) (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n) Integer -> Integer -> Integer
`f` Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))
axiom :: Dict c
axiom :: Dict c
axiom = Dict (() :: Constraint) -> Dict c
forall a b. a -> b
unsafeCoerce (Dict (() :: Constraint)
forall (a :: Constraint). a => Dict a
Dict :: Dict ())
axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)
axiomLe :: Dict (a <= b)
axiomLe = Dict (a <= b)
forall (c :: Constraint). Dict c
axiom
eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)
eqLe :: (a ~ b) :- (a <= b)
eqLe = ((a ~ b) => Dict (a <= b)) -> (a ~ b) :- (a <= b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a ~ b) => Dict (a <= b)
forall (a :: Constraint). a => Dict a
Dict
dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
dividesGcd :: (Divides a b, Divides a c) :- Divides a (Gcd b c)
dividesGcd = ((Divides a b, Divides a c) => Dict (Divides a (Gcd b c)))
-> (Divides a b, Divides a c) :- Divides a (Gcd b c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Divides a b, Divides a c) => Dict (Divides a (Gcd b c))
forall (c :: Constraint). Dict c
axiom
dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c
dividesLcm :: (Divides a c, Divides b c) :- Divides (Lcm a b) c
dividesLcm = ((Divides a c, Divides b c) => Dict (Divides (Lcm a b) c))
-> (Divides a c, Divides b c) :- Divides (Lcm a b) c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Divides a c, Divides b c) => Dict (Divides (Lcm a b) c)
forall (c :: Constraint). Dict c
axiom
gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)
gcdCommutes :: Dict (Gcd a b ~ Gcd b a)
gcdCommutes = Dict (Gcd a b ~ Gcd b a)
forall (c :: Constraint). Dict c
axiom
lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)
lcmCommutes :: Dict (Lcm a b ~ Lcm b a)
lcmCommutes = Dict (Lcm a b ~ Lcm b a)
forall (c :: Constraint). Dict c
axiom
gcdZero :: forall a. Dict (Gcd 0 a ~ a)
gcdZero :: Dict (Gcd 0 a ~ a)
gcdZero = Dict (Gcd 0 a ~ a)
forall (c :: Constraint). Dict c
axiom
gcdOne :: forall a. Dict (Gcd 1 a ~ 1)
gcdOne :: Dict (Gcd 1 a ~ 1)
gcdOne = Dict (Gcd 1 a ~ 1)
forall (c :: Constraint). Dict c
axiom
lcmZero :: forall a. Dict (Lcm 0 a ~ 0)
lcmZero :: Dict (Lcm 0 a ~ 0)
lcmZero = Dict (Lcm 0 a ~ 0)
forall (c :: Constraint). Dict c
axiom
lcmOne :: forall a. Dict (Lcm 1 a ~ a)
lcmOne :: Dict (Lcm 1 a ~ a)
lcmOne = Dict (Lcm 1 a ~ a)
forall (c :: Constraint). Dict c
axiom
gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
gcdNat :: (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
gcdNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd
lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
lcmNat :: (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
lcmNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
lcm
plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
plusNat :: (KnownNat n, KnownNat m) :- KnownNat (n + m)
plusNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (n + m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
minusNat :: (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
minusNat = ((KnownNat n, KnownNat m, m <= n) => Dict (KnownNat (n - m)))
-> (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownNat n, KnownNat m, m <= n) => Dict (KnownNat (n - m)))
-> (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m))
-> ((KnownNat n, KnownNat m, m <= n) => Dict (KnownNat (n - m)))
-> (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
forall a b. (a -> b) -> a -> b
$ case (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (n - m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic @n @m (-) of Sub (KnownNat n, KnownNat m) => Dict (KnownNat (n - m))
r -> Dict (KnownNat (n - m))
(KnownNat n, KnownNat m) => Dict (KnownNat (n - m))
r
minNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)
minNat :: (KnownNat n, KnownNat m) :- KnownNat (Min n m)
minNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (If (m <=? n) m n)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min
maxNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)
maxNat :: (KnownNat n, KnownNat m) :- KnownNat (Max n m)
maxNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (If (m <=? n) n m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max
timesNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat :: (KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (n * m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)
powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
powNat :: (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
powNat = (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
(^)
divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
divNat :: (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
divNat = ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Div n m)))
-> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Div n m)))
-> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m))
-> ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Div n m)))
-> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
forall a b. (a -> b) -> a -> b
$ case (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (Div n m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic @n @m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div of Sub (KnownNat n, KnownNat m) => Dict (KnownNat (Div n m))
r -> Dict (KnownNat (Div n m))
(KnownNat n, KnownNat m) => Dict (KnownNat (Div n m))
r
modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
modNat :: (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
modNat = ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Mod n m)))
-> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Mod n m)))
-> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m))
-> ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Mod n m)))
-> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
forall a b. (a -> b) -> a -> b
$ case (Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat (Mod n m)
forall (n :: Nat) (m :: Nat) (o :: Nat).
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic @n @m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod of Sub (KnownNat n, KnownNat m) => Dict (KnownNat (Mod n m))
r -> Dict (KnownNat (Mod n m))
(KnownNat n, KnownNat m) => Dict (KnownNat (Mod n m))
r
plusZero :: forall n. Dict ((n + 0) ~ n)
plusZero :: Dict ((n + 0) ~ n)
plusZero = Dict ((n + 0) ~ n)
forall (a :: Constraint). a => Dict a
Dict
minusZero :: forall n. Dict ((n - 0) ~ n)
minusZero :: Dict ((n - 0) ~ n)
minusZero = Dict ((n - 0) ~ n)
forall (a :: Constraint). a => Dict a
Dict
timesZero :: forall n. Dict ((n * 0) ~ 0)
timesZero :: Dict ((n * 0) ~ 0)
timesZero = Dict ((n * 0) ~ 0)
forall (a :: Constraint). a => Dict a
Dict
timesOne :: forall n. Dict ((n * 1) ~ n)
timesOne :: Dict ((n * 1) ~ n)
timesOne = Dict ((n * 1) ~ n)
forall (a :: Constraint). a => Dict a
Dict
minZero :: forall n. Dict (Min n 0 ~ 0)
#if MIN_VERSION_base(4,16,0)
minZero = axiom
#else
minZero :: Dict (Min n 0 ~ 0)
minZero = Dict (Min n 0 ~ 0)
forall (a :: Constraint). a => Dict a
Dict
#endif
maxZero :: forall n. Dict (Max n 0 ~ n)
#if MIN_VERSION_base(4,16,0)
maxZero = axiom
#else
maxZero :: Dict (Max n 0 ~ n)
maxZero = Dict (Max n 0 ~ n)
forall (a :: Constraint). a => Dict a
Dict
#endif
powZero :: forall n. Dict ((n ^ 0) ~ 1)
powZero :: Dict ((n ^ 0) ~ 1)
powZero = Dict ((n ^ 0) ~ 1)
forall (a :: Constraint). a => Dict a
Dict
leZero :: forall a. (a <= 0) :- (a ~ 0)
leZero :: (a <= 0) :- (a ~ 0)
leZero = ((a <= 0) => Dict (a ~ 0)) -> (a <= 0) :- (a ~ 0)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= 0) => Dict (a ~ 0)
forall (c :: Constraint). Dict c
axiom
zeroLe :: forall (a :: Nat). Dict (0 <= a)
#if MIN_VERSION_base(4,16,0)
zeroLe = axiom
#else
zeroLe :: Dict (0 <= a)
zeroLe = Dict (0 <= a)
forall (a :: Constraint). a => Dict a
Dict
#endif
plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)
plusMinusInverse1 :: Dict (((m + n) - n) ~ m)
plusMinusInverse1 = Dict (((m + n) - n) ~ m)
forall (c :: Constraint). Dict c
axiom
plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)
plusMinusInverse2 :: (m <= n) :- (((m + n) - m) ~ n)
plusMinusInverse2 = ((m <= n) => Dict (((m + n) - m) ~ n))
-> (m <= n) :- (((m + n) - m) ~ n)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (m <= n) => Dict (((m + n) - m) ~ n)
forall (c :: Constraint). Dict c
axiom
plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)
plusMinusInverse3 :: (n <= m) :- (((m - n) + n) ~ m)
plusMinusInverse3 = ((n <= m) => Dict (((m - n) + n) ~ m))
-> (n <= m) :- (((m - n) + n) ~ m)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (n <= m) => Dict (((m - n) + n) ~ m)
forall (c :: Constraint). Dict c
axiom
plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)
plusMonotone1 :: (a <= b) :- ((a + c) <= (b + c))
plusMonotone1 = ((a <= b) => Dict ((a + c) <= (b + c)))
-> (a <= b) :- ((a + c) <= (b + c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b) => Dict ((a + c) <= (b + c))
forall (c :: Constraint). Dict c
axiom
plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)
plusMonotone2 :: (b <= c) :- ((a + b) <= (a + c))
plusMonotone2 = ((b <= c) => Dict ((a + b) <= (a + c)))
-> (b <= c) :- ((a + b) <= (a + c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (b <= c) => Dict ((a + b) <= (a + c))
forall (c :: Constraint). Dict c
axiom
powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))
powMonotone1 :: (a <= b) :- ((a ^ c) <= (b ^ c))
powMonotone1 = ((a <= b) => Dict ((a ^ c) <= (b ^ c)))
-> (a <= b) :- ((a ^ c) <= (b ^ c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b) => Dict ((a ^ c) <= (b ^ c))
forall (c :: Constraint). Dict c
axiom
powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))
powMonotone2 :: (b <= c) :- ((a ^ b) <= (a ^ c))
powMonotone2 = ((b <= c) => Dict ((a ^ b) <= (a ^ c)))
-> (b <= c) :- ((a ^ b) <= (a ^ c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (b <= c) => Dict ((a ^ b) <= (a ^ c))
forall (c :: Constraint). Dict c
axiom
divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)
divMonotone1 :: (a <= b) :- (Div a c <= Div b c)
divMonotone1 = ((a <= b) => Dict (Div a c <= Div b c))
-> (a <= b) :- (Div a c <= Div b c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b) => Dict (Div a c <= Div b c)
forall (c :: Constraint). Dict c
axiom
divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)
divMonotone2 :: (b <= c) :- (Div a c <= Div a b)
divMonotone2 = ((b <= c) => Dict (Div a c <= Div a b))
-> (b <= c) :- (Div a c <= Div a b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (b <= c) => Dict (Div a c <= Div a b)
forall (c :: Constraint). Dict c
axiom
timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)
timesMonotone1 :: (a <= b) :- ((a * c) <= (b * c))
timesMonotone1 = ((a <= b) => Dict ((a * c) <= (b * c)))
-> (a <= b) :- ((a * c) <= (b * c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b) => Dict ((a * c) <= (b * c))
forall (c :: Constraint). Dict c
axiom
timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)
timesMonotone2 :: (b <= c) :- ((a * b) <= (a * c))
timesMonotone2 = ((b <= c) => Dict ((a * b) <= (a * c)))
-> (b <= c) :- ((a * b) <= (a * c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (b <= c) => Dict ((a * b) <= (a * c))
forall (c :: Constraint). Dict c
axiom
minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)
minMonotone1 :: (a <= b) :- (Min a c <= Min b c)
minMonotone1 = ((a <= b) =>
Dict ((If (c <=? a) c a <=? If (c <=? b) c b) ~ 'True))
-> (a <= b) :- ((If (c <=? a) c a <=? If (c <=? b) c b) ~ 'True)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b) => Dict ((If (c <=? a) c a <=? If (c <=? b) c b) ~ 'True)
forall (c :: Constraint). Dict c
axiom
minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)
minMonotone2 :: (b <= c) :- (Min a b <= Min a c)
minMonotone2 = ((b <= c) =>
Dict ((If (b <=? a) b a <=? If (c <=? a) c a) ~ 'True))
-> (b <= c) :- ((If (b <=? a) b a <=? If (c <=? a) c a) ~ 'True)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (b <= c) => Dict ((If (b <=? a) b a <=? If (c <=? a) c a) ~ 'True)
forall (c :: Constraint). Dict c
axiom
maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)
maxMonotone1 :: (a <= b) :- (Max a c <= Max b c)
maxMonotone1 = ((a <= b) =>
Dict ((If (c <=? a) a c <=? If (c <=? b) b c) ~ 'True))
-> (a <= b) :- ((If (c <=? a) a c <=? If (c <=? b) b c) ~ 'True)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b) => Dict ((If (c <=? a) a c <=? If (c <=? b) b c) ~ 'True)
forall (c :: Constraint). Dict c
axiom
maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)
maxMonotone2 :: (b <= c) :- (Max a b <= Max a c)
maxMonotone2 = ((b <= c) =>
Dict ((If (b <=? a) a b <=? If (c <=? a) a c) ~ 'True))
-> (b <= c) :- ((If (b <=? a) a b <=? If (c <=? a) a c) ~ 'True)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (b <= c) => Dict ((If (b <=? a) a b <=? If (c <=? a) a c) ~ 'True)
forall (c :: Constraint). Dict c
axiom
powOne :: forall n. Dict ((n ^ 1) ~ n)
powOne :: Dict ((n ^ 1) ~ n)
powOne = Dict ((n ^ 1) ~ n)
forall (c :: Constraint). Dict c
axiom
plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
plusMod :: (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
plusMod = ((1 <= c) => Dict (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c))
-> (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (1 <= c) => Dict (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
forall (c :: Constraint). Dict c
axiom
timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
timesMod :: (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
timesMod = ((1 <= c) => Dict (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c))
-> (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (1 <= c) => Dict (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
forall (c :: Constraint). Dict c
axiom
modBound :: forall m n. (1 <= n) :- (Mod m n <= n)
modBound :: (1 <= n) :- (Mod m n <= n)
modBound = ((1 <= n) => Dict (Mod m n <= n)) -> (1 <= n) :- (Mod m n <= n)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (1 <= n) => Dict (Mod m n <= n)
forall (c :: Constraint). Dict c
axiom
euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))
euclideanNat :: (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
euclideanNat = ((1 <= c) => Dict (a ~ ((c * Div a c) + Mod a c)))
-> (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (1 <= c) => Dict (a ~ ((c * Div a c) + Mod a c))
forall (c :: Constraint). Dict c
axiom
plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))
plusCommutes :: Dict ((m + n) ~ (n + m))
plusCommutes = Dict ((m + n) ~ (n + m))
forall (c :: Constraint). Dict c
axiom
timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))
timesCommutes :: Dict ((m * n) ~ (n * m))
timesCommutes = Dict ((m * n) ~ (n * m))
forall (c :: Constraint). Dict c
axiom
minCommutes :: forall n m. Dict (Min m n ~ Min n m)
minCommutes :: Dict (Min m n ~ Min n m)
minCommutes = Dict (Min m n ~ Min n m)
forall (c :: Constraint). Dict c
axiom
maxCommutes :: forall n m. Dict (Max m n ~ Max n m)
maxCommutes :: Dict (Max m n ~ Max n m)
maxCommutes = Dict (Max m n ~ Max n m)
forall (c :: Constraint). Dict c
axiom
plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))
plusAssociates :: Dict (((m + n) + o) ~ (m + (n + o)))
plusAssociates = Dict (((m + n) + o) ~ (m + (n + o)))
forall (c :: Constraint). Dict c
axiom
timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))
timesAssociates :: Dict (((m * n) * o) ~ (m * (n * o)))
timesAssociates = Dict (((m * n) * o) ~ (m * (n * o)))
forall (c :: Constraint). Dict c
axiom
minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))
minAssociates :: Dict (Min (Min m n) o ~ Min m (Min n o))
minAssociates = Dict (Min (Min m n) o ~ Min m (Min n o))
forall (c :: Constraint). Dict c
axiom
maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))
maxAssociates :: Dict (Max (Max m n) o ~ Max m (Max n o))
maxAssociates = Dict (Max (Max m n) o ~ Max m (Max n o))
forall (c :: Constraint). Dict c
axiom
gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
gcdAssociates :: Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
gcdAssociates = Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
forall (c :: Constraint). Dict c
axiom
lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
lcmAssociates :: Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
lcmAssociates = Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
forall (c :: Constraint). Dict c
axiom
minIsIdempotent :: forall n. Dict (Min n n ~ n)
minIsIdempotent :: Dict (Min n n ~ n)
minIsIdempotent = Dict (Min n n ~ n)
forall (a :: Constraint). a => Dict a
Dict
maxIsIdempotent :: forall n. Dict (Max n n ~ n)
maxIsIdempotent :: Dict (Max n n ~ n)
maxIsIdempotent = Dict (Max n n ~ n)
forall (a :: Constraint). a => Dict a
Dict
gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)
gcdIsIdempotent :: Dict (Gcd n n ~ n)
gcdIsIdempotent = Dict (Gcd n n ~ n)
forall (a :: Constraint). a => Dict a
Dict
lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)
lcmIsIdempotent :: Dict (Lcm n n ~ n)
lcmIsIdempotent = Dict (Lcm n n ~ n)
forall (a :: Constraint). a => Dict a
Dict
minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
minDistributesOverPlus :: Dict ((n + Min m o) ~ Min (n + m) (n + o))
minDistributesOverPlus = Dict ((n + Min m o) ~ Min (n + m) (n + o))
forall (c :: Constraint). Dict c
axiom
minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))
minDistributesOverTimes :: Dict ((n * Min m o) ~ Min (n * m) (n * o))
minDistributesOverTimes = Dict ((n * Min m o) ~ Min (n * m) (n * o))
forall (c :: Constraint). Dict c
axiom
minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
minDistributesOverPow1 :: Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
minDistributesOverPow1 = Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
forall (c :: Constraint). Dict c
axiom
minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
minDistributesOverPow2 :: Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
minDistributesOverPow2 = Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
forall (c :: Constraint). Dict c
axiom
minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
minDistributesOverMax :: Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
minDistributesOverMax = Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
forall (c :: Constraint). Dict c
axiom
maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))
maxDistributesOverPlus :: Dict ((n + Max m o) ~ Max (n + m) (n + o))
maxDistributesOverPlus = Dict ((n + Max m o) ~ Max (n + m) (n + o))
forall (c :: Constraint). Dict c
axiom
maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))
maxDistributesOverTimes :: Dict ((n * Max m o) ~ Max (n * m) (n * o))
maxDistributesOverTimes = Dict ((n * Max m o) ~ Max (n * m) (n * o))
forall (c :: Constraint). Dict c
axiom
maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
maxDistributesOverPow1 :: Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
maxDistributesOverPow1 = Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
forall (c :: Constraint). Dict c
axiom
maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
maxDistributesOverPow2 :: Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
maxDistributesOverPow2 = Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
forall (c :: Constraint). Dict c
axiom
maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
maxDistributesOverMin :: Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
maxDistributesOverMin = Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
forall (c :: Constraint). Dict c
axiom
plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))
plusDistributesOverTimes :: Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
plusDistributesOverTimes = Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
forall (c :: Constraint). Dict c
axiom
timesDistributesOverPow :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))
timesDistributesOverPow :: Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
timesDistributesOverPow = Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
forall (c :: Constraint). Dict c
axiom
timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
timesDistributesOverGcd :: Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
timesDistributesOverGcd = Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
forall (c :: Constraint). Dict c
axiom
timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
timesDistributesOverLcm :: Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
timesDistributesOverLcm = Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
forall (c :: Constraint). Dict c
axiom
plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)
plusIsCancellative :: ((n + m) ~ (n + o)) :- (m ~ o)
plusIsCancellative = (((n + m) ~ (n + o)) => Dict (m ~ o))
-> ((n + m) ~ (n + o)) :- (m ~ o)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((n + m) ~ (n + o)) => Dict (m ~ o)
forall (c :: Constraint). Dict c
axiom
timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
timesIsCancellative :: (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
timesIsCancellative = ((1 <= n, (n * m) ~ (n * o)) => Dict (m ~ o))
-> (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (1 <= n, (n * m) ~ (n * o)) => Dict (m ~ o)
forall (c :: Constraint). Dict c
axiom
gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
gcdDistributesOverLcm :: Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
gcdDistributesOverLcm = Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
forall (c :: Constraint). Dict c
axiom
lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
lcmDistributesOverGcd :: Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
lcmDistributesOverGcd = Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
forall (c :: Constraint). Dict c
axiom
dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
dividesPlus = ((Divides a b, Divides a c) => Dict (Divides a (b + c)))
-> (Divides a b, Divides a c) :- Divides a (b + c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Divides a b, Divides a c) => Dict (Divides a (b + c))
forall (c :: Constraint). Dict c
axiom
dividesTimes :: Divides a b :- Divides a (b * c)
dividesTimes :: Divides a b :- Divides a (b * c)
dividesTimes = (Divides a b => Dict (Divides a (b * c)))
-> Divides a b :- Divides a (b * c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Divides a b => Dict (Divides a (b * c))
forall (c :: Constraint). Dict c
axiom
dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
dividesMin = ((Divides a b, Divides a c) => Dict (a ~ Gcd a (If (c <=? b) c b)))
-> (Divides a b, Divides a c) :- (a ~ Gcd a (If (c <=? b) c b))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Divides a b, Divides a c) => Dict (a ~ Gcd a (If (c <=? b) c b))
forall (c :: Constraint). Dict c
axiom
dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
dividesMax = ((Divides a b, Divides a c) => Dict (a ~ Gcd a (If (c <=? b) b c)))
-> (Divides a b, Divides a c) :- (a ~ Gcd a (If (c <=? b) b c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Divides a b, Divides a c) => Dict (a ~ Gcd a (If (c <=? b) b c))
forall (c :: Constraint). Dict c
axiom
dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
dividesDef :: Divides a b :- (Mod b a ~ 0)
dividesDef = (Divides a b => Dict (Mod b a ~ 0)) -> Divides a b :- (Mod b a ~ 0)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Divides a b => Dict (Mod b a ~ 0)
forall (c :: Constraint). Dict c
axiom
dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)
dividesPow :: (1 <= n, Divides a b) :- Divides a (b ^ n)
dividesPow = ((1 <= n, Divides a b) => Dict (Divides a (b ^ n)))
-> (1 <= n, Divides a b) :- Divides a (b ^ n)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (1 <= n, Divides a b) => Dict (Divides a (b ^ n))
forall (c :: Constraint). Dict c
axiom
timesDiv :: forall a b. Dict ((a * Div b a) <= b)
timesDiv :: Dict ((a * Div b a) <= b)
timesDiv = Dict ((a * Div b a) <= b)
forall (c :: Constraint). Dict c
axiom
leId :: forall (a :: Nat). Dict (a <= a)
leId :: Dict (a <= a)
leId = Dict (a <= a)
forall (a :: Constraint). a => Dict a
Dict
leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)
leEq :: (a <= b, b <= a) :- (a ~ b)
leEq = ((a <= b, b <= a) => Dict (a ~ b)) -> (a <= b, b <= a) :- (a ~ b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (a <= b, b <= a) => Dict (a ~ b)
forall (c :: Constraint). Dict c
axiom
leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)
leTrans :: (b <= c, a <= b) :- (a <= c)
leTrans = ((b <= c, a <= b) => Dict (a <= c)) -> (b <= c, a <= b) :- (a <= c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (a <= c)
forall (a :: Nat) (b :: Nat). Dict (a <= b)
axiomLe @a @c)