[Agda] Interesting issue with termination checker

[Andreas Abel]

Actually none of your versions should termination-check, since there is 
a non-wellfounded call relation

   reverse-inv --> lem2 --> reverse-inv --> lem2 ...

If there is yellow stuff left, the analysis of the termination checker 
is incomplete.

On 28.06.13 9:40 AM, Andreas Abel wrote:
> Hello Tom,
>
> first, please ALWAYS post self-contained code.  And say which version of
> Agda you are using.
>
> Your code is missing a definition of append.
>
> If I leave append undefined
>
>    append = ?
>
> then the version below does not termination check, but the swapped
> version.  (Using Agda development version).
>
> Cheers,
> Andreas
>
> On 27.06.13 11:38 AM, Tom Cumming wrote:
>> When the commented 'lem2' is swapped with the uncommented version agda
>> fails to prove termination. Could someone please shed some light as to
>> why:
>>
>> reverse-inv : {A : Set} {n : ℕ} -> (xs : Vec A n) -> xs ≡ reverse
>> (reverse xs)
>> reverse-inv [] = refl
>> reverse-inv (x ∷ xs) = sym (lem2 (lem x xs)) -- lem2 (lem x xs)
>>    where
>>      lem : {A : Set} {n : ℕ} -> (x : A) -> (xs : Vec A n) -> reverse (x
>> ∷ xs) ≡ append (reverse xs) x
>>      lem x xs = refl
>>
>> {- * This way cannot be proved to terminate
>>      lem2 : {A : Set} {n : ℕ} -> {xs ys : Vec A n} -> reverse xs ≡ ys
>> -> xs ≡ reverse ys
>>      lem2 {A} {n} {xs} {.(reverse xs)} refl = reverse-inv xs
>> -}
>>
>>      lem2 : {A : Set} {n : ℕ} -> {xs ys : Vec A n} -> xs ≡ reverse ys
>> -> reverse xs ≡ ys
>>      lem2 {A} {n} {.(reverse xs)} {xs} refl = sym (reverse-inv xs)
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/