I want to call a recursive function n time. Then check a relation (a<?b) between two input arguments(a b:nat) of function. If it is true then add c to the list else do nothing.
Fixpoint myfunction (n a b c d :nat): list nat := match n with | O => nil | S n' => match a <? b with | true => c:: (myfunction n' a b c d ) | false => (myfunction n' a b c d ) end end.
But I want to add a constrain that number of elements in the output list(in case of true test condition- a<b) is always equal to d. Please guide me how to adjust this constrain.
Do you mean something like
repeat from library
repeat c d instead of
c in the function?
c is the output of another function which is varying and is taken as input argument by myfunction. But it will add in the output list after (a<b) test condition is true.Some time it is true and some time false. As a result count of added elements in the output list is not known to me. But I want no of elements in the output list equal to d( nat). c is not fix therefore cannot use repeat function.Is it possible, when c add in the list ,I start increment a value when that value become equal to d then stop recursive call.
d are not modified through recursive calls, the output will always be a repetition of
c or the empty list:
Lemma myfunction_spec n a b c d: myfunction n a b c d = if a <? b then repeat c n else nil. Proof. induction n; simpl; destruct (a <? b); rewrite ? IHn; auto. Qed.
If c is not fix and its value is varying. First assigning value to c then how modify myfunction_spec.
c varying? is it given by a function of the position in the output list (
nat -> nat) or taken from an input list (
In above lemma c is input nat argument. But I have another function which gives c as output. The value of c is varying depends on calculation. So on each iteration different values of c pass to above myfunction(as input nat argument).Just want to add that c in output list if condition(a<b) holds.
c is given to
myfunction as a
nat, it will not vary through iterations. You probably have either to group
myfunction with the one computing
c, or to use a richer interface type between the two functions to encode the values of
nat -> nat,
list nat, etc.), so that
myfunction could have access to them.
Fixpoint myfunction (n a b f c d :nat)(l:list nat): list nat := let n := n + (f1 a l) in match n with | O => nil | S n' => match a <? b with | true => c:: (myfunction n' a b (S f) c d l) | false => (myfunction n' a b (S f) c d l) end end.
Initial value of n is some natural number. I want to write a lemma statement which relate the number of elements in the output list and (S f). How value of (S f) can be use to determine the number of elements in the list? f1 is another function gives natural number as output.
Your function may loop forever, thus is not accepted by Coq.
Error: Cannot guess decreasing argument of fix.
Let's take a numerical example. Assume for instance
f1 a l = 10(it's possible).
If you compute
myfunction 2 a b f c d l, you redeclare
n+ f1 a l, which gives
12, and you recursively call
my_function 11 a b (S f) c d l, then
my_function 20 a b (S (S f)) c d l, etc.
Please note that using the same variable name
nin the function arguments and the local variable introduced by the
letmakes it more difficult to read the code and make one believe at first sight that the function is structurally recursive in
n, If you rename the inner
p, the issue is more obvious.
f is incremented by 1 at each recursive call, but is not used in the tests nor in the value returned by
my_function. So, it would be better to remove it and make the code simpler. Likewise,
dis not used.
Value of n is increasing on each iteration . When it reaches a particular value then it reset to zero. This is done by function f1 which keeps an eye on n,on particular value of n reset it to zero,so it is not increasing function for ever.
You asked n =2 and f1 a l = 10 if n=2 is maximum value then f1 a l = 10 is not possible . What modification I should made so that requirement get fulfill?
Function (f1 a l) is just a function for controlling n.
Last updated: Oct 03 2023 at 21:01 UTC