Stream: Coq users

Topic: list length


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

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

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

view this post on Zulip zeesha huq (Dec 07 2021 at 15:19):

(deleted)

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

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

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

view this post on Zulip zohaze (Dec 18 2021 at 15:40):

Thank you.

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

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

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

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

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

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC