(deleted)

I am implementing following relation in Coq ,but get error message "not found decreasing argument".I don't know why it happens .Value of output function is decreasing on each recursive call(still get message).

a= (1+a) mod n. I want to save all resultant a(s) in a list and want to repeat this upto loop value(loop:nat). Value of a is continously increasing and it get zero when (1+a)=n. So this function should converge.I have performed matching on a and recursive call on natural number loop.

If it is the same function as in the "List formation" thread, then the convergence argument is not based on `a`

, but on the number of elements you still have to add to the list (what you called `loop`

and I called `size`

in my post). This argument is structurally decreasing and your function can be defined by `Fixpoint`

.

Otherwise, you would have to use some commands like `Function`

for instance.

Loop= no of time a function is recursively call(I have this)

size= no of elements that i will add in the output list OR total no of elements in the list. l will check all elements of the list if some elements fullfill a condition then they will be in the list otherwise not. In this case both have a difference. Now function is converging or not. When and why fix sometime appears ,especially when one function is being call by another one .Individually both are ok.

Last updated: Jun 16 2024 at 01:42 UTC