make Sorted complexity linear in the list length (#316)

src/Util.idr

@@ -101,17 +101,19 @@ namespace List
     map f [] {allOk = []} = []
     map f (x :: xs) {allOk = ok :: _} = f {ok} x :: map f xs
 
-  ||| A `Sorted f (x :: xs)` proves that `(x :: xs)` is sorted such that `f x y` exists for all `y`
-  ||| in `xs`. For example, a `Sorted LT xs` proves that all `Nat`s in `xs` appear in increasing
-  ||| numerical order.
+  ||| A `Sorted f xs` proves that for all consecutive elements `x` and `y` in `xs`, `f x y` exists.
+  ||| For example, a `Sorted LT xs` proves that all `Nat`s in `xs` appear in increasing numerical
+  ||| order.
   public export
   data Sorted : (a -> a -> Type) -> List a -> Type where
     ||| An empty list is sorted.
-    Nil : Sorted f []
+    SNil : Sorted f []
 
-    ||| A list is sorted if its tail is sorted and the head is sorted w.r.t. all elements in the
-    ||| tail.
-    (::) : (x : a) -> Sorted f xs -> {auto 0 ok : All (f x) xs} -> Sorted f (x :: xs)
+    ||| Any single element is sorted.
+    SOne : Sorted f [x]
+
+    ||| A list is sorted if its tail is sorted and the head is sorted w.r.t. the head of the tail.
+    SCons : (y : a) -> f y x -> Sorted f (x :: xs) -> Sorted f (y :: x :: xs)
 
   namespace Many
     ||| Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]

test/Unit/TestUtil.idr

@@ -92,6 +92,41 @@ namespace List
     deleteAtHeadAndLater _ _ _ [] = Refl
     deleteAtHeadAndLater _ _ _ (_ :: _) = Refl
 
+  repeatedNotLT : Sorted LT [x, x] -> Void
+  repeatedNotLT SNil impossible
+  repeatedNotLT SOne impossible
+  repeatedNotLT (SCons _ ok _) = succNotLTEpred ok
+
+  repeatedLaterNotLT : Sorted LT [x, y, y] -> Void
+  repeatedLaterNotLT SNil impossible
+  repeatedLaterNotLT SOne impossible
+  repeatedLaterNotLT (SCons _ _ tail) = repeatedNotLT tail
+
+  ltNotReflexive : (x, y : Nat) -> LT x y -> LT y x -> Void
+  ltNotReflexive 0 0 LTEZero _ impossible
+  ltNotReflexive 0 0 (LTESucc _) _ impossible
+  ltNotReflexive 0 (S _) (LTESucc _) LTEZero impossible
+  ltNotReflexive 0 (S _) (LTESucc _) (LTESucc _) impossible
+  ltNotReflexive (S _) 0 LTEZero _ impossible
+  ltNotReflexive (S _) 0 (LTESucc _) _ impossible
+  ltNotReflexive (S x) (S y) (LTESucc xlty) (LTESucc yltx) = ltNotReflexive x y xlty yltx
+
+  repeatedDispersedNotLT : Sorted LT [y, x, y] -> Void
+  repeatedDispersedNotLT (SCons y yltx (SCons x xlty SOne)) = ltNotReflexive x y xlty yltx
+
+  increasingLT : (x : Nat) -> Sorted LT [x, S x, S (S x)]
+  increasingLT x = SCons x (reflexive {ty=Nat}) (SCons (S x) (reflexive {ty=Nat}) SOne)
+
+  succNotLT : (x : Nat) -> LT (S x) x -> Void
+  succNotLT 0 LTEZero impossible
+  succNotLT 0 (LTESucc _) impossible
+  succNotLT (S x) (LTESucc lte) = succNotLT x lte
+
+  decreasingNotLT : (x : Nat) -> Sorted LT (S x :: x :: xs)  -> Void
+  decreasingNotLT _ SNil impossible
+  decreasingNotLT _ SOne impossible
+  decreasingNotLT x (SCons (S x) ok _) = succNotLT x ok
+
 export
 group : Group
 group = MkGroup "Util" $ [