sara lee (Aug 10 2021 at 17:40): 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.
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.
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.
sara lee (Aug 13 2021 at 17:41):Thank you Olivier Laurent.
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?
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.
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?
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.
zohaze (Oct 16 2021 at 06:27):Length determination is possible in above case?
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.
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...
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).
Paolo Giarrusso (Oct 16 2021 at 09:31):Would one or both those approaches be helpful?
Paolo Giarrusso (Oct 16 2021 at 09:31):I can sketch out the implementations; please just ask.
zohaze (Oct 16 2021 at 10:40):Better to find length separately,after removing count from function.
sara lee (Oct 16 2021 at 10:47):I can link n and length of output list?
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.
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.
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.
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.
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.
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 ?
Li-yao (Nov 30 2021 at 17:35):What's the error?
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.
What is (0,[]) myfunction n' a b c l supposed to mean? Are you applying a pair (0,[]) to something?
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.
As suggested by @ Paolo Giarrusso (16 october)
Paolo Giarrusso (Dec 03 2021 at 06:38):I had only answered a question you posed.
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,[]).
Paolo Giarrusso (Dec 03 2021 at 06:42):if you want to compute (EDIT: there's a type error)(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).
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.
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.
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 )
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.
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)
Paolo Giarrusso (Dec 03 2021 at 17:14):but why are you trying to do a recursive call?
Paolo Giarrusso (Dec 03 2021 at 17:15):in your original code, if n isO, then you just return [c] without recursing into myfunction.
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.
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.
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.
But I'm still not really sure what this function is good for :-|
sara lee (Dec 06 2021 at 15:23):I want to find total number of c in the list. Therefore finding length of list.
Paolo Giarrusso (Dec 06 2021 at 15:59):"the list" = the original list l? That's not what this code is doing
Paolo Giarrusso (Dec 06 2021 at 16:04):or at least, it can be done more directly
sara lee (Dec 07 2021 at 02:04):(deleted)
sara lee (Dec 09 2021 at 16:28):Thank you.
sara lee (Dec 11 2021 at 06:41):(deleted)
sara lee (Dec 11 2021 at 13:05):(deleted)
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).
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.
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?
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.
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
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 until 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.
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.
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.
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 .
Pierre Castéran (May 26 2022 at 16:02):Do we talk about the same function (posts of Oct 16 and Dec 03 by @Paolo Giarrusso ) ?
As mentionned in a previous post, this function can be simplified a lot (looking at the role of a, b, cand l` in the computation).
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 function you want to define, you will have to give a specification (as a relation between arguments and result).
I don't understand the questions about 2. Is it an interesting particular case or just an example?
The type of the returned value is nat * list nat, i.e. pair nat (list nat), but not pair (list * nat)which is not well-formed . 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.
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).
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.
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
*)
Please note also that my_fun_lengthis a simplified form of more complex forms which were previously posted and approved. May be it's not exactly what you wanted to define. When you have a function definition, before using it (in other functions or proofs), you should be convinced of its correctness (for instance, by tests with Computeor small simple lemmas). Such tests convinced me that the proposed function was just a wrapper to List.repeat.
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)
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.
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.
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.
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+1) 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.
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.
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.
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). Perhaps it’s useless, or there is an error 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.
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?
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?
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.
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 (undocumented role of some arguments, redundant tests, etc.)
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? Secondly, if c is not constant (its value is locally changing) then what would be be possible way to find list length?
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.
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.
```
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: Oct 13 2024 at 01:02 UTC