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
loopand I called
size in my post). This argument is structurally decreasing and your function can be defined by
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: Jan 29 2023 at 05:03 UTC