3
$\begingroup$

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).

$\endgroup$

1 Answer 1

5
$\begingroup$

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
$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.