Termination checker stumped by with-abstraction --without-K

[mjustus]

When using --without-K, Agda fails to see that the two mutually-recursive functions defined below are structurally recursive. Both enabling --with-K as well as replacing the with-abstraction by a helper function make the program pass the termination check.

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Nat

peek : Nat → Nat
pop  : Nat → Nat

pop zero    = 0
pop (suc n) = peek n

peek   zero    = 0
peek   (suc _) with 0
peek n@(suc _) | _ = pop n

[andreasabel]

This is a known issue, however, I could not find the number.
peek passes --with-K because there is a heuristics for with-clauses that is unsound --without-K.

This specific example, however, passes with increased termination depth:

{-# OPTIONS --without-K #-}
{-# OPTIONS --termination-depth=2 #-}
...

The reason is that the with-function is implemented as:

peek (suc m) = peek-with m 0
peek-with m k = pop (suc m)

and to track also argument increase (suc m) you need termination depth 2.

Both enabling --with-K as well as replacing the with-abstraction by a helper function ...

I think you meant:

Either enabling --with-K or replacing the with-abstraction by a helper function ...

[mjustus]

Thanks for the explanation! I suppose this really is just an instance of #59 (and #238).

I think you meant: [...]

Yeah, I could have phrased that a bit more clearly.

[nad]

This is a known issue, however, I could not find the number.

#1680, #1023?

[halfaya]

Here is another example that uses records rather than mutual recursion. As demonstrated by the two "ok" examples, using records or with alone is fine, but when they are combined, as in the original insert code, the termination checker fails. It passes if -without-K is turned off.

{-# OPTIONS --without-K #-}

module WithoutKTermination where

open import Data.List                             using (List; []; _∷_)
open import Relation.Binary.Core                  using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary                      using (yes; no)

record ListSet (A : Set) : Set where
  constructor listSet
  field
    set : List A
    eq  : Decidable {A = A} _≡_
open ListSet    

insertOk : {A : Set} → A → ListSet A → ListSet A
insertOk a (listSet []      e) = listSet (a ∷ []) e
insertOk a (listSet (b ∷ l) e) = listSet (b ∷ set (insertOk a (listSet l e))) e

insertOk2 : {A : Set} → Decidable {A = A} _≡_ → A → List A → List A
insertOk2 e a [] = a ∷ []
insertOk2 e a (b ∷ l) with e a b
insertOk2 e a l@(b ∷ _) | yes p = l
insertOk2 e a (b ∷ l)   | no ¬p = b ∷ (insertOk2 e a l)

insert : {A : Set} → A → ListSet A → ListSet A
insert a (listSet []      e) = listSet (a ∷ []) e
insert a (listSet (b ∷ l) e) with e a b
insert a (listSet l@(b ∷ _) e) | yes p = listSet l e
insert a (listSet   (b ∷ l) e) | no ¬p = listSet (b ∷ set (insert a (listSet l e))) e

[UlfNorell]

Closing as duplicate of #59.