[Agda] Termination checking (perhaps could be smarter)

[Sergei Meshveliani]

On Fri, 2015-01-16 at 01:22 +0400, flicky frans wrote:
> > 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)
> 

Only    ≤* x = All (_≤_ x)

looks simpler, and remains explicit.

 
> 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.

And what may be here a proof for that  []  is sorted?