src/Logic/Theory/Arithmetic.hs

   1 {-# LANGUAGE Safe #-}
   2
   3 module Logic.Theory.Arithmetic (
   4   type Zero (),
   5   type Zeroable (..),
   6   sign,
   7   type Succ (),
   8   type One,
   9   type Oneable (..),
  10   type PositiveOrNull (..),
  11   type PositiveNonNull (..),
  12   type NegativeOrNull (..),
  13   type NegativeNonNull (..),
  14   type Opposite (),
  15   type Oppositeable (..),
  16   type IntMax,
  17   intMax,
  18   type (+) (),
  19 ) where
  20
  21 import Data.Int (Int)
  22 import Data.Ord qualified as Ord
  23 import Logic.Kernel
  24 import Logic.Theory.Eq
  25 import Logic.Theory.Ord
  26 import Numeric.Natural (Natural)
  27 import Prelude (Integer, maxBound)
  28 import Prelude qualified
  29
  30 data Zero = ZeroAxiom
  31
  32 class Zeroable a where
  33   zero :: Zero ::: a
  34   default zero :: Prelude.Num a => Zero ::: a
  35   zero = ZeroAxiom ... 0
  36 instance Zeroable Int
  37 instance Zeroable Integer
  38 instance Zeroable Natural
  39
  40 newtype Succ n = SuccAxiom n
  41
  42 type One = Succ Zero
  43
  44 class Oneable a where
  45   one :: One ::: a
  46   default one :: Prelude.Num a => One ::: a
  47   one = SuccAxiom ZeroAxiom ... 1
  48 instance Oneable Int
  49 instance Oneable Integer
  50 instance Oneable Natural
  51
  52 class Signable a where
  53   sign :: x ::: a -> Compare Zero x ::: Ord.Ordering
  54   default sign :: Ord.Ord a => Prelude.Num a => x ::: a -> Compare Zero x ::: Ord.Ordering
  55   sign = compare (ZeroAxiom ... 0)
  56 instance Signable Natural
  57 instance Signable Int
  58 instance Signable Integer
  59
  60 newtype PositiveOrNull a x = PositiveOrNull (x ::: a / x >= Zero)
  61 instance Axiom (PositiveOrNull a Zero)
  62 instance Axiom (PositiveOrNull a (Opposite (Zero)))
  63 instance Axiom (PositiveOrNull a (Succ n))
  64
  65 newtype PositiveNonNull a x = PositiveNonNull (x ::: a / x > Zero)
  66 instance Axiom (PositiveNonNull a (Succ n))
  67
  68 newtype NegativeOrNull a x = NegativeOrNull (x ::: a / x <= Zero)
  69 instance Axiom (NegativeOrNull a Zero)
  70 instance Axiom (NegativeOrNull a (Opposite (Zero)))
  71 instance Axiom (NegativeOrNull a (Opposite ((Succ n))))
  72
  73 newtype NegativeNonNull a x = NegativeNonNull (x ::: a / x < Zero)
  74 instance Axiom (NegativeNonNull a (Succ n))
  75
  76 data Opposite n = OppositeAxiom
  77
  78 class Oppositeable a where
  79   opposite :: x ::: a -> Opposite x ::: a
  80   opposite (Named x) = OppositeAxiom ... x
  81
  82 instance Oppositeable Int
  83 instance Oppositeable Integer
  84
  85 instance Axiom (Opposite (Opposite (x ::: Integer)) == x)
  86
  87 data IntMax
  88 intMax :: Int
  89 intMax = maxBound
  90
  91 type AxiomUpperBound max i a = (i ::: a) < max -> (i ::: a) < ((i ::: a) + One)
  92 instance Axiom (AxiomUpperBound IntMax i Int)
  93
  94 type AxiomNoUpperBound i a = (i ::: a) < Succ (i ::: a)
  95 instance Axiom (AxiomNoUpperBound i Natural)
  96 instance Axiom (AxiomNoUpperBound i Integer)
  97
  98 data (+) xs ys
  99 type role (+) nominal nominal
 100
 101 -- | `(+)` commutes
 102 instance Axiom (Commutative (+) x y)
 103
 104 -- | `(+)` is associative
 105 instance Axiom (Associative (+) x y z)