[Agda] How to prove termination for the iterated halving function over the rationals?

[Nils Anders Danielsson]

On 2019-12-11 10:27, Marko Grdinic wrote:
> Sorry for being pushy, but lately I've gotten an interest in rational
> math and I really want some input from the experts here regarding how
> to prove termination of the above. Implementing the function was easy,
> but proving the termination seems impossible so at the very least I
> need to understand whether that impression is right or not. Silence as
> the reply just has too many possible interpretations to deal with.

You are trying to compute a number n such that b / 2 ^ n < a for some
rational number a strictly between 0 and the rational number b, right?
Your current approach is to try 1, then 2, then 3, and so on. This is
reminiscent of Markov's principle, which should not be provable in Agda.
Thus I suggest that you try a different approach that makes more "active
use" of the inputs a and b.

-- 
/NAD