## Stream: Coq users

### Topic: How to find length

#### pianke (Jul 04 2022 at 03:36):

I am modeling dice which have values from 0-6. I have stored natural numbers in this form 0,1,2,3,4,5,6,0,1,2,3,4,5,6,0,1....I am assigning these values to c one by one by function assign(initial value of c=0). As a result value of c are varying.But function is terminating because of n and it is decreasing on each recursive call. I have below function.

2) I want to find length of output list of myfunction.Please suggest some way . (like length_of_output_list)

``````Fixpoint myfuntion (n a b c : nat) (l : list nat) : nat * list nat :=
let c: assign (c)
match n with
| O => (1, [c])
| S n' =>
let (rec_n, rec_l) := myfuntion 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.

Lemma length_of_output_list  n a b c l:
length (snd (myfuntion n a b c l)) =   if  a <? nth b l 0 then S n else 1.
``````

#### Pierre Castéran (Jul 04 2022 at 06:18):

Your function, as it is posted, is not accepted by Coq. Besides syntax errors, it depends on a function `assign`, which (I assume) establish a relation between the list `l`and the successive values of `c`.
But this function is missing from your post. Moreover, how `assign` does work in a purely functional language such as Coq (i.e. without side effects) with only `c:nat` as argument?

Is `l`always a repetition of the same sequence or any list of natural numbers between 1 and 6 ? In this case, why make `l`an argument of `myfunction`?

I think you should give a precise specification of your function: arguments and result. Then, make a few tests (to be sure it's OK) before proving properties of this function.

#### pianke (Jul 05 2022 at 16:13):

Not same as List formation.Two differences 1) c is varying in each recursive call and f1 use c and l and after calculation give value to c .2)value of a is also changing on each call , f2 use c ,a , l and after some calculation give a nat to a( I have updated code after your reply) .a and c are initially zero.Now bool expression is also changing on each call. I want to find length of output list.

#### Pierre Castéran (Jul 05 2022 at 16:40):

If the value of `a`and `c` change (depending on `f1`and `f2`) at each recursive call, I think you can only prove that the length of the output list is some natural number `l` such that `1 <= l <= S n`.

#### pianke (Jul 05 2022 at 17:23):

In terms of lemma how i can write length of myfunction?( length (my function n a c l)<= 1 <= l <= S n.). Secondly, i have to use this length notation of given function in remaining code then how i will represent length l ?( Like i want to write length l >0.Here l is the output length of myfunction. )Third when i write length (myfunction n a cl)<= n then after simplification it look like length (fix myfunction n0 a0 c0 l0) what does it means? How to make it simple?

#### pianke (Jul 16 2022 at 07:38):

If n>0 , then after multiple recursive call different elements get add in the list(after satisfying the test condition).Now i have hypothesis
H1: count c1 l > count c2 l in the output list.
H2: n >0
H3: a < nth c l 0
under these conditions,according to function there is addition of another element in the list. How i can write it in the form of lemma statement?

#### pianke (Jul 16 2022 at 16:58):

``````H: count_occ l k2 <= count_occ l 0
goal: count_occ l k2  <=S ( count_occ l 0)
eauto. auto with arith (both are not working)
``````

#### sara lee (Aug 07 2022 at 05:23):

I am using above function to add natural numbers in the list. I have hypothesis which shows different natural numbers are in the output list.Now another element is going to be add because it full fill bool condition(a <? nth c l 0). How to write it in the form of lemma. Please give me an example, i am confuse with n ,how to check it? Because both condition & n are necessery for next call.

#### Pierre Castéran (Aug 07 2022 at 13:09):

Does "above function" refer to the post of 04 July on this thread? The definition contained syntax errors, and some helper functions like `f1`, `f2` were missing. We also mentioned that the proposed lemma was probably not provable.
It’s extremely difficult to understand such a function if its code is not completely given (including libraries to load) and error-free (unless the question itself is about a misunderstood error message). Moreover, it would be helpful to explain what the function is assumed to compute in function of its arguments (maybe with an example or two).

#### sara lee (Aug 08 2022 at 05:24):

Yes,post of 4 July. Just considering this function,i want to know way of writing this statement " Few different elements exist in the output list (like 2 and 0. count 0 l < count 2 l,where l is the extracted list from above pair) and in next call a new element will add in this list.(under these hypothesis/conditions)". While f1 & f2 are defined converging functions and use for changing values of used parameters in the code. Thanks.

#### sara lee (Aug 16 2022 at 07:38):

What could be the way of statement writing that if conditions fullfill then there is addition of element in the output list by using above defined function?

Last updated: Jan 27 2023 at 01:03 UTC