How to provide proof for termination in Agda?

Question

I am trying to write an integer division function from scratch in agda2 (as of 2.6.3):

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_∸_ : ℕ → ℕ → ℕ
_∸_ m n = {}0

div : ℕ → ℕ → ℕ
div m n with m ∸ n 
...     | 0  = 0
...     | x = suc (div x n)

The basic idea is to use the monus function ∸ (integer minus) to subtract n from m until the difference is zero. But when loading the file, there is an error:

Termination checking failed for the following functions:
  div
Problematic calls:
  div m n | m ∸ n
  div x n

I can see that the error happens because agda has no way to tell if the monus function is decreasing until it reaches zero (i.e. m ∸ n < m unless m is 0).

My questions are:

1. How do I provide a proof to agda that m ∸ n is less than m, and the recursion is decreasing on the first argument?

2. Is it OK if the argument is decreasing only before reaching the base case (zero here)?

Note: I looked at the documentation, which only says that one can use the following pragmas to basically ignore the termination check.

TERMINATING and NON_TERMINATING

But I'd like to provide a proof rather than dictate to agda that monus is decreasing (since what the human asserts could be wrong).

Answer 1

There are three possible approaches:

1. Use a different algorithm, like division in stdlib, see div-helper.
2. Use the well-founded induction library. There are many online resources with examples, like https://stackoverflow.com/a/61704076/7083401.
3. Use a natural number parameter as the indicator of termination, and make its initial value big enough. For instance, I can define it with an auxiliary parameter k, where the initial value of k is big enough, and k gets smaller as the recursion proceeds:

div' : ℕ → ℕ → ℕ → ℕ
div' zero m n = 0
div' (suc k) m n with m ∸ n
...     | 0  = 0
...     | x = suc (div' k x n)

div : ℕ → ℕ → ℕ
div m n = div' m m n