[Agda] Interesting issue with termination checker

[Andreas Abel]

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)