Stream: Coq users

Topic: list length

zohaze (Dec 03 2021 at 03:11):

Fixpoint count (v:nat) (l:list nat) : nat :=
  match l with
  | [] => 0
  | h :: t => (if beq_nat h v then 1 else 0) + (count v t)
  end.

Lemma lenth_1: forall (j: nat) (l: list nat),
length (0::l)=1->
count 0 (0::l)=1->
count( S j)(0::l)=0.

Julin S (Dec 03 2021 at 05:30):

I think it would be good to add a description so people here can get a better idea.

zohaze (Dec 03 2021 at 16:13):

Length of list is 1. It means one element is present in the list. At head position zero is present. Now presence of zero is confirm.Any other element which is not zero is not present in the list. We can say count_occ of (S j) in the list is zero. I can write this lemma as.

Lemma lenth_1: forall (j: nat) (l: list nat),
length (0::l)=1->
count 0 (0::l)=1->
(count( S j)(0::l)>0)->False.

zeesha huq (Dec 07 2021 at 15:19):

(deleted)

zohaze (Dec 07 2021 at 15:53):

Want to write lemma which shows that when one element exist in the list then list length is 1( Its means single element is present at the head and tail of the list is empty). Any element which is not part of list ,its occurrence in the same list is zero.

zohaze (Dec 15 2021 at 15:04):

Any one like to tell me the problem in above lemma's statement. I do not know the error/problem in above.

Pierre Castéran (Dec 15 2021 at 17:18):

zohaze said:

Any one like to tell me the problem in above lemma's statement. I do not know the error/problem in above.

There is no problem with your lemma. You can prove it by a case analysis on l.

Lemma length_1: forall (j: nat) (l: list nat),
length (0::l) =1 -> count 0 (0::l) = 1-> count(S j) (0::l)=0.
Proof.
  destruct l.
  - reflexivity.
  - discriminate.
Qed.

zohaze (Dec 18 2021 at 15:40):

Thank you.

sara lee (Dec 19 2021 at 16:30):

@Pierre Castéran. Above lemma is valid when length is 1. May I write a lemma that list length is 1 for the following list & function

c :: myfunction n' a b c (d+1) l &
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.

Initial d=0.

sara lee (Dec 29 2021 at 15:01):

Any one likes to help me in solving the above problem?

Pierre Castéran (Dec 29 2021 at 15:41):

Hi Sara,
It is difficult to answer whithout knowing what your function should compute in function of its arguments.
For instance how the result of a computation depends on d?
I noticed also also a, band l keep the same value along the computation,
and thus the test a <? nth b l 0 is always true, or always false.
My intuition is that, if a < nth b l 0, your function will return a list with n+1occurrences of c, otherwise the list [c].

Compute myfunction 6 1 2 42 0 (1::2::3::4::5::nil).
  = 42 :: 42 :: 42 :: 42 :: 42 :: 42 :: 42 :: nil
     : list nat

Compute myfunction 6 4 2 42 0 (1::2::3::4::5::nil).
  = 42 :: nil
     : list nat

Pierre

sara lee (Dec 30 2021 at 18:21):

First thanks.Initial value of a,b d=0. Value of d is incremented by the addition of element in the list.(1 element then d=1 ,2 elements then d=2). I am asking if have this list " c :: myfunction n' a b c (d+1) l" at output ,then I can prove list length is 1?

Pierre Castéran (Dec 31 2021 at 15:13):

Hi, Sara,
If a=b=d=0, and a <? nth b l 0 is true, then myfunction n a b c d lreturns a list of length n+1,
if a <? nth b l 0 is false, it returns a list of lenght 1.
Thus the whole expression you give c :: myfunction n' a b c (d+1) l has a length greater or equal than 2.

Note that the value of d does not matter.
Here are some examples you may execute, and try new ones of your own.

(**  a is less than the first element of the list *)
Compute 5::myfunction 5 0 0 5 0 (7::8::9::nil).

(**  a is greater or equal than the first element of the list *)
Compute 5::myfunction 5 0 0 5 0 (0::7::8::9::nil).

(** l is empty *)
Compute 5::myfunction 8 0 0 5 0 nil.

If you remove the useless dargument and rewrite the function in order to avoid repeated evaluations of the same test, you can obtain an equivalent and simpler definition.

Definition my_function (n a b c (* d removed *) :nat) l :=
  if (a <? nth b l 0)
  then repeat c (1+n)
  else c::nil.

Compute 5::my_function 5 0 0 5  (7::8::9::nil).

Compute 5::my_function 5 0 0 5  (0::7::8::9::nil).

Compute 5::my_function 8 0 0 5  nil.

Best regards,
Pierre

Last updated: Oct 08 2024 at 15:02 UTC