
  0 | module Data.Maybe.Lower
  1 | 
  2 | import Control.Function
  3 | import Data.Maybe
  4 | import Control.Relation
  5 | import Control.Relation.Trichotomy
  6 | 
  7 | %default total
  8 | 
  9 | ||| A total order for `Maybe a` where `a` has a total order
 10 | ||| and `Nothing` is the minimal value.
 11 | |||
 12 | ||| This is useful, for instance, when implementing provably
 13 | ||| sorted (assoc-) snoc-lists, indexed by a `Maybe key`, where
 14 | ||| the empty list has a `Nothing` index.
 15 | public export
 16 | data Lower : (lt : a -> a -> Type) -> (m1,m2 : Maybe a) -> Type where
 17 |   LNothing : Lower lt Nothing (Just v)
 18 |   LJust    :  {0 lt : a -> a -> Type}
 19 |            -> {0 v, w : a}
 20 |            -> lt v w -> Lower lt (Just v) (Just w)
 21 | 
 22 | public export
 23 | Uninhabited (Lower lt m Nothing) where
 24 |   uninhabited LNothing impossible
 25 |   uninhabited (LJust _) impossible
 26 | 
 27 | public export
 28 | Strict a lt => Uninhabited (Lower lt (Just k) (Just k)) where
 29 |   uninhabited LNothing impossible
 30 |   uninhabited (LJust refl) = void (irreflexive refl)
 31 | 
 32 | public export
 33 | fromLT : Lower lt (Just a) (Just b) -> lt a b
 34 | fromLT (LJust x) = x
 35 | 
 36 | ||| Implementation and alias for `trichotomy`.
 37 | export
 38 | comp : Trichotomous a lt => (m1,m2 : Maybe a) -> Trichotomy (Lower lt) m1 m2
 39 | comp (Just x) (Just y) = case trichotomy {rel = lt} x y of
 40 |   LT p c1 c2 => LT (LJust p) (\r => c1 (injective r)) (\x => c2 (fromLT x))
 41 |   EQ c1 p c2 => EQ (\x => c1 (fromLT x)) (cong Just p) (\x => c2 (fromLT x))
 42 |   GT c1 c2 p => GT (\x => c1 (fromLT x)) (\r => c2 (injective r)) (LJust p)
 43 | comp (Just x) Nothing  = GT absurd absurd LNothing
 44 | comp Nothing  (Just y) = LT LNothing absurd absurd
 45 | comp Nothing  Nothing  = EQ absurd Refl absurd
 46 | 
 47 | ||| If `lt` is a total order of `a`, then `Lower lt` is a
 48 | ||| total order of `Maybe a`.
 49 | export %inline
 50 | Trichotomous a lt => Trichotomous (Maybe a) (Lower lt) where
 51 |   trichotomy = comp
 52 | 
 53 | export %inline
 54 | Transitive a lt => Transitive (Maybe a) (Lower lt) where
 55 |   transitive y         LNothing  = absurd y
 56 |   transitive (LJust x) (LJust y) = LJust $ transitive x y
 57 |   transitive LNothing  (LJust y) = LNothing
 58 |