recursive function and pattern matching · Coq users

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.

Lessness (Aug 15 2021 at 11:21):

Do you mean something like repeat from library List?
repeat c d instead of c in the function?

sara lee (Aug 15 2021 at 17:42):

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.

Olivier Laurent (Aug 19 2021 at 11:42):

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.

sara lee (Sep 01 2021 at 15:35):

If c is not fix and its value is varying. First assigning value to c then how modify myfunction_spec.

Olivier Laurent (Sep 01 2021 at 15:56):

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)?

sara lee (Sep 04 2021 at 03:38):

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.

Olivier Laurent (Sep 04 2021 at 05:16):

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.

sara lee (Feb 04 2022 at 17:45):

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.

Pierre Castéran (Feb 04 2022 at 20:34):

Error: Cannot guess decreasing argument of fix.

Let's take a numerical example. Assume for instance n=2and f1 a l = 10(it's possible).
If you compute myfunction 2 a b f c d l, you redeclare nas 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 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, dis not used.

sara lee (Feb 05 2022 at 08:42):

sara lee (Apr 24 2022 at 12:39):

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.

Stream: Coq users

Topic: recursive function and pattern matching

sara lee (Aug 15 2021 at 05:32):