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

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.

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.

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`

.

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?

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?

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

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.

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

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.

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