[Agda] Termination not being proven

[Dan Licata]

Hi Will,

I think the problem is with the 'with'.  The 'with' gets compiled as a
helper function, and I think what is happening is that both y and ys are
getting passed as separate arguments to the helper function, so Agda
loses sight of the fact that, when you put them back together, what you
get is something smaller than the input.  

For example, if you rewrite it as follows:

  sorted' : List Nat -> Bool
  sorted' [] = True
  sorted' (x :: t) with t 
  ... | [] = True
  ... | y :: xs with lte x y 
  ...              | True = sorted' t
  ...              | False = False

(sorry for switching notation to my library)

then it termination-checks.  

The nicest way to write it is to define _andalso_ : Bool -> Bool -> Bool
and then avoid using a 'with' at all:

  sorted'' : List Nat -> Bool
  sorted'' [] = True
  sorted'' (x :: []) = True
  sorted'' (x :: y :: xs) = lte x y andalso sorted'' (y :: xs)

In this version Agda spots what you want it to.

Make sense?
-Dan

On Feb27, Will Sonnex wrote:
> I have a structurally recursive function which checks whether a list
> is sorted, but Agda tells me it cannot prove termination:
> 
> _<=_ : ℕ → ℕ → Bool
> zero <= _ = true
> suc x <= zero = false
> suc x <= suc y = x <= y
> 
> sorted : List ℕ → Bool
> sorted [] = true
> sorted (_ ∷ []) = true
> sorted (x ∷ (y ∷ ys)) with x <= y
> ... | true = sorted (y ∷ ys)
> ... | false = false
> 
> 
> It seems strange to me that Agda can show "xs ≺ x :: xs" but not "y ::
> ys ≺ x :: (y :: ys)", since the former is a more general case of the
> latter.
> 
>