I'd like to understand why this function is not accepted as a terminating one:
val while_items: ni: nat -> ni_max: nat -> nw: nat -> bool
let rec while_items ni ni_max nw =
(if ni < ni_max
then while_items (ni + nw) ni_max nw
else true)
FStar rejects it and sends the following message:
(Error) Could not prove termination of this recursive call: The solver found a (partial) counterexample...
It's likely not the same binding issue here as the one in my related question under FStar function strange behavior
Can FStar show the counter example?
As explained in the tutorial, by default F* uses a decreases measure that puts all arguments in lexicographic order
val while_items: ni: nat -> ni_max: nat -> nw: nat -> Tot bool (decreases %[ni,ni_max;nw])
which doesn't work for proving this function terminating, since clearly ni + nw is not smaller than ni.
With a correct decreases measure and a precondition that nw is positive this does go through:
val while_items: ni: nat -> ni_max: nat -> nw: pos ->
Tot bool (decreases (if ni < ni_max then ni_max-ni else 0))
Not exactly the original example, but that one definitely loops forever for nw=0! And anyway, even after this fix this code makes little sense as is and using such loops is not idiomatic for functional programming.
Finally, F* can't produce counterexamples, and this error message has recently been fixed: https://github.com/FStarLang/FStar/pull/2075