[Agda] Termination checking (perhaps could be smarter)

[flicky frans]

> There also exists the following possibility.
> If you express sortedness as a certain type, like
>
>   data Sorted ... : Set _
>     where
>     empty  : Sorted []
>     single : \forall x -> Sorted (x ∷ [])
>     step   : x ≤ y -> Sorted (y ∷ ys) -> Sorted (x ∷ y ∷ ys)

To my small experience this is not a good way to express sortedness. I
verified once something like a quicksort in Coq and that definition
caused a lof of problems, since I needed double pattern-matching
everywhere to decide, whether the ``single'' or the ``step''
constructor must be applied.

A better definition, which I took from [1], is

    -- A proof that x is less than all values in xs
    data _≤*_ (x : A) : List A → Set where
      []  : x ≤* []
      _∷_ : ∀ {y ys} → (x ≤ y) → x ≤* ys → x ≤* (y ∷ ys)

    -- Proof that a list is sorted
    data IsSorted : List A → Set where
      []  : IsSorted []
      _∷_ : ∀ {x xs} → x ≤* xs → IsSorted xs → IsSorted (x ∷ xs)

My code became much clearer, when I switched to this definition.

Also, some time ago I wrote the ``insert'' function [2], which inserts
an element into a sorted list represented similarly, maybe it could be
useful.

One another representation, taken from [3], is

    data OList : Nat -> Set where
      Nil : {b : Nat} -> OList b
      Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b

I haven't tried to use it, but it looks like the best.

There is also the "Bag Equivalence via a Proof-Relevant Membership
Relation" paper about permutations by Nils Anders Danielsson.

[1] http://twanvl.nl/blog/agda/sorting
[2] http://lpaste.net/118527
[3] http://www.iis.sinica.edu.tw/~scm/2007/agda-exercise-proving-that-mergesort-returns-ordered-list/