[Agda] proving termination trouble again

[Ruben Henner Zilibowitz]

In relation to issue 59:

http://code.google.com/p/agda/issues/detail?id=59&can=1&q=termination

Here is another problem I've encountered along similar lines. In the code below, the functions f, g, h, and i all are in principal the same. However, only g and h pass the termination checker. Function f suffers from the problem in issue 59. Function g solves it with the same workaround suggested in issue 59. Function h solves it in a similar way. The problem is function i. It is very similar to function h but the argument (sn < ssn) in the helper function is concealed inside a product type and needs to be extracted using proj₂ which breaks this example. Is this a bug? Sorry for the hard to read code and function names..

The code below is based on Andreas Abel's earlier example..

Ruben

----------

module TerminationTwoConstructors where

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

bla : ℕ -> ℕ
bla m = m

f : ℕ -> ℕ
f zero = zero
f (suc zero) = zero
f (suc (suc n)) with bla (suc (suc n))
.... | m = f (suc n)

g : ℕ -> ℕ
g zero = zero
g (suc zero) = zero
g (suc (suc n)) = helper (suc (suc n)) (suc n) refl (bla (suc (suc n)))
  where
  helper : (ssn : ℕ) -> (sn : ℕ) -> (suc sn ≡ ssn) -> (m : ℕ) -> ℕ
  helper ssn sn _ m = g sn

≤-refl : _≡_ ⇒ _≤_
≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))

h : ℕ -> ℕ
h zero = zero
h (suc zero) = zero
h (suc (suc n)) = helper (suc (suc n)) (suc n) (≤-refl refl) (bla (suc (suc n)))
  where
  helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) -> ℕ
  helper ssn sn _ m = h sn

zog : (n : ℕ) -> (ℕ × n < suc n)
zog n = n , ≤-refl refl

i : ℕ -> ℕ
i zero = zero
i (suc zero) = zero
i (suc (suc n)) = let whee = zog (suc n) in helper (suc (suc n)) (proj₁ whee) (proj₂ whee) (bla (suc (suc n)))
  where
  helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) -> ℕ
  helper ssn sn _ m = i sn

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100112/5cbb4606/attachment.html