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. a is the sum of two randomly selected nats. Simply function f2 assign variable values to a by using c and l.

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

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

Is this the same function as in the `List formation`

thread ? If so, creating a new thread is useless.

We already mentionned that the role of all the arguments `n`

`a`

`b`

, `c`

and `l`

have not been clearly explained and that your function computes the same boolean expression at each recursive call, which makes your function less efficient and more difficult to prove.

In your last function, it's not clear whether the function `assign`

depends on `l`

, or is any function of type `nat -> nat`

.

Note that the snippet you posted contains a syntax error, and lacks a definition or a declaration of `assign`

.

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 strictly positive natural number less or equal than (S n).

Any body like to reply my question . I am considering above function where values of c are changing ,therefore output list contain different values of c. Under what condition count of particular value of c is greater or equal to another value of c . I want to write some relation/hypothesis so that i get some thing like this ((a 1 <? nth c1 l 0) < ( a 2 <? nth c2 l 0 ) then count c1 l < count c2 l )

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? Simply i want to write statement by using above function that there will be addition of natural number in the output list (untill condition is true).

(deleted)

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

Another remark: When asking about a difficult sub-goal, it would be better to show which lemma statement and tactics led to this sub-goal (instead of showing a few hypotheses and the conclusion to be proved). It may happen that the issue comes from an impossible-to-prove statement and/or a bad sequence of tactics, in which case the considered sub-goal doesn't need to be considered.

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: Jun 20 2024 at 11:02 UTC