{-# language DataKinds #-}
{-# language ExplicitForAll #-}
{-# language KindSignatures #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}

module Arithmetic.Lt
  ( -- * Special Inequalities
    zero
    -- * Substitution
  , substituteL
  , substituteR
    -- * Increment
  , incrementL
  , incrementR
    -- * Weaken
  , weakenL
  , weakenR
    -- * Composition
  , plus
  , transitive
  , transitiveNonstrictL
  , transitiveNonstrictR
    -- * Convert to Inequality
  , toLteL
  , toLteR
    -- * Absurdities
  , absurd
    -- * Integration with GHC solver
  , constant
  ) where

import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))
import Arithmetic.Unsafe (type (<=)(Lte))
import GHC.TypeNats (CmpNat,type (+))

import qualified GHC.TypeNats as GHC

toLteR :: (a < b) -> (a + 1 <= b)
toLteR :: (a < b) -> (a + 1) <= b
toLteR a < b
Lt = (a + 1) <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte

toLteL :: (a < b) -> (1 + a <= b)
toLteL :: (a < b) -> (1 + a) <= b
toLteL a < b
Lt = (1 + a) <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte

-- | Replace the left-hand side of a strict inequality
-- with an equal number.
substituteL :: (b :=: c) -> (b < a) -> (c < a)
substituteL :: (b :=: c) -> (b < a) -> c < a
substituteL b :=: c
Eq b < a
Lt = c < a
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Replace the right-hand side of a strict inequality
-- with an equal number.
substituteR :: (b :=: c) -> (a < b) -> (a < c)
substituteR :: (b :=: c) -> (a < b) -> a < c
substituteR b :=: c
Eq a < b
Lt = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Add a strict inequality to a nonstrict inequality.
plus :: (a < b) -> (c <= d) -> (a + c < b + d)
plus :: (a < b) -> (c <= d) -> (a + c) < (b + d)
plus a < b
Lt c <= d
Lte = (a + c) < (b + d)
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Add a constant to the left-hand side of both sides of
-- the strict inequality.
incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
  (a < b) -> (c + a < c + b)
incrementL :: (a < b) -> (c + a) < (c + b)
incrementL a < b
Lt = (c + a) < (c + b)
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Add a constant to the right-hand side of both sides of
-- the strict inequality.
incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
  (a < b) -> (a + c < b + c)
incrementR :: (a < b) -> (a + c) < (b + c)
incrementR a < b
Lt = (a + c) < (b + c)
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Add a constant to the left-hand side of the right-hand side of
-- the strict inequality.
weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
  (a < b) -> (a < c + b)
weakenL :: (a < b) -> a < (c + b)
weakenL a < b
Lt = a < (c + b)
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Add a constant to the right-hand side of the right-hand side of
-- the strict inequality.
weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
  (a < b) -> (a < b + c)
weakenR :: (a < b) -> a < (b + c)
weakenR a < b
Lt = a < (b + c)
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Compose two strict inequalities using transitivity.
transitive :: (a < b) -> (b < c) -> (a < c)
transitive :: (a < b) -> (b < c) -> a < c
transitive a < b
Lt b < c
Lt = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Compose a strict inequality (the first argument) with a nonstrict
-- inequality (the second argument).
transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c)
transitiveNonstrictR :: (a < b) -> (b <= c) -> a < c
transitiveNonstrictR a < b
Lt b <= c
Lte = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt

transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)
transitiveNonstrictL :: (a <= b) -> (b < c) -> a < c
transitiveNonstrictL a <= b
Lte b < c
Lt = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Zero is less than one.
zero :: 0 < 1
zero :: 0 < 1
zero = 0 < 1
forall (a :: Nat) (b :: Nat). a < b
Lt

-- | Nothing is less than zero.
absurd :: n < 0 -> void
absurd :: (n < 0) -> void
absurd n < 0
Lt = [Char] -> void
forall a. HasCallStack => [Char] -> a
error [Char]
"Arithmetic.Nat.absurd: n < 0"

-- | Use GHC's built-in type-level arithmetic to prove
-- that one number is less than another. The type-checker
-- only reduces 'CmpNat' if both arguments are constants.
constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b)
constant :: a < b
constant = a < b
forall (a :: Nat) (b :: Nat). a < b
Lt