I have defined a function & lemma related to this function. But have error (prop error).How i can remove it and add element d in the list and then prove length of the list is 1.

Definition my_fun1 (a b c d: nat):list nat=

(a=0) ->

(b < c) ->

l= d::nil.

Lemma out_value: forall (a b c d : nat),

(a=0) ->

(b < c) ->

length(my_fun1 a b c)=1.

Elements `a`

, `b`

, and `c`

as well as hypotheses `a=0`

and `b<c`

do not seem to play any role here, so you can just consider:

```
Definition my_fun1 (d : nat) := d :: nil.
```

Then you can prove:

```
Lemma out_value: forall d, length (my_fun1 d) = 1.
```

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.

Thank you Olivier Laurent.

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)(l:list nat): list nat :=
match n with
| O => c::nil
| S n' => match a <?nth b l 0 with
| true =>c:: (myfunction n' a b c d l )
| false => (myfunction n' a b c d l )
end
end.
Want to find length of output list (which fulfill the criteria- true case). There should be some relation between n and length l?
```

If I add count (nat, initial value is zero) then on each recursive call,it get increment. Like

Fixpoint myfunction (n a b c d count:nat)(l:list nat): list nat :=

Let a= f(a) in

Let c= f'(c) in

match n with

| O => c::nil

| S n' => match a <?nth b l 0 with

| true => c:: (myfunction n' a b c d (S count) l )

| false => (myfunction n' a b c d count l )

end

end.

Now I can write

length (myfunction n a b c d count l)= count.

It seems you could test a <? b once, and you'll get either repeat n c ++ l, or l. Then the length is n + length l, or length l?

Sorry ,I forget writing two facts.1) b is the index and comparing value at this index. 2) a is changing value . Now on each recursive call value of a is compared with index value of input list. a<? nth b l 0 is not once but on each recursive call till n=0 with varying values of a & c.

Length determination is possible in above case?

Length finding and list formation are related to each other. I also want to know how to find length l in case of changing values.

The statement wit count does not work as-is: this function computes the count but does not return it. One can change the function to return it...

Or one can write a different function that just computes the final length (by doing the same comparisons) without producing a list (that'd be less efficient code but I don't know if that matters).

Would one or both those approaches be helpful?

I can sketch out the implementations; please just ask.

Better to find length separately,after removing count from function.

I can link n and length of output list?

Or one can write a different function that just computes the final length (by doing the same comparisons) without producing a list (that'd be less efficient code but I don't know if that matters).

Here's how that could look like, as a self-contained example. I've removed `d`

since it was not used.

`mylen`

is derived systematically from `myfunction`

:

```
Require Import List PeanoNat.
Import ListNotations.
Fixpoint myfunction (n a b c : nat) (l : list nat) : list nat :=
match n with
| O => [c]
| S n' =>
if a <? nth b l 0 then
c :: myfunction n' a b c l
else
myfunction n' a b c l
end.
Fixpoint mylen (n a b : nat) (l : list nat) : nat :=
match n with
| O => 1
| S n' =>
if a <? nth b l 0 then
1 + mylen n' a b l
else
mylen n' a b l
end.
Lemma myfun_len n a b c l : length (myfunction n a b c l) = mylen n a b l.
Proof.
induction n; simpl. { easy. }
rewrite <-IHn. now destruct (_ <? _).
Qed.
```

As you can see, `mylen`

follows `myfunction`

, but at each step returns _the length_ of what `myfunction`

would compute: 1 instead of `[c]`

(or `c :: nil`

), `mylen ...`

instead of `myfunction ...`

, and `1 + mylen ...`

instead of ` c :: myfunction n' a b c l`

.

As you might note, this assumes recursive calls to `mylen`

return the "expected" argument, so the proof of correctness must be by induction. Since `myfunction`

and `mylen`

recurse on `n`

, this should be induction on `n`

— which indeed works.

The statement wit count does not work as-is: this function computes the count but does not return it. One can change the function to return it...

FWIW, that one would mean writing `Fixpoint myfunction' (n a b c : nat) (l : list nat) : nat * list nat :=`

, returning a pair of the final length and the list. You'd have to destruct and rebuilt the pair at each recursive call.

Reference 16-oct. n1 > n2 & s < n2. It means recursive call is equal to n2 (lower value of pattern matching). We can prove mylen23=n2 ?

```
Require Import List PeanoNat.
Import ListNotations.
Fixpoint mylen2 (n1 n2 a b s c: nat) (l : list nat) : list nat :=
match n1 ,s <? n2 with
| O,true => [c]
| O, false=>nil
|_ ,false =>nil
|S n',true =>
if a <? nth b l 0 then
c:: mylen2 n' n2 a b (S s) c l
else
mylen2 n' n2 a b (S s) c l
end.
Fixpoint mylen23 (n1 n2 a b s c: nat) (l : list nat) : nat :=
match n1 ,s <? n2 with
| O,true => 1
| O, false=>0
|_ ,false =>0
|S n',true =>
if a <? nth b l 0 then
1+ mylen23 n' n2 a b (S s) c l
else
mylen23 n' n2 a b (S s) c l
end.
```

Output of function (myfunction) is list. I want to count a specific natural number in the output list. I am using count function (with argument n l) function from library but it has a error. Is there any other way for doing the same ?

What's the error?

```
Require Import List PeanoNat.
Import ListNotations.
Fixpoint myfunction (n a b c : nat) (l : list nat) :(nat * list nat) :=
match n with
| O => (1,[c])
| S n' =>
if a <? nth b l 0 then
((S 0), [c]) myfunction n' a b c l
else
(0,[]) myfunction n' a b c l
end.
```

What is `(0,[]) myfunction n' a b c l`

supposed to mean? Are you applying a pair `(0,[])`

to something?

Want to combine both, then extract list from pair

```
Fixpoint myfunction (n a b c : nat) (l : list nat) : list nat :=
match n with
| O => [c]
| S n' =>
if a <? nth b l 0 then
c :: myfunction n' a b c l
else
myfunction n' a b c l
end.
Fixpoint mylen (n a b : nat) (l : list nat) : nat :=
match n with
| O => 1
| S n' =>
if a <? nth b l 0 then
1 + mylen n' a b l
else
mylen n' a b l
end.
```

As suggested by @ Paolo Giarrusso (16 october)

I had only answered a question you posed.

~~it seems that instead of ~~`(0,[]) myfunction n' a b c l`

you want `(S 0), [c])`

, and instead of `(0,[]) myfunction n' a b c l`

you want `(0,[])`

.

~~if you want to compute ~~ (EDIT: there's a type error)`(myfunction n a b c l, mylen n a b c l)`

in one pass, it seems that instead of `((S 0), [c]) myfunction n' a b c l`

you want `(S 0), c :: myfunction n' a b c l)`

, and instead of `(0,[]) myfunction n' a b c l`

you want `(0, myfunction n' a b c l)`

.

Thank you. But now error message is this:

```
Fixpoint myfunction (n a b c : nat) (l : list nat) : nat * list nat :=
match n with
| O => c :: myfunction n' a b c l)
Error message : The reference n' was not found in the current environment.
```

The error message is pretty explicit though? It says `n'`

is not bound because it isn't. You cannot use `n'`

without introducing it. You have it in the `S n'`

branch however.

@Paolo Giarrusso & @Théo Winterhalter Thanks. But I have to use n' to reduce recursive call , for this I have to introduce it in input arguments.(for first case only )

When defining a fixpoint, one of the arguments must get smaller at each recursive call. It seems to be `n`

which does get smaller. But that means that when you reach `0`

you can no longer make recursive calls.

Right. When i write | O => c :: myfunction n' a b c l). Then I am unable to execute the function because of error message "The reference n' was not found in the current environment". Now what to do?(when add it in input arguments to remove the error then number of input arguments get increase.Not assigning n' to n)

but why are you trying to do a recursive call?

in your original code, if `n`

is`O`

, then you just return `[c]`

without recursing into `myfunction`

.

when add it in input arguments to remove the error then number of input arguments get increase.Not assigning n' to n

Adding input arguments without motivation is seldom a good idea, and it's never been clear what `myfunction`

tries to compute.

@sara lee this might be what you're looking for:

```
Fixpoint myfun_len (n a b c : nat) (l : list nat) : nat * list nat :=
match n with
| O => (1, [c])
| S n' =>
let rec := myfun_len n' a b c l in
if a <? nth b l 0 then
(S (fst rec), c :: snd rec)
else
rec
end.
```

or

```
Fixpoint myfun_len (n a b c : nat) (l : list nat) : nat * list nat :=
match n with
| O => (1, [c])
| S n' =>
let (rec_n, rec_l) := myfun_len n' a b c l in
if a <? nth b l 0 then
(S rec_n, c :: rec_l)
else
(rec_n, rec_l)
end.
```

But I'm still not really sure what this function is good for :-|

I want to find total number of c in the list. Therefore finding length of list.

"the list" = the original list `l`

? That's not what this code is doing

or at least, it can be done more directly

(deleted)

Thank you.

(deleted)

(deleted)

Want to convert the output of below function into pair(nat * list nat) like above.There is difference of only one argument .But change in this argument is different after result of test condition

```
Fixpoint myfunction (n a b c d: nat) (l : list nat) : list nat :=
match n with
| O => [c]
| S n' =>
if a <? nth b l 0 then
c :: myfunction n' a b c (d+1) l
else
myfunction n' a b c d l
end.
```

Secondly,d is incremented in case of true condition. Can i associate d with the length of output list? (if I set d=0 initially).

@Paolo Giarrusso. I can find the length of above by adding one , when there is addition of c in the list (after true condition). I want to ask that is there any way to find length of list by counting d's in the list ? If I set first time d=0 then on addition of new element in the list there is increment in the value of d. At the end , value of d & length of list will be same.

By using same above function may I control number of iterations to a particular value say z? If z is smaller than n .Then what modifications i should made in code?

Do you talk about @Paolo Giarrusso 's `my_fun_len`

function ?

As Paolo mentionned, it's not clear what this function computes, mainly because of some arguments which are used once (hence don't count in recursive calls). By a slight code modification, I obtained:

```
Definition my_fun_length n a b c l : nat * list nat :=
if a <? nth b l 0
then (S n, repeat c (S n))
else (1, [c]).
```

Is this function you are interested in ? Otherwise, it would be better to describe what the function should compute (arguments, result), and not necessarily implementation details.

Thanks for reply. Not exactly above but main purpose is to define a recursive function f with input arguments (n loop:nat) and output list. In first recursive call f should give 0 in the output list. In second 1, in third 2..till number is equal to given n then it re-start giving 1,2..n again.This process should run loop(no time) .

repeat function helps in giving sequence upto n time but i want to reset it multiple time , therefore i am doing patteren matching on number(loop)

like n=5 (before first reset ,next time n= 4)loop=11 , l= 0,1,2,3,4,1,2,3,4,1,2

You may write a simple recursive function with the wanted length as main recursive argument.

Here is a function with repeats the sequence `0, 1,...,n`

until the wanted length is reached.

```
Fixpoint loop n size x : list nat :=
match size with
0 => nil
| S s => x :: loop n s (if Nat.eq_dec n x then 0 else S x)
end.
Definition f n size := loop n size 0.
Compute f 4 11 .
```

In your example, the sequence starts with `0,1,2,3,4`

, but follows with the repeated pattern `1,2,3,4`

.

If you really want this irregularity, you will have to change sligthly the code above.

Thanks for both of you. you suggested to have a pair at output.(ok) Want to ask if myfun_len is being call two time and test condition is also being satisified .It means length is 2. I want to write a lemma which show that length of list is 2.

Is this not the same function which is corrected by @Paolo Giarrusso (16-oct). Value of n is goning to be decrease on each recursive call. If it follows a particular check then it will move in the list else not. From value n function is deriving output list. We can find its length also. It means we can write lemma when its length will be two. Why you are saying its function is not clear? If I have total n then we will be able to find number of elements which will appear and which will not appear. (n= number not appear+ number appear).

If some one requires list and length both then use pair(2* list nat). After having 2 and list, we have to show only that number 2 is length and we can write lemma that length of given list is 2 by writing specific conditions.

@Paolo Giarrusso corrected my function by removing some variables which were not using in the function. So final function posted on 16-oct is correct. I required both list and its length. Both requirements were fulfilled by having pair(list*nat) at output. I think for a particular case where we have pair (list and 2) can be address by setting preconditions.

@Paolo Giarrusso & @Pierre Castéran can relate output of above function with length two under specific conditions or extracting information from pair ( list and 2) and then proving 2 is the length of above used function .

Do we talk about the same function (posts of Oct 16 and Dec 03 by @Paolo Giarrusso ) ?

As mentionned in a previous post, this function can be simplified a lot (looking at the role of `a`

, `b, `

c`and `

l` in the computation).

```
Definition my_fun_length n a b c l : nat * list nat :=
if a <? nth b l 0 then (S n, repeat c (S n)) else (1, [c]).
```

If it's not the function you want to define, you will have to give a specification (as a relation between arguments and result).

I don't understand the questions about `2`

. Is it an interesting particular case or just an example?

The type of the returned value is `nat * list nat`

, i.e. `pair nat (list nat)`

, but not `pair (list * nat)`

which is not well-formed . A large part of the trust we have in Coq comes from its type system, so we have to be very precise when we mention the expected type of a function.

Ok ,post of 3 dec. Now we have list and length both. I want to write output list has two elements only,this is possible under what condition. Or want to write a lemma that length of output is two.I just want to see under what conditions it would be possible .( lemma which finds a relation between function and length).

I mean output of function is pair. While pair consist of nat list and nat value. Length 2 means when list have only two elements.

Lemma which express function and its relation with the number of elements in the output list.

The following lemma expresses the relation between the arguments and the length of the output list (using the version with `repeat`

of this function).

```
Lemma length_of_output_list n a b c l:
length (snd (my_fun_length n a b c l)) =
if a <? nth b l 0 then S n else 1.
Proof.
unfold my_fun_length; case (a <? nth b l 0); cbn;
[now rewrite repeat_length | reflexivity].
Qed.
```

Note that the use of `nth b l 0`

implies that if `l`

is too short (less than b+1 elements) , then the result is `(1,[c])`

.

```
Compute my_fun_length 3 1 7 42 [1;2;3].
(* = (1, [42])
: nat * list nat
*)
```

Please note also that `my_fun_length`

is a simplified form of more complex forms which were previously posted and approved. May be it's not exactly what you wanted to define. When you have a function definition, before using it (in other functions or proofs), you should be convinced of its correctness (for instance, by tests with `Compute`

or small simple lemmas). Such tests convinced me that the proposed function was just a wrapper to `List.repeat`

.

First thanks a lot. Exactly this is the lemma about which i am talking. By considering the same lemma i want to set the conditions, under which above function will give length 2.(output list have two elements).

when i compared both functions I found that I am unable to locally change value of c(just because of repeat function). but this option exists in previous one.

Secondly there are total n recursive call. If have z(nat) which is smaller than n. Then I can stop the recursive call at z by performing match on d<z. These are two problems which are stopping me from using this. Now problem is that in older function i am unable to write lemma about length like new one. Is it possible to write lemma like new one but by using old function? What to do ?(suggest plz)

It's not clear what you call "the old function" . It's better to give all the needed information in the questions (for instance a small snippet inside triple backquotes).

Let us assume you refer to a previous post:

```
Fixpoint myfunction (n a b c d: nat) (l : list nat) : list nat :=
match n with
| O => [c]
| S n' =>
if a <? nth b l 0 then
c :: myfunction n' a b c (d+1) l
else
myfunction n' a b c d l
end.
```

The argument `d`

looks unused to me, and I think this function computes also

`if a <? nth b l 0 then repeat c (S n) else [c]`

.

If this function is not what you wanted initially, you will have to first specify what you want to compute, then make some tests (with `Compute`

) before writing some proofs.

You are right. Both functions compute the same as long as c is fix. New specification: I am going to change value of c recursively ( locally) during each recursive call (by adding function....which increase the value of c up to certain extend and then decrease it to 0 then repeat it again and again till n goes to 0) and want to add new value of c in the list after test condition? Want to find list length. I will omit d for time being.

Ok, but there is probably a misunderstanding about the term "specification". For a function in a purely functional language like Coq's gallina, it should just make precise the role of the arguments with respect to the expected result, not implementation details like "change of values during the computation".

Let's take a simplified example of the pattern you describe : putting into a list a repetition of some values until some length is reached. Consider this specification:

- (repeat_app [] n) returns []
- if l is not empty, (repeat_app l n) returns a list of length n of the form l++l++l++ ... ++ l') where l' is a prefix of l

A possible solution (among other ones) is :

```
Fixpoint aux x u n (l:list nat) :=
match n, l with
0, _ => []
| S p, [] => x :: aux x u p u
| S p, a:: l' => a:: aux x u p l'
end.
Definition repeat_app l n :=
match l with
| [] => []
| x:: u => aux x u n []
end.
```

If I want to repeat only the elements of `l`

which satisfy a boolean predicate, it's easy to define:

```
Definition repeat_app_P (P: nat -> bool) l n :=
repeat_app (filter P l) n.
Compute repeat_app_P (fun n => Nat.leb 3 n) [1;2;33;4;1;8] 10.
Compute repeat_app_P (fun n => Nat.leb 73 n) [1;2;33;4;1;8] 10.
Compute repeat_app_P (fun n => Nat.leb 33 n) [1;2;33;4;1;8] 10.
```

Test condition is not missing in above definition(aux)? Please solve my issue also. Why you are not considering my function to be right one? Is it complex or it have some functional problem or difficult to prove? It fulfill my requirements ,therefore I am around this function . It is not always increasing function that increase the value of c ,It start decreasing after some nat value(3). Process continue . I am stopping it by n. Is it not proper recursive function?

```
Fixpoint myfunction (n a b c d :nat)(l:list nat): list nat :=
let c := f1( c+1) in
match n with
| O => c::nil
| S n' => match a <?nth b l 0 with
| true =>c:: (myfunction n' a b c d l )
| false => (myfunction n' a b c (d+1) l )
end
end.
```

f1 is separately defined function which control value of c .it start increasing c by assigning c=(f1 c+1),and when reach a particular value( let say 3 if start from 0.) then decrease it to 1. repeat it again and again. This continuous process stop by n.

then c=[1,2,3,1,2,3....] and output list= [1,2,3,1,2,3,1,2,3....] and number of elements in output list control by n(9). I am just storing the value of c in each recursive call and interested in length of output list . Regards sara.

You evaluate the condition `a <? nth b l 0`

at each recursive call, although `a`

, `b`

and `l`

keep the same value during the computation. This will probably make your proofs more complex.

Another solution may be of the form:

```
Definition myfunction' n a b c l := if a <? nth b l 0
then f_true c n
else f_false c n.
```

where `f_true`

and `f_false`

are auxiliary recursive function (do define).

Anyway, if the present version is accepted by Coq and fullfills your requirements, it's also OK.

Above function in the form of pair .

```
Fixpoint myfun_len (n a b c d: nat) (l : list nat) : nat * list nat :=
match n with
| O => (1, [c])
| S n' =>
let rec := myfun_len n' a b c (d+1) l in
if a <? nth b l 0 then
(S (fst rec), c :: snd rec)
else
rec
end.
```

From myfun_len

rec := myfun_len n' a b c (d+1) l. In case of true condition output = (S (fst rec), c :: snd rec) , otherwise rec.

But according to myfunction it should be , rec := myfun_len n' a b c d l. Is there any way to get d instead of d+1 in rec in case of false?

If this happen then i will get same result in both cases.

The argument called `d`

is unused in your function (the result doesn't depend on it). Perhaps it’s useless, or there is an error in the function definition.

You may try to simplify this function as most as possible, then do a sufficient set of tests in order to be sure that the function fullfills your requirements.

I get one element in the list in two cases

1) when n=0

2) n= S n and (a<? nth b l 0 is not fulfill) . n is decreasing on each call and get 1 element at the end. If length is 1 then how to differentiate it is one because of which one?

Plz correct me , how to write lemma about list length ,particularly when length l=1.

Now i have 1* [c] at output. How to extract available information that 1 shows the length of output list whose element is c? what hypothesis i should set so that get length=1?

Related to same question discussing from long period of time , i have these three questions ( Plz reply) . I have (nat * list nat) at output. So that i have list and its length information. But i need list as input argument in remaining code . Therefore i extract list information from pair. I have used n just make function simple. Actually it is the nat value which is the output of function (f x y z) ,after iteration function value get change like (f x' y z) . Now output is like this " 2::myfunction n' a b c l. I am writing lemma that this output can happen when i have following hypothesis

n= S n' & a < nth b l 0 -> 2::myfunction n' a b c l.

Q1) By using function i should write in this way?

n = S (f x y z) & a < nth b l 0 -> 2::myfunction (f x' y z) a b c l. (Error message : unknown variables x', I have declared x x' both).

How to remove this error?

Q2) From this "2::myfunction n' a b c l." i have no information about elements present in tail. Because length information i have lost during extraction from pair.

Q3) Elements are adding in the list till n goes to zero. For counting number of elements in this output list ,its length information is necessary?

@Pierre Castéran . You said in post of 29 May that if variables get change then it become complex. My problem is that these variable are changing and also have check variable condition . Want to clear my point that if I have H: count 3 l > count 2 l , according to function defined in the post one nat value added in the list and have goal statement like count 3 (3::l) > count 2 (3::l)after recursive call .Then what possible ways are there to solve the goal statement. To prove this i have to prove that number of recursive calls have decreased after one time execution. Suggest some possible ways. plz.

It may be difficult to help you if you don't post a snippet with the exact version of the function you are talking about, and which goal you want to solve (please include also the `Require Import`

statements that are necessary to replay your development). Several previous versions of this function were difficult to understand (undocumented role of some arguments, redundant tests, etc.)

I want to use your suggested function. By reading post i came to know that we can find length of output list.I want to ask if i select first 3 elements of the output list and move them in another list then length of resultant list will be 3, is provable? Secondly, if c is not constant (its value is locally changing) then what would be be possible way to find list length?

Sorry for asking question related to previous post. I have to prove below type of lemma,may i prove it? I have to add some other hypothesis to prove it?

count 2( 2::myfunction n a b c l) >0 by using function discuss in the post.

I assume you mean `count_occ`

? Please give us all the precise definitions we may need to answer your questions (without having to search in the history of previous posts). Your goal doesn't depend on `myfunction`

.

```
Require Import List Arith .
Lemma L (anylist: list nat):
count_occ Nat.eq_dec (2::anylist) 2 > 0.
Proof. cbn. auto with arith. Qed.
```
```

According to myfunction only two conditions should satisfy before the addition of an element in the list.1) a <? nth b l 0

and n may be 0 or Sn.If these conditions meet then c::myfunction n a b c l. I have the same case both conditions are satisfying and goal statement is about the addition of one element( c::myfunction n a b c l) . I just want to know which command i should apply to tell the Coq that every thing is according to given function and now just add one element according to the function? ( intuition. cbn.

eauto.auto with arith is not working.)

Last updated: Sep 28 2023 at 10:01 UTC