src/Logic/Theory/Ord.hs

   1 -- For `(<)`
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE Safe #-}
   4 -- For `axiom`
   5 {-# OPTIONS_GHC -Wno-deprecations #-}
   6
   7 module Logic.Theory.Ord (
   8   -- * Lower than
   9   type (<),
  10   (<),
  11
  12   -- * Lower or equal
  13   type (<=),
  14   (<=),
  15
  16   -- * Greater than
  17   type (>),
  18   (>),
  19
  20   -- * Greater or equal
  21   type (>=),
  22   (>=),
  23
  24   -- * Compare
  25   type Compare (),
  26   compare,
  27   type CompareProof (..),
  28 ) where
  29
  30 import Control.Applicative ((<*>))
  31 import Data.Bool (Bool)
  32 import Data.Bool qualified as Bool
  33 import Data.Either (Either (..))
  34 import Data.Functor ((<$>))
  35 import Data.Ord qualified as Ord
  36
  37 import Logic.Kernel
  38 import Logic.Theory.Bool
  39 import Logic.Theory.Eq
  40
  41 data (<) x y = LowerThanAxiom
  42 data (<=) x y = LowerOrEqualAxiom
  43 data (>) x y = GreaterThanAxiom
  44 data (>=) x y = GreaterOrEqualAxiom
  45 data Compare x y = Compare
  46
  47 type role (<) nominal nominal
  48 type role (<=) nominal nominal
  49 type role (>) nominal nominal
  50 type role (>=) nominal nominal
  51 type role Compare nominal nominal
  52
  53 infix 4 <
  54 infix 4 <=
  55 infix 4 >
  56 infix 4 >=
  57 infix 4 `Compare`
  58
  59 instance Axiom (x <= y <-> (x < y || x == y))
  60 instance Axiom (x >= y <-> (x > y || x == y))
  61 instance Axiom (x <= y && x >= y <-> x == y)
  62
  63 instance Axiom (x <= y <-> Not (x > y))
  64 instance Axiom (x < y <-> Not (x >= y))
  65 instance Axiom (x >= y <-> Not (x < y))
  66 instance Axiom (x > y <-> Not (x <= y))
  67
  68 instance Axiom (x < y -> Not (x == y))
  69 instance Axiom (x > y -> Not (x == y))
  70
  71 instance Provable ((x <= y) ::: Bool) where
  72   type ProofOf ((x <= y) ::: Bool) = Either (Proof (x > y)) (Proof (x <= y))
  73   prove (Named b) = case b of
  74     Bool.False -> Left (proven GreaterThanAxiom)
  75     Bool.True -> Right (proven LowerOrEqualAxiom)
  76
  77 instance Provable ((x < y) ::: Bool) where
  78   type ProofOf ((x < y) ::: Bool) = Either (Proof (x >= y)) (Proof (x < y))
  79   prove (Named b) = case b of
  80     Bool.False -> Left (proven GreaterOrEqualAxiom)
  81     Bool.True -> Right (proven LowerThanAxiom)
  82
  83 instance Provable ((x >= y) ::: Bool) where
  84   type ProofOf ((x >= y) ::: Bool) = Either (Proof (x < y)) (Proof (x >= y))
  85   prove (Named b) = case b of
  86     Bool.False -> Left (proven LowerThanAxiom)
  87     Bool.True -> Right (proven GreaterOrEqualAxiom)
  88
  89 instance Provable ((x > y) ::: Bool) where
  90   type ProofOf ((x > y) ::: Bool) = Either (Proof (x <= y)) (Proof (x > y))
  91   prove (Named b) = case b of
  92     Bool.False -> Left (proven LowerOrEqualAxiom)
  93     Bool.True -> Right (proven GreaterThanAxiom)
  94
  95 (<=) :: Ord.Ord a => x ::: a -> y ::: a -> (x <= y) ::: Bool
  96 (<=) (Named x) (Named y) = LowerOrEqualAxiom ... x Ord.<= y
  97
  98 (<) :: Ord.Ord a => x ::: a -> y ::: a -> (x < y) ::: Bool
  99 (<) (Named x) (Named y) = LowerThanAxiom ... x Ord.< y
 100
 101 (>=) :: Ord.Ord a => x ::: a -> y ::: a -> (x >= y) ::: Bool
 102 (>=) (Named x) (Named y) = GreaterOrEqualAxiom ... x Ord.>= y
 103
 104 (>) :: Ord.Ord a => x ::: a -> y ::: a -> (x > y) ::: Bool
 105 (>) (Named x) (Named y) = GreaterThanAxiom ... x Ord.> y
 106
 107 data CompareProof x y
 108   = CompareProofLT (Proof (x < y))
 109   | CompareProofEQ (Proof (x == y))
 110   | CompareProofGT (Proof (x > y))
 111 data OrdEq x y = OrdEqAxiom
 112 instance Axiom (OrdEq x y <-> (==) x y)
 113
 114 compare :: Ord.Ord a => x ::: a -> y ::: a -> Compare x y ::: Ord.Ordering
 115 compare (Named x) (Named y) = Compare ... Ord.compare x y
 116
 117 instance Provable (Compare x y ::: Ord.Ordering) where
 118   type ProofOf (Compare x y ::: Ord.Ordering) = CompareProof x y
 119   prove (Named o) = case o of
 120     Ord.LT -> CompareProofLT (proven LowerThanAxiom)
 121     Ord.EQ -> CompareProofEQ ((-->) <$> axiom @(OrdEq x y <-> (==) x y) <*> proven OrdEqAxiom)
 122     Ord.GT -> CompareProofGT (proven GreaterThanAxiom)
 123
 124 -- instance Axiom (x ::: Int == y ::: Int <-> Forall (z:::Int) (z <= x <-> z <= y))