Stream: Coq users

Topic: List formation


view this post on Zulip sara lee (Aug 10 2021 at 17:40):

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.

view this post on Zulip Olivier Laurent (Aug 10 2021 at 19:12):

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.

view this post on Zulip sara lee (Aug 11 2021 at 15:18):

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.

view this post on Zulip sara lee (Aug 13 2021 at 17:41):

Thank you Olivier Laurent.

view this post on Zulip sara lee (Oct 14 2021 at 10:53):

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?

view this post on Zulip sara lee (Oct 14 2021 at 10:59):

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.

view this post on Zulip Paolo Giarrusso (Oct 14 2021 at 20:23):

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?

view this post on Zulip sara lee (Oct 16 2021 at 03:16):

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.

view this post on Zulip zohaze (Oct 16 2021 at 06:27):

Length determination is possible in above case?

view this post on Zulip zohaze (Oct 16 2021 at 06:34):

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.

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 09:28):

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

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 09:30):

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

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 09:31):

Would one or both those approaches be helpful?

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 09:31):

I can sketch out the implementations; please just ask.

view this post on Zulip zohaze (Oct 16 2021 at 10:40):

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

view this post on Zulip sara lee (Oct 16 2021 at 10:47):

I can link n and length of output list?

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 12:20):

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.

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 12:23):

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.

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 12:26):

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.

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 12:29):

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.

view this post on Zulip zohaze (Oct 26 2021 at 17:18):

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.

view this post on Zulip sara lee (Nov 30 2021 at 17:34):

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 ?

view this post on Zulip Li-yao (Nov 30 2021 at 17:35):

What's the error?

view this post on Zulip sara lee (Dec 02 2021 at 14:49):

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.

view this post on Zulip Théo Winterhalter (Dec 02 2021 at 14:51):

What is (0,[]) myfunction n' a b c l supposed to mean? Are you applying a pair (0,[]) to something?

view this post on Zulip sara lee (Dec 02 2021 at 14:57):

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.

view this post on Zulip sara lee (Dec 03 2021 at 03:15):

As suggested by @ Paolo Giarrusso (16 october)

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 06:38):

I had only answered a question you posed.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 06:40):

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,[]).

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 06:42):

if you want to compute (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). (EDIT: there's a type error)

view this post on Zulip zohaze (Dec 03 2021 at 15:32):

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.

view this post on Zulip Théo Winterhalter (Dec 03 2021 at 15:37):

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.

view this post on Zulip sara lee (Dec 03 2021 at 15:44):

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

view this post on Zulip Théo Winterhalter (Dec 03 2021 at 15:46):

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.

view this post on Zulip sara lee (Dec 03 2021 at 15:54):

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)

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 17:14):

but why are you trying to do a recursive call?

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 17:15):

in your original code, if n isO, then you just return [c] without recursing into myfunction.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 17:16):

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.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 17:23):

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

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 17:24):

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.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 17:25):

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

view this post on Zulip sara lee (Dec 06 2021 at 15:23):

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

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 15:59):

"the list" = the original list l? That's not what this code is doing

view this post on Zulip Paolo Giarrusso (Dec 06 2021 at 16:04):

or at least, it can be done more directly

view this post on Zulip sara lee (Dec 07 2021 at 02:04):

(deleted)

view this post on Zulip sara lee (Dec 09 2021 at 16:28):

Thank you.

view this post on Zulip sara lee (Dec 11 2021 at 06:41):

(deleted)

view this post on Zulip sara lee (Dec 11 2021 at 13:05):

(deleted)

view this post on Zulip sara lee (Dec 11 2021 at 17:03):

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

view this post on Zulip sara lee (Dec 15 2021 at 14:32):

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

view this post on Zulip zohaze (May 21 2022 at 15:57):

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?

view this post on Zulip Pierre Castéran (May 21 2022 at 16:51):

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.

view this post on Zulip zohaze (May 22 2022 at 07:34):

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

view this post on Zulip Pierre Castéran (May 22 2022 at 09:23):

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

view this post on Zulip zohaze (May 25 2022 at 04:12):

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.

view this post on Zulip zohaze (May 26 2022 at 04:47):

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.

view this post on Zulip sara lee (May 26 2022 at 14:05):

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

view this post on Zulip Pierre Castéran (May 26 2022 at 16:02):

Do we talk about the same function ?
If I'm not wrong, the function can be written as follows:

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 right function, you will have to tell how (as an input/result relation) it is specified.

One can easily prove the following lemma:

Lemma my_fun_length_Ok n a b c l:
  let (p, r) := my_fun_length n a b c l
                              in p = length r.
  unfold my_fun_length; destruct (a <? nth b l 0).
  - induction n; cbn; auto.
  - reflexivity.
Qed.

I don't understand the questions about 2. The type the the returned value is nat * list nat, i.e.
pair nat (list nat), but not pair (list * nat), nor pair(list and 2). 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.

view this post on Zulip zohaze (May 27 2022 at 00:51):

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

view this post on Zulip sara lee (May 27 2022 at 00:57):

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.

view this post on Zulip Pierre Castéran (May 27 2022 at 05:58):

The following lemma expresses the relation between the arguments and the length of the output list
(using the version with repeatof 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 lis 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
*)

view this post on Zulip zohaze (May 27 2022 at 13:57):

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)

view this post on Zulip Pierre Castéran (May 27 2022 at 15:30):

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.

view this post on Zulip zohaze (May 27 2022 at 18:36):

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.

view this post on Zulip Pierre Castéran (May 28 2022 at 08:37):

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:

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

view this post on Zulip sara lee (May 29 2022 at 05:08):

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

view this post on Zulip Pierre Castéran (May 29 2022 at 06:20):

You evaluate the condition a <? nth b l 0 at each recursive call, although a, band 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.

view this post on Zulip sara lee (May 29 2022 at 07:20):

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.

view this post on Zulip Pierre Castéran (May 29 2022 at 09:48):

The argument called d is unused in your function (the result doesn't depend on it).
Either one can remove it, or there is an issue 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 (whichever the value of the arguments ).

view this post on Zulip zohaze (Jun 07 2022 at 14:21):

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?

view this post on Zulip sara lee (Jun 11 2022 at 12:16):

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?

view this post on Zulip pianke (Jun 27 2022 at 09:04):

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

view this post on Zulip Pierre Castéran (Jun 27 2022 at 09:44):

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 (role of some arguments, redundant tests, etc.)

view this post on Zulip pianke (Jun 29 2022 at 17:57):

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?

view this post on Zulip pianke (Jun 30 2022 at 18:06):

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.

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

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

view this post on Zulip pianke (Jul 02 2022 at 07:31):

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: Jan 29 2023 at 05:03 UTC