[Agda] Termination not being proven

[gallais at EnsL.org]

Hi Will,

This issue is an instance of a the well known « merge issue » [1] and
you should be able to fix it by pre-computing [sorted (y :: ys)]:

===============================

sorted : List ℕ → Bool
sorted [] = true
sorted (_ ∷ []) = true
sorted (x ∷ (y ∷ ys)) with x <= y | sorted (y ∷ ys)
... | true | b = b
... | false | _ = false

===============================

If I'm not mistaken the computational behavior should be the same
(lazyness & all that).

Cheers,

--
guillaume

[1] http://code.google.com/p/agda/issues/detail?id=59


On 27 February 2011 21:51, Will Sonnex <will at sonnex.name> 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.
>
>
> Cheers,
>
> Will
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>