[Agda] Interesting issue with termination checker

Andreas Abel andreas.abel at ifi.lmu.de
Fri Jun 28 09:40:22 CEST 2013

```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/
-------------- next part --------------
module TerminationCumming where

open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality

append : {A : Set}{n : ℕ} (xs : Vec A n) (x : A) → Vec A (suc n)
append = ?
{-
append []       y = y ∷ []
append (x ∷ xs) y = x ∷ append xs y
-}

module Swapped where

reverse-inv : {A : Set} {n : ℕ} -> (xs : Vec A n) -> xs ≡ reverse (reverse xs)
reverse-inv [] = refl
reverse-inv (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

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

module Orig where

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