[Agda] Termination checking (perhaps could be smarter)

[Sergei Meshveliani]

On Thu, 2015-01-15 at 15:55 -0200, Carlos Camarao wrote:
> Hello.
> 
> I am writing a simple insertion sort program in Agda, and proving its
> correctness. I am using the following predicate (the full code of the
> program is attached; I am using Agda version 2.3.2.2):
> 
> sorted : List A → Bool
> sorted []           = true
> sorted (_ ∷ [])    = true
> sorted (a ∷ b ∷ x) with a ≤? b
> ... | yes _ = sorted (b ∷ x)
> ... | no  _ = false
> 
> [..]

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),

then a proof of sortedness becomes explicit, becomes an Agda data.
Respectively, the function `sort' could build the sorted list  zs
together with the witness  proof : Sorted zs.

(Also we keep in mind that correctness here includes a certain condition
besides sortedness).

Regards,

------
Sergei