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 `List`

?

`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.

Since `a`

, `b`

, `c`

and `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.

How is `c`

varying? is it given by a function of the position in the output list (`nat -> nat`

) or taken from an input list (`list nat`

)?

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.

If `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 `c`

(`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 `n=2`

and `f1 a l = 10`

(it's possible).

If you compute `myfunction 2 a b f c d l`

, you redeclare `n`

as `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 `n`

in the function arguments and the local variable introduced by the `let`

makes 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 `n`

into `p`

, the issue is more obvious.

The variable `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, `d`

is not used.

(deleted)

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