zohaze (May 21 2022 at 17:37): zohaze (May 21 2022 at 17:37):(deleted)
zohaze (May 21 2022 at 17:48):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.
Pierre Castéran (May 22 2022 at 13:29):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 Fixpoint.
Otherwise, you would have to use some commands like Function for instance.
zohaze (May 22 2022 at 18:34):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: Sep 23 2023 at 14:01 UTC