I was trying to train on this kata about longest common subsequences of a list which I slightly modified so that it worked with my versions of agda and the standard library (Agda 2.6.2, stdlib 1.7) which results in this code
{-# OPTIONS --safe #-}
module pg where
open import Data.List
open import Data.Nat
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
data Subseq {n} { A : Set n } : List A → List A → Set where
subseq-nil : Subseq [] []
subseq-take : ∀ a xs ys → Subseq xs ys → Subseq (a ∷ xs) (a ∷ ys)
subseq-drop : ∀ a xs ys → Subseq xs ys → Subseq xs (a ∷ ys)
is-lcs : ∀ {n} {A : Set n} → List A → List A → List A → Set n
is-lcs zs xs ys =
(Subseq zs xs × Subseq zs ys) ×
(∀ ts → Subseq ts xs → Subseq ts ys → length ts ≤ length zs)
longest : ∀ {n} {A : Set n} → List A → List A → List A
longest s1 s2 with length s1 ≤? length s2
... | yes _ = s2
... | no _ = s1
lcs : ∀ {n} {A : Set n} → Decidable {A = A} _≡_ → List A → List A → List A
lcs _ [] _ = []
lcs _ _ [] = []
lcs dec (x ∷ xs) (y ∷ ys) with dec x y
... | yes _ = x ∷ lcs dec xs ys
... | no _ = longest (lcs dec (x ∷ xs) ys) (lcs dec xs (y ∷ ys))
Unfortunetaly, Agda fails to recognize that lcs is a terminating function, which I honestly don't understand : the recursive calls are made on structurally smaller arguments if I get it right ? If anyone can explain me what the problem is here, it would help tremendously. Thanks in advance !
Try to avoid using with when dealing with termination. The termination checker is successful when your code is refactored as follows (note that I removed your first two definitions because they are irrelevant in your question, maybe you should edit it accordingly):
{-# OPTIONS --safe #-}
open import Data.List
open import Data.Nat
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Data.Bool using (if_then_else_)
module Term where
longest : ∀ {a} {A : Set a} → List A → List A → List A
longest s1 s2 with length s1 ≤? length s2
... | yes _ = s2
... | no _ = s1
lcs : ∀ {a} {A : Set a} → Decidable {A = A} _≡_ → List A → List A → List A
lcs _ [] _ = []
lcs _ _ [] = []
lcs dec (x ∷ xs) (y ∷ ys) = if does (dec x y) then
x ∷ lcs dec xs ys else
longest (lcs dec (x ∷ xs) ys) (lcs dec xs (y ∷ ys))
Apparently, this is a known limitation of the with abstraction combined with the termination checker as noted in the wiki:
https://agda.readthedocs.io/en/v2.6.2.1/language/with-abstraction.html#termination-checking
Here is a similar question: