
  0 | ||| Irreflexive and trichomotomous relations, and total orders
  1 | module Control.Relation.TotalOrder
  2 | 
  3 | import Data.Nat
  4 | import Decidable.Equality
  5 | 
  6 | 
  7 | public export
  8 | interface Irreflexive (0 a : Type) (0 r : a -> a -> Type) | r where
  9 |   irrefl : {0 x : a} -> r x x -> Void
 10 | 
 11 | ||| Alternative version of irreflexivity
 12 | public export
 13 | irrefl' : Irreflexive a r => {0 x : a} -> {0 y : a} -> r x y -> x = y -> Void
 14 | irrefl' p Refl = irrefl p
 15 | 
 16 | public export
 17 | natIrrefl : LT x x -> Void
 18 | natIrrefl (LTESucc y) = natIrrefl y
 19 | 
 20 | public export
 21 | Irreflexive Nat LT where
 22 |   irrefl = natIrrefl
 23 | 
 24 | 
 25 | {-
 26 | totalOrderAntisymmetry : (Irreflexive a r, Transitive a r) => {0 x : a} -> {0 y : a} -> r x y -> r y x -> Void
 27 | totalOrderAntisymmetry p q = irrefl (transitive p q)
 28 | -}
 29 | 
 30 | 
 31 | public export
 32 | data Trichotomy : (0 r : a -> a -> Type) -> a -> a -> Type where
 33 |   LT : {0 x : a} -> {0 y : a} -> r x y -> Trichotomy r x y
 34 |   EQ : x = y -> Trichotomy r x y
 35 |   GT : {0 x : a} -> {0 y : a} -> r y x -> Trichotomy r x y
 36 | 
 37 | public export
 38 | interface Trichotomous a r | r where
 39 |   trichotomy : (x : a) -> (y : a) -> Trichotomy r x y
 40 | 
 41 | public export
 42 | trichotomySucc : Trichotomy LT m n -> Trichotomy LT (S m) (S n)
 43 | trichotomySucc (LT l) = LT (LTESucc l)
 44 | trichotomySucc (EQ e) = EQ (cong S e)
 45 | trichotomySucc (GT l) = GT (LTESucc l)
 46 | 
 47 | public export
 48 | Trichotomous Nat LT where
 49 |   trichotomy 0 0 = EQ Refl
 50 |   trichotomy 0 (S n) = LT (LTESucc LTEZero)
 51 |   trichotomy (S m) 0 = GT (LTESucc LTEZero)
 52 |   trichotomy (S m) (S n) = trichotomySucc (trichotomy m n)
 53 | 
 54 | 
 55 | public export
 56 | succLTE : LTE x y -> LTE x (S y)
 57 | succLTE LTEZero = LTEZero
 58 | succLTE (LTESucc a) = LTESucc (succLTE a)
 59 | 
 60 | public export
 61 | precLTE : LTE (S x) y -> LTE x y
 62 | precLTE (LTESucc z) = succLTE z
 63 | 
 64 | public export
 65 | Transitive Nat LT where
 66 |   transitive a b = transitive a (precLTE b)
 67 | 
 68 | 
 69 | ||| Very similar to LinearOrder (in Control.TotalOrder) but based off LT rather than LTE
 70 | public export
 71 | interface (Irreflexive a r, (Transitive a r, Trichotomous a r)) => TotalOrder a r | r where
 72 | 
 73 | public export
 74 | TotalOrder Nat LT where
 75 |