[Agda] termination checking

[Peter Selinger]

I have a question about termination checking. The following example
has been vexing me. I do not understand why the function
RecordExample.div-aux fails termination checking, while both
RecordExample.fibonacci and DataTypeExample.div-aux pass it.

Agda version 2.4.2.2. Might this be a subtle bug in the termination
checker with respect to inductive records? Or is there something
obvious that I am missing.

Any help appreciated! Thanks, -- Peter

P.S.: although the example works if I use a datatype, I prefer using a
record, because then I can use the constructor in let-bindings, and
also when matching against irrelevant arguments. In the case of
datatypes, these two kinds of pattern matches are not allowed.

----------------------------------------------------------------------
open import Data.Nat
open import Relation.Nullary

module TerminationExample where

-- Some true lemmas about natural numbers. Proofs omitted for brevity.
postulate
  lemma-refl : ∀ n -> n ≤ n
  lemma-suc : ∀ n -> n ≤ suc n
  lemma-order : ∀ {n m} -> ¬ n ≤ m -> n > 0
  lemma-minus : ∀ n m -> n > 0 -> n ∸ suc m < n

module RecordExample where

  -- A natural number is inductive if all smaller numbers are inductive.
  record Inductive (n : ℕ) : Set where
    inductive
    constructor cind
    field cind-field : ∀ {m} -> m < n -> Inductive m
  
  -- All natural numbers are inductive. Proof omitted for brevity.
  postulate
    lemma-inductive : ∀ n -> Inductive n
  
  -- Auxiliary function for integer division. The termination checker
  -- fails but I don't know why.  The third argument is clearly
  -- decreasing:
  -- 
  -- h proof < cind h
  
  {-# NON_TERMINATING #-}
  div-aux : (n : ℕ) -> ℕ -> Inductive n -> ℕ 
  div-aux n zero (cind h) = zero
  div-aux n (suc m) (cind h) with n ≤? suc m
  div-aux n (suc m) (cind h) | yes p = zero
  div-aux n (suc m) (cind h) | no p = suc (div-aux (n ∸ suc m) (suc m) (h proof))
    where
    proof : n ∸ suc m < n
    proof = lemma-minus n m (lemma-order p)
  
  -- Integer division.
  div : ℕ -> ℕ -> ℕ
  div n m = div-aux n m (lemma-inductive n)

  -- However, it does not *always* fail. Here is a situation that is a
  -- priori very similar, but termination checking succeeds without
  -- any problems.
  fibonacci-aux : (n : ℕ) -> Inductive n -> ℕ
  fibonacci-aux 0 (cind h) = 1
  fibonacci-aux 1 (cind h) = 1
  fibonacci-aux (suc (suc n)) (cind h) = fibonacci-aux n (h proof1) + fibonacci-aux (suc n) (h proof2)
    where
    proof1 : n < suc (suc n)
    proof1 = s≤s (lemma-suc n)
    
    proof2 : suc n < suc (suc n)
    proof2 = lemma-refl (suc (suc n))


module DataTypeExample where

  -- Redoing the same example using an inductive datatype instead of
  -- an inductive record.

  data Inductive : (n : ℕ) -> Set where
    cind : ∀ {n} -> (∀ {m} -> m < n -> Inductive m) -> Inductive n
  
  postulate
    lemma-inductive : ∀ n -> Inductive n

  -- This time it works like a charm.
  div-aux : (n : ℕ) -> ℕ -> Inductive n -> ℕ 
  div-aux n zero (cind h) = zero
  div-aux n (suc m) (cind h) with n ≤? suc m
  div-aux n (suc m) (cind h) | yes p = zero
  div-aux n (suc m) (cind h) | no p = suc (div-aux (n ∸ suc m) (suc m) (h proof))
    where
    proof : n ∸ suc m < n
    proof = lemma-minus n m (lemma-order p)
  
  -- Integer division.
  div : ℕ -> ℕ -> ℕ
  div n m = div-aux n m (lemma-inductive n)
----------------------------------------------------------------------