[Agda] Termination checking with Lexicographic recursive calls

[Sergey Goncharov]

Dear all,

the following definitions of mutually recursive function h₁ and h₂ are 
not accepted without the TERMINATING pragma, although the recursive 
calls are arranged lexicographically, i.e. either the first argument 
decreases, or it remains the same and the second one decreases.

This is analogous the the implementation of the Ackermann function from 
the Agda documentation, where it works.

Any ideas why the following is not accepted?

I've managed to amend these definitions, by adding an explicit parameter 
of a suitable well-order type, mimicking the lexicographic descend in a 
straightforward way, and then the code is accepted, but I am still 
dubious why I had to do it.

Many thanks for any eventual hints!

Sergey



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

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Function
open import Data.Empty using (⊥-elim)

-- -----
π′ : ℕ → ℕ
π′ 0 = 0
π′ (suc n) = π′ n + (suc n)

{-# TERMINATING #-}
h₁ : ∀ (n k : ℕ) → (k ≤ n) → π₁⁻¹ (π′ n + k) ≡ n ∸ k
h₂ : ∀ (n k : ℕ) → (k ≤ n) → π₂⁻¹ (π′ n + k) ≡ k

h₁ zero k p rewrite n≤0⇒n≡0 p = refl

h₁ (suc n) zero p rewrite +-identityʳ (π′ n + suc n) | +-suc (π′ n) n 
with (π₁⁻¹ (π′ n + n)) | inspect π₁⁻¹ (π′ n + n)
h₁ (suc n) zero p | zero  | [ eq ] = cong suc (h₂ n n ≤-refl)
h₁ (suc n) zero p | suc m | [ eq ] = ⊥-elim (1+n≢0 (trans (sym eq) 
(trans (h₁ n n ≤-refl) (n∸n≡0 n))))

h₁ (suc n) (suc k) p rewrite +-suc (π′ n + suc n) k with (π₁⁻¹ (π′ n + 
suc n + k)) | inspect π₁⁻¹ (π′ n + suc n + k)
h₁ (suc n) (suc k) p | zero  | [ eq ] = ⊥-elim (1+n≰n (≤-trans 
(m∸n≡0⇒m≤n {suc n} {k} (trans (sym (h₁ (suc n) k (≤-trans (n≤1+n k) p))) 
eq)) (≤-pred p)))
h₁ (suc n) (suc k) p | suc m | [ eq ] = suc-injective (trans (sym eq) 
(trans (h₁ (suc n) k (≤-trans (n≤1+n k) p)) (+-∸-assoc 1 (≤-pred p))))

h₂ zero k p rewrite n≤0⇒n≡0 p = refl
h₂ (suc n) zero p rewrite +-identityʳ (π′ n + suc n) | +-suc (π′ n) n | 
h₁ n n ≤-refl | n∸n≡0 n = refl
h₂ (suc n) (suc k) p rewrite +-suc (π′ n + suc n) k | h₁ (suc n) k 
(≤-trans (n≤1+n k) p) with (suc n ∸ k) | inspect (suc n ∸_) k
... | 0     | [ eq ] =  ⊥-elim (1+n≰n (≤-trans (m∸n≡0⇒m≤n{suc n}{k} eq) 
(≤-pred p)))
   where h = ≤-trans (m∸n≡0⇒m≤n{suc n}{k} eq) (≤-pred p)
... | suc m | [ eq ] = cong suc (h₂ (suc n) k (≤-trans (n≤1+n k) p))


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5384 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200217/b7518b00/attachment.p7s>