Stream: Coq users

Topic: How to find length

view this post on Zulip 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)
      (rec_n, rec_l)

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.

view this post on Zulip 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 land 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 lalways a repetition of the same sequence or any list of natural numbers between 1 and 6 ? In this case, why make lan 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.

view this post on Zulip 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.

view this post on Zulip Pierre Castéran (Jul 05 2022 at 16:40):

If the value of aand c change (depending on f1and 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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